Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed Systems
Last modified: Sat Nov 6 15:16:47 2021 GMT.
Authors
Wolf HonoreJieung Kim
Ji-Yong Shin
Zhong Shao
|
|
Much ADO about Failures: A Fault-Aware Model for Compositional Verification of Strongly Consistent Distributed SystemsLast modified: Sat Nov 6 15:16:47 2021 GMT.
AuthorsWolf HonoreJieung Kim Ji-Yong Shin Zhong Shao AbstractDespite 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.PublishedIn Proc. 2021 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA'21), Chicago, IL, October 2021. Published as Proceedings of the ACM on Programming Languages (PACMPL), Volume 5, Number OOPSLA, Article 97 (October 2021), 31 pages. |
|
Copyright © 1996-2024 The FLINT Group
<flint at cs dot yale dot edu>
Yale University Department of Computer Science |
colophon |