Authors
Wolf Honore
Longfei Qiu
Yoonseung Kim
Ji-Yong Shin
Jieung Kim
Zhong Shao
Abstract
Achieving consensus is a challenging and ubiquitous problem in
distributed systems that is only made harder by the introduction of
malicious byzantine servers. While significant effort has been
devoted to the benign and byzantine failure models individually, no
prior work has considered the mechanized verification of both in a
generic way. We claim this is due to the lack of an appropriate
abstraction that is capable of representing both benign and byzantine
consensus without either losing too much detail or becoming
impractically complex. We build on recent work on the atomic
distributed object model to fill this void with a novel abstraction
called AdoB. In addition to revealing important insights into
the essence of consensus, this abstraction has practical benefits for
easing distributed system verification. As a case study, we proved
safety and liveness properties for AdoB in Coq, which are the
first such mechanized proofs to handle benign and byzantine consensus
in a unified manner. We also demonstrate that AdoB faithfully
models real consensus protocols by proving it is refined by standard
network-level specifications of Fast Paxos and a variant of Jolteon.
Published
In
Proc. 2024 ACM SIGPLAN
International Conference on Object-Oriented Programming, Systems,
Languages, and Applications (OOPSLA'24), Pasadena, CA, October 2024.
Published as
Proceedings of the ACM on Programming Languages (PACMPL), Volume 8, Number OOPSLA1, Article 109 (April 2024), 30 pages.