Skip to content
Snippets Groups Projects
README.org 13.1 KiB
Newer Older
# +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:
erwan's avatar
erwan committed

#+BEGIN_SRC sh
ocamlfind ocamlopt -shared -package sasacore p.ml -o p.cmxs
sasa g.dot
#+END_SRC
erwan's avatar
erwan committed

erwan's avatar
erwan committed
The source code is available at
https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa

* Topology
erwan's avatar
erwan committed

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
erwan's avatar
erwan committed

#+BEGIN_SRC dot :file ring.ml :exports code
erwan's avatar
erwan committed
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"]
erwan's avatar
erwan committed

 p1 -- p2 -- p3 -- p4 -- p5 -- p6 -- p7 -- p1 
}
#+END_SRC

Of course the =some_algo.ml= file must exist. 

erwan's avatar
erwan committed
* Algorithms

Those algorithms, implemented in =ocaml=,  must provide:
erwan's avatar
erwan committed
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

erwan's avatar
erwan committed
More precisely, each algorithm should provide 3 functions that must be
registred using the string used in dot file algo fields with:
erwan's avatar
erwan committed
-  =reg_vars=
-  =reg_enable=
-  =reg_step=

erwan's avatar
erwan committed
which profiles is defined in [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli][algo.mli]]
erwan's avatar
erwan committed

#+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

erwan's avatar
erwan committed
Algorithms must then be compiled with =ocamlopt -shared= to produce
the =.cmxs= files corresponding to the =.ml= mentionned in the dot
file algo fields.
erwan's avatar
erwan committed

#+BEGIN_SRC sh
erwan's avatar
erwan committed
ocamlopt -shared -I +sasa some_algo.ml -o some_algo.cmxs
erwan's avatar
erwan committed
#+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.
erwan's avatar
erwan committed



** Running batch simulations with Built-in demons

To launch batch simulations, one can use the =sasa= Command Line Interface.
erwan's avatar
erwan committed

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: 


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
erwan's avatar
erwan committed
  sasa --help
erwan's avatar
erwan committed

#+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)
erwan's avatar
erwan committed

#+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
erwan's avatar
erwan committed
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