This assignment is about the well-known Peterson's algorithm for mutual exclusion. Open the following files in Uppaal:
These files contain a model of the algorithm. Read the explanation below and experiment a bit with the simulator before continuing with the assignment.
There are two instances of template P: two processes that run in parallel: one with pid value 0 and one with pid value 1. The algorithm uses three variables, flag, flag and turn. A flag value of 1 indicates that a process wants to enter the critical section. The variable turn contains the name ("process identifier" or "pid") of the process which turn it is to enter the critical section. In pseudo code the algorithm for process P(pid) looks as follows:
flag[pid] = 1
turn = 1-pid
while( flag[1-pid] && turn == 1-pid );
// do nothing
// critical section
// end of critical section
flag[pid] = 0
The translation from pseudo code to Uppaal is straightforward. It is important to realize that the condition flag[1-pid] && turn == 1-pid is not "atomic". It may happen, for instance, that process P(0) first evaluates flag, next process P(1)takes a number of steps, and only then the second part of the condition conditie turn == 1 is evaluated. In the model the evaluation of the condition is therefore described by a pair of consecutive transitions: if in location try2 variable flag[1-pid] is false then the condition flag[1-pid] && turn == 1-pid can not evaluate to true, and thus the process may enter the critical section. If however flag[1-pid] is true then the second part of the condition must also be evaluated. This happens in location try3: if turn==pid then the process may enter the critical section, otherwise it returns to try2.
With the Uppaal verifier we can easily check that Peterson’s algorithm satisfies the condition of mutual exclusion: for all reachable states it holds that P(0) and P(1) cannot be simultaneously in the critical section:
A ( not( P(0).cs and P(1).cs ))
Using Uppaal we may also check that the algorithm has no deadlocks, that is, in any reachable state a transition is possible.
Wikipedia devotes a special page to Peterson's algoritme. A few years ago, it was claimed on this page that
If P0 is in its critical section, then flag is 1 and either flag is false or turn is 0.
Show that this claim is incorrect by exhibiting an execution that ends in a state in which the above property does not hold. Formulate the property in Uppaal and use the verifier to generate a counterexample. Tip: logical "or" is written in Uppaal as || and logical "implication" as imply. If necessary you may also consult the Uppaal help menu. See "Language Reference -> Requirement Specification" en "Language Reference -> Expressions" for examples of correctness properties.
In the model we describe an implementation in which in location try2 first the condition flag[1-pid] is evaluated and only after that (if necessary) condition turn == 1-pid. Adapt the model to an implementation in which the order is reversed and first turn == 1-pid is evaluated and flag[1-pid]. Does this change affect the correctness of the algorithm? Make also a version of the model in which the evaluation may occur in both orders. Does this make a difference?
An important property of Peterson's algorithm is that a process has to wait for at most one time for the other process. We can prove this by making an version of the model in which timing information is added. We assume that the execution of an assignment or test takes at most l time units, and that a process may stay for at most c time units in the critical section. The extended model can be found here:
In the model we have introduced in the global declaration section two constants l and c, and assigned values 4 and 100, respectively; you can easily change these values yourself. The idea is that each process has a local clock x, which is reset to 0 each time when the process jumps to a new location. The invariant x<=1 of location try0 ensures that the process may stay for at most l time unit in this location. In this way we model that execution of the instruction flag[pid]=true takes at most l time units. In a similar fashion the rest of the model has been annotated. In order to determine how much time elapses maximally between the moment at which a process indicates that it wants to enter the critical section (by jumping to try0) and the moment at which the process enters the critical section, we introduce for each process an auxiliary clock y, that is set to 0 when the process jumps to try0. We now may ask Uppaal if the following property holds:
A (P(0).try0 || P(0).try1 || P(0).try2 || P(0).try3) imply P(0).y <= 1000
In words: as long as process P(0) is in the trying region (one of the locations try0-try3) the value of clock y will not exceed 1000. This implies that process P(0) has to wait at most 1000 time units before entering the critical section.: the only way to leave the set of locations try0-try3 is by entering the critical section!
Determine the maximal waiting time m, that ism the maximal time that may elapse between the moment that a process enters the trying region and the moment that it enters the critical section. You can do this by playing with the upper bound 1000 in the above formula. Repeat this for all possible combinations with l = 1, 2, 4 and c = 50, 100. Can you give an expression for m in terms of l and c? Describe a run of the algorithm in which it takes maximally long before process P(0) enters the critical section.