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:

  1. a topology, made of nodes and transitions (via a dot file)
  2. 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

  1. follow the graphviz/dot format
  2. 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.

nb : sasa uses ml files, and salut lustre files. Therefore the extension used in this algo field is actually ignored by tools. Then sasa will remove the extension, and add an .ml one, while salut will add a .lus one.

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

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.

  1. test/skeleton/: a fake algorithm meant to be used as a skeleton
  2. test/dijkstra-ring/: Dijkstra token ring
  3. test/unison/: Synchronous unison
  4. test/coloring/: a graph coloring algorithm
  5. test/alea-coloring/: a randomized variant of the previous one
  6. test/bfs-spanning-tree/: a Breadth First Search Spanning tree construction

It also contains implementations of algorithms found in the literature:

  1. test/async-unison/: Asynchronous unison ("Asynchronous unison" by Couvreur, J., Francez, N., and Gouda, M. G. in 1992)
  2. test/st-CYH91: another Spanning tree construction ("A self-stabilizing algorithm for constructing spanning trees" by Chen, Yu, and Huang in 1991)
  3. test/bfs-st-HC92: another BFS Spanning tree construction ("A self-stabilizing algorithm for constructing breadth-first trees" by Huang and Chen in 1992)
  4. test/st-KK06_algo1 and test/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)
  5. 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)
  6. test/dfs-list/: the same Depth First Search, but using lists instead or arrays
  7. test/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 directory 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, uo can have a look at the test/*/Makefile files, present in each directory (which all include the test/Makefile.incand the test/Makefile.dot ones).

The test directory also contains sub-directories which gather programs shared by all examples:

  • test/lustre/: contains Lustre programs used as (test/*/*.lus) oracles
  • test/rdbg-utils/: contains ocaml functions that can be used from rdbg

5 Batch

Sorry, your browser does not support SVG.

5.1 TL;DR

In order to run an algorithm, e.g., the coloring algorithm, on a 5x5 grid topology, do:

cd test/coloring
make grid5.dot  # actually optional; the command below would generate it
make grid5.cmxs
sasa grid5.dot

5.2 Running batch simulations

Once you have defined your algorithm and your topology, you can launch batch simulations with the sasa CLI (Command Line Interface). To do that, one needs to:

  1. write or generate some registration (Ocaml) code
  2. 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, and
  • config.ml which contains optional function definitions, such as the legitimate 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

But all of these commands can actually be automated with make and dune:

make ring.cxms

If you have created a fresh directory from scratch, do not forget to copy (or sym-sink) the Makefile* and the dune* files that are in one of the test/*/* directories.

Hence, to sum-up, to simulate the coloring algorithm on 5x5 grid:

 cd test/coloring # from the sasa git repository
 make grid5.cmxs   # generate and compile all necessary files
 sasa grid5.dot    # launch a simulation

nb: the simulation output (in the green frame) follows the RIF conventions.

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

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.

5.5 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.6 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.7 The sasa CLI

  sasa --help
usage: sasa [<option>]* <topology>.dot 
use -h to see the available options.

--length, -l <int>
            Maximum number of steps to be done (10000 by default).

--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-daemon, -gd
            Use the daemon that maximizes the potential function at each step.
            Performs 2^|enabled| trials (per step). 
--greedy-central-daemon, -gcd
            Ditto, but restricted to central daemons. Performs |enabled| trials.
--exhaustive-daemon, -ed
            Use the daemon that maximizes the number of steps. 
            The search is stopped when the maximum number of steps has been reached 
            (which is controlled by the -l/--length option)
--exhaustive-central-daemon, -ecd
            Ditto, but for central daemons
--local-init-search, -is <int>
            Use local search algorithms to find an initial configuration that pessimize 
            the step number. The argument is the maximum number of trials to do the search. 
            Require the state_to_nums Algo.to_register field to be defined.
--global-init-search, -gis <int>
            Use global (i.e., completely random)  search to find an initial configuration 
            that pessimize the step number. The argument is the maximum number of trials
             to do the search. 
--cores-nb, -cn
            Number of cores to use during --init-search simulations (default is 1)
--outfile, -o
            Generate simulation data in a file (use stdout otherwise)
--seed, -seed <int>
            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
--version, -version, -v
            Display the sasa version and exit.
--quiet, -q Set the quiet mode
--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 Print only outputs (i.e., behave as a rif input file)
--no-data-file, -nd
            Do not print any data
--gen-lutin-daemon, -gld
            Generate Lutin daemons and exit (not finished)
--gen-lustre-oracle-skeleton, -glos
            Generate a Lustre oracle skeleton
--list-algos, -algo
            Output the algo files used in the dot file and exit. 
--gen-register, -reg
            Generates the registering files 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 simulations

In order to run interactive simulations, one can run sasa under the control of rdbgui4sasa. More specifically, instead of running

sasa ring4.dot

you run

rdbgui4sasa -sut "sasa ring4.dot"

The name rdbgui4sasa comes from the fact that is it GUI designed for sasa, that is built on top of rdbg, but you don't need to know rdbg to use rdbgui4sasa.

The -sut option stands for "System Under Test". This terminology comes from the fact that rdbg is an extension of lurette, which is an automated testing tool.

All the CLI options of sasa can be used when invoking rdbgui4sasa.

rdbgui4sasa -sut "sasa ring4.dot [any valid sasa option]*"

Using rdbgui4sasa ought to be intuitive. It first asks if you want to re-use a previous session, or create a fresh one.

Enter one of the following key (the first is the default one):
 [] create a fresh session
 [q] quit

By default, the first choice in the list ([]) is executed if you just press <Return>. The first time rdbgui4sasa in invoked, no session is available and thus if you press <Return>, a fresh session is created – and of course, if you press q, you will quit (more precisely it creates a .rdbg-session.ml file, that loads all the necessary modules to run an interactive session with rdbg, and stores the command-line arguments you invoked rdbgui4sasa with).

Then of course, the next time you launch rdbgui4sasa (with or without arguments), you will be prompted with the possibility to reuse this first session:

rdbgui4sasa
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

Another convenient way of launching rdbgui4sasa is by taking advantage of some of the generic Makefile rules available in test/Makefile.dot and test/Makefile.inc (that are included in all the test/*/Makefile of the git repo):

