Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] New AFP entry: Consensus Refined


view this post on Zulip Email Gateway (Aug 19 2022 at 17:25):

From: Tobias Nipkow <nipkow@in.tum.de>
http://afp.sourceforge.net/entries/Consensus_Refined.shtml

Consensus Refined
Ognjen Maric and Christoph Sprenger

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.

Enjoy!
smime.p7s


Last updated: Mar 29 2024 at 12:28 UTC