Reliable Concurrent Software Development Via Reliable Concurrency Controllers

University Of California-Santa Barbara, Santa Barbara CA

Investigators

Abstract

This proposal presents a framework for reliable concurrent programming based on interface-based specification and verification of concurrency controllers. Proposed specification and verification techniques for concurrency controllers are modularized by decoupling behavior and interface specifications. The behavior specification is a set of actions (which correspond to methods or procedures) composed of guarded commands. The interface specification is a finite state machine whose transitions represent actions. Con-currency controllers can be designed modularly by composing their interfaces. The proposed approach separates the verification of the concurrency controllers (behavior verification) from the verification of the threads, which use them (interface verification). For behavior verification it is possible to use symbolic and infinite-state verification techniques, which enables verification of controllers with parameterized constants, unbounded variables and arbitrary number of client threads. For interface verification it is possible to use explicit state program verification techniques, which enables verification of arbitrary thread implementations without any restrictions. The correctness of the user threads can be verified using stubs generated from the concurrency controller interfaces, which improves the efficiency of the thread verification significantly. It is possible to synthesize efficient Java monitors from the concurrency controller specifications, and the generated implementations preserve the verified properties of the specifications. The proposed framework will be implemented as a set of tools for concurrency controller specification, verification and synthesis