Parameterized synthesis of self-stabilizing protocols in symmetric networks | Acta Informatica Skip to main content
Springer Nature Link
Log in

Parameterized synthesis of self-stabilizing protocols in symmetric networks

  • Original Article
  • Published:
Acta Informatica Aims and scope Submit manuscript

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 networks, including ring, line, mesh, and torus. First, we develop cutoffs that guarantee (1) closure in legitimate states, and (2) deadlock-freedom outside the legitimate states. We also develop a sufficient condition for convergence in self-stabilizing systems. Since some of our cutoffs grow with the size of the local state space of processes, scalability of the synthesis procedure is still a problem. We address this problem by introducing a novel SMT-based technique for counterexample-guided synthesis of self-stabilizing algorithms in symmetric networks. We have fully implemented our technique and successfully synthesized solutions to maximal matching, three coloring, and maximal independent set problems for ring and line topologies.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (Japan)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9

Similar content being viewed by others

Notes

  1. Note that a computation may be terminating in a state in \(\textit{LS}\).

  2. One can see that it is possible to find such a sequence of length \(l^2\) by an induction on l.

  3. Note that this property can be easily transformed to a property without the universal quantifier by introducing new variables that can take arbitrary values at the initialization and then keep their values.

  4. This approach is inspired by similar abstraction-based methods for the verification and synthesis of systems with many processes [3, 10].

  5. For example, for a topology with \(l=3\) in a torus with \(|m|=3\), the cutoff for the first case will be 2187.

