Usage of a formal result to design a causally and totally ordered multicast protocol

The paper aims at a causal and total order for overlapping multicast groups. A communication tree is considered. The messages are propagated to the different multicast groups through different covering sub-trees. Since a reliable transmission exists between the different entities, a total order is provided by propagation across the relevant sub-trees. A formal result enables to prove that a total order, using such a tree, provides a causal order when the emitter belongs to the group and when a local order (FIFO) is satisfied. Thus, the design of a causal layer of protocol is completely avoided. Paper presents the use of the formal result and the proofs. The implementation over the Internet is described briefly. It includes a reliable transmission, a routing module maintaining different multicast roots and a group membership component. Except the reliable transmission, the system does not use any sequencing nor any reordering. That solution, called CTOP, runs on Unix and Windows systems. It can be integrated to a simulation middleware to guaranty the logical ordering of the simulation events.