# +SETUPFILE: theme-readtheorg-local.setup #+SETUPFILE: theme-bigblow-local.setup #+TOC: headlines 2 #+LANGUAGE: en #+OPTIONS: H:3 num:nil \n:nil @:t ::t |:t ^:t -:t f:t *:t TeX:t LaTeX:nil skip:nil tags:not-in-toc #+LINK_UP:http://www-verimag.imag.fr/ #+LINK_HOME:http://www-verimag.imag.fr/ #+OPTIONS: toc:nil #+TOC: listings #+TOC: tables #+EMAIL: erwan.jahier@univ-grenoble-alpes.fr #+AUTHOR: Erwan Jahier #+TITLE: Self-stabilizing Algorithms SimulAtor: sasa * TL;DR SASA is a *Self-stabilizing Algorithms SimulAtor*, based on the so-called *state model* introduced by _Dijkstra_ in its seminal article on [[http://www.cs.utexas.edu/~EWD/ewd04xx/EWD426.PDF][Self-stabilizing distributed algorithms]] Basically, one needs to provide: 1. a topology, made of nodes and channels (via a dot file) 2. the algorithms attached to nodes (via =ocaml= programs) Now, suppose you have a topology defined in =ring.dot=, that refers to an algorithm defined in the ocaml program =p.ml= (cf =test/skeleton/= directory), you can simulate it as follows: #+BEGIN_SRC sh ocamlfind ocamlopt -shared -package sasacore p.ml -o p.cmxs sasa g.dot #+END_SRC The source code is available at https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa * Topology The topology is given via =.dot= files, that should 1. follow the [[https://en.wikipedia.org/wiki/DOT_(graph_description_language)][graphviz/dot format]] 2. have nodes *labelled* by the =algo= field #+BEGIN_SRC dot :file ring.ml :exports code graph ring { p1 [algo="some_algo.ml"] p2 [algo="some_algo.ml"] p3 [algo="some_algo.ml"] p4 [algo="some_algo.ml"] p5 [algo="some_algo.ml"] p6 [algo="some_algo.ml"] p7 [algo="some_algo.ml"] p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1 } #+END_SRC Of course the =some_algo.ml= file must exist. * Algorithms Those algorithms, implemented in =ocaml=, must provide: 1. a set of variables (registers) 2. an =enable= fonction that says which actions are enabled (i.e., that can be activated) 3. a =step= function that executes enabled actions More precisely, each algorithm should provide 3 functions that must be registred using the string used in dot file algo fields with: - =reg_vars= - =reg_enable= - =reg_step= which profiles is defined in [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli][algo.mli]] #+BEGIN_SRC ocaml let x = ref 6 in !x type t #+END_SRC #+BEGIN_SRC lutin let x = ref 6 in !x type t #+END_SRC #+INCLUDE: "../../lib/algo/algo.mli" src ocaml :export code Optionnaly, one can register a function that provides initial values to local variables (=reg_init=). If not such registration is done, local variables will be set according to =init= annotations in the dot file. If no such annotations exists, initial values will be chosen at random. #+BEGIN_SRC dot :file ring-init.ml graph ring { p1 [algo="some_algo.ml" init="v=1" init="x=3"] p2 [algo="some_algo.ml"] p3 [algo="some_algo.ml"] p4 [algo="some_algo.ml"] p5 [algo="some_algo.ml"] p6 [algo="some_algo.ml"] p7 [algo="some_algo.ml"] p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1 } #+END_SRC Algorithms must then be compiled with =ocamlopt -shared= to produce the =.cmxs= files corresponding to the =.ml= mentionned in the dot file algo fields. #+BEGIN_SRC sh ocamlopt -shared -I +sasa some_algo.ml -o some_algo.cmxs #+END_SRC Actions names (=string=) must be registered if one wants to use =sasa= with custom demons (cf below). Some examples can be found in the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test][test]] directory. * Batch Simulations ** Running batch simulations with Built-in demons To launch batch simulations, one can use the =sasa= Command Line Interface. For instance, in order to simulate an algorithm defined in the =ring.dot= (cf [[file:../../test/coloring]]), you can launch the following command: #+BEGIN_SRC sh sasa ring.dot #+END_SRC By default, the distributed demon will be used to activate actions. Several other demon can be used, via one of the following options: #+BEGIN_SRC sh :results output :exports both sasa -h | grep "\-demon" #+END_SRC #+RESULTS: : --synchronous-demon, -sd : --central-demon, -cd : --locally-central-demon, -lcd : --distributed-demon, -dd : --custom-demon, -custd ** Running batch simulations with manual demons By using the =--custom-demon= option (or =-custd= for short), you can play the role of the demon. More precisely, you will be prompted for stating which actions should be activated, among the set of enabled actions. #+BEGIN_SRC sh :results output :exports both :var input="t t t t t t t" cd ../../test/unison sasa ring.dot --custom-demon #+END_SRC #+RESULTS: At each step, xxx In the custom demon mode, the demon is executed outside =sasa=, by a process that communicates via the standard input/output using [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-5][RIF]] conventions. More precisely, =sasa= writes on =stdout= a Boolean for each action and each process, that states if the corresponding action is enabled for the current step. Then it reads on =stdin= a Boolean for each action and each process that tells which actions (among the enabled ones) should be activated. The demon can thus be played by users that read and enter Boolean values. In order to enter such input more easily, one can use [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-8][=luciole-rif=]] #+BEGIN_SRC sh luciole-rif sasa ring.dot --custom-demon #+END_SRC It can also by simulated by [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-4][=lutin=]] programs via the use of [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-9][=lurette=]] (for batch executions) or [[http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/#outline-container-sec-10][=rdbg=]] (for interactive sessions). Built-in demons can of course be programmed in Lutin. One can generate such demons using the =--gen-lutin-demon= option: =sasa --gen-lutin-demon a_graph.dot=. It can be handy at least to get the demons variables names in the good order if one to write its own demon. Moreover, for using the custom mode, it is mandatory to register actions (via =Algo.reg_actions=). ** Running batch simulations with =lurette= If you want to perform simulations with custom demons, you need to use =lurette=. For instance, in order to simulate an algorithm defined in the =ring.dot= (cf [[file:../../test/coloring]]) using a Lutin demon defined in =ring.lut=, you can launch the following command: #+BEGIN_SRC sh lurette \ -env "sasa ring.dot -custd" \ -sut "lutin ring.lut -n distributed" #+END_SRC ** The =sasa= CLI #+BEGIN_SRC sh :results output :exports both sasa --help #+END_SRC #+RESULTS: #+begin_example usage: sasa [<option>]* <topology>.dot use -h to see the available options. --synchronous-demon, -sd Use a Synchronous demon --central-demon, -cd Use a Central demon (selects exactly one action) --locally-central-demon, -lcd Use a Locally Central demon (i.e., never activates two neighbors actions in the same step) --distributed-demon, -dd Use a Distributed demon (which select at least one action) --custom-demon, -custd Use a Custom demon (forces --rif) --rif, -rif Follows RIF conventions --seed, -seed Set the pseudo-random generator seed of build-in demons --length, -l <int> Maximum number of steps to be done (10000 by default). --verbose, -vl <int> Set the verbose level --help, -help, -h Display main options --more, -m Display more options #+end_example More =sasa= options: #+BEGIN_SRC sh :results output :exports both sasa --more #+END_SRC #+RESULTS: #+begin_example --gen-lutin-demon, -gld Generate Lutin demons and exit --dummy-input Add a dummy input to sasa so that built-in demon can be used from rdbg --ignore-first-inputs, -ifi Ignore first inputs (necessary to use luciole via lurette/rdbg/luciole-rif) --version, -version, -v Display the sasa version and exit. --ocaml-version Display the version ocaml version sasa was compiled with and exit. #+end_example * Interactive Simulation If you want to perform interaction Lutin, =lurette=, and =rdbg= cf =Makefile= in the [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/tree/master/test][test]] directory. In each sub-directory of [[file:../../test/][../../test/]], there is a =rdbg-session.ml= file that takes care of the red-tape for using =rdbg= with the corresponding examples. ** Running interactive sessions with =rdbg= 1. type =rdbg= 2. press enter to load the defaut session (=rdbg-session.ml=). Then you can type: 3. =d= for displaying a (dynamic) dot graph with =dot= 4. or ALTERNATIVELY =ne= to use the =neato= layout engine (=tw=, =ci=, =fd=, =sf=, =pa=, =os= to use the =twopi=, =circo=, =fdp=, =sfd=, =patchwork=, =osage= layout engines respectively) 5. =s= to move one step forward 6. =sd= to move one step forward and call =d= (to update the graph display []) 7. =nr= to move one round forward 8. =pr= to move one round backward 9. =go= to move forward until convergence All those commands are defined in [[file:../../test/my-rdbg-tuning.ml][../../test/my-rdbg-tuning.ml]] that is included in =test/*/rdbg-session.ml= files. This file contain straigthforward =ocaml= code that defines various =rdbg= shortcuts to ease the simulation of =sasa= systems. Feel free to tailor those command to yours needs! For instance, go to the =test/alea-coloring/= directory. It contains the following files: - =my-rdbg-tuning.ml= that is actually a symbolic link to the [[file:../../test/my-rdbg-tuning.ml][../../test/my-rdbg-tuning.ml]] file - =ring.dot=: the topology - =p.ml=: the algo used in =ring.dot= - =Makefile=: demonstrate various ways of using =sasa= #+BEGIN_SRC sh make rdbg #+END_SRC This rule - generates the =p.cmxs= and =p.cma= files, resulting from the compilation of =p.ml= (the makefile rules are in =../Makefile.inc=). - generates a =ring.lut= file (out of =ring.dot= and =p.cmxs=) that defines various Lutin demons - launch =rdbg= with some arguments. =rdbg= then prompts the user to enter some commands. #+BEGIN_SRC sh rdbg -o ring.rif \ -env "sasa -seed 42 -l 100 ring.dot -custd -rif" \ -sut-nd "lutin ring.lut -n distributed" [c] create a fresh session [q] quit [s] do nothing [0/s/q/c/1/2/...]: #+END_SRC hence let's create a fresh session by typing 'c' and then 'return'. This will result in the creation of the =rdbg_session.ml= file, that load all the necessary modules to run an interactive session with =rdbg=, where =rdbg= simulates ring.dot with =sasa= using a distributed demon. For instance, you can type =nr [return]=, a rdbg command defined in [[file:../../test/my-rdbg-tuning.ml][../../test/my-rdbg-tuning.ml]] that steps until the next round is reached. Then, by typing =[return]=; =rdbg= will run the lastly used command, which is =nr=, which allow you to move forward in the execution from rounds to rounds. If you want to go backwards to the previous round, you can use the =br= command=, also defined in [[file:../../test/my-rdbg-tuning.ml][../../test/my-rdbg-tuning.ml]]. nb: the next time rdbg is launched (even without argument), you will be prompted with the possibility to reuse this session. #+BEGIN_SRC sh rdbg [0] #use "rdbg-session.ml" [c] create a fresh session [q] quit [s] do nothing [0/s/q/c/1/2/...]: #+END_SRC Typing '0' will therefore also load the =rdbg_session.ml= file we have just been using. ** Running batch sessions with =lurette= XXX TODO * Viewing Results =sasa -rif= and =lurette= generates =.rif= files that can be viewed with =gnuplot-rif= or =sim2chro=; cf http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v6/ * Install ** From source You will need: - =make= (gnu) - a set of tools installable via [[https://opam.ocaml.org/][opam]] - =dune= - =ocamlgraph= - =lutin= (not for compiling actually, but for using sasa with custom demons) One can mimick the content of the =test= job in the project [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/.gitlab-ci.yml][Gitlab CI script]]. ** Via opam (not yet working) #+BEGIN_SRC sh :tangle sh/install-opam.sh :noweb yes :tangle-mode (identity #o444) opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository" opam update -y opam install -y sasa #+END_SRC Once this is done, upgrading to the last version of the tools is as simple as: #+BEGIN_SRC yaml opam update opam upgrade #+END_SRC In order to install the tools mentionned in this documentation that can be used with =sasa= (namely, =gnuplot-rif=, =sim2chro=, =luciole-rif=, =lutin=, =lurette=, =rdbg=): #+BEGIN_SRC sh :tangle sh/install-opam.sh :noweb yes :tangle-mode (identity #o444) opam depext -y rdbg lutin opam install -y rdbg lutin #+END_SRC * More - Releases Notes: https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/releases - Sources: https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa * FAQ ** Is there a FAQ? yes