Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems
Much ADO about failures: a fault-aware model for compositional verification of strongly consistent distributed systems
复制标题
DOI：
10.1145/3485474
复制
发表时间：
2021-10
影响因子：
--
通讯作者：
Wolf Honoré;Jieung Kim;Ji-Yong Shin;Zhong Shao
中科院分区：
文献类型：
--
作者：
Wolf Honoré;Jieung Kim;Ji-Yong Shin;Zhong Shao
尽管最近的进展，保证大规模分布式应用程序的正确性，而不影响性能仍然是一个具有挑战性的问题。网络和节点故障是不可避免的，对于某些应用程序，仔细控制如何处理它们是必不可少的。不幸的是，现有的方法要么完全隐藏这些故障背后的原子状态机复制（SMR）接口，或暴露所有的网络级的细节，牺牲原子性。我们提出了一种新的，成分，原子分布式对象（ADO）模型强一致的分布式系统，结合了这两个选项中最好的。面向对象的API抽象了特定于协议的细节，并从实现选择中提取了高级正确性推理。同时，它有意地公开了某些关键分布式故障情况的抽象视图，从而允许对它们进行比SMR类模型更细粒度的控制。我们证明，证明即使是复合分布式系统的属性，可以直接与我们的Coq验证框架，广告，由于ADO模型。我们还表明，各种常见的协议，包括多Paxos和链复制细化ADO语义，它允许一个自由选择其中的应用程序的实现，而无需修改ADO级的正确性证明。
Despite recent advances, guaranteeing the correctness of large-scale distributed applications without compromising performance remains a challenging problem. Network and node failures are inevitable and, for some applications, careful control over how they are handled is essential. Unfortunately, existing approaches either completely hide these failures behind an atomic state machine replication (SMR) interface, or expose all of the network-level details, sacrificing atomicity. We propose a novel, compositional, atomic distributed object (ADO) model for strongly consistent distributed systems that combines the best of both options. The object-oriented API abstracts over protocol-specific details and decouples high-level correctness reasoning from implementation choices. At the same time, it intentionally exposes an abstract view of certain key distributed failure cases, thus allowing for more fine-grained control over them than SMR-like models. We demonstrate that proving properties even of composite distributed systems can be straightforward with our Coq verification framework, Advert, thanks to the ADO model. We also show that a variety of common protocols including multi-Paxos and Chain Replication refine the ADO semantics, which allows one to freely choose among them for an application's implementation without modifying ADO-level correctness proofs.