Static Detection of Atomic-Set-Serializability Violations
File(s)
Date
2007Author
Kidd, Nicholas
Reps, Thomas
Dolby, Julian
Vaziri, Mandana
Publisher
University of Wisconsin-Madison Department of Computer Sciences
Metadata
Show full item recordAbstract
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
http://digital.library.wisc.edu/1793/60610Citation
TR1623