Programming in a general model of synchronization

Abstract

We propose a programming formalism that provides multiprocess synchronization and priorities. As in CCS and CSP, processes communicate by executing pairs of complementary actions. Processes are labelled transition systems, where the labels are formed by combining atomic actions with the operators Λ, ⌝. Intuitively, a Λ b expresses multiple synchronization on actions a, b, while ⌝ e expresses that the actions specified by e cannot be performed in the current environment. The operational semantics is based on a notion of stratification, like that in logic programming. Stratification requires a partial order on actions, which is related to priority. We allow systems to place different priorities on actions at different states. The goals of the language are: to serve as a high level executable specification language for concurrent programs, and to enable mechanical reasoning techniques such as model checking to be applied to specifications. We identify a large class of specifications that are efficiently executable, and present a simple synchronization algorithm. The language is being used to design multiprocess systems for controlling telephone switching. We describe progress towards the goal of applying model checking to complex software systems.