Efficient and Sound Dynamic Atomicity Violation Checking


Student thesis: Doctoral Thesis

View graph of relations


  • Shangru WU

Related Research Unit(s)


Awarding Institution
Award date10 May 2016


Atomicity is a desirable correctness property for multithreaded programs. Each code region exhibiting this property indicates that any execution of that region in a trace can be reordered to become a serial execution in some equivalent trace. However, programs may not always enforce this property, leading to atomicity violations at run time. A survey reports that 69% of non-deadlock concurrency bugs in real-world multithreaded programs are atomicity violations. In this thesis, I propose an efficient and sound framework to detect atomicity violations dynamically with atomicity specifications and without them.
To detect atomicity violations with specifications, state-of-the-art dynamic detectors first build a transactional happens-before graph along an execution trace, and check the presence of any cycle in such a graph. If a cycle is detected, then they may report a violation on one of the transactions involved in the cycle. To be efficient, these detectors resolve to capture at most one happens-before relation between each pair of transactions, which nonetheless makes the captured relations imprecise. Their detections report false positives or false negatives.
The first contribution of this thesis is to have formulated a novel sound and complete dynamic detector to report atomicity violations on transactions that are expected to be atomic. We have proven that dividing transactions into dynamic subregions and representing happens-before relations implicitly and transitively at the sub-region level guarantee both soundness and completeness in detecting atomicity violations. We have proposed our detector based on this theoretical guarantee. The experiment has further shown that our detector incurs significantly lower memory and slowdown overheads than the state-of-the-art dynamic detectors.
To detect atomicity violations without specifications, state-of-the-art sound dynamic detectors employ a two-phase strategy. Such a strategy first predicts a set of suspicious instances of non-serializable interleavings from one trace, and then examines each such instance by generating a confirmation trace. The amount of suspicious instances predicted however can be large, making the overall examination on all these instances time-consuming.
The second contribution of this thesis is to present the first work in designing instance prioritization and reduction techniques for atomicity violation detection. We have proposed the abstraction level and subspace projection as two orthogonal dimensions in modeling whether suspicious instances are equivalent. After having assigned them to equivalent classes, our techniques either prioritize the suspicious instances or reduce the number of suspicious instances for examination. The empirical results have shown that the proposed strategy can effectively separate instances of atomicity violation bugs from all suspicious instances, resulting in a novel family of eight prioritization techniques and six reduction techniques that are significantly more cost-effective than the techniques modeled after a state-of-the-art detector.
In summary, this thesis makes two major contributions. First, it is the first work to propose an efficient, sound and complete dynamic detector to detect atomicity violations with low memory overhead. Second, it is the first work to systematically study prioritization and reduction of suspicious instances of atomicity violation bugs and successfully formulate cost-effective dimensions for instances prioritization and reduction.