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
turn := i;
// beginning critical region
b[i] := false;
i identifies the process executing
the code (i.e., has the value 1 or 2), and
j is the identifier of the
b is an array
with indices 1 and 2. Moreover let
turn be either
- 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.