A Semantics of Synchronization.
Abstract
This paper presents a rigorous framework to discuss the synchronization necessary to coordinate accesses to a resource. The framework, among other things, provides a method for specifying concurrency and forms the semantic basis of a synchronization mechanism which avoids certain unfortunate characteristics of monitors and serializers. Synchronization is viewed as being managed by a resource guardian. A synchronization problem is defined as a predicate on event sequences. The interaction of a guardian and the rest of the system is formalized in terms of a two person game. This formalization results in precise definitions of guardian and guardian behavior. The notion of a 'good' or optimal solution is defined, and the solutions to certain classes of synchronization problems are characterized. An abstract description of the general actions of a guardian is given. This general description, with some restrictions, forms the basis of a simple synchronization mechanism for actually implementing solutions. The mechanism is given a rigorous semantics based on the definition of guardian. This facilitates the verification of correctness. Many examples of the use of the mechanism are given and its advantages are discussed. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1980
- Accession Number
- ADA091015
Entities
People
- Carl R. Seaquist
Organizations
- Massachusetts Institute of Technology