Consider the following mutual exclusion algorithm for n processors (Algorithm 4.7), suggested by Lamport.
Prove that the algorithm provides mutual exclusion.
Hint. Suppose in contradiction that there is a configuration when two processors, pi and pj, are in the critical section simultaneously. Observe all the possible cases, e.g.: pi enters through the fast path whereas pj enters through the slow path, etc.
Prove the no deadlock property of the algorithm.
Hint. Assume that there is a deadlock, i.e., some processors are trying to enter the critical section, and none of them succeeds (although the execution is infinite).
- Show that there is no processor that continually executes goto in Line 6 or Line 13.
- Show that all the processors cannot be forever stuck waiting in Line 5/Line 10/Line 12.
Does the algorithm satisfy the no lockout property?