This paper concerns automatically verifying safety properties of concurrent programs. In our work, the safety property of interest is to check for multi-location data races in concurrent Java programs, where a multi-location data race arises when a program is supposed to maintain an invariant over multiple data locations, but accesses/updates are not protected correctly by locks.

The main technical challenge that we address is how to generate a program model that retains (at least some of) the synchronization operations of the concrete program, when the concrete program uses dynamic memory allocation. In the presence of dynamic memory allocation, the finite number of abstract objects of the abstract program must represent the unbounded number of concrete objects that the concrete program may allocate, and thus by the pigeon-hole principle some of the abstract objects must be summary objects -- they represent more than one concrete object. Because abstract summary objects represent multiple concrete objects, the program analyzer typically must perform weak updates on the abstract state of a summary object, where a weak update accumulates information. Because weak updates accumulate rather than overwrite, the analyzer is only able to determine weak judgements on the abstract state, i.e., that some property possibly holds, and not that it definitely holds. The problem with weak judgements is that determining whether an interleaved execution respects program synchronization requires the ability to determine strong judgements, i.e., that some lock is definitely held, and thus the analyzer needs to be able to perform strong updates -- an overwrite of the abstract state -- to enable strong judgements.

We present the random-isolation abstraction as a new principle for enabling strong updates of special abstract objects. The idea is to associate with a program allocation site two abstract objects, r^# and o^#, where r^# is a non-summary object and o^# is a summary object. Abstract object r^# models a distinguished concrete object that is chosen at random in each program execution. Because r^# is a non-summary object---i.e, it models only one concrete object---strong updates are able to be performed on its abstract state. Because which concrete object r^# models is chosen randomly, a proof that a safety property holds for r^# generalizes to all objects modeled by o^#.

We implemented the random-isolation abstraction in a tool called Empire, which verifies atomic-set serializability of concurrent Java programs. (Atomic-set serializability is one notion of multi-location data-race freedom.) Random isolation allows Empire to track lock states in ways that would not otherwise have been possible with conventional approaches.

(Click here to access the paper: PDF.)