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