Static Detection of Atomic-Set-Serializability Violations

Vaziri et al. propose a data-centric approach to synchronization. The key underlying concept of their work is the atomic set, which specifies the existence of an invariant that holds on a set of fields of an object type. In addition, they formalize a set of eleven data-access scenarios that completely specify the set of non-serializable interleaving patterns that can lead to an atomic-set serializability violation of the expressed invariant. The authors present an algorithm that uses state-space exploration techniques to statically detect atomic-set serializability violations. The key idea is that the data-access scenarios can be used as a property specification for a software model checker.