# Consensus Refined

 Title: Consensus Refined Authors: Ognjen Maric 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{https://isa-afp.org/entries/Consensus_Refined.html}, Formal proof development}, ISSN = {2150-914x}, } License: BSD License Depends on: Heard_Of, Stuttering_Equivalence