Finding Concurrency-Related Bugs using Random Isolation
Nicholas Kidd, Thomas Reps, Julian Dolby, and Mandana Vaziri
This paper describes the methods used in Empire, a tool to detect
concurrency-related bugs, namely atomic-set serializability violations in Java
programs. The correctness criterion is based on atomic sets of memory
locations, which share a consistency property, and units of work, which
preserve consistency when executed sequentially. Empire checks that, for
each atomic set, its units of work are serializable. This notion subsumes data
races (single-location atomic sets), and serializability (all locations in one
atomic set).
To obtain a sound, finite model of locking behavior for
use in Empire, we devised a new abstraction principle, random
isolation, which allows strong updates to be performed on the
abstract counterpart of each randomly-isolated object.
This permits Empire to track the status
of a Java lock, even for programs that use an unbounded
number of locks.
The advantage of random isolation is that properties proved about a
randomly-isolated object can be generalized to all objects
allocated at the same site.
We ran Empire on eight programs from the ConTest benchmark
suite, for which Empire detected numerous violations.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)