×

zbMATH — the first resource for mathematics

Parameterized synthesis of self-stabilizing protocols in symmetric networks. (English) Zbl 1435.68201
Summary: 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.
MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68M10 Network design and communication in computer systems
68M12 Network protocols
68M14 Distributed systems
68R10 Graph theory (including graph drawing) in computer science
Software:
Cubicle; NuSMV
PDF BibTeX XML Cite
Full Text: DOI
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)
[3] Attie, Pc; Emerson, Ea, Synthesis of concurrent systems with many similar processes, ACM Trans. Program. Lang. Syst., 20, 1, 51-115 (1998)
[4] Außerlechner, Simon; Jacobs, Swen; Khalimov, Ayrat, Tight Cutoffs for Guarded Protocols with Fairness, Lecture Notes in Computer Science, 476-494 (2015), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 06559872
[5] Basu, Samik; Ramakrishnan, C. R., Compositional Analysis for Verification of Parameterized Systems, Tools and Algorithms for the Construction and Analysis of Systems, 315-330 (2003), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1031.68543
[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, Roderick; Braud-Santoni, Nicolas; Jacobs, Swen, Synthesis of Self-Stabilising and Byzantine-Resilient Distributed Systems, Computer Aided Verification, 157-176 (2016), Cham: Springer International Publishing, Cham · Zbl 1411.68073
[8] Bloem, Roderick; Jacobs, Swen; Khalimov, Ayrat, Parameterized Synthesis Case Study: AMBA AHB, Electronic Proceedings in Theoretical Computer Science, 157, 68-83 (2014)
[9] Clarke, Em; Grumberg, O.; Jha, S., Verifying parameterized networks, ACM Trans. Program. Lang. Syst. (TOPLAS), 19, 5, 726-750 (1997)
[10] Clarke, Edmund; Talupur, Muralidhar; Veith, Helmut, Environment Abstraction for Parameterized Verification, Lecture Notes in Computer Science, 126-141 (2005), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1176.68117
[11] Conchon, Sylvain; Goel, Amit; Krstić, Sava; Mebsout, Alain; Zaïdi, Fatiha, Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems, Computer Aided Verification, 718-724 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[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) · Zbl 1320.68047
[13] Dijkstra, Ew, Self-stabilizing systems in spite of distributed control, Commun. ACM, 17, 11, 643-644 (1974) · Zbl 0305.68048
[14] Dijkstra, Ew, A belated proof of self-stabilization, Distrib. Comput., 1, 1, 5-6 (1986) · Zbl 0604.68015
[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) · Zbl 1346.68038
[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) · Zbl 1433.68254
[18] Emerson, Ea; Namjoshi, Ks, On reasoning about rings, Int. J. Found. Comput. Sci., 14, 4, 527-550 (2003) · Zbl 1101.68371
[19] Cimatti, Alessandro; Clarke, Edmund; Giunchiglia, Enrico; Giunchiglia, Fausto; Pistore, Marco; Roveri, Marco; Sebastiani, Roberto; Tacchella, Armando, NuSMV 2: An OpenSource Tool for Symbolic Model Checking, Computer Aided Verification, 359-364 (2002), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1010.68766
[20] Faghih, Fathiyeh; Bonakdarpour, Borzoo, SMT-Based Synthesis of Distributed Self-stabilizing Systems, Lecture Notes in Computer Science, 165-179 (2014), Cham: Springer International Publishing, Cham
[21] Faghih, F.; Bonakdarpour, B., SMT-based synthesis of distributed self-stabilizing systems, ACM Trans. Auton. Adapt. Syst. (TAAS), 10, 3, 21 (2015)
[22] Faghih, F., Bonakdarpour, B.: ASSESS: A tool for automated synthesis of distributed self-stabilizing algorithms. In: SSS, pp. 219-233 (2017)
[23] Faghih, Fathiyeh; Bonakdarpour, Borzoo; Tixeuil, Sébastien; Kulkarni, Sandeep, Specification-Based Synthesis of Distributed Self-Stabilizing Protocols, Formal Techniques for Distributed Objects, Components, and Systems, 124-141 (2016), Cham: Springer International Publishing, Cham · Zbl 1398.68056
[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) · Zbl 1398.68056
[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, Bernd; Jacobs, Swen, Lazy Synthesis, Lecture Notes in Computer Science, 219-234 (2012), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1326.68183
[28] Finkbeiner, B.; Schewe, S., Bounded synthesis, Int. J. Softw. Tools Technol. Transf. (STTT), 15, 5-6, 519-539 (2013)
[29] Gascón, A., Tiwari, A.: Synthesis of a simple self-stabilizing system (2014). arXiv preprint arXiv:1407.5392
[30] Gouda, Mohamed G.; Acharya, Hrishikesh B., Nash Equilibria in Stabilizing Systems, Lecture Notes in Computer Science, 311-324 (2009), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[31] Hanna, Youssef; Samuelson, David; Basu, Samik; Rajan, Hridesh, Automating Cut-off for Multi-parameterized Systems, Formal Methods and Software Engineering, 338-354 (2010), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[32] Jackson, D., Software Abstractions: Logic, Language, and Analysis (2012), Cambridge: MIT Press, Cambridge
[33] Jacobs, S., Bloem, R.: Parameterized synthesis. In: Logical Methods in Computer Science, vol. 10, No. 1 (2014) · Zbl 1325.68149
[34] Jacobs, Swen; Sakr, Mouhammad, A Symbolic Algorithm for Lazy Synthesis of Eager Strategies, Automated Technology for Verification and Analysis, 211-227 (2018), Cham: Springer International Publishing, Cham
[35] Jacobs, Swen; Sakr, Mouhammad, Analyzing Guarded Protocols: Better Cutoffs, More Systems, More Expressivity, Lecture Notes in Computer Science, 247-268 (2017), Cham: Springer International Publishing, Cham
[36] Khalimov, Ayrat; Jacobs, Swen; Bloem, Roderick, Towards Efficient Parameterized Synthesis, Lecture Notes in Computer Science, 108-127 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1426.68051
[37] Klinkhamer, Alex; Ebnenasir, Ali, On the Complexity of Adding Convergence, Fundamentals of Software Engineering, 17-33 (2013), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1434.68110
[38] Klinkhamer, Alex P.; Ebnenasir, Ali, Verifying Livelock Freedom on Parameterized Rings and Chains, Lecture Notes in Computer Science, 163-177 (2013), Cham: Springer International Publishing, Cham
[39] Klinkhamer, Alex; Ebnenasir, Ali, Synthesizing Self-stabilization through Superposition and Backtracking, Lecture Notes in Computer Science, 252-267 (2014), Cham: Springer International Publishing, Cham
[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)
[41] Klinkhamer, Alex P.; Ebnenasir, Ali, Synthesizing Parameterized Self-stabilizing Rings with Constant-Space Processes, Fundamentals of Software Engineering, 100-115 (2017), Cham: Springer International Publishing, Cham
[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) · Zbl 1163.68372
[44] Mcmillan, K. L., Parameterized Verification of the FLASH Cache Coherence Protocol by Compositional Model Checking, Lecture Notes in Computer Science, 179-195 (2001), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 1002.68674
[45] Raymond, Kerry, A tree-based algorithm for distributed mutual exclusion, ACM Trans. Comput. Syst., 7, 1, 61-77 (1989)
[46] Siirtola, Antti; Heljanko, Keijo, Dynamic Cut-Off Algorithm for Parameterised Refinement Checking, Formal Aspects of Component Software, 256-276 (2018), Cham: Springer International Publishing, Cham
[47] Solar-Lezama, A., Program sketching, STTT, 15, 5-6, 475-495 (2013)
[48] Weise, T.; Tang, K., Evolving distributed algorithms with genetic programming, IEEE Trans. Evol. Comput., 16, 2, 242-265 (2011)
[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)
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.