Case study : Philosophers
Presentation :
This case study for the verification tool Quasar presents a solution to the well known problem of the dining philosophers initially introduced by E. W. Dijkstra.
This one has been given by Laurent Pautet in an advanced computing science course at ENST Paris. Laurent Pautet solves the problem by a subtle use of the requeue mechanism. This results in a non trivial solution that human reasoning can't easily handle. However, the use of a verification program such Quasar, which is based on the Petri net formalism, enables us to formally prove some critical properties like the deadlock presence.
On this example, Quasar reports no deadlock after a few seconds search. This is a due to the egg-shell model semantic of the protected objects.
A small modification of the program, for example changing the following assignment :
- Updating := Get_Left_Q'count > 0 or Get_Right_Q'count > 0
at line 41 by this one :
- Updating := Get_Left'count > 0 and Get_Right'count > 0
leads to a "deadlockable" program that even many simulations didn't report because of the queuing policy implemented. Using Quasar on the modified program show us the execution which leads on the deadlock. By this way, we can prove that this solution doesn't allow any modification.
Major Ada language components added :
- Protected type declaration
- Protected entry call and requeue
- Count attribute
- Task type declaration
- Tasks table
- Task entry call
Downloads :
Pictures :
|
|
| The dining philosophers example | Petri nets view |
|
|
| Automata view | No deadlock ! |
last update : 10/02/2004