Sciweavers

Share
VMCAI
2009
Springer

Finding Concurrency-Related Bugs Using Random Isolation

9 years 5 months ago
Finding Concurrency-Related Bugs Using Random Isolation
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 Emdevised a new abstraction principle, random isolation, which trong 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 ...
Nicholas Kidd, Thomas W. Reps, Julian Dolby, Manda
Added 20 May 2010
Updated 20 May 2010
Type Conference
Year 2009
Where VMCAI
Authors Nicholas Kidd, Thomas W. Reps, Julian Dolby, Mandana Vaziri
Comments (0)
books