Axis: Automatically fixing atomicity violations through solving control constraints

Atomicity, a general correctness criterion in concurrency programs, is often violated in real-world applications. The violations are difficult for developers to fix, making automatic bug fixing techniques attractive. The state of the art approach aims at automating the manual fixing process but cannot provide any theoretical reasoning and guarantees. We provide an automatic approach that applies well-studied discrete control theory to guarantee deadlocks are not introduced and maximal preservation of the concurrency of the original code. Under the hood, we reduce the problem of violation fixing to a constraint solving problem using the Petri net model. Our evaluation on 13 subjects shows that the slowdown incurred by our patches is only 40% of that of the state of the art. With the deadlock-free guarantee, our patches incur moderate overhead (around 10%), which is a worthwhile cost for safety.