Abstract
Algorithms for solving the consensus problem are fundamental to
distributed computing. Despite their brevity, their
ability to operate in concurrent, asynchronous and failure-prone
environments comes at the cost of complex and subtle
behaviors. Accordingly, understanding how they work and proving
their correctness is a non-trivial endeavor where abstraction
is immensely helpful.
Moreover, research on consensus has yielded a large number of
algorithms, many of which appear to share common algorithmic
ideas. A natural question is whether and how these similarities can
be distilled and described in a precise, unified way.
In this work, we combine stepwise refinement and
lockstep models to provide an abstract and unified
view of a sizeable family of consensus algorithms. Our models
provide insights into the design choices underlying the different
algorithms, and classify them based on those choices.
BSD LicenseDepends On
Topics
Related Entries
Theories
- Infra
- Consensus_Types
- Quorums
- Consensus_Misc
- Two_Steps
- Three_Steps
- Refinement
- HO_Transition_System
- Voting
- Voting_Opt
- OneThirdRule_Defs
- OneThirdRule_Proofs
- Ate_Defs
- Ate_Proofs
- Same_Vote
- Observing_Quorums
- Observing_Quorums_Opt
- Two_Step_Observing
- Uv_Defs
- Uv_Proofs
- BenOr_Defs
- BenOr_Proofs
- MRU_Vote
- MRU_Vote_Opt
- Three_Step_MRU
- New_Algorithm_Defs
- New_Algorithm_Proofs
- Paxos_Defs
- Paxos_Proofs
- CT_Defs
- CT_Proofs