Saint's Log

Modelling the Infamous Dining Philosophers

A sample implementation of the dining philosophers problem is provided in the JPF core source code. The solution I gave to this problem was to use the following locking scheme: if a thread has an even id i, then it should lock fork i first and then fork (i + 1) % N. If its id i is odd, then it should lock fork (i + 1) % N first and then lock fork i. Replacing

new Philosopher(forks[i], forks[(i + 1) % N]);

with

Fork leftFork, rightFork;
if (i % 2 == 0) {
    leftFork = forks[i];
    rightFork = forks[(i + 1) % N];
} else {
    leftFork = forks[(i + 1) % N];
    rightFork = forks[i];
}
new Philosopher(leftFork, rightFork);

Should do the trick. DiningPhil.jpf can then be launched to verify the absence of deadlock with this new locking scheme.