On atomicity enforcement in concurrent software via Discrete Event Systems theory

Atomicity violations are among the most severe and prevalent defects in concurrent software. Numerous algorithms and tools have been developed to detect atomicity bugs, but few solutions exist to automatically fix such bugs. Some existing solutions add locks to enforce atomicity, which can introduce deadlocks into programs. Our recent work avoids deadlock bugs in concurrent programs by adding control logic synthesized using Discrete Event Systems theory. In this paper, we extend this control framework to address single-variable atomicity violation bugs. We use the same class of Petri net models as in our prior work to capture program semantics, and handle atomicity violations by control specifications in the form of linear inequalities. We propose two methodologies for synthesizing control logic that enforces these linear inequalities without causing deadlocks; the resulting control logic is embedded into the program´s source code by program instrumentation. These results extend the scope of concurrency bugs in software systems that can be handled by techniques from control engineering. Case studies involving two real Java programs demonstrate our solution procedure.