LCS Publication Details
Publication Title: CORRECTNESS PROOFS OF THE PETERSON-FISCHER MUTUAL EXCLUSION ALGORITHM.
Publication Author: Colby, Christopher P.
Additional Authors:
LCS Document Number: MIT-LCS-TM-399
Publication Date: 6-1-1989
LCS Group: No Group Specified
Additional URL: No URL Given
Abstract:
The Peterson-Fischer 2-process mutual exclusion algorithm is introduced in a slightly modified form. An invariant-assertional proof of mutual exclusion is presented for the 2-process algorithm. Next, the Peterson-Fischer n -process mutual exclusion algorithm is introduced conceptually as a tournament of [lg n ] 2-process competitions. A mutual-exclusion proof of the n-process algorithm is presented, based on a mapping between states of the n -process system and states of the 2-process system. This mapping delineates the correspondence between the 2-process code and one iteration (competition) of the n -process code. In this way, the statement of correctness of the 2-process algorithm is used as a lemma for the n-process proof.
To obtain this publication:

To purchase a printed copy of this publication please contact MIT Document Services.