全局分布式协议在考虑网络架构下的可实现性
Implementability of Global Distributed Protocols modulo Network Architectures
AI总结：
本文研究了全局分布式协议在不同网络架构下的可实现性，提出网络参数化一致性条件，并通过Sprout(A)工具验证了其有效性。
摘要：
全局协议从宏观视角指定分布式、消息传递协议，并用于合成局部实现。可实现性询问给定的全局协议是否允许分布式实现。我们首次对全局协议在考虑网络架构下的可实现性进行了全面研究。我们提出了一组网络参数化的一致性条件，并展示了在某些充分假设下，这些条件精确地刻画了可实现性。我们进一步将这些假设减少到一组描述单个消息缓冲区插入和移除行为的操作公理集。这种减少立即表明，五个常见的异步网络架构，即点对点FIFO、邮箱、发送箱、单箱和袋，都是我们网络参数化结果的实例。我们利用这种刻画来推导在考虑网络下的可实现性最优复杂性结果，各类可实现全局协议之间的关系，以及用于决定在考虑网络下的可实现性的符号算法。我们实现了后者，作为第一个网络参数化工具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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
