entry(i) {
1: flag[i] := true;
2: turn := j;
3: while flag[j] and turn=j do skip;
}
exit(i) {
4: flag[i] := false;
}
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.