Implementability of Global Distributed Protocols Modulo Network Architectures
summary
This work gives a precise, network-parametric characterization of when a bird’s-eye global message protocol admits a distributed implementation: coherence conditions reduce to a small set of algebraic channel axioms and further to eight operational buffer axioms B1–B8 buffer axioms. The result proves five common asynchronous models (peer-to-peer FIFO, mailbox, senderbox, monobox, bag) fit the framework, presents a sound-and-complete reduction to mu‑calculus, and ships as the Sprout(A) tool that preserves performance while supporting network generality.
AI-written summary · about
chapters (9)
- 0:00Global protocols introduction
- 1:51Key features
- 3:17Realizability challenges
- 7:30Asynchronous network models
- 10:00Network architectures as languages
- 12:07Coherence conditions
- 13:32Buffer axioms
- 14:36Tool results
- 15:40Q&A
related talks
13mCharacterizing Implementability of Global Protocols with Infinite States and Data
22mA Partial Order View of Message-Passing Communication Models
20mModel Checking Distributed Protocols in Must
48mFrom Byzantine Generals to Global Harmony, Modularly
01h 11mA Programmable Cloud: CALM Foundations and Open Challenges
39mProtocol engineering for communicating actors
31mMulti-version Coding and Shared Memory Emulation
44mUnderstanding Distributed Calculi in Haskell