Assignment: Peterson's Algorithm for Mutual Exclusion
Background
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[0], flag[1] 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:
while(true)
{ 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[1], 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.
Question 1
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[0] is 1 and
either flag[1] 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.
Question 2
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?
Question 3
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.