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

Proof outline
Proof document

Browse theories

Download this entry