Skip to main content
SpringerLink
Log in
Book cover

International Conference on Tests and Proofs

TAP 2020: Tests and Proofs pp 143–154Cite as

sasa: A SimulAtor of Self-stabilizing Algorithms

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

This study was partially supported by the French anr projects ANR-16-CE40-0023 (descartes) and ANR-16 CE25-0009-03 (estate).

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

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    A transient fault occurs at an unpredictable time, but does not result in a permanent hardware damage. Moreover, as opposed to intermittent faults, the frequency of transient faults is considered to be low.

  2. 2.

    http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa.

  3. 3.

    To the best of our knowledge, this model is exclusively used in the self-stabilizing area.

  4. 4.

    At the first step, the simulation loop starts in (1-b).

References

  1. Altisen, K., Corbineau, P., Devismes, S.: A framework for certified self-stabilization. Log. Methods Comput. Sci. 13(4) (2017)

    Google Scholar 

  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)

    Book  Google Scholar 

  3. Arora, A., Dolev, S., Gouda, M.G.: Maintaining digital clocks in step. Parallel Process. Lett. 1, 11–18 (1991)

    Article  Google Scholar 

  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-5

    Book  MATH  Google Scholar 

  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_29

    Chapter  Google Scholar 

  6. Collin, Z., Dolev, S.: Self-stabilizing depth-first search. Inf. Process. Lett. 49(6), 297–301 (1994)

    Article  Google Scholar 

  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. Dijkstra, E.W.: Self-stabilizing systems in spite of distributed control. Commun. ACM 17(11), 643–644 (1974)

    Article  Google Scholar 

  9. Dolev, S.: Self-Stabilization. MIT Press, Cambridge (2000)

    Book  Google Scholar 

  10. Erdös, P., Rényi, A.: On random graphs I. Publ. Math. Debrecen. 6, 290 (1959)

    MathSciNet  MATH  Google Scholar 

  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. 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)

    Article  Google Scholar 

  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. Halbwachs, N., Caspi, P., Raymond, P., Pilaud, D.: The synchronous data flow programming language Lustre. Proc. IEEE 79(9), 1305–1320 (1991)

    Article  Google Scholar 

  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. Jahier, E.: Verimag tools tutorials: tutorials related to SASA. https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/

  17. Jahier, E.: RDBG: a reactive programs extensible debugger. In: International Workshop on Software and Compilers for Embedded Systems (2016)

    Google Scholar 

  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. Jahier, E., Raymond, P.: The synchrone reactive tool box. http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/reactive-toolbox

  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. 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. 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 1991

    Google Scholar 

  23. Raymond, P., Roux, Y., Jahier, E.: Lutin: a language for specifying and executing reactive scenarios. EURASIP J. Embed. Syst. 2008, 1–11 (2008)

    Article  Google Scholar 

  24. Trivedi, K.S.: Probability and Statistics with Reliability, Queuing and Computer Science Applications, 2nd edn. Wiley, Hoboken (2002)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Univ. Grenoble Alpes, CNRS, Grenoble INP, VERIMAG, Grenoble, 38000, France

    Karine Altisen, Stéphane Devismes & Erwan Jahier

Authors
  1. Karine Altisen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Stéphane Devismes
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Erwan Jahier
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Erwan Jahier .

Editor information

Editors and Affiliations

  1. Chalmers University of Technology, Gothenburg, Sweden

    Wolfgang Ahrendt

  2. Paderborn University, Paderborn, Germany

    Heike Wehrheim

A Artifact

A Artifact

We have set up a zenodo entry that contains the necessary materials to reproduce the results given in this article: https://doi.org/10.5281/zenodo.3753012. This entry contains:

  • a zip file containing an artifact based on the (public) TAP 2020 Virtual Machine (https://doi.org/10.5281/zenodo.3751283). It is the artefact that has been validated by the TAP 2020 evaluation committee.

  • a zip file made out of a public git repository containing the same set of scripts; the differences are that it is much smaller, and that the top-level script uses docker to replay the experiments. The entry also contains a link to this git repository.

  • a zip file containing the raw data produced by the experiment scripts via a Gitlab CI pipeline of the git repository.

In more details, the artefact contains instructions to install the necessary tools, to replay the interactive session described in Sect. 2 of the present paper, and to automatically generate the data contained in Table 1 of Sect. 4. The objective of this artifact is only to let one reproduce the results. If you want to learn more about the tool-set, we advice the reader to look at the documentation and tutorials online [16].

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Altisen, K., Devismes, S., Jahier, E. (2020). sasa: A SimulAtor of Self-stabilizing Algorithms. In: Ahrendt, W., Wehrheim, H. (eds) Tests and Proofs. TAP 2020. Lecture Notes in Computer Science(), vol 12165. Springer, Cham. https://doi.org/10.1007/978-3-030-50995-8_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-50995-8_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-50994-1

  • Online ISBN: 978-3-030-50995-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation