The Coq mailing list

[Stephane Demri <demri AT lsv.ens-cachan.fr>]

                               Séminaire 
                 Laboratoire Spécification et Vérification
                        http://www.lsv.ens-cachan.fr/


Mardi 10 décembre 2002 à 11 h, 
Salle de Conférence - Pavillon des Jardins, 


Catuscia Palamidessi (INRIA Futurs) fera un exposé sur
        
                        ''Generalized Dining Philosophers''





BASED ON WORKS IN COLLABORATION WITH: Oltea Mihaela Herescu and Michael
Pilquist

ABSTRACT: The problem of the dining philosophers, proposed by Dijkstra,
is a well-known example of control problem in distributed systems. In
the classic formulation the philosophers sit at a round table and there
is a fork between any two philophers. In order to eat, each philosopher
needs both his adjacent forks. The aim is to make sure that if there are
hungry philosophers then some of them  will eventually eat (deadlock
freedom), or, more ambitiously, that every hungry philosopher will
eventually eat (lockout freedom).

In the early 80's, Lehman and Rabin showed that there exist no
deterministic, symmetric and fully distributed solution to the problem
of the dining philosophers, and they proposed two randomized solutions:
one which guarrantees deadlock freedom with probability 1 and another
one which guarrantees lockout freedom with probability 1.

In this talk, we consider two generalization of the dining philosophers
problem and we investigate deadlock-free solutions for them.
We first consider the case where the number of philosophers
can exceed the number of forks, but where
each philosopher can still only access two forks, and we investigate
whether the randomized algorithms of Lehman and Rabin would still work
in this situation. We show that the answer is "No": in most cases, a
malicious scheduler can induce a deadlock. However, it is easy
to modify the algorithm so to obtain a randomized
solution, still fully distributed and symmetric, which works for any
number of philosophers and any kind of connection graph, and
guarrantees deadlock freedom with probability 1.

Then, we consider the yet more general case of forks shared and needed by
arbitrarily many philosophers, on an arbitrary connection graph. We show that
the solution proposed above does not work in this more general case, and we
propose a solution based on a completely different idea, still fully 
distributed
and symmetric, which guarrantees deadlock freedom with probability 1.

This work is part of a project which aims at providing a fully distributed
implementation of the $\pi$-calculus via an encoding into a randomized version
of the asynchronous $\pi$-calculus. The solution to the generalized dining
philosophers is used to solve the conflicts associated to the competition
for channels arising in presence of guarded-choices commands.







Cordialement,


---
Stéphane Demri

Laboratoire Spécification et Vérification 
CNRS UMR 8643, École Normale Supérieure de Cachan 
61, avenue du Président Wilson          
94235 CACHAN Cedex - France
demri AT lsv.ens-cachan.fr
                    http://www.lsv.ens-cachan.fr/~demri
Tel: ++ 33 1 47 40 55 68                Secret.: ++ 33 1 47 40 24 04
Fax: ++ 33 1 47 40 24 64                Office: RH-E-01b