Liveness analysis and the automatic generation of concurrent programs
Ugo A. Buy, Robert N. Moll · DIMACS series in discrete mathematics and theoretical computer science · 1991
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 in