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.