Martin, Alain J. (1981) An Axiomatic Definition of Synchronization Primitives. Acta Informatica, 16 (2). pp. 219-235. ISSN 0001-5903. http://resolver.caltech.edu/CaltechCSTR:1982.5046-tr-82
Full text is not posted in this repository. Consult Related URLs below.
Use this Persistent URL to link to this item: http://resolver.caltech.edu/CaltechCSTR:1982.5046-tr-82
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.
|Additional Information:||© Springer-Verlag 1981. Received July 3, 1979 /June 21, 1981.|
|Group:||Computer Science Technical Reports|
|Usage Policy:||No commercial reproduction, distribution, display or performance rights in this work are provided.|
|Deposited By:||Kristin Buxton|
|Deposited On:||15 Jul 2014 23:02|
|Last Modified:||15 Jul 2014 23:02|
Repository Staff Only: item control page