The following program is a mutual exclusion protocol for two processes due to Pnueli [1]. There is a single shared variable s which is either 0 or 1, and initially 1. Besides, each process has a local Boolean variable y that initially equals 0. The program text for process Pi (i = 0, 1) is as follows:
loop forever do begin
l1: Noncritical section
l2: (yi, s) := (1, i);
l3: wait until ((y1−i = 0) ∨ (s ≠ i)); l4: Critical section
l5: yi := 0
end.
Here, the statement (yi, s) := (1, i); is a multiple assignment in which variable yi := 1 and s := I is a single, atomic step.
Answer following questions:
a) Define the program graph of a process in Pnueli’s algorithm.
b) Determine the transition system for each process.
c) Construct their parallel composition.
d) Check whether the algorithm ensures mutual exclusion.
e) Check whether the algorithm ensures starvation freedom.
f) The last two questions may be answered by inspecting the transition system.