Mechanical Verification of a Constructive Proof for FLP
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 pro
- PDF / 242,887 Bytes
- 16 Pages / 439.37 x 666.142 pts Page_size
- 33 Downloads / 159 Views
ation
·
FLP
·
Introduction
Many informal proofs have been found to be incorrect and even plausible ones come to invalid results. One example is the “Effective Implementation for the Generalized Input-Output Construct of CSP” [3] where a later attempt of a proof produced a counterexample [9]. Hence, increasing the confidence in the correctness of fundamental results is a good idea in general. The impossibility of fault-tolerant distributed consensus in asynchronous systems is a fundamental result in computer science. Originally, it has been established and proved by Fischer, Lynch and Paterson (FLP) [6]. Since the result implies major consequences in distributed computing, it is worth verifying its correctness to achieve the highest level of certainty. To our knowledge, it has not yet been verified mechanically. Due to its relevance we checked the claim in the interactive theorem prover Isabelle/HOL. We base our formalization on V¨ olzer’s paper “A Constructive Proof for FLP” [13]. Compared to the original proof in [6], V¨ olzer is more precise and more c Springer International Publishing Switzerland 2016 J.C. Blanchette and S. Merz (Eds.): ITP 2016, LNCS 9807, pp. 107–122, 2016. DOI: 10.1007/978-3-319-43144-4 7
108
B. Bisping et al.
extensive in defining the model and in the subproofs leading to the crucial contradiction. V¨ olzer argues in [13], it is “not only showing that a non-terminating execution does exist but also how it can be constructed”. Due to its higher degree of detail and constructiveness, we chose V¨olzer’s proof as foundation for proving FLP. Accordingly, all design decisions are based on the motivation to stay as close as possible to V¨olzer. We extend the proof by providing a higher level of precision and clarify the proof details. Moreover, we formalize a notion of fairness and prove that the constructed execution is fair, which V¨ olzer states without proof or proof sketch. Ultimately, we show that FLP’s result is correct, up to the correctness of Isabelle/HOL. Our complete formalization is available in the Archive of Formal Proofs [2]. Overview. We start in Sect. 2 with a brief introduction into distributed systems, consensus and Isabelle/HOL. In Sect. 3 we sketch our Isabelle formalization of the model and the proven properties. Section 4 gives an overview of our formalization of the FLP proof and we discuss our observations. We conclude with a brief summary and an outlook in Sect. 5. Related Work. In “Nonblocking Consensus Procedures Can Execute Forever” [4], Constable shows another way of proving the FLP result. He uses the idea of nonblocking consensus protocols and states that similar work has been formally verified using Nuprl [5] up to a certain point. In contrast, we fully formalized it using Isabelle/HOL [11]. More recently, there is a project1 formalizing the original FLP paper in the theorem prover Coq [1], which has not yet been finished. Contributions. Our main contributions are (1) the formalization of a generic model for distributed systems, (2) the constructive proof in the
Data Loading...
