Dynamic Detection of Atomic-Set-Serializability Violations

Programmer-specified atomic sets of memory locations provide a flexible correctness criterion for synchronization of concurrent tasks that only requires serializability (atomicity) with respect to atomic sets rather than all of memory. We call this criterion atomic-set serializability. This criterion can be used to check for traditional data races (single-location atomic sets), standard notions of serializability (all locations in one set), and a range of options in between. We present a new dynamic analysis that checks for violations of atomic-set serializability. It is based on a complete set of problematic patterns that characterizes possible atomic-set-serializability violations, and uses state machines to track possible occurrences of these patterns in the program as it runs. The nature of these patterns enables an efficient implementation that does not need the entire execution trace. We implemented this analysis and evaluated it on a suite of real programs and benchmarks. We found a number of violations that correspond to both well-known high- and low-level race conditions as well as new bugs.



.pdf