This paper describes the methods used in EMPIRE, a toolto detect concurrency-related bugs, namely atomic-set serializability vi-olations in Java programs. The correctness criterion is based on atomicsets of memory locations, which share a consistency property, and unitsof work, which preserve consistency when executed sequentially. EMPIREchecks that, for each atomic set, its units of work are serializable. Thisnotion subsumes data races (single-location atomic sets), and serializ-ability (all locations in one atomic set). To obtain a sound, finite model of locking behavior for use in EM-PIRE, we devised a new abstraction principle, random isolation, whichallows strong updates to be performed on the abstract counterpart ofeach randomly-isolated object. This permits EMPIRE to track the sta-tus of a Java lock, even for programs that use an unbounded number oflocks. The advantage of random isolation is that properties proved abouta randomly-isolated object can be generalized to all objects allocated atthe same site. We ran EMPIRE on eight programs from the ConTestbenchmark suite, for which EMPIRE detected numerous violations.
展开▼
