| << Chapter < Page | Chapter >> Page > |
They following algorithm is an attempt to implement
mutual exclusion for two processes.Here, each process is willing to defer to the other.
(It also introduces Promela's
goto , which lets
you branch to a label; this is an alternate wayof implementing loops and other control flow.)
Verify whether the algorithm is correct or not.
1 int x, y, z;
23 active[2] proctype user()4 {
5 int me = _pid+1; /* me is 1 or 2. */6
7 L1:8 x = me;
9 if10 :: (y != 0&&y != me) ->goto L1 /* Try again. */
11 :: (y == 0 || y == me) /* Continue... */12 fi;
1314 z = me;
15 if16 :: (x != me) ->goto L1 /* Try again. */
17 :: (x == me) /* Continue... */18 fi;
1920 y = me;
21 if22 :: (z != me) ->goto L1 /* Try again. */
23 :: (z == me) /* Continue... */24 fi;
2526 /* Entering critical section. */
27 /* ... */28
29 /* Leaving critical section. */30 } As usual, we must check that no more than one process
is in the critical section at a time. We canour usual code
in_crit++;
assert(in_crit == 1);in_crit--; and declaring
in_crit global.
This code passes verification,
but warns us that this code isn't necessarily even executed!
For a critical section protocol to be valid, it must
also guarantee that each process eventually entersthe critical section.
Since the
goto s create a control flow loop,
we can check this by looking for non-progress cycles,labeling the critical section as progress.
me are not shown, since they cannot vary.Using temporal logic, we can create a formula that describe
our desired behavior:``Eventually, each process gets to the critical section,
but not both at the same time.''One such formula is
where we define
#define p (user[0]@crit)#define q (user[1]@crit) and define the label
crit in the critical section.
This is a Promela version of an algorithm once recommended by a major computer manufacturer.As you can see, like many other mutual exclusion algorithms that have been proposed, it is flawed.
The following is pseudocode for an attempt to implement
critical sections for
n processes.
It is based on the idea that processes take numbers,and the one with the lowest number proceeds next.
This algorithm has one small flaw.Your task is to find and fix the flaw.
In particular, show the following steps of this process.
Hints: First, do not radically change the algorithm.
There is a straightforward solution that only changes/addsa line or two.
Second, do not overly serialize the code.Since the entry protocol's
for loop is already serialized, this really means that each
each process should be able to calculate
max concurrently.
/* Is Pi choosing a number? */
boolean choosing[n];
/* Pi's number, or 0 if Pi has none. */unsigned int number[n]; /* No process has a number. */
for all j{0,,n-1}
number[j]= 0; i .
/* Choose Pi's number. */
choosing[i]= true;
number[i]= max(number[0],number[1],,number[n-1]) + 1;choosing[i] = false;/* For all other processes,*/
for all j{0,,i-1, i+1,,n-1} in some serial order
/* Wait if the other process is currently choosing. */while (choosing[j]) /* nothing */ ;/* Wait if the other process has a number and comes ahead of us. */
if ((number[j]>0)&&(number[j]<number[i]))while (number[j]>0) /* nothing */ ; Note that, because of the
if 's test,
it is equivalent to allow
j to get
the value
i in this loop, as well.
Although less intuitive, that simplifies the loop.i .
/* Clear Pi's number. */
number[i]= 0; The problem with the given code is that the concurrent
max computations
does not necessarily result in each element of
number[] being unique.
Uniqueness is assumed by the following conditional toprioritize the processes:
if ((number[j]>0)&&(number[j]<number[i]))
One of the hints precludes changing the
max calculation to produce
uniqueness. So, we need a way to prioritize processes whenthey receive the same number. This is most easily accomplished
by using their process IDs:
if ((number[j]>0)&&((number[j]<number[i]) ||((number[j] == number[i])&&j<i)))
Of course,
j>i is also fine.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|