Causal Group Multicast: A Formal Description

P. Tyler
Basser Department of Computer Science
University of Sydney
Sydney, N.S.W. 2006, Australia

ABSTRACT
This paper presents two specifications of causal group multicast. In the first, causal ordering will be explained and explored in the context of group multicast. Failures will be introduced and a specification of causal group multicast which includes node crashes will be given. This final specification describes the service provided by ISIS's causal multicast facility. The models are expressed using the I/O automaton.

1. Introduction

This paper presents formal specifications for causal group multicast systems, one assuming no failures, the second allowing the possibility of real node failures and perceived node/link failures. The second specification is a specification for the ISIS[1][2] causal multicast service.

In the past specifications may have been given in languages open to some interpretation, but here we provide a precise specification using the I/O Automaton [6]. In Fekete[4], it is argued that formal methods can play an important part in specification and exploration of a service. Further it is suggested that a user of a service relies on "what is provided" rather than "how it is provided". The specification gives the user a precise definition of what a service provides, and can be used as a tool for a system designer in verifying compatibility of newer algorithms.

Multicast is a network service similar to broadcast, except that it restricts message delivery to a specific set of nodes. The delivery set can be defined in many ways, including requiring the sending client to provide a list of nodes at which to deliver the message, or by the service providing a grouping mechanism. A grouping mechanism is simply a single identification for a group of nodes. The nodes in the group will usually have a common task or purpose and communicate using a unique group identification (group id). A node is free to join and leave the group, with the underlying communication protocol keeping track of which nodes are currently members of the group. To send a message, a sending node need only supply the message and the group identification, knowing that the nodes who require the message have joined the group. A node is responsible for joining or leaving a group and is not restricted to belonging to one group. ISIS however requires that a node belong to a group to which it sends a message, and this is what we model. Using groups assumes that the node knows the group id or is able to get it independently of the multicast algorithm. Usually we expect the group id