The Doomsday Distributed Termination Detection Protocol

Distributed termination detection (DTD) algorithms are important since they detect globally stable states in distributed computations. Here we introduce a new DTD mechanism, the Doomsday protocol together with its proof of correctness. Doomsday is generic since it forms the basis for a number of new and existing DTD algorithms for which the correctness proof may be reused. The paper describes the Doomsday protocol, provides its formal proof, derives one new DTD algorithm and shows how other hitherto unrelated algorithms, Dijkstra-Scholten, Task Balancing and Credit Recovery, can be derived from the protocol. The paper concludes by examining various properties of the protocol in the context of existing DTD algorithms.