Liveness Analysis and the Automatic Generation of Concurrent Programs

this paper we discuss an aspect of the automatic synthesis of synchronization code for asynchronous processes. Our synthesis approach conforms to the following paradigm: (1) a specification is written in a nonconstructive specification language; (2) that specification is analyzed in an attempt to establish that crucial concurrency properties are respected; and (3) if the concurrency properties of the specification are established, then Ada code is generated. Here we report on the most difficult part of this process: establishing that a program specification satisfies a crucial concurrency requirement, namely liveness. (Other related aspects of our proposed approach, such as safety properties and deadlock avoidance, are discussed elsewhere [4]). By a liveness property we mean a condition that must be satisfied at some point during the execution of a program. A liveness property contrasts with a safety property, a condition that must hold continuously during program execution. Underlying our approach to synthesis is a model of a concurrent program i