jpf-concurrent: An extension of Java PathFinder for java.util.concurrent
This work addresses verification challenges for developers of multi-threaded Java applications, but it is incremental as it builds on existing Java PathFinder tools.
The paper tackles the state space explosion problem in verifying multi-threaded Java applications by proposing a method to minimize it under the Java PathFinder model checker, resulting in faster verification and significantly smaller state spaces compared to the JDK implementation.
One of the main challenges when verifying multi-threaded Java applications is the state space explosion problem. Due to thread interleavings, the number of states that the model checker has to verify can grow rapidly and impede the feasibility of verification. In the Java language, the source of thread interleavings can be the system under test as well as the Java Development Kit (JDK) itself. In our paper, we propose a method to minimize the state space explosion problem for applications verified under the Java PathFinder (JPF) model checker. Our method is based on abstracting the state of the application to a smaller domain and implementing application behavior using the Model Java Interface (MJI) of JPF. To show the capabilities of our approach, we have created a JPF extension called jpf-concurrent which abstracts classes from the Java Concurrency Utilities. Several benchmarks proved the usefulness of our approach. In all cases, our implementation was faster than the JDK implementation when running under the JPF model checker. Moreover, our implementation led to significantly smaller state spaces.