Document Open Access Logo

Certified Round Complexity of Self-Stabilizing Algorithms

Authors Karine Altisen , Pierre Corbineau , Stéphane Devismes

PDF
Thumbnail PDF

File

LIPIcs.DISC.2023.2.pdf
  • Filesize: 0.94 MB
  • 22 pages

Document Identifiers

Author Details

Karine Altisen
  • Université Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000 Grenoble, France
Pierre Corbineau
  • Université Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, 38000 Grenoble, France
Stéphane Devismes
  • Université de Picardie Jules Verne, MIS, 80039 Amiens, France

Funding

This work has been partially funded by the ANR project SkyData (ANR-22-CE25-0008-01).

Cite AsGet BibTex

Karine Altisen, Pierre Corbineau, and Stéphane Devismes. Certified Round Complexity of Self-Stabilizing Algorithms. In 37th International Symposium on Distributed Computing (DISC 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 281, pp. 2:1-2:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.DISC.2023.2

Abstract

A proof assistant is an appropriate tool to write sound proofs. The need of such tools in distributed computing grows over the years due to the scientific progress that leads algorithmic designers to consider always more difficult problems. In that spirit, the PADEC Coq library has been developed to certify self-stabilizing algorithms. Efficiency of self-stabilizing algorithms is mainly evaluated by comparing their stabilization times in rounds, the time unit that is primarily used in the self-stabilizing area. In this paper, we introduce the notion of rounds in the PADEC library together with several formal tools to help the certification of the complexity analysis of self-stabilizing algorithms. We validate our approach by certifying the stabilization time in rounds of the classical Dolev et al’s self-stabilizing Breadth-first Search spanning tree construction.

Subject Classification

ACM Subject Classification
  • Theory of computation → Distributed algorithms
  • Theory of computation → Logic and verification
Keywords
  • Certification
  • proof assistant
  • Coq
  • self-stabilization
  • round complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Karine Altisen, Pierre Corbineau, and Stéphane Devismes. A framework for certified self-stabilization. Log. Methods Comput. Sci., 13(4), 2017. URL: https://doi.org/10.23638/LMCS-13(4:14)2017.
  2. Karine Altisen, Pierre Corbineau, and Stéphane Devismes. Certification of an exact worst-case self-stabilization time. In ICDCN '21: International Conference on Distributed Computing and Networking, Virtual Event, Nara, Japan, January 5-8, 2021, pages 46-55. ACM, 2021. URL: https://doi.org/10.1145/3427796.3427832.
  3. Karine Altisen, Alain Cournier, Stéphane Devismes, Anaïs Durand, and Franck Petit. Self-stabilizing leader election in polynomial steps. Inf. Comput., 254:330-366, 2017. URL: https://doi.org/10.1016/j.ic.2016.09.002.
  4. Karine Altisen, Stéphane Devismes, Swan Dubois, and Franck Petit. Introduction to Distributed Self-Stabilizing Algorithms. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, 2019. URL: https://doi.org/10.2200/S00908ED1V01Y201903DCT015.
  5. Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, and Xavier Urbain. Certified impossibility results for byzantine-tolerant mobile robots. In Teruo Higashino, Yoshiaki Katayama, Toshimitsu Masuzawa, Maria Potop-Butucaru, and Masafumi Yamashita, editors, Stabilization, Safety, and Security of Distributed Systems - 15th International Symposium, SSS 2013, Osaka, Japan, November 13-16, 2013. Proceedings, volume 8255 of Lecture Notes in Computer Science, pages 178-190. Springer, 2013. URL: https://doi.org/10.1007/978-3-319-03089-0_13.
  6. Cédric Auger, Zohir Bouzid, Pierre Courtieu, Sébastien Tixeuil, and Xavier Urbain. Certified impossibility results for byzantine-tolerant mobile robots. In Teruo Higashino, Yoshiaki Katayama, Toshimitsu Masuzawa, Maria Potop-Butucaru, and Masafumi Yamashita, editors, Stabilization, Safety, and Security of Distributed Systems - 15th International Symposium, SSS 2013, Osaka, Japan, November 13-16, 2013. Proceedings, volume 8255 of Lecture Notes in Computer Science, pages 178-190. Springer, 2013. Google Scholar
  7. Yves Bertot and Pierre Castéran. Interactive Theorem Proving and Program Development - Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, 2004. Google Scholar
  8. Frédéric Blanqui and Adam Koprowski. Color: a coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Mathematical Structures in Computer Science, 21(4):827-859, 2011. URL: https://doi.org/10.1017/S0960129511000120.
  9. Roderick Bloem, Nicolas Braud-Santoni, and Swen Jacobs. Synthesis of self-stabilising and byzantine-resilient distributed systems. In Computer Aided Verification - 28th International Conference, CAV 2016, pages 157-176, 2016. Google Scholar
  10. Pierre Castéran and Vincent Filou. Tasks, types and tactics for local computation systems. Stud. Inform. Univ., 9(1):39-86, 2011. Google Scholar
  11. Bernadette Charron-Bost, Henri Debrat, and Stephan Merz. Formal verification of consensus algorithms tolerating malicious faults. In Xavier Défago, Franck Petit, and Vincent Villain, editors, Stabilization, Safety, and Security of Distributed Systems, pages 120-134, Berlin, Heidelberg, 2011. Springer Berlin Heidelberg. Google Scholar
  12. Bernadette Charron-Bost and Stephan Merz. Formal verification of a consensus algorithm in the heard-of model. Int. J. Software and Informatics, 3(2-3):273-303, 2009. Google Scholar
  13. Alain Cournier, Ajoy K. Datta, Franck Petit, and Vincent Villain. Snap-Stabilizing PIF Algorithm in Arbitrary Networks. In Proceedings of the 22nd International Conference on Distributed Computing Systems (ICDCS'02), pages 199-206, 2002. Google Scholar
  14. Pierre Courtieu. Proving self-stabilization with a proof assistant. In 16th International Parallel and Distributed Processing Symposium (IPDPS 2002), 15-19 April 2002, Fort Lauderdale, FL, USA, CD-ROM/Abstracts Proceedings, volume 1, page 8pp. IEEE Computer Society, 2002. Google Scholar
  15. Pierre Courtieu, Lionel Rieg, Sébastien Tixeuil, and Xavier Urbain. Impossibility of gathering, a certification. Inf. Process. Lett., 115(3):447-452, 2015. Google Scholar
  16. Denis Cousineau, Damien Doligez, Leslie Lamport, Stephan Merz, Daniel Ricketts, and Hernán Vanzetto. TLA + proofs. In FM 2012: Formal Methods - 18th International Symposium, Paris, France, August 27-31, 2012. Proceedings, pages 147-154, 2012. Google Scholar
  17. Ajoy Kumar Datta, Stéphane Devismes, Karel Heurtefeux, Lawrence L. Larmore, and Yvan Rivierre. Competitive self-stabilizing k-clustering. Theor. Comput. Sci., 626:110-133, 2016. URL: https://doi.org/10.1016/j.tcs.2016.02.010.
  18. Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, and Leslie Lamport. Adaptive register allocation with a linear number of registers. In Distributed Computing - 27th International Symposium, DISC 2013, 2013. Google Scholar
  19. Stéphane Devismes and Colette Johnen. Silent self-stabilizing BFS tree algorithms revisited. J. Parallel Distributed Comput., 97:11-23, 2016. URL: https://doi.org/10.1016/j.jpdc.2016.06.003.
  20. Stéphane Devismes, Anissa Lamani, Franck Petit, Pascal Raymond, and Sébastien Tixeuil. Optimal grid exploration by asynchronous oblivious robots. In Stabilization, Safety, and Security of Distributed Systems - 14th International Symposium, SSS 2012, Toronto, Canada, October 1-4, 2012. Proceedings, volume 7596 of Lecture Notes in Computer Science, pages 64-76. Springer, 2012. Google Scholar
  21. Edsger W. Dijkstra. Self-stabilizing systems in spite of distributed control. Commun. ACM, 17(11):643-644, 1974. URL: https://doi.org/10.1145/361179.361202.
  22. Shlomi Dolev, Amos Israeli, and Shlomo Moran. Self-stabilization of dynamic systems assuming only Read/Write atomicity. Distributed Computing, 7(1):3-16, 1993. Google Scholar
  23. Fathiyeh Faghih, Borzoo Bonakdarpour, Sébastien Tixeuil, and Sandeep S. Kulkarni. Specification-based synthesis of distributed self-stabilizing protocols. In Formal Techniques for Distributed Objects, Components, and Systems - 36th IFIP WG 6.1 International Conference, FORTE 2016, 2016. Google Scholar
  24. Lin Fei, Sun Yong, Ding Hong, and Ren Yizhi. Self stabilizing distributed transactional memory model and algorithms. Journal of Computer Research and Development, 51(9):2046, 2014. Google Scholar
  25. Wan Fokkink, Jaap-Henk Hoepman, and Jun Pang. A note on k-state self-stabilization in a ring with k=n. Nordic Journal of Computing, 12(1):18-26, 2005. Google Scholar
  26. Wim H. Hesselink. Mechanical verification of lamport’s bakery algorithm. Science of Computer Programming, 78(9):1622-1638, 2013. Google Scholar
  27. Shing-Tsaan Huang and Nian-Shing Chen. A self-stabilizing algorithm for constructing breadth-first trees. Information Processing Letters, 41(2):109-117, 1992. Google Scholar
  28. Mauro Jaskelioff and Stephan Merz. Proving the correctness of disk paxos. Archive of Formal Proofs, 2005, 2005. Google Scholar
  29. Philipp Küfner, Uwe Nestmann, and Christina Rickmann. Formal verification of distributed algorithms - from pseudo code to checked proofs. In Jos C. M. Baeten, Thomas Ball, and Frank S. de Boer, editors, Theoretical Computer Science - 7th IFIP TC 1/WG 2.2 International Conference, TCS 2012, Amsterdam, The Netherlands, September 26-28, 2012. Proceedings, volume 7604 of Lecture Notes in Computer Science, pages 209-224, 2012. Google Scholar
  30. S. S. Kulkarni, J. Rushby, and N. Shankar. A case-study in component-based mechanical verification of fault-tolerant programs. In 19th IEEE International Conference on Distributed Computing Systems, pages 33-40, 1999. Google Scholar
  31. Marta Kwiatkowska, Gethin Norman, and David Parker. Probabilistic verification of herman’s self-stabilisation algorithm. Form. Asp. Comput., 24(4–6):661-670, July 2012. URL: https://doi.org/10.1007/s00165-012-0227-6.
  32. Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co., Inc., Boston, MA, USA, 2002. Google Scholar
  33. Stephan Merz. On the verification of a self-stabilizing algorithm. Technical report, University of Munich, 1998. Google Scholar
  34. Lawrence C. Paulson. Natural deduction as higher-order resolution. J. Log. Program., 3(3):237-258, 1986. URL: https://doi.org/10.1016/0743-1066(86)90015-4.
  35. S. Qadeer and N. Shankar. Verifying a self-stabilizing mutual exclusion algorithm. In International Conference on Programming Concepts and Methods (PROCOMET '98) 8-12 June 1998, Shelter Island, New York, USA, pages 424-443, Boston, MA, 1998. Springer US. Google Scholar
  36. Vincent Rahli, David Guaspari, Mark Bickford, and Robert L. Constable. Formal specification, verification, and implementation of fault-tolerant systems using eventml. ECEASST, 72, 2015. Google Scholar
  37. Vincent Rahli, David Guaspari, Mark Bickford, and Robert L. Constable. Eventml: Specification, verification, and implementation of crash-tolerant state machine replication systems. Sci. Comput. Program., 148:26-48, 2017. Google Scholar
  38. Vincent Rahli, Ivana Vukotic, Marcus Völp, and Paulo Jorge Esteves Veríssimo. Velisarios: Byzantine fault-tolerant protocols powered by coq. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, pages 619-650, 2018. Google Scholar
  39. Gerard Tel. Introduction to Distributed Algorithms. Cambridge University Press, 2 edition, 2000. URL: https://doi.org/10.1017/CBO9781139168724.
  40. The Coq Development Team. The Coq Proof Assistant Documentation, June 2012. URL: http://coq.inria.fr/refman/.
  41. Tatsuhiro Tsuchiya, Shin'ichi Nagano, Rohayu Bt Paidi, and Tohru Kikuno. Symbolic model checking for self-stabilizing algorithms. IEEE TPDS, 12(1):81-95, 2001. URL: https://doi.org/10.1109/71.899941.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact