|
A
Constructive
Proof
for
FLP
Title: |
A Constructive Proof for FLP |
Authors:
|
Benjamin Bisping (benjamin /dot/ bisping /at/ campus /dot/ tu-berlin /dot/ de),
Paul-David Brodmann (p /dot/ brodmann /at/ tu-berlin /dot/ de),
Tim Jungnickel (tim /dot/ jungnickel /at/ tu-berlin /dot/ de),
Christina Rickmann (c /dot/ rickmann /at/ tu-berlin /dot/ de),
Henning Seidler (henning /dot/ seidler /at/ mailbox /dot/ tu-berlin /dot/ de),
Anke Stüber (anke /dot/ stueber /at/ campus /dot/ tu-berlin /dot/ de),
Arno Wilhelm-Weidner (arno /dot/ wilhelm-weidner /at/ tu-berlin /dot/ de),
Kirstin Peters (kirstin /dot/ peters /at/ tu-berlin /dot/ de) and
Uwe Nestmann
|
Submission date: |
2016-05-18 |
Abstract: |
The impossibility of distributed consensus with one faulty process is
a result with important consequences for real world distributed
systems e.g., commits in replicated databases. Since proofs are not
immune to faults and even plausible proofs with a profound formalism
can conclude wrong results, we validate the fundamental result named
FLP after Fischer, Lynch and Paterson.
We present a formalization of distributed systems
and the aforementioned consensus problem. Our proof is based on Hagen
Völzer's paper "A constructive proof for FLP". In addition to the
enhanced confidence in the validity of Völzer's proof, we contribute
the missing gaps to show the correctness in Isabelle/HOL. We clarify
the proof details and even prove fairness of the infinite execution
that contradicts consensus. Our Isabelle formalization can also be
reused for further proofs of properties of distributed systems. |
BibTeX: |
@article{FLP-AFP,
author = {Benjamin Bisping and Paul-David Brodmann and Tim Jungnickel and Christina Rickmann and Henning Seidler and Anke Stüber and Arno Wilhelm-Weidner and Kirstin Peters and Uwe Nestmann},
title = {A Constructive Proof for FLP},
journal = {Archive of Formal Proofs},
month = may,
year = 2016,
note = {\url{http://isa-afp.org/entries/FLP.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
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.
|
|