Uncovering Symmetries in Irregular Process Networks

Distributed protocols are often designed to run on arbitrary networks. The verification of such protocols is a challenge, as symmetry reduction arguments do not apply to irregular networks. On the other hand, the protocols often have correctness proofs which treat all nodes similarly, glossing over structural differences. In this work, we set up an abstraction framework which helps to formalize a lack of distinguishability between nodes. Specifically, we show that abstracting the neighborhood of a process helps to uncover local symmetries in a process network. This turns an irregular, concrete process network into a regular, abstract process network. Using these ideas, we show how to obtain a simple, compositional invariance proof for the Dining philosophers protocol, which applies to any network. As the proof works in the same manner for all networks, it actually results in a parameterized proof of correctness, one which holds for networks of arbitrary size and topology.