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.