CaltechAUTHORS
  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. 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

Abstract

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
http://dx.doi.org/10.1007/BF00261260DOIArticle
http://link.springer.com/article/10.1007/BF00261260PublisherArticle
Additional Information:© Springer-Verlag 1981. Received July 3, 1979 /June 21, 1981.
Group:Computer Science Technical Reports
Record Number:CaltechCSTR:1982.5046-tr-82
Persistent URL:http://resolver.caltech.edu/CaltechCSTR:1982.5046-tr-82
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:47235
Collection:CaltechCSTR
Deposited By: Kristin Buxton
Deposited On:15 Jul 2014 23:02
Last Modified:15 Jul 2014 23:02

Repository Staff Only: item control page