## Partial mutual exclusion for infinitely many processes

Partial mutual exclusion is the *drinking philosophers
problem* for complete graphs. It is the problem that a process
may enter a critical section *CS* of its code only when some
finite set *nbh* of other processes are not in their critical
sections. For each execution of *CS*, the set *nbh* can be
given by the environment. We have posted this paper Partial mutual exclusion for
infinitely many processes, with a starvation free solution of this
problem in a setting with infinitely many processes, each with finite
memory, that communicate by asynchronous messages. The solution has
the property of first-come first-served, in so far as this can be
guaranteed by asynchronous messages. For every execution of *CS*
and every process in *nbh*, between three and six messages are
needed. The correctness of the solution is argued with invariants and
temporal logic. It has been verified with the proof assistant PVS;
readers familiar with PVS can inspect and process the gzipped PVS
dump file.

Comments and questions are welcome.

Back to my home page.

Wim H. Hesselink

Last modified: Tue Dec 6 13:35:07 CET 2011