Model checking of concurrent programs with static analysis of field accesses

摘要

Systematic exploration of all possible thread interleavings is a popular approach to detect errors in multi-threaded programs. A common strategy is to use a partial order reduction technique and perform a non-deterministic thread scheduling choice only when the next instruction to be executed may possibly read or modify the global state. However, some verification frameworks and software model checkers, including Java Pathfinder (JPF), construct the program state space on-the-fly during traversal. The partial order reduction technique built into such a tool can use only the information available in the current state to determine whether the execution of a given instruction is globally-relevant. For example, the reduction technique has to make a thread choice at every field access on a heap object reachable from multiple threads, even in the case of fields that are really accessed only by a single thread during program execution, because it does not have any information about what may happen in the future after a particular state. These conservative decisions cause many redundant thread choices. We propose static analyses that identify globally-relevant field accesses more precisely. For each program state, the analyses give information about field accesses that may occur in the future after the given state. The state space traversal algorithm can use this information to soundly avoid creating unnecessary thread choices, and thus to reduce the number of thread interleavings that must be explored to cover all distinct behaviors of the given program. We implemented the proposed analyses using WALA and integrated them with JPF. Results of experiments on several Java programs show that the static analyses greatly improve the performance and scalability of JPF. In particular, it is now possible to check more complex programs than before in reasonable time.