QUASAR : Examples

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 :

at line 41 by this one :

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 :

Downloads :

Source code / Pdf version

Pictures :

The dining philosophers example Petri nets view
The dining philosophers example Petri nets view
Automata view No deadlock !
Automata view No deadlock !

last update : 10/02/2004