Synthesis of Synchronization Code for Data Abstractions.
Abstract
Synchronization code is necessary to control shared access of an abstract data object in a parallel-processing environment. This thesis explores an approach in which a synchronization property can be specified in a high-level nonprocedural language, and an implementation for the specified property can be synthesized algorithmically. A problem specification language is introduced in which synchronization properties can be expressed in a structured but natural manner. A method is then presented for synthesizing an implementation. An intermediate form, called a solution specification, is first derived, representing an abstract solution to the problem. The derivation of the solution specification accomplishes the transformation of the specification from nonprocedural to procedural form. The solution specification can be translated directly into a source language synchronization mechanism, such as a monitor. Specifications for common synchronization properties, such as the readers-writers and bounded buffer problems, are expressed in the problem specification language. Corresponding implementations are then synthesized for these problems. In addition, the derived solution specification can be used in analyzing the soundness of the original problem specification with respect to criteria such as freedom from deadlock and starvation. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Jun 23, 1978
- Accession Number
- ADA058232
Entities
People
- Mark Steven Laventhal
Organizations
- Massachusetts Institute of Technology