make ring10.rdbgui

which is a shortcut for

make ring10.dot
make ring10.cmxs
rdbgui4sasa -sut "sasa ring10.dot"

For more information: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/articles/rdbgui4sasa/

7 Install

7.1 Install sasa via opam: TL;DR

On debian-based distributions, open a terminal and copy/paste (on other Linux (or mac) distributions, the packages names should be more or less the same):

## Fisrt you need to install opam
sudo apt install -y  opam
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.14.1
eval $(opam env)
opam install -y merlin tuareg
opam user-setup install

Once opam is installed:

opam repo add -a verimag-sync-repo "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam update -y
opam install -y sasa rdbgui4sasa

# optionally (to perform automated tests):
opam depext  -y lutin || echo "useless with opam >= 2.1"
opam install -y lutin lustre-v6

For running examples in the sasa/test/ directory of the git repo to check the installation has worked:

git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa/test/
make test

7.2 Install sasa via opam (long version)

Follows more or less the same instructions as above, but described into more details in case you want to understand the rationale for each command and adapt it to your distribution.

As using sasa requires to 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 -y opam
opam init -y
eval $(opam env)

The opam init ought to have populated your shell resource file with the necessary configurations commands, but it case it didn't you can run something like:

echo "eval $(opam env)" >> ~/.bashrc

Once opam is installed and configured, you may want to install (or not) the last version of the compiler.

opam switch create 4.14.1
eval $(opam env)
echo "eval $(opam env)" >> ~/.bashrc

Then, you need to add the verimag-sync-repo into your set of opam's repository:

opam repo add -a verimag-sync-repo \
  "http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/opam-repository"
opam update -y

Now you should be able to install sasa:

opam install -y sasa

as well as the rdbgui4sasa Graphical User Interface:

(opam depext -y rdbgui4sasa || echo "useless since opam 2.1") && opam install -y rdbgui4sasa

If you want to be able to use the automated test framework, you can also install the following packages:

opam install -y lustre-v6
(opam depext -y lutin  || echo "useless since opam 2.1") && opam install -y lutin

Then, if one day you want to upgrade your sasa version:

opam update
opam upgrade

7.2.1 Not strictly mandatory, but useful, third-party software

In order to perform interactive simulations, you need to install a pdf viewer that is able to auto-refresh (for instance zathura):

sudo apt install zathura

You also need an editor, for instance 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 "export LUSTRE_INSTALL=~/lv4/lustre-v4-III-e-linux64" >> ~/.bashrc # if you are using bash
echo  "export PATH=$LUSTRE_INSTALL/bin:$PATH"  >> ~/.bashrc
sudo apt install -y wish

For more information: http://www-verimag.imag.fr/DIST-TOOLS/SYNCHRONE/lustre-v4/distrib/index.html

7.3 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 --deps-only ./sasa.opam

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.4 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.5 Use sasa via a Virtual Machine

8 Screencasts

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

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

Author: Erwan Jahier

Created: 2023-02-27 Mon 16:19

Validate