A Client-Server Approach to Virtually Synchronous Group Multicast: Specifications, Algorithms, and Proofs.

Authors:Idit Keidar and Roger Khazan.
 

Abstract:

This paper presents a formal design for a novel group communication service targeted for WANs. The service provides Virtual Synchrony semantics. Such semantics facilitate the design of fault tolerant distributed applications.  The presented design is more suitable for WANs than previously suggested ones. In particular, it features the first algorithm to achieve Virtual Synchrony semantics in a single communication round. The design also employs a scalable WAN-oriented architecture: it effectively decouples the main two components of Virtually Synchronous group communication --- group membership and reliable group multicast.

The design is carried out formally and rigorously.  This paper includes formal specifications of both safety and liveness properties.  The algorithm is formally modeled and assertionally verified.
 
 
20th International Conference on Distributed Computing Systems (ICDCS), April 2000: (12 pages) ps, pdf, ps.gz
A Virtually Synchronous Group Multicast Algorithm for WANs: Formal Approach. SIAM Journal on Computing. Volume 32. Number 1. pp. 78-130, 2002.: ps, pdf, ps.gz
Journal version submitted to SIAM JComp September 2000): (more discussion, explanations, and proofs, 55 pages) ps, pdf, ps.gz
Technical Report (MIT-LCS-TR-794, November 1999): ps, pdf, ps.gz

r_o_g_e_r_AT_l_c_s_._m_i_t_._e_d_u