Verifiable Concurrent Programming Environment

We present a framework for verifiable concurrent programming in Java, based on a design pattern for concurrency controllers. Using this pattern, a programmer can write concurrency controller classes by specifying a set of guarded commands and without using any of the error-prone synchronization primitives in Java. We show that the concurrency controllers written based on the proposed design pattern can be automatically verified and optimized. We present a modular approach to verification of concurrent programs by separating the verification of the concurrency controllers (behavior verification) from the verification of the threads which use them (interface verification). The interface of a concurrency controller is a finite state machine with transitions representing controller actions. For behavior verification we use symbolic and infinite state model checking techniques, which enables verification of controllers with parameterized constants, unbounded variables and arbitrary number of user threads. For interface verification we use explicit state model checking techniques, which allows verification of arbitrary thread implementations without any restrictions. We show that the correctness of the user threads can be verified using the concurrency controller interfaces as stubs, which improves the efficiency of the interface verification significantly. We also show that the concurrency controllers can be automatically optimized using the specific notification pattern. We demonstrate the effectiveness of our approach using a concurrent editor as a case study. The presented approach scales to this large concurrent program which consists of about 2800 lines of Java code with complex synchronization constraints.

Usage

To generate optimized version 

java MV infile.java -interface intf.java -j

To generate Action Language specification: (in this example, we generate 2 thread processes) 


java MV infile.java -interface intf.java -a 2

To generate Action Language specification with counting abstraction: (in order to verify for arbitrary number of threads) 

java MV infile.java -interface intf.java -a 1 -A

Before running the program you need to add to your LD_LIBRARY_PATH to the directory where you have Omega library and CUDD. To be able to compile the controller classes you need to have the following Java classes:

These classes facilitate the guarded-command usage.

Examples

Case Study:Concurrent Editor

javadoc source code

Access

This system consists of a Java part and a C++ part.