{Complexity}

Dining philosophers problem is a typical example of dead-lock situation, in this case, we already know that in this dining philosophers model, there exists a dead-lock problem. But most of practical cases, it is pretty hard to figure out dead-lock problem.

Spin can make us test a model before we implement that model.

the following is Promela code which describe dining philosophers problem.
then we can simulate it with spin.

• spin file.prom — simulate the system (one randomly selected run)
• spin -a file.prom — generate a verifier (in pan.c)
• gcc pan.c — compile the verifier
• a. out — run the verifier (exhaustive searching of all possible runs)
• spin -t -p file.prom — make the simulator follow the failure trace if the verifier found an error. without ‘-p’ it only prints the final state; with ‘-p’ te whole state trce is printed (can be long!)
• gcc -DNP pan.c — compile the verifier for liveness (need “progress” labels in your promela code)

[ diningphil.prom ]

#define   N 4
byte Fork[N];
#define Think( I )  printf( "Think %dn", I )
#define Eat( I )    printf( "Eat %dn", I )

proctype Philosopher( byte I ) {
do
:: Think( I ) ;
atomic { (Fork[I] > 0);       Fork[I]-- } ;
atomic { (Fork[(I+1)%N] > 0); Fork[(I+1)%N]-- } ;
progress:
Eat( I ) ;
Fork[I]++;
Fork[(I+1)%N]++;
od
}

init {
byte   ind ;
assert( N > 2 ) ;
atomic {
ind = 0;
do
:: (ind >= N) ->
break;
:: else ->
Fork[ind] = 1;
ind++;
od;
ind = 0;
do
:: (ind >= N) ->
break;
:: else ->
run Philosopher( ind );
ind++;
od;
}
}