Skip to content
Snippets Groups Projects
README.org 13.14 KiB

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:

  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:

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

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

  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:

  • 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

  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 ../../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 in ring.dot
  • Makefile: demonstrate various ways of using sasa
make rdbg

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