According to Java's relaxed memory model, programs that contain data races need not be sequentially consistent. Executions that are not sequentially consistent may exhibit surprising behavior such as operations on a thread occurring in a different order than indicated by the source code or different threads having inconsistent views of updates of shared variables. Java Racefinder (JRF) is an extension of Java Pathfinder (JPF), a model checker for Java bytecode. JRF precisely detects data races as defined by the memory model and can thus be used to verify sequential consistency. We describe an extension to JRF, JRF-Eliminator (JRF-E), that analyzes information collected during model checking, specifically counterexample traces and acquiring histories, and provides advice to the programmer on how to eliminate detected data races from a program. If data races have been eliminated, standard model checking and other verification techniques that implicitly assume sequential consistency can be soundly employed to verify additional properties.

Most approaches to reasoning about multithreaded programs, including model checking, make the implicit assumption that the system being considered is sequentially consistent. This is, however, invalid in most modern computer architectures and results in unsound reasoning for programs that contain data races, where data races are defined by the memory model of the programming environment. We describe an extension to the model checker Java PathFinder that incorporates knowledge of the Java Memory Model to precisely detect data races in Java byte code. Our tool incorporates special purpose heuristic algorithms that result in shorter counterexample paths. Once data races have been eliminated from a program, Java PathFinder can be soundly employed to verify additional properties.

We describe the ideas behind a method to use assertional reasoning to statically show that all sequentially consistent executions of a concurrent program are free from data races.