Specification, Verification, and Synthesis of Concurrency Control Components

Run-time errors in concurrent programs are generally due to wrong usage ofsynchronization primitives such as monitors. Conventional validationtechniques such as testing become ineffective for concurrent programs since thestate space increases exponentially with the number of concurrentprocesses. In this paper, we propose an approach in which 1) the concurrency controlcomponent of a concurrent program is formally specified, 2) it is verifiedautomatically using model checking, and 3) the code for concurrency controlcomponent is automatically generated. We use monitors as the synchronizationprimitive to control access to a shared resource by multiple concurrentprocesses. Since our approach decouples concurrency control component fromrest of the implementation it is scalable. We demonstrate its scalability byapplying our approach to a case study on airport ground traffic control.We use Action Language to specify the concurrency control component of asystem. Action Language is a specification language for reactive softwaresystems. It is supported by an infinite-state model checker that can verifysystems with boolean, enumerated and unbounded integer variables. Our codegeneration tool automatically translates the verified Action Languagespecification into a Java monitor. We discuss correctness of our translationalgorithm in terms of preservation of the verified properties. Our translationalgorithm employs symbolic manipulation techniques and the specificnotification pattern to generate an optimized monitor class by eliminating thecontext switch overhead introduced as a result of unnecessary threadnotification. Using counting abstraction, we show that we can automaticallyverify the monitor specifications for arbitrary number of threads.