SAT-Based Control of Concurrent Software for Deadlock Avoidance

We present a highly efficient boolean satisfiability (SAT) formulation for deadlock detection and avoidance in concurrent programs modeled by Gadara nets, a class of Petri nets. The SAT formulation is used in an optimal control synthesis framework based on Discrete Control Theory. We compare our method with existing methods and show a significant increase in scalability. Stress tests show that our technique is capable of synthesizing deadlock avoidance control logic in programs modeled by Gadara nets with over 10⁹ unsafe states.