. Please consider the following mutual exclusion algorithm that uses the shared variables y1 and y2 (initially both 0).
Process P1:
while true do
. . . noncritical section . . .
y1 := y2 + 1;
wait until (y2 = 0) ∨ (y1 < y2)
. . . critical section . . .
y1 := 0;
od
Process P2:
while true do
. . . noncritical section . . .
y2 := y1 + 1;
wait until (y1 = 0) ∨ (y2 < y1)
. . . critical section . . .
y2 := 0;
od
Please answer following questions:
a) Give the program graph representations of both processes. (A pictorial representation suffices.)
b) Give the reachable part of the transition system of P1 || P2 where y1 ≤ 2 and y2 ≤ 2.
c) Describe an execution that shows that the entire transition system is infinite.
d) Check whether the algorithm indeed ensures mutual exclusion.
e) Check whether the algorithm never reaches a state in which both processes are mutually waiting for
each other.
f) Is it possible that a process that wants to enter the critical section has to wait ad infinitum?