The application of supervisory control to deadlock avoidance in concurrent software

Ensuring deadlock-free execution of concurrent programs is a notoriously difficult problem, but an increasingly important one as multicore processors compel performance-conscious software developers to parallelize applications. We propose and validate a novel methodology for dynamically controlling the execution of concurrent software in order to provably avoid deadlocks. The methodology is based on supervisory control of discrete event systems modeled by Petri nets. Specifically, we synthesize feedback controllers for concurrent programs based on the theory of supervision based on place invariants and implement the controllers online to guarantee deadlock avoidance. We describe a full implementation of this methodology and report initial experimental results demonstrating its effectiveness and scalability.