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;
}
It is
sufficient to show that when one process enters the CS the other process is not
in the CS.
o
Case
1.2.1. Suppose
flag[0]=false at t2. Then P0 is in NCS at time t2. Therefore at some time t3 in
the interval (t2, t1), P0 sets turn to 1. From t3 to t1, P0 does not change
turn. From t2 to t1, P1 remains in CS, hence P1 cannot set turn to 0. Hence
turn should be 1 at t1. Contradiction.
end 1.2.1
end 1.2
end 1
end of
safety proof
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
Symmetric
to the argument of progress proof for P0.