Consensus Refined

 

Title: Consensus Refined
Authors: Ognjen Maric (omaric /at/ inf /dot/ ethz /dot/ ch) and Christoph Sprenger (sprenger /at/ inf /dot/ ethz /dot/ ch)
Submission date: 2015-03-18
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.
BibTeX:
@article{Consensus_Refined-AFP,
  author  = {Ognjen Maric and Christoph Sprenger},
  title   = {Consensus Refined},
  journal = {Archive of Formal Proofs},
  month   = mar,
  year    = 2015,
  note    = {\url{http://isa-afp.org/entries/Consensus_Refined.html},
            Formal proof development},
  ISSN    = {2150-914x},
}
License: BSD License
Depends on: Heard_Of, Stuttering_Equivalence
Status: [ok] This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.