Eliminating concurrency bugs in multithreaded software: an approach based on control of Petri nets. (English) Zbl 1381.68209

Colom, José-Manuel (ed.) et al., Application and theory of Petri nets and concurrency. 34th international conference, PETRI NETS 2013, Milan, Italy, June 24–28, 2013. Proceedings. Berlin: Springer (ISBN 978-3-642-38696-1/pbk). Lecture Notes in Computer Science 7927, 21-28 (2013).
Summary: 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.
For the entire collection see [Zbl 1266.68010].


68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)


RacerX; Gadara
Full Text: DOI