On the Formal Specification of Group Membership Services

Abstract

: The problem of group membership has been the focus of much theoretical and experimental work on fault-tolerant distributed systems. This has resulted in a voluminous literature and several formal specifications of this problem have been given. In this paper, we examine the two most referenced formal specifications of group membership and show that they are unsatisfactory: One has flaws in the formalism and allows undesirable executions, and the other can be satisfied by useless protocols. Key-words: group membership, asynchronous systems, primary partition, single group view, partitionable group, multiple group views, safety, liveness. (R'esum'e : tsvp) Research partially supported by NSF grant CCR-9402894 and DARPA/NASA Ames grant NAG-2-593 INRIA, B.P. 105, 78153 Le Chesnay Cedex, FRANCE. Laboratoire d'Informatique LIX, Ecole Polytechnique, 91128 Palaiseau Cedex, FRANCE. INRIA, B.P. 105, 78153 Le Chesnay Cedex, FRANCE. Department of Computer Science, Upson Hall, Cornell Univers...