Document Open Access Logo

Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings

Authors Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs , Borzoo Bonakdarpour

PDF
Thumbnail PDF

File

LIPIcs.OPODIS.2018.29.pdf
  • Filesize: 0.5 MB
  • 17 pages

Document Identifiers

Author Details

Nahal Mirzaie
  • University of Tehran, North Kargar St., Tehran, Iran
Fathiyeh Faghih
  • University of Tehran, North Kargar St., Tehran, Iran
Swen Jacobs
  • CISPA Helmholtz Center i.G., Saarbrücken, Germany
Borzoo Bonakdarpour
  • Iowa State University, 207 Atanasoff Hall, Ames, IA 50011, USA

Funding

  • Jacobs, Swen: This research was supported by the German Research Foundation (DFG) under the project ASDPS (JA 2357/2-1).
  • Bonakdarpour, Borzoo: This research has been partially supported by the NSF SaTC-1813388 and a grant from Iowa State University.

Cite As Get BibTex

Nahal Mirzaie, Fathiyeh Faghih, Swen Jacobs, and Borzoo Bonakdarpour. Parameterized Synthesis of Self-Stabilizing Protocols in Symmetric Rings. In 22nd International Conference on Principles of Distributed Systems (OPODIS 2018). Leibniz International Proceedings in Informatics (LIPIcs), Volume 125, pp. 29:1-29:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.OPODIS.2018.29

Abstract

Self-stabilization in distributed systems is a technique to guarantee convergence to a set of legitimate states without external intervention when a transient fault or bad initialization occurs. Recently, there has been a surge of efforts in designing techniques for automated synthesis of self-stabilizing algorithms that are correct by construction. Most of these techniques, however, are not parameterized, meaning that they can only synthesize a solution for a fixed and predetermined number of processes. In this paper, we report a breakthrough in parameterized synthesis of self-stabilizing algorithms in symmetric rings. First, we develop tight cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimates states. We also develop a sufficient condition for convergence in silent self-stabilizing systems. Since some of our cutoffs grow with the size of local state space of processes, we also present an automated technique that significantly increases the scalability of synthesis in symmetric networks. Our technique is based on SMT-solving and incorporates a loop of synthesis and verification guided by counterexamples. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic and verification
  • Computer systems organization → Dependable and fault-tolerant systems and networks
Keywords
  • Parameterized synthesis
  • Self-stabilization
  • Formal methods

Metrics

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

References

  1. R. Bloem, N. Braud-Santoni, and S. Jacobs. Synthesis of self-stabilising and byzantine-resilient distributed systems. In CAV, pages 157-176, 2016. Google Scholar
  2. S. Devismes, S. Tixeuil, and M. Yamashita. Weak vs. Self vs. Probabilistic Stabilization. In ICDCS, pages 681-688, 2008. Google Scholar
  3. E. W. Dijkstra. Self-stabilizing systems in spite of distributed control. Communications of the ACM, 17(11):643-644, 1974. Google Scholar
  4. E. W. Dijkstra. A Belated Proof of Self-Stabilization. Distributed Computing, 1(1):5-6, 1986. Google Scholar
  5. A. Ebnenasir and A. Farahat. A Lightweight Method for Automated Design of Convergence. In IPDPS, pages 219-230, 2011. Google Scholar
  6. E. A. Emerson and K. S. Namjoshi. On Reasoning About Rings. International Journal on Foundations of Computer Science., 14(4):527-550, 2003. Google Scholar
  7. A. Cimatti et. al. Nusmv 2: An opensource tool for symbolic model checking. In CAV, pages 359-364, 2002. Google Scholar
  8. F. Faghih and B. Bonakdarpour. SMT-based synthesis of distributed self-stabilizing systems. In SSS, pages 165-179, 2014. Google Scholar
  9. F. Faghih and B. Bonakdarpour. SMT-based synthesis of distributed self-stabilizing systems. ACM Transactions on Autonomous and Adaptive Systems (TAAS), 10(3):21, 2015. Google Scholar
  10. F. Faghih and B. Bonakdarpour. ASSESS: A tool for automated synthesis of distributed self-stabilizing algorithms. In SSS, pages 219-233, 2017. Google Scholar
  11. F. Faghih, B. Bonakdarpour, S. Tixeuil, and S. Kulkarni. Specification-based Synthesis of Distributed Self-Stabilizing Protocols. In FORTE, pages 124-141, 2016. Google Scholar
  12. F. Faghih, B. Bonakdarpour, S. Tixeuil, and S. Kulkarni. Specification-based Synthesis of Distributed Self-Stabilizing Protocols. Logical Methods in Computer Science, To appear. Google Scholar
  13. B. Finkbeiner and S. Jacobs. Lazy Synthesis. In VMCAI, 2012. Google Scholar
  14. M. G. Gouda and H. B. Acharya. Nash Equilibria in Stabilizing Systems. In SSS, pages 311-324, 2009. Google Scholar
  15. D. Jackson. Software Abstractions: Logic, Language, and Analysis. MIT Press Cambridge, 2012. Google Scholar
  16. S. Jacobs and R. Bloem. Parameterized Synthesis. Logical Methods in Computer Science, 10(1), 2014. Google Scholar
  17. A. Khalimov, S. Jacobs, and R. Bloem. Towards Efficient Parameterized Synthesis. In VMCAI, volume 7737 of Lecture Notes in Computer Science, pages 108-127. Springer, 2013. Google Scholar
  18. A. Klinkhamer and A. Ebnenasir. On the Complexity of Adding Convergence. In FSEN, pages 17-33, 2013. Google Scholar
  19. A. Klinkhamer and A. Ebnenasir. Verifying Livelock Freedom on Parameterized Rings and Chains. In SSS, pages 163-177, 2013. Google Scholar
  20. A. Klinkhamer and A. Ebnenasir. Synthesizing Self-stabilization through Superposition and Backtracking. In SSS, pages 252-267, 2014. Google Scholar
  21. A. Klinkhamer and A. Ebnenasir. Synthesizing Parameterized Self-stabilizing Rings with Constant-Space Processes. In FSEN, pages 100-115, 2017. Google Scholar
  22. Marijana Lazic, Igor Konnov, Josef Widder, and Roderick Bloem. Synthesis of Distributed Algorithms with Parameterized Threshold Guards. In OPODIS, 2017. Google Scholar
  23. F. Manne, M. Mjelde, L. Pilard, and S. Tixeuil. A new self-stabilizing maximal matching algorithm. Theoretical Computer Science, 410(14):1336-1345, 2009. Google Scholar
  24. Kerry Raymond. A Tree-Based Algorithm for Distributed Mutual Exclusion. ACM Transactions on Computer Systems, 7(1):61-77, 1989. Google Scholar
  25. Armando Solar-Lezama. Program sketching. STTT, 15(5-6):475-495, 2013. Google Scholar
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 About DROPS Imprint Privacy Contact