Distributed protocols such as 2PC and Paxos lie at the core of many systems in the cloud, but standard implementations do not scale. New scalable distributed protocols are developed through careful analysis and rewrites, but this process is ad hoc and error-prone. This paper presents an approach for scaling any distributed protocol by applying rule-driven rewrites, borrowing from query optimization. Distributed protocol rewrites entail a new burden: reasoning about spatiotemporal correctness. We leverage order-insensitivity and data dependency analysis to systematically identify correct coordination-free scaling opportunities. We apply this analysis to create preconditions and mechanisms for coordination-free decoupling and partitioning, two fundamental vertical and horizontal scaling techniques. Manual rule-driven applications of decoupling and partitioning improve the throughput of 2PC by $5\times$ and Paxos by $3\times$, and match state-of-the-art throughput in recent work. These results point the way toward automated optimizers for distributed protocols based on correct-by-construction rewrite rules.

翻译：分布式协议（如2PC和Paxos）是云中许多系统的核心，但标准实现不具备可扩展性。新的可扩展分布式协议通过仔细分析和重写来开发，但这一过程是临时且容易出错的。本文提出了一种通过应用规则驱动的重写来扩展任何分布式协议的方法，借鉴了查询优化技术。分布式协议重写引入了一个新的负担：需要推理时空正确性。我们利用顺序不敏感性和数据依赖性分析，系统地识别正确的无协调扩展机会。我们将此分析应用于创建无协调解耦和分区（两种基本的垂直和水平扩展技术）的前提条件和机制。手动应用规则驱动的解耦和分区使2PC的吞吐量提高了$5\times$，Paxos的吞吐量提高了$3\times$，并与近期工作中最先进的吞吐量相匹配。这些结果指明了基于正确性构建重写规则的分布式协议自动优化器的方向。