SASA: a SimulAtor of Self-stabilizing Algorithms

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:

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

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.

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

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

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/

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/

  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.

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 (some my-rdbg-tuning.ml files define more commands, such as the one in test/async-unison/my-rdbg-tuning.ml).
• ring.dot: a possible topology
• p.ml: an algorithm used in ring.dot
• Makefile: a Makefile that daemonstrates various ways of using sasa. In particular, it contains a rule named rdbg.

Try for instance:

cd test/coloring
make rdbg

This make rule (defined in Makefile and ../Makefile.inc)

1. generates the ring.ml file, that contains the registration code (that can indeed be generated by sasa, as explained in algo.mli).
2. 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

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/: contains ocaml functions that can be used from rdbg
• test/my-rdbg-tuning.ml: contains useful shortcuts/commands that can be used from rdbg.
• test/*/my-rdbg-tuning.ml: includes test/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 name my-rdbg-tuning.ml (it it exists).

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 (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!

Here are 2 useful entry-points to rdbg on-line help:

1. rdbg --help and
2. at the rdbg prompt, you can use the l 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) 

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/

Some modules, used by the sasa core engine, can be useful from rdbg.

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

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

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

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.

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

https://verimag.gricad-pages.univ-grenoble-alpes.fr/synchrone/sasa/sasaVM.ova

• login:sasa
• passwd:sasa

Yes.

Beside, some tutorials are also available here: https://verimag.gricad-pages.univ-grenoble-alpes.fr/vtt/tags/sasa/

• 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

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