An axiomatic definition of synchronization primitives |
| |
Authors: | Alain J. Martin |
| |
Affiliation: | (1) Philips Research Laboratories, 5600 MD Eindhoven, The Netherlands |
| |
Abstract: | 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. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|