Adore: Atomic Distributed Objects with Certified Reconfiguration

Last modified: Wed Mar 6 14:36:55 2024 GMT.

Authors

Wolf Honore
Ji-Yong Shin
Jieung Kim
Zhong Shao

Abstract

Finding the right abstraction is critical for reasoning about complex systems such as distributed protocols like Paxos and Raft. Despite a recent abundance of impressive verification work in this area, we claim the ways that past efforts model distributed state are not ideal for protocol-level reasoning: they either hide important details, or leak too much complexity from the network. As evidence we observe that nearly all of them avoid the complex, but important issue of reconfiguration. Reconfiguration's primary challenge lies in how it interacts with a protocol's core safety invariants. To handle this increased complexity, we introduce the Adore model, whose novel abstract state hides network-level communications while capturing dependencies between committed and uncommitted states, as well as metadata like election quorums. It includes first-class support for a generic reconfiguration command that can be instantiated with a variety of implementations. Under this model, the subtle interactions between reconfiguration and the core protocol become clear, and with this insight we completed the first mechanized proof of safety of a reconfigurable consensus protocol.

Published

In Proc. 2022 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'22), San Diego, California, USA, 16 pages, June 2022.

Conference Paper [PDF]

Extended Technical Report [PDF]

Artifact [URL]

colophon