Advertisement

On a Verification Framework for Certifying Distributed Algorithms: Distributed Checking and Consistency

  • Kim Völlinger
  • Samira Akili
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10854)

Abstract

A major problem in software engineering is assuring the correctness of a distributed system. A certifying distributed algorithm (CDA) computes for its input-output pair (io) an additional witness w – a formal argument for the correctness of (io). Each CDA features a witness predicate such that if the witness predicate holds for a triple (iow), the input-output pair (io) is correct. An accompanying checker algorithm decides the witness predicate. Consequently, a user of a CDA does not have to trust the CDA but its checker algorithm. Usually, a checker is simpler and its verification is feasible. To sum up, the idea of a CDA is to adapt the underlying algorithm of a program at design-time such that it verifies its own output at runtime. While certifying sequential algorithms are well-established, there are open questions on how to apply certification to distributed algorithms. In this paper, we discuss distributed checking of a distributed witness; one challenge is that all parts of a distributed witness have to be consistent with each other. Furthermore, we present a method for formal instance verification (i.e. obtaining a machine-checked proof that a particular input-output pair is correct), and implement the method in a framework for the theorem prover Coq.

Keywords

Certification Distributed algorithm Formal instance verification 

References

  1. 1.
    Alkassar, E., Böhme, S., Mehlhorn, K., Rizkallah, C.: Verification of certifying computations. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 67–82. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_7CrossRefGoogle Scholar
  2. 2.
    Alkassar, E., Böhme, S., Mehlhorn, K., Rizkallah, C.: A framework for the verification of certifying computations. J. Autom. Reason. 52(3), 241–273 (2014)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Arkoudas, K., Rinard, M.C.: Deductive runtime certification. Electron. Notes Theor. Comput. Sci. 113, 45–63 (2005)CrossRefGoogle Scholar
  4. 4.
    Bruce, D., Hoàng, C.T., Sawada, J.: A certifying algorithm for 3-colorability of P\(^{5}\)-free graphs. In: Dong, Y., Du, D.-Z., Ibarra, O. (eds.) ISAAC 2009. LNCS, vol. 5878, pp. 594–604. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-10631-6_61CrossRefGoogle Scholar
  5. 5.
    Censor-Hillel, K., Fischer, E., Schwartzman, G., Vasudev, Y.: Fast distributed algorithms for testing graph properties. In: Gavoille, C., Ilcinkas, D. (eds.) DISC 2016. LNCS, vol. 9888, pp. 43–56. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-53426-7_4CrossRefzbMATHGoogle Scholar
  6. 6.
    Corneil, D.G., Dalton, B., Habib, M.: LDFS-based certifying algorithm for the minimum path cover problem on cocomparability graphs. SIAM J. Comput. 42(3), 792–807 (2013)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  8. 8.
    Duprat, J.: A Coq toolkit for graph theory. Rapport de recherche 15 (2001)Google Scholar
  9. 9.
    Finkler, U., Mehlhorn, K.: Checking priority queues. In: Proceedings of the Tenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 1999, pp. 901–902. Society for Industrial and Applied Mathematics, Philadelphia (1999)Google Scholar
  10. 10.
    Glesner, S.: Program checking with certificates: separating correctness-critical code. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 758–777. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-45236-2_41CrossRefGoogle Scholar
  11. 11.
    Heggernes, P., Kratsch, D.: Linear-time certifying recognition algorithms and forbidden induced subgraphs. Nord. J. Comput. 14(1), 87–108 (2007)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Hell, P., Huang, J.: Certifying LexBFS recognition algorithms for proper interval graphs and proper interval bigraphs. SIAM J. Disc. Math. 18, 554–570 (2004)MathSciNetCrossRefGoogle Scholar
  13. 13.
    Hung, R.W., Chang, M.S.: An efficient certifying algorithm for the Hamiltonian cycle problem on circular-arc graphs. Theoret. Comput. Sci. 412(39), 5351–5373 (2011)MathSciNetCrossRefGoogle Scholar
  14. 14.
    INRIA: The Coq Proof Assistant. http://coq.inria.fr/
  15. 15.
    Kaplan, H., Nussbaum, Y.: Certifying algorithms for recognizing proper circular-arc graphs and unit circular-arc graphs. Disc. Appl. Math. 157(15), 3216–3230 (2009)MathSciNetCrossRefGoogle Scholar
  16. 16.
    Korman, A., Kutten, S., Peleg, D.: Proof labeling schemes. Distrib. Comput. 22(4), 215–233 (2010)CrossRefGoogle Scholar
  17. 17.
    Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996)zbMATHGoogle Scholar
  18. 18.
    McConnell, R.M.: A certifying algorithm for the consecutive-ones property. In: Proceedings of the Fifteenth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA 2004, pp. 768–777. Society for Industrial and Applied Mathematics, Philadelphia (2004)Google Scholar
  19. 19.
    McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5, 119–161 (2011)CrossRefGoogle Scholar
  20. 20.
    Mehlhorn, K., Näher, S.: From algorithms to working programs: on the use of program checking in LEDA. In: Brim, L., Gruska, J., Zlatuška, J. (eds.) MFCS 1998. LNCS, vol. 1450, pp. 84–93. Springer, Heidelberg (1998).  https://doi.org/10.1007/BFb0055759CrossRefGoogle Scholar
  21. 21.
    Mostafa, M., Bonakdarpour, B.: Decentralized runtime verification of LTL specifications in distributed systems. In: Proceedings of the 2015 IEEE International Parallel and Distributed Processing Symposium, IPDPS 2015, pp. 494–503. IEEE Computer Society, Washington, DC (2015)Google Scholar
  22. 22.
    Necula, G.C., Lee, P.: The Design and implementation of a certifying compiler. In: Proceedings of the ACM SIGPLAN 1998 Conference on Programming Language Design and Implementation, PLDI 1998, pp. 333–344. ACM, New York (1998)Google Scholar
  23. 23.
    Nikolopoulos, S.D., Palios, L.: An O(nm)-time certifying algorithm for recognizing HHD-free graphs. Theor. Comput. Sci. 452, 117–131 (2012)MathSciNetCrossRefGoogle Scholar
  24. 24.
    Noschinski, L., Rizkallah, C., Mehlhorn, K.: Verification of certifying computations through autocorres and simpl. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 46–61. Springer, Cham (2014).  https://doi.org/10.1007/978-3-319-06200-6_4CrossRefGoogle Scholar
  25. 25.
    Raynal, M.: Distributed Algorithms for Message-Passing Systems. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38123-2CrossRefzbMATHGoogle Scholar
  26. 26.
    Rizkallah, C.: Verification of program computations. Ph.D. thesis (2015)Google Scholar
  27. 27.
    Schmidt, J.M.: Construction sequences and certifying 3-connectivity. Algorithmica 62, 192–208 (2012)MathSciNetCrossRefGoogle Scholar
  28. 28.
    Völlinger, K.: Verifying the output of a distributed algorithm using certification. In: Lahiri, S., Reger, G. (eds.) RV 2017. LNCS, vol. 10548, pp. 424–430. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-67531-2_29CrossRefGoogle Scholar
  29. 29.
    Völlinger, K., Akili, S.: Verifying a class of certifying distributed programs. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 373–388. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-57288-8_27CrossRefGoogle Scholar
  30. 30.
    Völlinger, K., Reisig, W.: Certification of distributed algorithms solving problems with optimal substructure. In: Calinescu, R., Rumpe, B. (eds.) SEFM 2015. LNCS, vol. 9276, pp. 190–195. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-22969-0_14CrossRefGoogle Scholar
  31. 31.
    Wilcox, J.R., Woos, D., Panchekha, P., Tatlock, Z., Wang, X., Ernst, M.D., Anderson, T.: Verdi: a framework for implementing and formally verifying distributed systems. In: ACM SIGPLAN Notices, vol. 50, pp. 357–368. ACM (2015)Google Scholar

Copyright information

© IFIP International Federation for Information Processing 2018

Authors and Affiliations

  1. 1.Humboldt University of BerlinBerlinGermany

Personalised recommendations