VVS: model checking

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

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:
  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: 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, 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

The maximum grade for this exercise is 2 points. Use campusvirtual.udc.gal platform (task: práctica SPIN). Upload your work as a single .zip file containing all the files with pml code and a report, in PDF or plain ASCII format. The report must explain the experiments you performed to check the 3 properties in each of the 4 algorithms, and the obtained results in each case. Exercises can be made by two students at most. If so, the students' names must be included in the first lines of each file and only one of the students needs to upload the files to his campusvirtual account.

The deadline for delivery is Friday,  April 5th,  2024 (23:59).