In this exercise we will play with a
classical example of concurrency problem proposed by E.
W. Dijkstra in 1965 as a student exam exercise.
"N=5 dining
philosophers sit on a table around a bowl of spaghetti.
A fork is placed between each pair of philosophers. Each
philosopher must alternatively think and eat. However, a
philosopher can only eat spaghetti when he has both left
and right forks. Each fork can be held by only one
philosopher and so a philosopher can use the fork only
if it's not being used by another philosopher. After he
finishes eating, he needs to put down both forks so they
become available to others. A philosopher can grab the
fork on his right or the one on his left as they become
available, but can't start eating before getting both of
them. Eating is not limited by the amount of spaghetti
left: assume an infinite supply." (source: wikipedia)
Goals
The goal of this exercise is playing with the example in
SPIN and verifying three main conditions. We will try
four
possible algorithms, checking in each case the
following properties:
- absence of deadlock: we cannot reach a state
in which all philosophers get blocked waiting for a
fork to become available.
- mutual exclusion: we cannot reach a state in
which two adjacent philosophers are simultaneously
eating.
- absence of starvation (liveness): we must
guarantee that no philosopher will starve, that is,
they can eat as much as they want (i.e. infinitely
many times).
Note that absence of deadlock does not imply absence of
starvation: perhaps two philosophers are eating and
thinking all the time, while the others get waiting
forever. On the other hand, if a deadlock exists, there is
no need to check liveness.
Note also that, as all philosophers execute the same code
and their behaviours are analogous, there is no need to
check all of them. We can just check liveness for
philosopher 0, and mutual exclusion between philosophers 0
and 1.
Algorithm 1 (naive)
The first algorithm tries to represent the physical
situation of the forks and uses a naive protocol (get both
forks and start eating). To this aim, we will represent
the forks as an array of
N
boolean flags:
bool
ontable[N]=1;
to tell us whether fork
i
is on the table (
ontable[i]==1) or not.
Each philosopher will be represented as a different
process numbered by
_pid
and will execute the following infinite loop:
do
:: printf("%d is thinking\n",
_pid);
pick_fork(LEFT);
pick_fork(RIGHT);
cs: printf("%d is eating\n", _pid);
leave_fork(RIGHT);
leave_fork(LEFT)
od
Complete the rest of the Promela code. Note that the macro
pick_fork(i) must
wait if the fork is not on the table.
Algorithm 2 (Dijkstra's solution)
The second algorithm is a simple variation of the naive
solution where rather than picking first the LEFT fork,
each philosopher always start picking her adjacent fork
with a
lowest number. The order in which forks are
left is irrelevant. Note: this solution, provided by
Dijkstra, avoids deadlocks but is not extrapolable to
other practical problems, since it assumes that we know
the resources (and their numbering) we will need in
advance.
Algorithm 3 (fixed turn)
In this case, we only use a general variable
byte
turn=0;
Each philosopher just checks that turn==_pid before
eating, and passes the turn to his right side
(circularly) once finished. There is no need to
represent the forks, as only one philosopher eats at
each moment.
Algorithm 4 (using a status array)
In the fourth algorithm (the classical solution using
semaphores), we will use a shared array to represent the
current status of each philosopher, an array
of semaphores S
plus a mutex
semaphore for the table. The status can be any of the
following three:
mtype={thinking, eating,
hungry};
mtype status[N]=thinking;
bool S[N]=0;
bool mutex=1;
The protocol is similar to Algorithm 1, but picking
forks is now done as follows:
wait(mutex);
status[_pid]=hungry;
test(_pid);
signal(mutex);
wait( S[_pid] );
whereas leaving forks corresponds to:
wait(mutex);
status[_pid]=thinking;
test(LEFT(_pid));
test(RIGHT(_pid));
signal(mutex);
The pseudocode for test(k)
is as follows
If k is hungry and his
adjacent philosophers are not eating,
then he begins eating
and releases semaphore S[k].
Otherwise, it does nothing
Assessment & delivery