CMSC 412


Feb 27, 1999

Peterson's Solution for 2-Process Mutual Exclusion

1. Solution

Peterson's algorithm is the simplest known solution to the mutual exclusion problem for the special case of two process, i.e., processes Pi for i = 0 and 1.

Xvars(i) {
   boolean flag[0..1] := false;
     // flag[i]=true implies Pi is hungry or eating
   integer turn := 0 or 1;
     // turn indicates the process of higher priority in case of contention

    entry(i) {
1:   flag[i] := true;
2:   turn := j;
3:   while flag[j] and turn=j do skip;

   exit(i) {
4:   flag[i] := false;

2. Proof of Safety

It is sufficient to show that when one process enters the CS the other process is not in the CS. end of safety proof

3. Proof of Progress for P0

Suppose P0 becomes hungry at time t1 (i.e., executes 1).
We need to show that P0 eventually enters the CS, i.e., gets past 3.
At some time t2 (> t1), P0 starts testing the condition in 3 (because 1 and 2 cannot block).

Case 1: P1 is thinking at t2.
Then flag[1]=false at t2, when P0 executes 3, and P0 gets past 3 at t2.

Case 2: P1 is eating at t2.
Then turn=1 and P1 has to wait (recall that we already proved safety).
Eventually at some time t3 (>t2) P1 finishes eating and does 4.

   Case 2.1: P1 stays thinking until P0 tests condition.
   Then P0 gets past 3 (at some time after t3).

   Case 2.2: P1 becomes hungry at time t4 (>t3) before P0 tests condition.
   Then P1 eventually executes 3, setting turn to 0.
   After this turn remains 0 and P0 eventually gets past 3 (at some time after t4).

Case 3: P1 is hungry at t2.
Then flag[1]=true at t2, and turn determines who gets to eat next.

   Case 3.1: P1 was the last to update turn.
   Then turn=0 at t2 and P0 gets past 3.

   Case 3.2: P0 was the last to update turn.
   Then turn=1 at t2, P0 waits, and P1 gets past 3 at some time t3 (>t2).
   At this point, P1 is eating and this case reduces to case 2.
end of progress proof for P0

4. Proof of progress for P1

Symmetric to the argument of progress proof for P0.