SASA: a SimulAtor of Self-stabilizing Algorithms
Table of Contents
1 TL;DR
SASA is a Self-stabilizing Algorithms SimulAtor, based on the so-called Atomic State model (ASM) introduced by Dijkstra in its seminal article on Self-stabilizing distributed algorithms. This model is also sometimes named "locally shared memory model with composite atomicity"
Basically, one needs to provide:
- a topology, made of nodes and transitions (via a dot file)
- the algorithms attached to nodes (via
ocaml
programs)
The fastest way to get started is to copy the files provided in the
test/skeleton
directory, and to modify them:
cd test cp -rf skeleton my_algo # copy a simple example cd my_algo # one may want to edit "p.ml" and "ring.dot" make ring.cmxs # compile anything that needs to be compiled sasa ring.dot -l 4 # run a batch simulation for 4 steps
2 Topology
The topology is given via .dot
files, that should
- follow the graphviz/dot format
- have nodes labeled 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 and contains an algorithm.
In order to define an initial configuration, one can use the init
node attribute.
graph ring { p1 [algo="some_algo.ml" init="i=1"] p2 [algo="some_algo.ml" init="i=2"] p3 [algo="some_algo.ml" init="i=42"] 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 }
One can use graph attributes to set parameters that can be used by all nodes during the simulation.
graph ring { graph [diameter="4" some_other_global_parameter="42"] p1 [algo="some_algo.ml" init="i=1"] p2 [algo="some_algo.ml" init="i=2"] p3 [algo="some_algo.ml" init="i=42"] 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 }
Such parameters can be retrieved in algorithms using the
Algo.get_graph_attribute : string -> string
function. For example,
if you know the graph diameter, you can define it as a graph
attribute (a Algo.diameter: unit -> int
function is provided, but
it can be expensive to use for large graphs).
Some tools are provided in the sasa
distributions to generate such
kinds of dot
graphs:
https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-gg/
3 Algorithms
The following has been generated from algo.mli
<iframe title="The Algo API" name="algo-api" width="700" height="700" src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/algo/Algo/index.html" alt="html/algo/Algo/index.html";> </iframe>
4 Examples
git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa/test
The test directory contains various examples of self-stabilizing distributed programs taken from the book ``Introduction to Distributed Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
test/skeleton/
: a fake algorithm meant to be used as a skeletontest/dijkstra-ring/
: Dijkstra token ringtest/unison/
: Synchronous unisontest/async-unison/
: Asynchronous unisontest/coloring/
: a graph coloring algorithmtest/alea-coloring/
: a randomized variant of the previous onetest/bfs-spanning-tree/
: a Breadth First Search Spanning tree construction
It also contains implementations of algorithms found in the literature:
test/st-CYH91
: another Spanning tree construction ("A self-stabilizing algorithm for constructing spanning trees" by Chen, Yu, and Huang in 1991)test/bfs-st-HC92
: another BFS Spanning tree construction ("A self-stabilizing algorithm for constructing breadth-first trees" by Huang and Chen in 1992)test/st-KK06_algo1
andtest/st-KK06_algo2
: another Spanning tree construction ("A Self-stabilizing Algorithm for Finding a Spanning Tree in a Polynomial Number of Moves" by Kosowski and Kuszner, 2006)test/dfs/
: a Depth First Search using arrays (the ``atomic state model'' version of a Depth First Search algorithm proposed by Collin and Dolev in 1994)test/dfs-list/
: the same Depth First Search, but using lists instead or arraystest/rsp-tree/
: The Algorithm 1 of "Self-Stabilizing Disconnected Components Detection and Rooted Shortest-Path Tree Maintenance in Polynomial Steps" by Stéphane Devismes, David Ilcinkas, Colette Johnen.
Each directories contains working examples, which are checked using the Continuous Integration facilities of Gitlab (cf the .gitlab-ci.yml script and the CI pipelines results).
If you want to reproduce or understand what those non-regression tests
do, please look at the test/*/Makefile
, present in each directory
(which all include the test/Makefile.inc one).
The test
directory also contains sub-directories which gathers
programs shared by all examples:
test/lustre/
: contains Lustre programs used as (test/*/*.lus
) oraclestest/rdbg-utils/
: containsocaml
functions that can be used fromrdbg
test/my-rdbg-tuning.ml
: contains useful shortcuts/commands that can be used fromrdbg
.test/*/my-rdbg-tuning.ml
: includestest/my-rdbg-tuning.ml
and defines commands specific to the example of the directory. Indeed,rdbg
, once launched, first tries to read the content of the file namemy-rdbg-tuning.ml
(if it exists).
5 Batch mode
5.1 Running batch simulations
Once you have defined your algorithm and your topology, you can launch
batch simulations with the sasa
Command Line Interface. To
do that, one needs to:
- write or generate some registration (Ocaml) code
- compile the Ocaml programs.
The easiest way to get registration code is to let sasa
generate it.
cd test/coloring sasa -reg ring.dot
This command will generate the ring.ml
file, that contains the
registration code. It will also generate, if they do not already
exist, 2 other (skeleton) files:
state.ml
which contains types and functions definition related to algorithm states, andconfig.ml
which contains optional function definitions, such as thelegitimate
function that allows one to define what a legitimate configuration is (but we'll come to that later).
The ring.ml
file refers to state.ml
, config.ml
, and p.ml
;
p.ml
needs the definitions in state.ml
; moreover, definitions in
p.ml
can be used useful in config.ml
. We need to take those
dependencies into account to compile those files and generate the
.cmxs
file (that should be named according to the topology file
name).
ocamlfind ocamlopt -shared -package algo state.ml p.ml config.ml ring.ml -o ring.cmxs
Now we are ready to launch our first batch simulation:
sasa ring.dot
All the CLI commands above can be run automatically using a make
rule
contained in test/Makefile.inc. Hence, by including this file the
Makefile
of the current directory (cf test/coloring/Makefile), one
can generate the ring.cmxs
file straightforwardly:
cd test/coloring # from the sasa git repository make ring.cmxs # compile what's need to be compiled sasa ring.dot # launch the simulation
nb: the simulation output (in the green frame) follows the RIF conventions.
5.2 Running batch simulations with Built-in daemons
By default, the distributed daemon is used to activate enabled actions. Several other daemons can be used, via one of the following options:
sasa -h | grep "\-daemon"
--synchronous-daemon, -sd --central-daemon, -cd --locally-central-daemon, -lcd --distributed-daemon, -dd --custom-daemon, -custd --greedy-central-daemon, -gcd --greedy-daemon, -gd
5.3 Running batch simulations with manual (a.k.a. custom) daemons
By using the --custom-daemon
option (or -custd
for short), you can
play the role of the daemon. More precisely, you will be prompted for
stating which actions should be activated, among the set of enabled
actions.
cd test/unison make ring.cmxs echo " # here we provide input in batch via echo, but it can be done interactively t t t t t t t # Active all the processes for the first step f f f f f f t # Active only p7 at the second step q # and then quit " | sasa ring.dot --custom-daemon
sasa -reg ring.dot ocamlfind ocamlopt -package algo -shared state.ml unison.ml config.ml ring.ml -o ring.cmxs #inputs "p1_g":bool "p2_g":bool "p3_g":bool "p4_g":bool "p5_g":bool "p6_g":bool "p7_g":bool #outputs "p1_c":int "p2_c":int "p3_c":int "p4_c":int "p5_c":int "p6_c":int "p7_c":int "Enab_p1_g":bool "Enab_p2_g":bool "Enab_p3_g":bool "Enab_p4_g":bool "Enab_p5_g":bool "Enab_p6_g":bool "Enab_p7_g":bool 2 2 5 1 3 3 4 t t t t t t t 3 3 2 2 2 4 3 t f t t t t t 3 3 2 2 2 4 4 t f t t t t f
In the custom daemon mode, the daemon 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 daemon can thus be played by users that read and enter Boolean
values. In the example above, the user has played t t t t t t t
,
i.e., it has asked to trigger all the processes (which were all
activated at the first step). At the second step, only the process p2
is
not activated. In the session above we have chosen to activate only p7
.
In order to enter such input more easily, one can use (requires the lustre V4 tool box):
luciole-rif
luciole-rif sasa ring.dot --custom-daemon
Daemons can also by simulated by lutin
programs via the use of
lurette
(for batch executions) or rdbg
(for interactive sessions).
5.4 Running batch simulations with lurette
If one wants to use a test oracle to check at runtime some
algorithms properties, one can use lurette
as follows:
cd test/coloring make ring.cmxs lurette -sut "sasa ring.dot" -oracle "lv6 ring_oracle.lus -n oracle -exec"
Here the oracle is specified in Lustre V6. For more information on this topic: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-oracles/
lurette
can also be used to perform simulations with programmed
daemons. For instance, in order to simulate an algorithm defined in
ring.dot
(cf test/coloring) using a Lutin daemon defined in
ring.lut
, you can launch the following:
lurette -env "sasa ring.dot -custd" -sut "lutin ring.lut -n distributed"
Note that for lurette
, the role of the SUT (System Under Test) and
the one of the environment is dual: the outputs of the SUT are the
inputs of the environment, and vice-versa. The only difference is
that the environment plays first. But sasa
needs to play first, to
be able to state which actions are enabled at the very first step.
Hence sasa
is used as a lurette
environment, and the daemon
program is used a lurette
SUT.
For more information on this topic: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/sasa-daemons/
5.5 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/reactive-toolbox/
5.6 The sasa
CLI
sasa --help
usage: sasa [<option>]* <topology>.dot use -h to see the available options. --synchronous-daemon, -sd Use a Synchronous daemon --central-daemon, -cd Use a Central daemon (selects exactly one action) --locally-central-daemon, -lcd Use a Locally Central daemon (i.e., never activates two neighbors actions in the same step) --distributed-daemon, -dd Use a Distributed daemon (which select at least one action). This is the default daemon. --custom-daemon, -custd Use a Custom daemon (forces --rif) --greedy-central-daemon, -gcd Use the central daemon that maximizes the potential function for the next step (greedy). Performs |enabled| trials) --greedy-daemon, -gd Use the daemon that maximizes the potential function for the next step (greedy). Performs 2^|enabled| trials) --seed, -seed Set the pseudo-random generator seed of build-in daemons (wins over --replay) --replay, -replay Use the last generated seed to replay the last run --gen-register, -reg Generates the registering file and exit. --length, -l <int> Maximum number of steps to be done (10000 by default). --version, -version, -v Display the sasa version and exit. --verbose, -vl <int> Set the verbose level --help, -help, -h Display main options --more, -m Display more options
More sasa
options:
sasa --more
--rif, -rif Display only outputs on stdout (i.e., behave as a rif input file) --no-data-file, -nd Do not generate any data file --gen-lutin-daemon, -gld Generate Lutin daemons and exit --gen-lustre-oracle-skeleton, -glos Generate a Lustre oracle skeleton --list-algos, -algo Output the algo files used in the dot file and exit. --dummy-input Add a dummy input to sasa so that built-in daemon can be used from rdbg --ignore-first-inputs, -ifi [Deprecated] make sasa ignore its first input vector --ocaml-version Display the version ocaml version sasa was compiled with and exit.
6 Interactive mode
If you want to perform step-by-step simulations, you can use
the -custd
option. But if you want to perform step-by-step
simulations without the burden of playing the role of the daemon, you
can launch sasa
under the control of rdbg.
Another advantage of rdbg is its ability to display a graphical view of the current configuration during the simulation, to move step by step, or round by round, forward or backwards.
cf https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbg-sasa/
Before reading this section, please read at least the Basic usage Section if the rdbg documentation.
6.1 Example: use rdbg
from the test/alea-coloring/
directory
All the sub-directories of the test
directory are organized similarly.
Let's have a look at the test/alea-coloring/
directory.
It contains the following files:
my-rdbg-tuning.ml
that just includes test/my-rdbg-tuning.ml (somemy-rdbg-tuning.ml
files define more commands, such as the one in test/async-unison/my-rdbg-tuning.ml).ring.dot
: a possible topologyp.ml
: an algorithm used inring.dot
Makefile
: a Makefile that daemonstrates various ways of usingsasa
. In particular, it contains a rule namedrdbg
.
Try for instance:
cd test/coloring
make rdbg
This make rule (defined in Makefile
and ../Makefile.inc
)
- generates the
ring.ml
file, that contains the registration code (that can indeed be generated by sasa, as explained inalgo.mli
). - launches
rdbg
with some arguments (rdbg -o ring.rif -sut "sasa ring.dot --locally-central-daemon"
).rdbg
then prompts the user to enter one of the following commands:
Enter one of the following key (the first is the default one): [] create a fresh session [q] quit
By default, the first in the list is executed; hence if you press
[Return]
without any command, a fresh session is created. More precisely
it creates a rdbg_session.ml
file, that loads all
the necessary modules to run an interactive session with rdbg
,
where rdbg
simulates ring.dot with sasa
using a locally
distributed daemon.
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 (without argument), you will
be prompted with the possibility to reuse this session.
rdbg
Enter one of the following key (the first is the default one): [] #use "rdbg-session.ml" (2/11/2020: rdbg -o ring.rif -sut sasa ring.d[...]) [c] create a fresh session [q] quit
6.2 The examples of test directory
The test directory contains several files and directories
that take advantage of the versatility (programmability) of
rdbg
to perform interactive sasa
simulations:
test/rdbg-utils/
: containsocaml
functions that can be used fromrdbg
test/my-rdbg-tuning.ml
: contains useful shortcuts/commands that can be used fromrdbg
.test/*/my-rdbg-tuning.ml
: includestest/my-rdbg-tuning.ml
and defines commands specific to the example of the directory. Indeed,rdbg
, once launched, first tries to read the content of the file namemy-rdbg-tuning.ml
(it it exists).
6.3 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 forwardsd
to move one step forward and calld
(to update the graph display [])nr
to move one round forwardpr
to move one round backwardgo
to move forward until convergence
All those commands are defined in (the common)
test/my-rdbg-tuning.ml that is included in (locals)
test/*/my-rdbg-tuning.ml
that are included in (generated)
test/*/rdbg-session.ml
files. my-rdbg-tuning.ml
contains
straigthforward ocaml
code that defines various rdbg
shortcuts to
ease the simulation of sasa
systems. Feel free to tailor those
command to yours needs by modyfying the local my-rdbg-tuning.ml
!
6.4 Getting rdbg
on-line help
Here are 2 useful entry-points to rdbg on-line help:
rdbg --help
and- at the
rdbg
prompt, you can use thel
command:
(rdbg) l
Here is the list of rdbg Level 0 commands (i.e., defined in rdbg-cmds.ml) : - forward moves: n: Moves forward of one event ni i: Moves forward of i events s: Moves forward of one step si i: Moves forward of n steps nm <string>: Moves forward until an event which name matches a <string> fc pred:Moves forward until a predicate (of type unit -> bool) becomes true exit: Goes to the exit of the current event - backward moves: b: Moves backward of one event bi i: Moves backward of i events g i: Goes to event number i pm <string>: Moves backward until a function which name matches a <string> - Call graphs (requires GraphViz dot) cg: Generates the call graph from the current event cgf: Generates the full call graph recursively (i.e., nodes are clickable) dcg: Displays the generated call graph - Breakpoints: break <brpt>: Adds a breakpoint on a node or a file. A breakpoint is a string of the form: "node" "node@line" "file" "file@line" c: Continues forward until the next breakpoint cb: Continues backward until the previous breakpoint blist: Lists of the current breakpoints delete: Removes all breakpoints - misc: where: Prints the call stack with source information sinfo: Returns source information attached to the current event (if available) vv: Returns the value of a variable attached to the current event (if available) - main: l: Prints this list of L0 commands description i: A Shortcut for info r: Restarts to the first event u: Undo the last move q: Quits rdbg a: A Shortcut for apropos h: A Shortcut for help - sasa commands + Display network with GraphViz tools d: update the current network with dot ne: update the current network with neato tw: update the current network with twopi ci: update the current network with circo fd: update the current network with fdp sf: update the current network with sfdp pa: update the current network with patchwork os: update the current network with osage nb: for algorithms that have a field named 'par', you can try of the following (which only draw the parent arcs) d_par: update the current network with dot (parent arcs only) ne_par: update the current network with neato (parent arcs only) tw_par: update the current network with twopi (parent arcs only) ci_par: update the current network with circo (parent arcs only) fd_par: update the current network with fdp (parent arcs only) sf_par: update the current network with sfdp (parent arcs only) pa_par: update the current network with patchwork (parent arcs only) os_par: update the current network with osage (parent arcs only) + Moving commands [*] sd: go to the next step and update the network with one of the GraphViz tools nd: go to the next event and update the network bd: go to the previous event and update the network nr: go to the next round and update the network pr: go to the previous round and update the network [*] in order to change the current graph drawing engine, you can use the dot_view command as follows: dot_view := ci (rdbg)
6.5 A rdbg
sasa
GUI
To install it:
opam depext -y rdbgui4ocaml opam install -y rdbgui4ocaml
To use it: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/
6.6 Useful Modules
Some modules, used by the sasa core engine, can be useful from rdbg
.
<iframe title="The Topology API" name="topology-api" width="700" height="500" src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/sasacore/Sasacore/Topology/index.html" alt="./_html/sasacore/Sasacore/Topology/index.html";> </iframe>
<iframe title="The Diameter API" name="diameter-api" width="700" height="300" src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/sasacore/Sasacore/Diameter/index.html" alt="./_html/sasacore/Sasacore/Diameter/index.html";> </iframe>
<iframe title="The Process API" width="700" height="300" src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/sasacore/Sasacore/Process/index.html" alt="./_html/sasacore/Sasacore/Process/index.html";> </iframe>
<iframe title="The StringOf API" width="700" height="300" src="https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/_html/sasacore/Sasacore/StringOf/index.html" alt="./_html/sasacore/Sasacore/StringOf/index.html";> </iframe>
7 Install
7.1 TL;DR
On debian-based distributions, open a terminal and copy/paste:
sudo apt install -y zathura graphviz emacs opam
On other Linux (or mac) distributions, the packages names should be more or less the same.
Then:
opam init -y eval $(opam env) echo "test -r ~/.opam/opam-init/init.sh && . ~/.opam/opam-init/init.sh > /dev/null 2> /dev/null || true" >> ~/.bashrc opam switch create 4.11.1 eval $(opam env) opam install -y merlin tuareg opam user-setup install opam repo add -a verimag-sync-repo \ "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository" opam update -y opam install -y sasa
And optionally (to define test oracles in Lustre or daemons in Lutin):
opam depext -y rdbgui4sasa lutin opam install -y rdbgui4sasa lutin lustre-v6
and optionally too (for luciole
, a gtk-based UI useful to play daemon manually):
mkdir ~/lv4 # for example cd ~/lv4 wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz tar xvzf lustre-v4-III-e-linux64.tgz echo "LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash echo "PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc sudo apt install -y wish
and finally (for running examples in the sasa/test/
directory):
git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
7.2 Not strictly mandatory, but useful, third-party software
In order to perform interactive simulations, you need to install the
graphviz tools suite and a pdf viewer that is able to auto-refresh
(for instance zathura
). E.g., on debian-based distribution:
sudo apt install zathura graphviz
Moreover, as you will write Ocaml programs, you definitely need to
install the ocaml package manager opam. opam
works out of the box
with most Linux distributions and OSX (mac). opam
ought to work on
windows too.
sudo apt install opam opam init opam switch create 4.11.1 eval $(opam env) echo "eval $(opam env)" >> ~/.bashrc
You also need an editor. We advice emacs
with merlin
and tuareg
.
sudo apt install emacs opam install -y merlin tuareg opam user-setup install -y
In order to be able to use luciole
(a small GUI useful to
interactively play the role of the daemon using gtk buttons) you can
also install the Lustre V4 distribution. On linux:
mkdir ~/lv4 # for example cd ~/lv4 wget http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/linux64/lustre-v4-III-e-linux64.tgz tar xvzf lustre-v4-III-e-linux64.tgz echo "LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash echo "PATH=$LUSTRE_INSTALL/bin:$PATH" >> ~/.bashrc sudo apt install -y wish
Otherwise: http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html
7.3 Install sasa
via opam (version >= 2.*)
Once opam (version >= 2.*!) is installed and configured (see above),
you can install sasa
as follows:
opam repo add -a verimag-sync-repo \ "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository" opam update -y opam install -y sasa
If you want to use the rdbgui4sasa
Graphical User Interface:
opam depext -y rdbgui4sasa && opam install -y rdbgui4sasa
If you want to be able to defined daemons in Lutin, or test oracles in Lustre, you can also install the corresponding packages packages.
opam install -y lustre-v6 opam depext -y lutin && opam install -y lutin
Once this is done, upgrading to the last version of sasa
is as
simple as:
opam update opam upgrade
7.4 Install sasa
via git
You will need:
make
(gnu)git
graphviz
lablgtk3
opam
For instance, on ubuntu,
apt install graphviz git make lablgtk3 opam
And of course you need ocaml
.
And a set of tools installable via opam
dune
ocamlgraph
rdbg
lutin
(not for compiling actually, but for using sasa with custom daemons)
Hence, once opam
is installed, one just need to:
opam install dune ocamlgraph ocamlfind rdbg lutin lustre-v6
And then:
git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa
make
make install
make test
One can also mimic the content of the test
job in the project
.gitlab-ci.yml Gitlab CI script.
7.5 Use sasa
via docker
cf the Docker Install section of the Synchrone Reactive Tool Box.
This docker image contains all the tools mentioned in this section
(sasa
, lustre
, opam
, ocaml
, emacs, graphviz, etc.).
7.6 Use sasa
via a Virtual Machine
https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/sasaVM.ova
- login:sasa
- passwd:sasa
8 Screencasts
- a SASA tutorial given at SSS'2020 (Symposium on Stabilization, Safety, and Security of Distributed Systems)
- Installing sasa:
- Create a xubuntu 20.4 VM: 2 minutes video (20 min of real time)
- Clone that VM and install sasa via opam 2:39 minutes video (37 min of real time)
- Sasa demos (done on the VM build above, which is available here:
- demo 1: write and execute an algo (Dijkstra ring) first-demo.avi
- demo 2: re-define what a legitimate configuration is (Dijkstra ring) legitimate-demo.avi
cf http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/sasa/screencasts/
9 More
10 FAQ
10.1 Is there a FAQ?
Yes.
Beside, some tutorials are also available here: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/
10.2 I have a compilation error that I don't understand
- Look at recent
.log
files (e.g.,rdbg.log
); they sometimes contain more information than what is printed onto the screen. - Do a
make clean
- Read carefully the error message. Sometimes it helps.
- If the message is totally useless, please feel free to add an issue here https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa/issues
10.3 I have the error Invalid_argument("compare: functional value")
Most probably you a try to compare 2 's Algo.neighbor
. It's an
abstract type, hence you cannot compare them, i.e., you cannot use
Stdlib.compare
, nor its twins (<>
, >
, <
, etc.), nor functions that
use them (min
, max
, List.sort
, etc.). You should compare their
pid
instead (if the network is not anonymous).