Sound Predictive Atomicity Violation Detection§

Many concurrency bugs are hidden deeply behind thread interleaving and are hard to detect. Existing dynamic predictive checkers can analyze execution traces to expose predictive cases of data races and deadlocks hidden by the thread interleavings of execution traces and inferable from these inter-leavings. To the best of our knowledge, however, no existing work for the detection of atomicity violation at the transaction level (AV) can expose predictive atomicity violations. In this paper, we present the first work to address this problem. Our technique, Meteor, formulates a novel algorithm with a thread-centric pipeline to capture enumerable dependency sequences containing reversible dependencies incrementally, implicitly, and soundly. It detects predictive atomicity violations without producing false positives. We prove its soundness by theorems. We have evaluated Meteor on 19 subjects, which confirms the soundness and effectiveness of Meteor to detect predictive atomicity violations in the programs.