Summary
The semantics of a pair of synchronization primitives is characterized by three fundamental axioms: boundedness, progress, and fairness. The class of primitives fulfilling the three axioms is semantically defined. Unbuffered communication primitives, the symmetrical P and V operations, and the usual P and V operations are proved to be the three instances of this class. The definitions obtained are used to prove a series of basic theorems on mutual exclusion, producer-consumer coupling, deadlock, and linear and circular arrangements of communicating buffer-processes. An implementation of P and V operations fulfilling the axioms is proposed.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Dijkstra, E.W.: Co-operating sequential processes. In: Programming languages, pp. 43–112 (F. Genuys, Ed.), New York: Academic Press, 1968
Dijkstra, E.W.: Guarded commands, non-determinancy, and formal derivation of programs. Comm. ACM 18, 453–457 (1975)
Dijkstra, E.W.: A class of allocation strategies inducing bounded delays only. Proc. S.J.C.C., pp.933–936 (1972)
Habermann, A.N.: Synchronization of communicating processes. Comm. ACM 15, 171–176 (1972)
Hoare, C.A.R.: Communicating sequential processes. Comm. ACM 21, 666–677 (1978)
Morris, J.M.: A starvation-free solution to the mutual exclusion problem. Information Processing Lett. 8, 76–80 (1979)
Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Comm. ACM 19, 279–285 (1976)
Author information
Authors and Affiliations
Rights and permissions
About this article
Cite this article
Martin, A.J. An axiomatic definition of synchronization primitives. Acta Informatica 16, 219–235 (1981). https://doi.org/10.1007/BF00261260
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00261260