A Virtually Synchronous Group Multicast Algorithm for WANs: Formal Approach.

Authors: Idit Keidar and Roger Khazan.

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.


This paper presents a formal design for a novel group multicast service that provides virtually synchronous semantics in asynchronous fault-prone environments. The design employs a client-server architecture in which group membership is maintained not by every process but only by dedicated membership servers while virtually synchronous group multicast is implemented by service end-points running at the clients. This architecture allows the service to be scalable in the topology it spans, in the number of groups, and in the number of clients. Our design allows the virtual synchrony algorithm to run in a single message exchange round, in parallel with the membership algorithm: it does not require pre-agreement upon a common identifier by the membership algorithm.

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.


Preprint of SICOMP paper: ps, ps.gz, pdf.
ICDCS 2000 paper: ps, ps.gz, pdf.
ICDCS talk slides (powerpoint): ppt.
1999 Technical Report: ps, ps.gz, pdf.

Last modified: Sun Dec 29 13:13:57 IST 2002