In SIAM Journal on Computing (SICOMP), 32(1), pages 78-130, November 2002.
Previous version in the 20th International Conference on Distributed Computing Systems (ICDCS), pages 344-355, April 2000.
Older paper: Massachusetts Institute of Technology, Laboratory for Computer Science Technical Report LCS-TR-794, November 1999.
Specifically, the paper defines service semantics for the client-server interface, that is, for the group membership service. The paper then specifies virtually synchronous semantics for the new group multicast service, as a collection of safety and liveness properties. These properties have been previously suggested and have been shown to be useful for distributed applications. The paper then presents new algorithms that use the defined group membership service to implement the specified properties. The specifications and algorithms are presented incrementally, using a novel inheritance-based formal construct (see [Keidar et al., 2002]). The algorithm that provides the complete virtually synchronous semantics executes in a single message round, and is therefore more efficient than previously suggested algorithms providing such semantics. The algorithm has been implemented in C++. All the specifications and algorithms are presented using the I/O automaton formalism. Furthermore, the paper includes formal proofs showing that the algorithms meet their specifications. Safety properties are proven using invariant assertions and simulations. Liveness is proven using invariant assertions and careful operational arguments.