Hyman's Mutual Exclusion Algorithm

Two processes are trying to enter their critical sections, executing the same program:

while true do begin
  b[i] := true;
  while not(turn=i) do begin
    while b[j] do begin
      skip; // do nothing
    end
    turn := i;
  end
  // beginning critical region
  b[i] := false;
end

The constant i identifies the process executing the code (i.e., has the value 1 or 2), and j is the identifier of the other process. b is an array with indices 1 and 2. Moreover let turn be either 1 or 2 initially.

Tasks:

• Model Hyman's algorithm in Uppaal.
• Formulate the correctness condition as a property, i.e., at most one process can be in the critical section at any given time.
• Formulate the condition that states that a process eventually enters it's critical section.
• Do the properties hold? Why/why not? If they do not, examine the resulting trace from verification in the simulator to learn more about the behaviour of the algorithm.