### 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Distributed

### Session Consensus_Refined

- 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

### Depends on

- Verifying Fault-Tolerant Distributed Algorithms in the Heard-Of Model
- Stuttering Equivalence

## Cite

×

Consensus_Refined-AFP

    @article{Consensus_Refined-AFP,
      author  = {Ognjen Marić and Christoph Sprenger},
      title   = {Consensus Refined},
      journal = {Archive of Formal Proofs},
      month   = {March},
      year    = {2015},
      note    = {\url{https://isa-afp.org/entries/Consensus_Refined.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Mar 19, 2015 : Isabelle2014