Abstract
We introduce a very high level language for specifying synchronization properties. It is designed using the primitives of temporal logic which facilitates the specification of both invariant and time-dependent properties. The paper begins with a discussion of properties that affect synchronization. The specification language then introduced features constructs to express each of these in a fairly natural and modular fashion. Since the statements in the language have intuitive interpretations, specifications are humanly readable. Also, since they possess appropriate formal semantics, unambiguous specifications result.
This material is based upon work supported by the National Science Foundation under Grant MCS-77-09369 A01.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Agerwala, T. A Complete Model for Representing the Coordination of Asynchronous Processes. Technical Report Computer Research Report 32, John Hopkins University, 1974.
Courtois, P.J., Heymans, F. and Parnas, D.L. Concurrent Control with ‘Readers’ and ‘Writers'. Communications of the ACM 14:667–668, Oct, 1971.
Griffiths, P. SYNVER: A System for the Automatic Synthesis and Verification of Synchronization Processes. Technical Report TR 22-74, Harvard University, 1974.
Habermann, A.N. Path Expressions. Technical Report, Carnegie-Mellon University, June, 1975.
Hoare, C.A.R. Monitors: An Operating System Structuring Concept. Communications of the ACM 17:540–557, Oct, 1974.
Hoare, C.A.R. Communicating Sequencial Processes. Communications of the ACM 21:666–677, Aug, 1978.
Lamport, L. 'sometime’ is Sometimes ‘Not Never'. In Proc. Seventh Annual Symposium on POPL, pages 174–185. Jan, 1980.
Laventhal, M.S. Synthesis of synchronization code for data abstractions. PhD thesis, Massachusetts Institute of Technology, June, 1978.
Pnueli, A. The Temporal Semantics of Concurrent Programs. Springer-verlag, 1979, pages 1–20.
Pnueli, A. On the Temporal Ananysis of Fairness. In Proc. Seventh Annual Symposium on POPL, pages 163–173. Jan, 1980.
Ramamritham, K. and Keller, R.M. Specification and Synthesis of Synchronizers. In Proc. 1980 International Conference on Parallel Processing. Aug, 1980.
Schmid, H.A. On the efficient Implementation of Conditional Critical Regions and the Construction of Monitors. Acta Informatica 6:227–249, 1976.
Shaw, A.C. Software Specification Languages Based on Regular Expressions. In Software Tools Workshop, pages 1–39. May, 1979.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1981 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ramamritham, K., Keller, R.M. (1981). On synchronization and its specification. In: Brauer, W., et al. Conpar 81. CONPAR 1981. Lecture Notes in Computer Science, vol 111. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0105124
Download citation
DOI: https://doi.org/10.1007/BFb0105124
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-10827-6
Online ISBN: 978-3-540-38715-2
eBook Packages: Springer Book Archive