Specifying and Using a Partitionable Group Communication Service

Group communication services are becoming widely accepted as useful building blocks for the construction of fault-tolerant distributed applications. Many system designers and researchers have proposed formal specifications for group communication services. However, there is still no agreement about what these specifications should say, especially in cases where the services are partitionable, that is, where disjoint sets of members may simultaneously believe they constitute the whole group. In this paper, we present a new, simple specification for a partitionable group communication service. We use the specification to construct an ordered-broadcast application, using an algorithm (based on algorithms of Amir, Dolev, Keidar and others) that reconciles information derived from different instantiations of the group. We prove the correctness and analyze the performance and fault-tolerance of the resulting application. Our specification has a simple implementation, based on the membership ..