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.

翻译：全局协议从宏观视角描述分布式消息传递协议，并作为合成本地实现的规约。可实现性关注给定全局协议是否允许分布式实现。本文首次系统研究了网络架构下的全局协议可实现性问题。我们提出了一组网络参数化的协调条件，并展示了在何种充分假设下该条件能精确刻画可实现性。我们进一步将这些假设简化为描述单个消息缓冲区插入与删除行为的最小操作公理集。该简化直接证明了五种常用异步网络架构——点对点FIFO、邮箱、发送箱、单箱和包结构——均是我们网络参数化结果的实例。利用该特征刻画，我们推导出网络架构下可实现性的最优复杂度结果、各类可实现的全局协议之间的关系，以及判定网络架构下可实现性的符号算法。我们在首个网络参数化工具Sprout(A)中实现了后者，并证明该工具在保持性能与模块化的同时实现了网络通用性。