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

erwan
committed
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:
which profiles is defined in [[https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/blob/master/lib/algo/algo.mli][algo.mli]]

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

erwan
committed
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.
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.

erwan
committed
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:

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

erwan
committed
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

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

erwan
committed
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=).

erwan
committed
** 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
committed
#+END_SRC

erwan
committed
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
#+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

erwan
committed
#+BEGIN_SRC sh :results output :exports both

erwan
committed
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

erwan
committed

erwan
committed
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=

erwan
committed
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

erwan
committed
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!
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
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/

erwan
committed
** 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

erwan
committed
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