Quorum Tree Abstractions of Consensus Protocols
Berk Cirisci, Constantin Enea, Suha Orhun Mutluergil

TL;DR
This paper introduces a novel quorum tree abstraction for consensus protocols, simplifying reasoning about their safety across various algorithms like Paxos, PBFT, Raft, and HotStuff, especially in blockchain contexts.
Contribution
It proposes a new abstract representation focusing on quorum responses, enabling uniform safety proofs for diverse consensus algorithms.
Findings
Supports reasoning about safety of multiple protocols
Provides a unified framework for protocol analysis
Facilitates induction-based safety proofs
Abstract
Distributed algorithms solving agreement problems like consensus or state machine replication are essential components of modern fault-tolerant distributed services. They are also notoriously hard to understand and reason about. Their complexity stems from the different assumptions on the environment they operate with, i.e., process or network link failures, Byzantine failures etc. In this paper, we propose a novel abstract representation of the dynamics of such protocols which focuses on quorums of responses (votes) to a request (proposal) that form during a run of the protocol. We show that focusing on such quorums, a run of a protocol can be viewed as working over a tree structure where different branches represent different possible outcomes of the protocol, the goal being to stabilize on the choice of a fixed branch. This abstraction resembles the description of recent protocols…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsDistributed systems and fault tolerance · Logic, Reasoning, and Knowledge · Semantic Web and Ontologies
