Model-checking ASM algorithms with salut

salut is a tool that translates a .dot file into a Lustre program. The dot file ought to be made of nodes that refers to (via nodes algo attributes) a Lustre file that defines the ASM guard (the enable node) and actions (the step node) of the algorithm. More examples can be found in the git repository: salut/test/

The objective of this tutorial is to show how one can use salut to check algorithms properties using the Dijkstra token algorithm as an example.

Preliminaries

Let’s clone the sasa git repository (if needed) and go to the salut/test/dijkstra-ring/ directory.

[ -d "sasa" ] || git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa/salut/test/dijkstra-ring

This directory contains several (symbolic links to) Ocaml files that you can ignore for now. It also contains some Makefiles files that eases the generation of topologies and the compilation what whatever needs to be compiled. Let’s use them to generate a directed ring of 4 nodes.

Generate a topology

make diring4.dot
cat  diring4.dot

digraph diring4 {
graph []
  p0 [algo="root.ml"]
  p1 [algo="p.ml"]
  p2 [algo="p.ml"]
  p3 [algo="p.ml"]

  p0 -> p1
  p1 -> p2
  p2 -> p3
  p3 -> p0
}

The salut/test/dijkstra-ring/Makefile is written in such a way that .ml files are used in the algo nodes attributes. Actually, the file extension is ignored by salut, and if an p.ml file is set, salut will search for a p.lus file1.

Define ASM algorithms in Lustre (V6)

salut diring4.dot

will generate 2 Lustre files: diring4.lus and diring4_const.lus. If you look at diring4.lus, you may notice that it

  • includes 3 Lustre files: p.lus, root.lus, and state.lus
  • uses 4 undefined nodes: p_enable, p_step, root_enable, root_step.

The idea is to define those 4 nodes into those 3 files. Here is a possible way to implement the dijkstra algorithm in Lustre:

Two directories contains Lustre (v6) files that can be used to implement the algorithms:

  • salut/test/lib/ that contains utils to define Lustre/salut ASM algos
  • test/lustre/ that contains utils to define test oracles of Ocaml/sasa ASM algos that may also be useful

Other examples can be found here: salut/test/

Simulate Lustre-based ASM Algorithms

The rdbgui4sasa GUI (presented here) can be used to perform interactive step-by-step simulations:

make diring4.simu

Confront the Lustre implementation against the ocaml one

If the directory <dir> you have defined your Lustre-based algorithm contains:

  • a <dir>_oracle.lus that defines a <dir>_oracle node that returns a Boolean
  • an ocaml/sasa version of it (e.g., via symbolic link)

then the Makefiles that are provided allows

make diring4.lurette

to confront the behavior of the Lustre and the Ocaml implementations.

Automatic verification with kind2

Once simulations have shown that the algorithm (or its encoding) seems to behave correctly, it’s time to try to model-check algorithms properties. To do that, we will use the kind2 model-checker (that you need to install, ask google).

salut generates Lustre V6 constructs that kind2 does not support, but the lv6 compiler is able to generate kind2-compatible Lustre.

This process, plus a few other transformations, is automated via a small bash script, salut/test/run-kind2.sh.

../run-kind2.sh

usage:
  ../run-kind2.sh topology n [[[[property] [daemon]] [int]] [solver]]

where:
  - topology is one of graph supported by gg (ring, diring, grid, etc.)
  - n is the size of the topology [1]
  - property is one of the verify node variable (in verify.lus) (ok by default)
  - daemon is in {synchronous,distributed,central,locally_central}  (distributed by default)
  - int is in {int, int8, uint8, int16, uint16, ..., uinit64} [2] (int by default)
  - solver is in {Z3, Bitwuzla, cvc5, MathSAT, Yices, Yices2} [3] (Bitwuzla by default)

example of use (that are equivalent because of the default values):
  ../run-kind2.sh diring 5
  ../run-kind2.sh diring 5 ok
  ../run-kind2.sh diring 5 ok distributed
  ../run-kind2.sh diring 5 ok distributed int8
  ../run-kind2.sh diring 5 ok distributed int8 Bitwuzla

nb: '\''../run-kind2.sh file_name_unknown_to_gg 5'\'' works if '\''file_name_unknown_to_gg5.dot'\'' exists

[1] except for grids, where the size of the topology is n*n
[2] int means natural numbers (infinite)
  uint8  : 0 to 255
  uint16 : 0 to 65535
  uint32 : 0 to 4294967295
  uint64 : 0 to 18446744073709551615
  int8   : -128 to 127
  int16  : -32768 to 32767
  int32  : -2147483648 to 2147483647
  int64  : -9223372036854775808 to 9223372036854775807
