On a verification framework for certifying distributed algorithms: distributed checking and consistency. (English) Zbl 1508.68080
Baier, Christel (ed.) et al., Formal techniques for distributed objects, components, and systems. 38th IFIP WG 6.1 international conference, FORTE 2018, held as part of the 13th international federated conference on distributed computing techniques, DisCoTec 2018, Madrid, Spain, June 18–21, 2018. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 10854, 161-180 (2018).
Summary: 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 \((i, o)\) an additional witness \(w\) – a formal argument for the correctness of \((i, o)\). Each CDA features a witness predicate such that if the witness predicate holds for a triple \((i, o, w)\), the input-output pair \((i, o)\) 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.
For the entire collection see [Zbl 1387.68012].
For the entire collection see [Zbl 1387.68012].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68W15 | Distributed algorithms |
References:
| [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_7 · doi:10.1007/978-3-642-22110-1_7 |
| [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) · Zbl 1314.68180 · doi:10.1007/s10817-013-9289-2 |
| [3] | Arkoudas, K., Rinard, M.C.: Deductive runtime certification. Electron. Notes Theor. Comput. Sci. 113, 45-63 (2005) · doi:10.1016/j.entcs.2004.01.035 |
| [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_61 · Zbl 1272.05191 · doi:10.1007/978-3-642-10631-6_61 |
| [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_4 · Zbl 1393.68181 · doi:10.1007/978-3-662-53426-7_4 |
| [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) · Zbl 1272.05192 · doi:10.1137/11083856X |
| [7] | Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000) · Zbl 1026.93001 |
| [8] | Duprat, J.: A Coq toolkit for graph theory. Rapport de recherche 15 (2001) |
| [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) · Zbl 0931.68122 |
| [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_41 · doi:10.1007/978-3-540-45236-2_41 |
| [11] | Heggernes, P., Kratsch, D.: Linear-time certifying recognition algorithms and forbidden induced subgraphs. Nord. J. Comput. 14(1), 87-108 (2007) · Zbl 1169.68653 |
| [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) · Zbl 1069.05056 · doi:10.1137/S0895480103430259 |
| [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) · Zbl 1235.68083 · doi:10.1016/j.tcs.2011.06.009 |
| [14] | INRIA: The Coq Proof Assistant. http://coq.inria.fr/ |
| [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) · Zbl 1213.05248 · doi:10.1016/j.dam.2009.07.002 |
| [16] | Korman, A., Kutten, S., Peleg, D.: Proof labeling schemes. Distrib. Comput. 22(4), 215-233 (2010) · Zbl 1267.68061 · doi:10.1007/s00446-010-0095-3 |
| [17] | Lynch, N.A.: Distributed Algorithms. Morgan Kaufmann Publishers Inc., San Francisco (1996) · Zbl 0877.68061 |
| [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) · Zbl 1318.68189 |
| [19] | McConnell, R.M., Mehlhorn, K., Näher, S., Schweitzer, P.: Certifying algorithms. Comput. Sci. Rev. 5, 119-161 (2011) · Zbl 1298.68289 · doi:10.1016/j.cosrev.2010.09.009 |
| [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/BFb0055759 · doi:10.1007/BFb0055759 |
| [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) |
| [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) |
| [23] | Nikolopoulos, S.D., Palios, L.: An O(nm)-time certifying algorithm for recognizing HHD-free graphs. Theor. Comput. Sci. 452, 117-131 (2012) · Zbl 1251.05173 · doi:10.1016/j.tcs.2012.06.006 |
| [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_4 · doi:10.1007/978-3-319-06200-6_4 |
| [25] | Raynal, M.: Distributed Algorithms for Message-Passing Systems. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38123-2 · Zbl 1282.68004 · doi:10.1007/978-3-642-38123-2 |
| [26] | Rizkallah, C.: Verification of program computations. Ph.D. thesis (2015) |
| [27] | Schmidt, J.M.: Construction sequences and certifying 3-connectivity. Algorithmica 62, 192-208 (2012) · Zbl 1239.05110 · doi:10.1007/s00453-010-9450-9 |
| [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_29 · doi:10.1007/978-3-319-67531-2_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_27 · doi:10.1007/978-3-319-57288-8_27 |
| [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_14 · doi:10.1007/978-3-319-22969-0_14 |
| [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) |
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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
