Fischer's Mutual Exclusion Algorithm

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

while true do begin
  // Noncritical section.
  L: if not(id=0) then goto L;
  id := i; 
  pause(delay);
  if not(id=i) then goto L;
  // Inside critical section.
  id := 0; 
end

The constant i identifies the process (i.e., has the value 1 or 2), and id is a global variable, with value 0 initially. The statement pause(delay) delays the execution for delay time units. It is assumed that the assignment id := i; takes at most t time units.

Tasks:

• Model Fischer'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.
• For what range of values for delay and t does the algorithm work? Hint: there is a relation between the two time parameters.
• Experiment with different values for delay and t. Simulate the systems. Verify them against the correctness properties. Did your intuition coincide with the experiment results?