The Doorman Solution for the Dining Philosophers Problem
The dining philosophers problem is one of the best-known
problems in distributed computing theory. In this problem
we have a table, around which are seated N philosophers.
In the center there is a large plate containing an unlimited
amount of spaghetti. Halfway between each pair of
philosophers there is a fork. In order to eat, a philosopher
needs two forks. Using forks that are beyond a philosopher's
reach is forbidden. The desired live cycle of a philosopher
consists of carrying out his or her private activities (for example,
thinking, and then writing up the results for publication),
becoming hungry and trying to eat, eating, and then back to
the private activities, ad infinitum.
How should the philosophers go about their rituals without
starving?
One solution to this problem involves introducing a new
player into the game, the dining room doorman. Philosophers
are instructed to leave the room when they are not interested
in eating, and try to re-enter when they are. The doorman
is required to keep the count of philosophers currently in the
room, limiting their number to N-1. That is, if the room contains
all but one philosopher, the last one will be kept waiting at the
door until someone leaves.
When appropriately formalized, this solution can be shown to
be satisfactory.
Problem 1 (2 points)
Formalize the problem to be solved - lack of starvation -
by a formula in propositional linear time temporal logic,
using the following set of atomic assertions:
-
Private(I): Philosopher I is carrying out his or her
private activity
-
Hungry(I): Philosopher I is hungry
-
Eating(I): Philosopher I is eating
Problem 2 (2 points)
Explain why if there are at most N-1 philosophers at the
table at any particular time, then at least one of them
can eat.
Problem 3 (2 points)
Formalize a rigorous version of the solution as an
I/O automaton
Problem 4 (4 points)
Prove correctness of the solution.
Pagina voor het laatst veranderd op 19/10/02 door
Frits Vaandrager.