Skip to content Skip to navigation
Give an English translation of the following LTL formulae. Try to give a natural wording for each, not just a transliteration of the logical operators.
In the following, give an LTL formula that formalizes the given English wording. If the English is subject to any ambiguity, as it frequently is, describe how you are disambiguating it, and why.
Recall the
Dining Philosophers Problem from the previous homework.
Using temporal logic, formally specify the following desired
properties of solutions to the D.P. Problem.
Use the following logic variables, where
For each question, your answer should cover exactly the given
condition -- nothing more or less.
You may assume
if statements, one per configuration,
and this is abbreviated.
¶
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 way
of implementing loops and other control flow.)
Verify whether the algorithm is correct or not.
1 int x, y, z;
2
3 active[2] proctype user()
4 {
5 int me = _pid+1; /* me is 1 or 2. */
6
7 L1:
8 x = me;
9 if
10 :: (y != 0 && y != me) -> goto L1 /* Try again. */
11 :: (y == 0 || y == me) /* Continue... */
12 fi;
13
14 z = me;
15 if
16 :: (x != me) -> goto L1 /* Try again. */
17 :: (x == me) /* Continue... */
18 fi;
19
20 y = me;
21 if
22 :: (z != me) -> goto L1 /* Try again. */
23 :: (z == me) /* Continue... */
24 fi;
25
26 /* 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 can our usual code
in_crit++;
assert(in_crit == 1);
in_crit--;
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 enters
the critical section.
Since the gotos create a control flow loop,
we can check this by looking for non-progress cycles,
labeling the critical section as progress.
 |
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
#define p (user[0]@crit)
#define q (user[1]@crit)
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/adds
a 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.
I.e., each process has the following
code immediately before its critical section.
¶
/* 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 */ ;
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.
I.e., each process has the following
code immediately after its critical section.
/* 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 to
prioritize 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 when
they 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.
More about this module: Metadata | Downloads | Version History
This work is licensed by John Greiner, Ian Barland, and Moshe Vardi under a Creative Commons Attribution License (CC-BY 2.0), and is an Open Educational Resource.
Last edited by John Greiner on Oct 6, 2005 3:45 pm -0500.