×

Mechanical verification of a constructive proof for FLP. (English) Zbl 1478.68146

Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 107-122 (2016).
Summary: 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 by using the interactive theorem prover Isabelle/HOL. 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”, Inf. Process. Lett. 92, No. 2, 83–87 (2004; Zbl 1173.68392)]. 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 may serve as a starting point for similar proofs of properties of distributed systems.
For the entire collection see [Zbl 1343.68004].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68M14 Distributed systems
68M15 Reliability, testing and fault tolerance of networks and computer systems
68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
68V20 Formalization of mathematics in connection with theorem provers

Citations:

Zbl 1173.68392
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science An EATCS Series. Springer, Heidelberg (2013) · Zbl 1069.68095
[2] Bisping, B., Brodmann, P.D., Jungnickel, T., Rickmann, C., Seidler, H., Stüber, A., Wilhelm-Weidner, A., Peters, K., Nestmann, U.: A Constructive Proof for FLP. Archive of Formal Proofs (2016). http://isa-afp.org/entries/FLP.shtml . Formal proof development · Zbl 1478.68146
[3] Buckley, G.N., Silberschatz, A.: An effective implementation for the generalized input-output construct of CSP. ACM Trans. Program. Lang. Syst. (TOPLAS) 5(2), 223–235 (1983) · Zbl 0516.68026
[4] Constable, R.L.: Effectively Nonblocking Consensus Procedures can Execute Forever - a Constructive Version of FLP. Tech. Rep. 11513, Cornell University (2011)
[5] Constable, R.L., Allen, S.F., Bromley, H.M., Cleaveland, W.R., Cremer, J.F., Harper, R.W., Howe, D.J., Knoblock, T.B., Mendler, N.P., Panangaden, P., Sasaki, J.T., Smith, S.F.: Implementig Mathematics with the Nuprl Proof Development System. Prentice-Hall, Upper Saddle River (1986)
[6] Fischer, M.J., Lynch, N.A., Paterson, M.S.: Impossibility of distributed consensus with one faulty process. J. ACM (JACM) 32(2), 374–382 (1985) · Zbl 0629.68027
[7] Kammüller, F., Wenzel, M., Paulson, L.C.: Locales - a sectioning concept for Isabelle. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 149–165. Springer, Heidelberg (1999)
[8] Küfner, P., Nestmann, U., Rickmann, C.: Formal verification of distributed algorithms. In: Baeten, J.C.M., Ball, T., de Boer, F.S. (eds.) TCS 2012. LNCS, vol. 7604, pp. 209–224. Springer, Heidelberg (2012) · Zbl 1362.68285
[9] Kumar, D., Silberschatz, A.: A counter-example to an algorithm for the generalized input-output construct of CSP. Inform. Proc. Lett. 61(6), 287 (1997) · Zbl 0925.68085
[10] Lamport, L.: The part-time parliament. ACM Trans. Comput. Syst. (TOCS) 16(2), 133–169 (1998) · Zbl 01935567
[11] Nipkow, T., Paulson, L.C., Wenzel, M. (eds.): Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131
[12] Ongaro, D., Ousterhout, J.: In Search of an Understandable Consensus Algorithm. In: Proceedings of USENIX, pp. 305–320 (2014)
[13] Völzer, H.: A constructive proof for FLP. Inform. Proc. Lett. 92(2), 83–87 (2004) · Zbl 1173.68392
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.