Eliminating Concurrency Bugs in Multithreaded Software: An Approach Based on Control of Petri Nets

摘要

We describe the Gadara project, a research effort whose goal is to eliminate certain classes of concurrency bugs in multithreaded software by controlling the execution of programs at run-time. The Gadara process involves three stages: modeling of the source code at compile time in the form of a Petri net, feedback control synthesis, and control logic implementation into the source code. The feedback control logic is synthesized using techniques from supervisory control of discrete event systems, where the specification captures the avoidance of certain types of concurrency bugs, such as deadlocks. We focus on the case of circular-wait deadlocks in multithreaded programs employing mutual exclusion locks for shared data. The application of the Gadara methodology to other classes of concurrency bugs is briefly discussed.