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;
if not(id=i) then goto L;
// Inside critical section.
id := 0;
i identifies the process (i.e.,
has the value 1 or 2), and
id is a global variable, with
value 0 initially.
pause(delay) delays the execution for
delay time units. It is assumed that the assignment
id := i; takes at most
t time units.
- 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
tdoes the algorithm work? Hint: there is a relation between the two time parameters.
- Experiment with different values for
t. Simulate the systems. Verify them against the correctness properties. Did your intuition coincide with the experiment results?