Precise race detection and efficient model checking using locksets

In this paper, we present a new algorithm for detecting data-races in an execution of a concurrent program. Our algorithm is sound and precise, that is, it reports a race in an execution if there are two accesses to a shared variable along the execution that are not ordered by the happens-before relation. Previous algorithms for computing the happens-before relation are based on clock vectors. On the other hand, our algorithm is based solely on the concept of locksets and is able to capture all mutual-exclusion synchronization idioms uniformly with one mechanism. Our lockset algorithm could be very useful for improving the precision of flow-sensitive static analyses, particularly those for detecting data-races and atomicity violations in concurrent programs. We present one such analysis, a model checking algorithm that uses our lockset algorithm both to check for races exhaustively and perform partial-order reduction when races are absent. Our characterization of the happens-before relation in terms of locksets rather than clock vectors is crucial for the fixpoint computation inherent in model checking and other flow-sensitive analyses. We have implemented our algorithm and used it to prove the absence of data-races and assertion failures on a number of examples containing a variety of synchronization idioms.