Generalised Dining Philosophers as Feedback Control

Abstract

We examine the mutual exclusion problem of concurrency through the systematic application of modern feedback control theory, by revisiting the classical problem involving mutual exclusion: the Generalised Dining Philosophers problem. The result is a modular development of the solution using the notions of system and system composition in a formal setting that employs simple equational reasoning. The modular approach separates the solution architecture from the algorithmic minutiae and has the benefit of simplifying the design and correctness proofs. Two variants of the problem are considered: centralised and distributed topology with N philosophers. In each case, solving the Generalised Dining Philosophers reduces to designing an appropriate feedback controller.