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 Self-stabilizing distributed algorithms
Basically, one needs to provide:
- a topology, made of nodes and channels (via a dot file)
- 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:
ocamlfind ocamlopt -shared -package sasacore p.ml -o p.cmxs
sasa g.dot
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
- follow the graphviz/dot format
- have nodes labelled by the
algo
field
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
}
Of course the some_algo.ml
file must exist.
Algorithms
Those algorithms, implemented in ocaml
, must provide:
- a set of variables (registers)
- an
enable
fonction that says which actions are enabled (i.e., that can be activated) - 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 algo.mli
let x = ref 6 in
!x
type t
let x = ref 6 in
!x
type t
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.
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
}
Algorithms must then be compiled with ocamlopt -shared
to produce
the .cmxs
files corresponding to the .ml
mentionned in the dot
file algo fields.
ocamlopt -shared -I +sasa some_algo.ml -o some_algo.cmxs
Actions names (string
) must be registered if one wants to use sasa
with custom demons (cf below).
Some examples can be found in the 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 ../../test/coloring), you can launch the following
command:
sasa ring.dot
By default, the distributed demon will be used to activate actions. Several other demon can be used, via one of the following options:
sasa -h | grep "\-demon"
--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.
cd ../../test/unison
sasa ring.dot --custom-demon
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 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 =luciole-rif=
luciole-rif sasa ring.dot --custom-demon
It can also by simulated by =lutin= programs via the use of =lurette= (for batch executions) or =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 ../../test/coloring) using a Lutin demon defined
in ring.lut
, you can launch the following command:
lurette \
-env "sasa ring.dot -custd" \
-sut "lutin ring.lut -n distributed"
The sasa
CLI
sasa --help
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
More sasa
options:
sasa --more
--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.
Interactive Simulation
If you want to perform interaction
Lutin, lurette
, and rdbg
cf Makefile
in the test directory.
In each sub-directory of ../../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
- type
rdbg
- press enter to load the defaut session (
rdbg-session.ml
). Then you can type: -
d
for displaying a (dynamic) dot graph withdot
- or ALTERNATIVELY
ne
to use theneato
layout engine (tw
,ci
,fd
,sf
,pa
,os
to use thetwopi
,circo
,fdp
,sfd
,patchwork
,osage
layout engines respectively) -
s
to move one step forward -
sd
to move one step forward and calld
(to update the graph display []) -
nr
to move one round forward -
pr
to move one round backward -
go
to move forward until convergence
All those commands are defined in ../../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 ../../test/my-rdbg-tuning.ml file -
ring.dot
: the topology -
p.ml
: the algo used inring.dot
-
Makefile
: demonstrate various ways of usingsasa
make rdbg
This rule
- generates the
p.cmxs
andp.cma
files, resulting from the compilation ofp.ml
(the makefile rules are in../Makefile.inc
). - generates a
ring.lut
file (out ofring.dot
andp.cmxs
) that defines various Lutin demons - launch
rdbg
with some arguments.rdbg
then prompts the user to enter some commands.
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/...]:
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
../../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
../../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.
rdbg
[0] #use "rdbg-session.ml"
[c] create a fresh session
[q] quit
[s] do nothing
[0/s/q/c/1/2/...]:
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 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 Gitlab CI
script.
Via opam (not yet working)
opam repo add verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam update -y
opam install -y sasa
Once this is done, upgrading to the last version of the tools is as simple as:
opam update
opam upgrade
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
):
opam depext -y rdbg lutin
opam install -y rdbg lutin
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