Synthesis of Efficient Drinking Philosphers Algorithms

Abstract

A variant of the drinking philosphers algorithm of Chandy and Misra is described and proved correct in a module way, using the I/O automaton model of Lynch and Tuttle. The algorithm of Chandy and Misra is based on an particular dining philosophers algorithm, and relies on certain properties of its implementation. The drinking philosophers algorithm presented in this paper is able to use an arbitrary dining philosophers algorithm as a true subroutine; nothing about the implementation needs to be known, only that is solves the dining philosophers problem. An important advantage of this modularity is that by substituting a more time-efficient dining philosophers algorithm with O(1) worst-case waiting time is obtained, whereas the drinking philosophers algorithm of Chandy and Misra has O(n) worst-case waiting time (for n philosophers). Formal definitions are given to distinguish the drinking and dining philosophers problems and to specify precisely varying degrees of concurrency.