Implementability of Global Distributed Protocols modulo Network Architectures

TL;DR

This paper investigates the conditions under which global distributed protocols can be implemented across various network architectures, providing a comprehensive framework, complexity results, and a practical tool for verification.

Contribution

It introduces network-parametric coherence conditions for protocol implementability, reducing assumptions to minimal axioms, and develops a general, efficient verification tool.

Findings

Five common network architectures are instances of the framework.

The characterization leads to optimal complexity results.

The Sprout(A) tool effectively verifies implementability across networks.

Abstract

Global protocols specify distributed, message-passing protocols from a birds-eye view, and are used as a specification for synthesizing local implementations. Implementability asks whether a given global protocol admits a distributed implementation. We present the first comprehensive investigation of global protocol implementability modulo network architectures. We propose a set of network-parametric Coherence Conditions, and exhibit sufficient assumptions under which it precisely characterizes implementability. We further reduce these assumptions to a minimal set of operational axioms describing insert and remove behavior of individual message buffers. Our reduction immediately establishes that five commonly studied asynchronous network architectures, namely peer-to-peer FIFO, mailbox, senderbox, monobox and bag, are instances of our network-parametric result. We use our characterization to derive optimal complexity results for implementability modulo networks, relationships between classes of implementable global protocols, and symbolic algorithms for deciding implementability modulo networks. We implement the latter in the first network-parametric tool Sprout(A), and show that it achieves network generality without sacrificing performance and modularity.