TY - JOUR
T1 - Peterson's mutual exclusion algorithm revisited
AU - Sommen, van der, F.W.
AU - Feijen, W.H.J.
AU - Gasteren, van, A.J.M.
PY - 1997
Y1 - 1997
N2 - A new derivation of Peterson's well-known mutual exclusion algorithm is presented. The derivation is driven by the formally stated requirements of Individual Progress, as opposed to the more traditional approach which starts from the requirement of Mutual Exclusion. The only formalisms used in the derivation are the predicate calculus and the theory of Owicki and Gries. No use is made of temporal logic. In particular, the so complicating oscillating behaviour of an await-condition is fully absorbed by the use of a variant function.
AB - A new derivation of Peterson's well-known mutual exclusion algorithm is presented. The derivation is driven by the formally stated requirements of Individual Progress, as opposed to the more traditional approach which starts from the requirement of Mutual Exclusion. The only formalisms used in the derivation are the predicate calculus and the theory of Owicki and Gries. No use is made of temporal logic. In particular, the so complicating oscillating behaviour of an await-condition is fully absorbed by the use of a variant function.
U2 - 10.1016/S0167-6423(97)00003-8
DO - 10.1016/S0167-6423(97)00003-8
M3 - Article
SN - 0167-6423
VL - 29
SP - 327
EP - 334
JO - Science of Computer Programming
JF - Science of Computer Programming
IS - 3
ER -