References

  1. Alur, R., Raghothaman, M., Stergiou, C., Tripakis, S., Udupa, A.: Automatic completion of distributed protocols with symmetry. In International Conference on Computer Aided Verification, pp. 395–412. Springer (2015)

  2. Alur, R., Tripakis, S.: Automatic synthesis of distributed protocols. SIGACT News 48(1), 55–90 (2017)

    Article  MathSciNet  Google Scholar 

  3. Attie, P.C., Emerson, E.A.: Synthesis of concurrent systems with many similar processes. ACM Trans. Program. Lang. Syst. 20(1), 51–115 (1998)

    Article  Google Scholar 

  4. Außerlechner, S., Jacobs, S., Khalimov, A.: Tight cutoffs for guarded protocols with fairness. In International Conference on Verification, Model Checking, and Abstract Interpretation, pp. 476–494 (2016)

    Google Scholar 

  5. Basu, S., Ramakrishnan, C.: Compositional analysis for verification of parameterized systems. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 315–330 (2003)

    Chapter  Google Scholar 

  6. Bingham, B., Greenstreet, M., Bingham, J.: Parameterized verification of deadlock freedom in symmetric cache coherence protocols. In International Conference on Formal Methods in Computer-Aided Design, pp. 186–195 (2011)

  7. Bloem, R., Braud-Santoni, N., Jacobs, S.: Synthesis of self-stabilising and byzantine-resilient distributed systems. In: Chaudhuri, S., Farzan, A. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 9779, pp. 157–176. Springer, Cham (2016)

    Chapter  Google Scholar 

  8. Bloem, R., Jacobs, S., Khalimov, A.: Parameterized synthesis case study: AMBA AHB. In Workshop on Synthesis, volume 157 of EPTCS, pp. 68–83 (2014)

    Article  MathSciNet  Google Scholar 

  9. Clarke, E.M., Grumberg, O., Jha, S.: Verifying parameterized networks. ACM Trans. Program. Lang. Syst. (TOPLAS) 19(5), 726–750 (1997)

    Article  Google Scholar 

  10. Clarke, E.M., Talupur, M., Veith, H.: Environment abstraction for parameterized verification. In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol 3855, pp. 126–141. Springer, Berlin, Heidelberg (2005)

    Google Scholar 

  11. Conchon, S., Goel, A., Krstić, S., Mebsout, A., Zaïdi, F.: Cubicle: A parallel SMT-based model checker for parameterized systems. In International Conference on Computer Aided Verification, pp. 718–724 (2012)

    Chapter  Google Scholar 

  12. Devismes, S., Tixeuil, S., Yamashita, M.: Weak vs. self vs. probabilistic stabilization. In: Proceedings of the 28th IEEE International Conference on Distributed Computing Systems (ICDCS), pp. 681–688 (2008)

  13. Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)

    Article  Google Scholar 

  14. Dijkstra, E.W.: A belated proof of self-stabilization. Distrib. Comput. 1(1), 5–6 (1986)

    Article  Google Scholar 

  15. Dolev, D., Heljanko, K., Järvisalo, M., Korhonen, J., Lenzen, Ch., Rybicki, J., Suomela, J., Wieringa, S.: Synchronous counting and computational algorithm design. J. Comput. Syst. Sci. 82(2), 310–332 (2016)

    Article  MathSciNet  Google Scholar 

  16. Ebnenasir, A., Farahat, A.: A lightweight method for automated design of convergence. In IPDPS, pp. 219–230 (2011)

  17. Ebnenasir, A., Klinkhamer, A.: Topology-specific synthesis of self-stabilizing parameterized systems with constant-space processes. IEEE Trans. Softw. Eng. (2019) (Available through Early Access)

  18. Emerson, E.A., Namjoshi, K.S.: On reasoning about rings. Int. J. Found. Comput. Sci. 14(4), 527–550 (2003)

    Article  MathSciNet  Google Scholar 

  19. Cimatti et. al. A.: Nusmv 2: An opensource tool for symbolic model checking. In: Brinksma, E., Larsen, K.G. (eds.) Computer Aided Verification. Lecture Notes in Computer Science, vol. 2404, pp. 359–364. Springer, Berlin, Heidelberg (2002)

    Chapter  Google Scholar 

  20. Faghih, F., Bonakdarpour, B.: SMT-based synthesis of distributed self-stabilizing systems. In: Felber, P., Garg, V. (eds.) Stabilization, Safety, and Security of Distributed Systems. Lecture Notes in Computer Science, vol. 8756, pp. 165–179. Springer, Cham (2014)

    Google Scholar 

  21. Faghih, F., Bonakdarpour, B.: SMT-based synthesis of distributed self-stabilizing systems. ACM Trans. Auton. Adapt. Syst. (TAAS) 10(3), 21 (2015)

    Google Scholar 

  22. Faghih, F., Bonakdarpour, B.: ASSESS: A tool for automated synthesis of distributed self-stabilizing algorithms. In: SSS, pp. 219–233 (2017)

  23. Faghih, F., Bonakdarpour, B., Tixeuil, S., Kulkarni, S.: Specification-based synthesis of distributed self-stabilizing protocols. In: International Conference on Formal Techniques for Distributed Objects, Components, and Systems (FORTE), pp. 124–141 (2016)

    Chapter  Google Scholar 

  24. Faghih, F., Bonakdarpour, B., Tixeuil, S., Kulkarni, S.: Specification-based synthesis of distributed self-stabilizing protocols. In: Logical Methods in Computer Science (to appear)

  25. Farahat, A.: Automated design of self-stabilization. PhD thesis, Michigan Technological University, (2012)

  26. Farahat, A., Ebnenasir, A.: Local reasoning for global convergence of parameterized rings. In: International Conference on Distributed Computing Systems, pp. 496–505 (2012)

  27. Finkbeiner, B., Jacobs, S.: Lazy synthesis. In: Kuncak, V., Rybalchenko, A. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 7148, pp. 219–234. Springer, Berlin, Heidelberg (2012)

    Google Scholar 

  28. Finkbeiner, B., Schewe, S.: Bounded synthesis. Int. J. Softw. Tools Technol. Transf. (STTT) 15(5–6), 519–539 (2013)

    Article  Google Scholar 

  29. Gascón, A., Tiwari, A.: Synthesis of a simple self-stabilizing system (2014). arXiv preprint arXiv:1407.5392

  30. Gouda, M. G., Acharya, H. B.: Nash equilibria in stabilizing systems. In: Guerraoui, R., Petit, F. (eds.) Stabilization, Safety, and Security of Distributed Systems. Lecture Notes in Computer Science, vol. 5873, pp. 311–324. Springer, Berlin, Heidelberg (2009)

    Google Scholar 

  31. Hanna, Y., Samuelson, D., Basu, S., Rajan, H.: Automating cut-off for multi-parameterized systems. In: International Conference on Formal Engineering Methods, pp. 338–354 (2010)

    Chapter  Google Scholar 

  32. Jackson, D.: Software Abstractions: Logic, Language, and Analysis. MIT Press, Cambridge (2012)

    Google Scholar 

  33. Jacobs, S., Bloem, R.: Parameterized synthesis. In: Logical Methods in Computer Science, vol. 10, No. 1 (2014)

  34. Jacobs, S., Sakr, M.: A symbolic algorithm for lazy synthesis of eager strategies. In Automated Technology for Verification and Analysis (ATVA) (2018)

    Chapter  Google Scholar 

  35. Jacobs, S., Sakr, M.: Analyzing guarded protocols: Better cutoffs, more systems, more expressivity. In: Dillig, I., Palsberg, J. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 10747, pp. 247–268. Springer, Cham (2018)

    Google Scholar 

  36. Khalimov, A., Jacobs, S., Bloem, R.: Towards efficient parameterized synthesis. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) Verification, Model Checking, and Abstract Interpretation. Lecture Notes in Computer Science, vol. 7737, pp. 108–127. Springer, Berlin, Heidelberg (2013)

    Google Scholar 

  37. Klinkhamer, A., Ebnenasir, A.: On the complexity of adding convergence. In: Arbab, F., Sirjani, M. (eds.) Fundamentals of Software Engineering. Lecture Notes in Computer Science, vol. 8161, pp. 17–33. Springer, Berlin, Heidelberg (2013)

    Chapter  Google Scholar 

  38. Klinkhamer, A., Ebnenasir, A.: Verifying livelock freedom on parameterized rings and chains. In: Higashino, T., Katayama, Y., Masuzawa, T., Potop-Butucaru, M., Yamashita, M. (eds.) Stabilization, Safety, and Security of Distributed Systems. Lecture Notes in Computer Science, vol. 8255, pp. 163–177. Springer, Cham (2013)

    Google Scholar 

  39. Klinkhamer, A., Ebnenasir, A.: Synthesizing self-stabilization through superposition and backtracking. In: SSS, pp. 252–267 (2014)

    Google Scholar 

  40. Klinkhamer, A., Ebnenasir, A.: Shadow/puppet synthesis: a stepwise method for the design of self-stabilization. IEEE Trans. Parallel Distrib. Syst. 27(11), 3338–3350 (2016)

    Article  Google Scholar 

  41. Klinkhamer, A., Ebnenasir, A.: Synthesizing parameterized self-stabilizing rings with constant-space processes. In Fundamentals of Software Engineering (FSEN), pp. 100–115 (2017)

    Chapter  Google Scholar 

  42. Lazic, M., Konnov, I., Widder, J., Bloem, R.: Synthesis of distributed algorithms with parameterized threshold guards. In: On Principles of Distributed Systems (OPODIS) (2017)

  43. Manne, F., Mjelde, M., Pilard, L., Tixeuil, S.: A new self-stabilizing maximal matching algorithm. Theor. Comput. Sci. 410(14), 1336–1345 (2009)

    Article  MathSciNet  Google Scholar 

  44. McMillan, K.: Parameterized verification of the flash cache coherence protocol by compositional model checking. In: Advanced Research Working Conference on Correct Hardware Design and Verification Methods, pp. 179–195 (2001)

    Google Scholar 

  45. Raymond, Kerry: A tree-based algorithm for distributed mutual exclusion. ACM Trans. Comput. Syst. 7(1), 61–77 (1989)

    Article  Google Scholar 

  46. Siirtola, A., Heljanko, K.: Dynamic cut-off algorithm for parameterised refinement checking. In: International Conference on Formal Aspects of Component Software, pp. 256–276 (2018)

    Chapter  Google Scholar 

  47. Solar-Lezama, A.: Program sketching. STTT 15(5–6), 475–495 (2013)

    Article  Google Scholar 

  48. Weise, T., Tang, K.: Evolving distributed algorithms with genetic programming. IEEE Trans. Evol. Comput. 16(2), 242–265 (2011)

    Article  Google Scholar 

  49. Wolper, P., Lovinfosse, V.: Verifying properties of large sets of processes with network invariants. In: International Conference on Computer Aided Verification, pp. 68–80. Springer (1989)

Download references

Author information

Authors and Affiliations

  1. College of Engineering, University of Tehran, North Kargar St., Tehran, Iran

    Nahal Mirzaie & Fathiyeh Faghih

  2. CISPA Helmholtz Center for Information Security, Saarland Informatics Campus, 66123, Saarbrücken, Germany

    Swen Jacobs

  3. Department of Computer Science, Iowa State University, 207 Atanasoff Hall, Ames, IA, 50011, USA

    Borzoo Bonakdarpour

Authors
  1. Nahal Mirzaie
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Fathiyeh Faghih
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Swen Jacobs
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Borzoo Bonakdarpour
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Fathiyeh Faghih.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Mirzaie, N., Faghih, F., Jacobs, S. et al. Parameterized synthesis of self-stabilizing protocols in symmetric networks. Acta Informatica 57, 271–304 (2020). https://doi.org/10.1007/s00236-019-00361-7

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s00236-019-00361-7

Search

Navigation