Implementability of Global Distributed Protocols modulo Network Architectures
Elaine Li, Thomas Wies

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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Formal Methods in Verification · Network Traffic and Congestion Control
