Specification and synthesis of synchronizers
Krithivasan Ramamritham · 1981
The formalism of Temporal Logic has been suggested to be an appropriate tool for expressing the semantics of concurrent programs. This thesis is concerned with the application of temporal logic to the specification and synthesis of synchronizers. A very high level specification language founded on temporal logic is introduced. This language is designed for expressing properties required among operations accessing shared resources in a concurrent environment. The language posseses constructs for expressing properties such as mutual exclusion of operation execution, priority among operations, invariance of resource state, and scheduling disciplines. Each of the above is expressed independent of the others, resulting in modular specifications. Statements in the language possess appropriate temporal semantics. This facilitates analysis of a set of specifications for possible inconsistencies. An algorithm is designed for systematically synthesizing code for a synchronizer from given specifications. Constraints on each type of access to the shared resource are derived by applying meaning preserving transformation rules to the high-level specifications. Code is generated in a specific target language utilizing knowledge pertaining to synchronization primitives in that language. The resulting synchronizer is synthesized so as to service requests according to the scheduling discipline specified. Examples of several standard synchronization problems are expressed in this specification language. Feasibility of the synthesis algorithm is demonstrated by providing an implementation to automatically generate resource controllers for a simulation of Applicative Multi Processor System (AMPS).