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?