Abstrakt
All techniques and tools for verification of multi-threaded programs must cope with the huge number of possible thread interleavings. Tools based on systematic exploration of a program state space employ partial order reduction to avoid redundant thread interleavings and unnecessary thread choices.
The key idea is to make non-deterministic thread choices only at statements that read or modify the global state shared by multiple threads. We focus on Java Pathfinder (JPF), which constructs the program state space on-the-fly, and therefore uses only information available in the current dynamic program state and execution history to identify statements that may be globally-relevant.
In our previous work, we developed a field access analysis that provides information about fields that may be accessed in the future during program execution, and used it with JPF for more precise identification of globally-relevant statements. We build upon that and propose a hybrid may-happen-before analysis that computes a safe approximation of the happens-before ordering.
JPF uses the happens-before ordering to detect pairs of globally-relevant field access statements that cannot be interleaved arbitrarily (due to synchronization between threads), and based on that avoids making unnecessary thread choices. The may-happen-before analysis combines static data flow analysis and usage of information available from the dynamic program state.
This report describes the may-happen-before analysis, and provides results of experiments with several Java programs showing that usage of the may-happen-before analysis together with the field access analysis improves the scalability of JPF.