[3] cf kind2 documentation
'
+ [[ 0 < 2 ]]
+ printf 'This script calls kind2 to model-check the algoritm of the current dir
(meant to be run from one of the salut/test/*/ directories).

usage:
  ../run-kind2.sh topology n [[[[property] [daemon]] [int]] [solver]]

where:
  - topology is one of graph supported by gg (ring, diring, grid, etc.)
  - n is the size of the topology [1]
  - property is one of the verify node variable (in verify.lus) (ok by default)
  - daemon is in {synchronous,distributed,central,locally_central}  (distributed by default)
  - int is in {int, int8, uint8, int16, uint16, ..., uinit64} [2] (int by default)
  - solver is in {Z3, Bitwuzla, cvc5, MathSAT, Yices, Yices2} [3] (Bitwuzla by default)

example of use (that are equivalent because of the default values):
  ../run-kind2.sh diring 5
  ../run-kind2.sh diring 5 ok
  ../run-kind2.sh diring 5 ok distributed
  ../run-kind2.sh diring 5 ok distributed int8
  ../run-kind2.sh diring 5 ok distributed int8 Bitwuzla

nb: '\''../run-kind2.sh file_name_unknown_to_gg 5'\'' works if '\''file_name_unknown_to_gg5.dot'\'' exists

[1] except for grids, where the size of the topology is n*n
[2] int means natural numbers (infinite)
  uint8  : 0 to 255
  uint16 : 0 to 65535
  uint32 : 0 to 4294967295
  uint64 : 0 to 18446744073709551615
  int8   : -128 to 127
  int16  : -32768 to 32767
  int32  : -2147483648 to 2147483647
  int64  : -9223372036854775808 to 9223372036854775807
[3] cf kind2 documentation
'
This script calls kind2 to model-check the algoritm of the current dir
(meant to be run from one of the salut/test/*/ directories).

usage:
  ../run-kind2.sh topology n [[[[property] [daemon]] [int]] [solver]]

where:
  - topology is one of graph supported by gg (ring, diring, grid, etc.)
  - n is the size of the topology [1]
  - property is one of the verify node variable (in verify.lus) (ok by default)
  - daemon is in {synchronous,distributed,central,locally_central}  (distributed by default)
  - int is in {int, int8, uint8, int16, uint16, ..., uinit64} [2] (int by default)
  - solver is in {Z3, Bitwuzla, cvc5, MathSAT, Yices, Yices2} [3] (Bitwuzla by default)

example of use (that are equivalent because of the default values):
  ../run-kind2.sh diring 5
  ../run-kind2.sh diring 5 ok
  ../run-kind2.sh diring 5 ok distributed
  ../run-kind2.sh diring 5 ok distributed int8
  ../run-kind2.sh diring 5 ok distributed int8 Bitwuzla

nb: '../run-kind2.sh file_name_unknown_to_gg 5' works if 'file_name_unknown_to_gg5.dot' exists

[1] except for grids, where the size of the topology is n*n
[2] int means natural numbers (infinite)
  uint8  : 0 to 255
  uint16 : 0 to 65535
  uint32 : 0 to 4294967295
  uint64 : 0 to 18446744073709551615
  int8   : -128 to 127
  int16  : -32768 to 32767
  int32  : -2147483648 to 2147483647
  int64  : -9223372036854775808 to 9223372036854775807
[3] cf kind2 documentation

This script (like the Makefile) takes advantage of naming conventions: the algorithm properties should defined in a Boolean local variable or a Boolean output of a node named verify in a file named verify.lus.

Since, the node verify in salut/test/dijkstra-ring/verify.lus defines the Booleans ok, closure, and converge_wc, you can ask kind2 to prove that those variables are always true under a distributed daemon:

  ../run-kind2.sh diring 4 converge_wc distributed int Z3
  ../run-kind2.sh diring 4 closure int Z3
  ../run-kind2.sh diring 4 ok int Z3

If your algorithm uses integers between 0 and 255 (which is the case for the Dijkstra algorithm on a directed ring of size 4), you can use uint8 machine integers.

  ../run-kind2.sh diring 4 converge_wc distributed uint8 Z3

If you algorithm state is only made of Boolean and finite integers, kind2 will bit-blast them and provide to the SMT solver a purely Boolean problem. For those kinds of problems, the Bitwuzla SAT solver is much efficient (on the examples we have tried so far), and can be used (if installed, as google) as follows:

  ../run-kind2.sh diring 4 converge_wc distributed uint8 Bitwuzla

The converge_wc property actually states that once the worst_case of steps have been performed, the configuration is necessarily legitimate:

converge_wc = (steps >= worst_case) => legitimate;

The verify node also define a Boolean named wc_is_tigth:

wc_is_tigth = (steps >= worst_case - 1) => legitimate;

This allows use to prove that this worst-case is tight indeed!

  ../run-kind2.sh diring 4 wc_is_tigth distributed int Z3

 kind2 v1.9.0
 [...]
<Failure> Property InvProp[l921c1] is invalid by bounded model checking for k=12 after 0.375s.

Counterexample:
  Node round__verify ()
 [...]

  == Inputs ==
active_0_0          F T F F F T F F F T F  F  F
active_1_0          F F F F T F F F T F F  F  T
active_2_0          F F F T F F F T F F F  T  F
active_3_0          F F T F F F T F F F T  F  F
== Locals ==
steps               0 1 2 3 4 5 6 7 8 9 10 11 12
config_0            0 1 1 1 1 2 2 2 2 3 3  3  3
config_1            2 2 2 2 1 1 1 1 2 2 2  2  3
config_2            1 1 1 2 2 2 2 1 1 1 1  2  2
config_3            0 0 1 1 1 1 2 2 2 2 1  1  1
wc_is_tigth T T T T T T T T T T T  T  F
 [...]
InvProp[l921c1]: invalid after 12 steps
  1. the rationale is to be able to use the same .dot file with either sasa (that needs ocaml programs) and salut (that needs Lustre program) [return]