Correctness of Broadcast via Multicast: Graphically and Formally

TL;DR

This paper investigates the correctness of data dissemination in networks, proving that multicast-based distribution behaves equivalently to ideal broadcast under certain topologies, using formal methods and graphical notation.

Contribution

It provides a formal proof of the equivalence between multicast and broadcast data distribution in specific network topologies, bridging theory and practical implementations.

Findings

Multicast and broadcast are equivalent in certain topologies.

Formal proof is machine-checked using Isabelle proof assistant.

Graphical notation aids in understanding the proof structure.

Abstract

Maintaining data consistency among multiple parties requires nodes to repeatedly send data to all other nodes. For example, the nodes of a blockchain network have to disseminate the blocks they create across the whole network. The scientific literature typically takes the ideal perspective that such data distribution is performed by broadcasting to all nodes directly, while in practice data is distributed by repeated multicast. Since correctness and security of consistency maintenance protocols usually have been established for the ideal setting only, it is vital to show that these properties carry over to real-world implementations. Therefore, it is desirable to prove that the ideal and the real behavior are equivalent. In the work described in this paper, we take an important step towards such a proof by proving a simpler variant of this equivalence statement. The simplification is that we consider only a concrete pair of network topologies, which nevertheless illustrates important phenomena encountered with arbitrary topologies. For describing systems that distribute data, we use a domain-specific language of processes that corresponds to a class of Petri nets and is embedded in a general-purpose process calculus. This way, we can outline our proof using an intuitive graphical notation and leverage the rich theory of process calculi in the actual proof, which is machine-checked using the Isabelle proof assistant.