VV: Exercise 2

Dining philosophers

Introduction

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

1. absence of deadlock: we cannot reach a state in which all philosophers get blocked waiting for a fork to become available.
2. mutual exclusion: a fork cannot be used by two different philosophers. In other words, we cannot reach a state in which two adjacent philosophers are simultaneously eating.
   
3. absence of starvation (liveness): we must guarantee that no philosopher will starve, that is, will alternate between thinking and eating forever.

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. For both algorithms, the philosopher pseudocode can be described as:

<think>;
<pick_forks>;
<eat>;
<leave_forks>

The actions of thinking and eating may take an arbitrary (but finite) number of steps. However, for verification purposes, we only have to guarantee that any possible ordering of events among different philosophers is considered. Since the option "spin -a ..." will always check all possible interleavings, the duration of thinking/eating actions is not relevant. In fact, they can just be a simple printf displaying what the philosopher is doing at that moment, or even an empty instruction.

Algorithm 1 (naive)

1. wait until grabbing the left fork
2. then wait until grabbing the right fork

Encode this solution in Promela and check its correctness. We should find a counterexample where a deadlock is reached. Print the counterexample trace using "spin -t -p ..." and add a textual or graphical explanation of what has happened. Try with different values for the number of philosophers: N=1..5

Hint: give a number to each philosopher 0..N-1 and a number to each fork 0..N-1. You can define the left and right fork for philosopher i using the pair of macros

#define left(i) (i)
#define right(i) ((i+1)%N)

Algorithm 2 (using a status array)

In the second algorithm, we will use a shared array to represent the current status of each philosopher, an array of general semaphores S and a mutex boolean variable. The status can be any of the following three:

mtype={thinking, eating, hungry};
mtype status[N];
bool S[N]; /* initialize to 0 */
bool mutex=1;

The main variation this time is that <pick_forks> looks like:

wait for mutex;
status[i]=hungry;
test(i);
release mutex;
wait for semaphore S[i]

whereas leave forks corresponds to:

wait for mutex;
status[i]=thinking;
test(left(i));
test(right(i));
release 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]

Assessment & delivery

The maximum grade for this exercise 2 is 1,3 points. You can do it alone or in couples. The deadline for delivery of exercises 1a and 1b is Friday, November 22nd, 2013 using the lab work mailbox or buzón de prácticas under the following instructions:

• Connect to any of the computers: 10.10.5.xxx with xxx from 118 to 126 (excepting 124)
• Copy all your files in the directory /PRACTICAS/GEI/VVS/P1/your_login
  

Optional (TGR)

Propose/implement a third variation that guarantees absence of deadlock, mutual exclusion and absence of starvation. This will add 0,6 extra points (TGR). One possibility is having a controller process or "waiter" to whom philosophers ask for permission to pick the forks.