A Caltech Library Service

An Axiomatic Definition of Synchronization Primitives

Martin, Alain J. (1981) An Axiomatic Definition of Synchronization Primitives. Acta Informatica, 16 (2). pp. 219-235. ISSN 0001-5903. doi:10.1007/BF00261260.

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item:


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.

Item Type:Article
Related URLs:
URLURL TypeDescription
Additional Information:© Springer-Verlag 1981. Received July 3, 1979 /June 21, 1981. Series numbering from Record Number: CaltechCSTR:1982.5046-tr-82
Group:Computer Science Technical Reports
Subject Keywords:Information System, Operating System, Data Structure, Communication Network, Information Theory
Other Numbering System:
Other Numbering System NameOther Numbering System ID
Computer Science Technical Reports1982.5046
Issue or Number:2
Record Number:CaltechCSTR:1982.5046-tr-82
Persistent URL:
Official Citation:Martin, A.J. Acta Informatica (1981) 16: 219.
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:47235
Deposited On:15 Jul 2014 23:02
Last Modified:10 Nov 2021 17:36

Repository Staff Only: item control page