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 ...

• Type: Conference
• Year: 2009
• Where: VMCAI
• Authors: Nicholas Kidd, Thomas W. Reps, Julian Dolby, Mandana Vaziri
• Keywords: Atomic Set, Empire, Random Isolation, Software Engineering, VMCAI 2009