Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Implementability of Global Distributed Protocols modulo Network Architectures

Elaine Li, Thomas Wies

TL;DR

This work addresses the implementability problem for global protocol specifications when target programs run over diverse network architectures. It introduces Generalized Coherence Conditions (GCC) that are network-parametric, reduces channel-compliance reasoning to a simple buffer-axiom model, and proves soundness and completeness under channel-compliance facts; it also derives complexity results and symbolic algorithms encoded via μ-calculus, implemented in Sprout(A). The approach yields a network-agnostic synthesis pipeline: a global protocol is implementable under a given architecture if and only if its canonical local-projection implementation realizes the architecture-specific asynchronous semantics, enabling modular synthesis across p2p, mailbox, senderbox, monobox, and bag models. Practically, this unifies disparate network models under a single theory, enables efficient automated checking, and broadens the applicability of top-down choreographic methodologies to heterogeneous, networked systems.

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.

Implementability of Global Distributed Protocols modulo Network Architectures

TL;DR

This work addresses the implementability problem for global protocol specifications when target programs run over diverse network architectures. It introduces Generalized Coherence Conditions (GCC) that are network-parametric, reduces channel-compliance reasoning to a simple buffer-axiom model, and proves soundness and completeness under channel-compliance facts; it also derives complexity results and symbolic algorithms encoded via μ-calculus, implemented in Sprout(A). The approach yields a network-agnostic synthesis pipeline: a global protocol is implementable under a given architecture if and only if its canonical local-projection implementation realizes the architecture-specific asynchronous semantics, enabling modular synthesis across p2p, mailbox, senderbox, monobox, and bag models. Practically, this unifies disparate network models under a single theory, enables efficient automated checking, and broadens the applicability of top-down choreographic methodologies to heterogeneous, networked systems.

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.
Paper Structure (39 sections, 16 theorems, 12 equations, 11 figures, 1 table)

This paper contains 39 sections, 16 theorems, 12 equations, 11 figures, 1 table.

Table of Contents

  1. Introduction
  2. Motivating Example
  3. Implementability modulo network architectures
  4. Determining implementability
  5. Preliminaries
  6. Words
  7. Message Alphabets
  8. Projections.
  9. Labeled Transition Systems
  10. Implementability modulo network architectures
  11. Channel compliance.
  12. Equality under local projection
  13. Global protocol semantics
  14. Characterization of generalized implementability
  15. Revisiting Send Coherence and No Mixed Choice
  16. ...and 24 more sections

Key Result

theorem 1

Let ${\mathbb{A}}$ be a network architecture that satisfies F1 through F6 and let $\mathcal{S}$ be a global protocol. Then, $\mathcal{S}$ is implementable under ${\mathbb{A}}$ if and only if it satisfies Generalized Coherence Conditions under ${\mathbb{A}}$.

Figures (11)

  • Figure 1: Task scheduler with task delegation.
  • Figure 2: Local implementation for ${\color{roleColor}\mathtt{s}}$
  • Figure 3: Local implementation for ${\color{roleColor}\mathtt{w_2}}$
  • Figure 4: Local implementation for ${\color{roleColor}\mathtt{w_1}}$
  • Figure 5: A protocol $\mathcal{S}_a$ that is not implementable on a bag network but implementable on a peer-to-peer box network.
  • ...and 6 more figures

Theorems & Definitions (31)

  • definition 1: Network architecture
  • definition 2: Network-parametric CLTS
  • definition 3: Network-parametric Protocol Implementability
  • definition 4: Canonical implementations Li25OopslaOfficial
  • definition 5: Generalized Receive Coherence
  • definition 6: Prefix Extensibility
  • definition 7: Generalized Coherence Conditions
  • theorem 1: Preciseness of Generalized Coherence Conditions
  • definition 8: Axiomatic network model
  • lemma 1
  • ...and 21 more