Advertisement

sasa: A SimulAtor of Self-stabilizing Algorithms

  • Karine Altisen
  • Stéphane Devismes
  • Erwan JahierEmail author
Conference paper
  • 28 Downloads
Part of the Lecture Notes in Computer Science book series (LNCS, volume 12165)

Abstract

In this paper, we present sasa, an open-source SimulAtor of Self-stabilizing Algorithms. Self-stabilization defines the ability of a distributed algorithm to recover after transient failures. sasa is implemented as a faithful representation of the atomic-state model. This model is the most commonly used in the self-stabilizing area to prove both the correct operation and complexity bounds of self-stabilizing algorithms.

sasa encompasses all features necessary to debug, test, and analyze self-stabilizing algorithms. All these facilities are programmable to enable users to accommodate to their particular needs. For example, asynchrony is modeled by programmable stochastic daemons playing the role of input sequence generators. Algorithm’s properties can be checked using formal test oracles.

The design of sasa relies as much as possible on existing tools: ocaml, dot, and tools developed in the Synchrone Group of the VERIMAG laboratory.

Keywords

Simulation Debugging Reactive programs Synchronous languages Distributed computing Self-stabilization Atomic-state model 

References

  1. 1.
    Altisen, K., Corbineau, P., Devismes, S.: A framework for certified self-stabilization. Log. Methods Comput. Sci. 13(4) (2017) Google Scholar
  2. 2.
    Altisen, K., Devismes, S., Dubois, S., Petit, F.: Introduction to Distributed Self-Stabilizing Algorithms. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers, New York (2019)CrossRefGoogle Scholar
  3. 3.
    Arora, A., Dolev, S., Gouda, M.G.: Maintaining digital clocks in step. Parallel Process. Lett. 1, 11–18 (1991)CrossRefGoogle Scholar
  4. 4.
    Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. TTCS. Springer, Heidelberg (2004).  https://doi.org/10.1007/978-3-662-07964-5CrossRefzbMATHGoogle Scholar
  5. 5.
    Champion, A., Mebsout, A., Sticksel, C., Tinelli, C.: The Kind 2 model checker. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 510–517. Springer, Cham (2016).  https://doi.org/10.1007/978-3-319-41540-6_29CrossRefGoogle Scholar
  6. 6.
    Collin, Z., Dolev, S.: Self-stabilizing depth-first search. Inf. Process. Lett. 49(6), 297–301 (1994)CrossRefGoogle Scholar
  7. 7.
    Couvreur, J.-M., Francez, N., Gouda, M.G.: Asynchronous unison (extended abstract). In: Proceedings of the 12th International Conference on Distributed Computing Systems, pp. 486–493 (1992)Google Scholar
  8. 8.
    Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)CrossRefGoogle Scholar
  9. 9.
    Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)CrossRefGoogle Scholar
  10. 10.
    Erdös, P., Rényi, A.: On random graphs I. Publ. Math. Debrecen. 6, 290 (1959)MathSciNetzbMATHGoogle Scholar
  11. 11.
    Flatebo, M., Datta, A.K.: Simulation of self-stabilizing algorithms in distributed systems. In: Proceedings of the 25th Annual Simulation Symposium, pp. 32–41. IEEE Computer Society (1992)Google Scholar
  12. 12.
    Gansner, E.R., North, S.C.: An open graph visualization system and its applications to software engineering. Softw. Pract. Exp. 30(11), 1203–1233 (2000)CrossRefGoogle Scholar
  13. 13.
    Gradinariu, M., Tixeuil, S.: Self-stabilizing vertex coloration and arbitrary graphs. In: Butelle, F. (ed.) Proceedings of the 4th International Conference on Principles of Distributed Systems (OPODIS). Studia Informatica Universalis, pp. 55–70 (2000)Google Scholar
  14. 14.
    Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language Lustre. Proc. IEEE 79(9), 1305–1320 (1991)CrossRefGoogle Scholar
  15. 15.
    Har-Tal, O.: A simulator for self-stabilizing distributed algorithms (2000). https://www.cs.bgu.ac.il/~projects/projects/odedha/html/. Distributed Computing Group at ETH Zurich
  16. 16.
    Jahier, E.: Verimag tools tutorials: tutorials related to SASA. https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/
  17. 17.
    Jahier, E.: RDBG: a reactive programs extensible debugger. In: International Workshop on Software and Compilers for Embedded Systems (2016)Google Scholar
  18. 18.
    Jahier, E., Halbwachs, N., Raymond, P.: Engineering functional requirements of reactive systems using synchronous languages. In: International Symposium on Industrial Embedded Systems (2013)Google Scholar
  19. 19.
    Jahier, E., Raymond, P.: The synchrone reactive tool box. http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox
  20. 20.
    Lamport, L.: Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley Longman Publishing Co. Inc., Boston (2002)Google Scholar
  21. 21.
    Müllner, N., Dhama, A., Theel, O.E.: Derivation of fault tolerance measures of self-stabilizing algorithms by simulation. In: Proceedings of the 41st Annual Simulation Symposium, pp. 183–192. IEEE Computer Society (2008)Google Scholar
  22. 22.
    Ratel, C., Halbwachs, N., Raymond, P.: Programming and verifying critical systems by means of the synchronous data-flow programming language LUSTRE. In: ACM-SIGSOFT 1991 Conference on Software for Critical Systems, New Orleans, December 1991Google Scholar
  23. 23.
    Raymond, P., Roux, Y., Jahier, E.: Lutin: a language for specifying and executing reactive scenarios. EURASIP J. Embed. Syst. 2008, 1–11 (2008)CrossRefGoogle Scholar
  24. 24.
    Trivedi, K.S.: Probability and Statistics with Reliability, Queuing and Computer Science Applications, 2nd edn. Wiley, Hoboken (2002)zbMATHGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2020

Authors and Affiliations

  • Karine Altisen
    • 1
  • Stéphane Devismes
    • 1
  • Erwan Jahier
    • 1
    Email author
  1. 1.Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAGGrenobleFrance

Personalised recommendations