一句话：首次系统研究全局分布式协议相对于网络架构的可实现性，提出网络参数化 Coherence Conditions，并归约到消息缓冲区操作公理，给出复杂度、算法与工具。
全局协议从全局视角描述分布式消息传递，并用于合成局部实现；可实现性问的是给定全局协议是否允许分布式实现。本文首次系统研究相对于网络架构的全局协议可实现性，提出网络参数化的 Coherence Conditions，并给出充分假设以精确刻画可实现性。作者进一步将假设归约为描述单个消息缓冲区插入与删除行为的最小操作公理，表明 peer-to-peer FIFO、mailbox、senderbox、monobox 与 bag 五种异步网络架构都是其特例。基于此，论文给出最优复杂度结果、可实现协议类之间的关系及符号判定算法，并实现首个网络参数化工具 Sprout(A)，展示其兼顾网络通用性、性能与模块性。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2602-10320,
title = {Implementability of Global Distributed Protocols Modulo Network Architectures},
author = {Elaine Li and Thomas Wies},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {PLDI},
year = {2026},
doi = {10.1145/3808319}
}