About This Item

Ask the MINDS@UW Librarian

Static Detection of Atomic-Set-Serializability Violations

Show full item record


Kidd, Nicholas; Reps, Thomas; Dolby, Julian; Dolby, Julian; Vaziri, Mandana
University of Wisconsin-Madison Department of Computer Sciences
Mar 15, 2012
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. We 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. We tested our technique on programs with known serialiability violations from the concurrency-testing benchmark created by Eytani et al. Of the ten programs analyzed, our tool reported eight atomic-set serializability violations, with seven of them being true bugs.
Permanent link
Export to RefWorks 

Part of

Show full item record

Search and browse


Deposit materials

  1. Register to deposit in MINDS@UW
  2. Need deposit privileges? Contact us.
  3. Already registered? Have deposit privileges? Deposit materials.