Oracle checking of sasa simulations using Lustre and Lurette
- to check, during batch simulations, that Algorithms expected properties are not violated
- such expected properties can be formalized in Lustre
- to reach a step that satisfy some (violated) property from
rdbg
We suppose you have already read the /articles/sasa-daemons/ tutorial.
Download and compile an example
Let’s first download a sasa self-stabilizing algorithm (if you
haven’t already done this clone) that solves graph coloring problems
(test/coloring/), and compile it as described in in
this post:
[ -d "sasa" ] || git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git
cd sasa/test/coloring
make grid4.dot
make grid4.cmxs
Add an oracle
lurette is a black-box testing tools of reactive programs that automates:
- the test decision (test oracle)
- the generation of sequences of inputs that takes into account the feedback loop
In this tutorial, we focus on oracles. If we launch sasa using
one of the pre-defined internal daemons (i.e., if we do not use the
--custom-daemon option) on the coloring algorithm (that do not have
input other than the values that come from node neighbors in
the graph), no input is needed, and this algorithm can be
simulated without any other tools.
sasa grid4.dot --locally-central-daemon
It can also be simulated under the control of lurette
lurette -o lurette-grid4.rif -sut "sasa ring.dot --locally-central-daemon"
Indeed, as we use an internal daemon, no input is needed, and so no
environment needs to be provided. The advantage of using lurette
here is that it allows one to add a test oracle. For lurette, an
oracle should be a reactive program written in Lustre, Lutin, or any
programs able to read/write its input/output on stdin/stderr using the
RIF conventions. The oracle first output must be a
Boolean that holds the property one wants to check. The oracle inputs
have access to all the System Under Test (SUT) inputs and outputs.
Here, the SUT is a sasa simulation that has no input, and that
outputs, for each process:
- its local state values
- a Boolean per action stating if the action is enabled
- a Boolean per action stating if the action is triggered
Hence, the oracle interface does not only depend on the algorithm state definition, but also on the topology. In order to write properties that do not depend on the topology, you can take advantage of:
- the
sasaoracle skeleton generator (usingsasa --gen-lustre-oracle-skeleton, orsasa -glosfor the close friends) - the Lustre V6 static parameters
Generate a Lustre V6 oracle skeleton
The call to
sasa -glos grid4.dot
generates the grid4_oracle.lus Lustre program (if not already
existing in the current directory):
|
|
Lines 5 to 16 define some constants relative to the graph, that may be useful to define properties. For instance, some properties may depend on the graph diameter (Line 11), or on the number of nodes (Line 7).
Lines 17 to 33 define the adjacency matrix of the graph (adjacency[p][q] ⇔ p is a neighbor of q).
Lines 36-38 contain the node inputs declaration:
- Line 36: local state variables (one per process)
- Line 37: variables stating if the action is enabled (there is only one actions named “conflict” in this algorithm)
- Line 38: variables stating if the action is triggered
Lines 40-45 pack the enabled and the triggered variables into 2 matrices, which dimensions correspond to:
- the number of actions per processes (
an, which is bound to1on Line 6) - the number of processes (
pn, which is bound to16on Line 7)
Finally, on Line 47, the oracle output is defined using a node named
coloring_oracle. This node is defined by users in a file named
coloring_oracle.lus, that is included on Line 5, and that ought to
be written by someone.
Defining a generic property
So you need to define a Lustre node that has in input 2 matrices of size an × pn. To help you, several Lustre nodes are available in the test/lustre/oracle_utils.lus file that provides nodes that:
- compute when a new round is reached
- compute (the step) when the algorithm becomes silent
- computes the daemon property (e.g., is it synchronous, distributed, etc.)
- and others
Here a Lustre oracle obtained from a formalization the theorem and
lemma given in the book ``Introduction to Distributed Self-Stabilizing
Algorithms”. Lemma 3.14 states that the execution terminates after at
most n-1 moves. By using nodes defined in
test/lustre/oracle_utils.lus that counts the number of
moves (move_count) and the step when the algorithm becomes silent
(silent), defining a Lustre version of this lemma is straightforward
(Ditto for Theorem 3.17 using the round and the count nodes). Cf
lustre tutorials to learn more about this language.
include "../lustre/oracle_utils.lus"
-----------------------------------------------------------------------------
-- Lemma 3.14 The execution terminates after at most n-1 moves
-- (under a Locally Central daemon).
node lemma_3_14<<const an:int; const pn: int>> (Enab, Acti: bool^an^pn)
returns (res:bool);
var
MoveNb:int;
Silent:bool;
let
MoveNb = move_count(Acti);
Silent = silent<<an,pn>>(Enab);
res = Silent => (MoveNb) <= pn-1;
tel
-----------------------------------------------------------------------------
-- Theorem 3.17 The stabilization time of Color is at most one round
-- (under a Locally Central daemon).
node theorem_3_17<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
returns (res:bool; RoundNb:int);
var
Round:bool;
-- RoundNb:int;
let
Round = round <<an,pn>>(Enab,Acti);
RoundNb = count(Round);
res = RoundNb <= 1; -- from theorem 3.17 page 29
tel
node coloring_oracle<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
returns (res:bool);
var res0:bool; RoundNb:int;
let
res0, RoundNb = theorem_3_17<<an,pn>>(Enab,Acti);
res = res0 and lemma_3_14<<an,pn>>(Enab,Acti);
tel
node test=coloring_oracle<< 5,2 >>
Once this node is defined, we can use lurette to run a simulation using this oracle:
make grid4_oracle.lus
lurette -o lurette-grid4.rif \
-sut "sasa grid4.dot -rif --locally-central-daemon" \
-oracle "lv6 grid4_oracle.lus -n oracle"
What to do when an oracle is violated?
When an oracle is violated (i.e., when the first output of the oracle
becomes false), it might be useful to run an interactive session to
better understand what’s going on. To do that, one just need to
replace lurette by rdbg as follows:
ledit rdbg --sasa -o rdbg-grid4.rif \
-sut "sasa grid4.dot -rif --locally-central-daemon " \
-oracle "lv6 grid4_oracle.lus -n oracle -exec"
nb: the call to ledit (a standalone wrapper for line-based interactive programs available in most distributions), is optional.
The use of sasa under the control of rdbg is described in this post.
Other examples
Note that this work of expected Algorithms property formalization and
checking has been done for all examples in the test directory of the
sasa git repository. Via the Makefile present is each of those
directories, one can run such simulation under the control of
lurette or rdbg.