Oracle checking of sasa simulations using Lustre and Lurette
This Tutorial shows how:
- 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
We suppose you have already read the /articles/sasa-daemons/ tutorial.
Download and compile an example
[ -d "sasa" ] || git clone https://gricad-gitlab.univ-grenoble-alpes.fr/verimag/synchrone/sasa.git cd sasa/test/coloring 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
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 -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
here is that it allows one to add a test oracle. For
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:
sasaoracle skeleton generator (using
sasa --gen-lustre-oracle-skeleton, or
sasa -glosfor the close friends)
- the Lustre V6 static parameters
Generate a Lustre V6 oracle skeleton
The call to
sasa -glos grid4.dot
grid4_oracle.lus Lustre program (if not already
existing in the current directory):
1-- Automatically generated by /home/jahier/.opam/4.09.0/bin/sasa version "2.14.15" ("716d608") 2-- on crevetete the 30/1/2020 at 17:27:15 3--sasa -glos grid4.dot 4 5include "coloring_oracle.lus" 6const an=1; -- actions number 7const pn=16; -- processes number 8const degree=4; 9const min_degree=2; 10const mean_degree=1.500000; 11const diameter=6; 12const card=16; 13const links_number=24; 14const is_cyclic=true; 15const is_connected=true; 16const is_a_tree=false; 17const adjacency=[ 18 [f,t,f,f,t,f,f,f,f,f,f,f,f,f,f,f], 19 [t,f,t,f,f,t,f,f,f,f,f,f,f,f,f,f], 20 [f,t,f,t,f,f,t,f,f,f,f,f,f,f,f,f], 21 [f,f,t,f,f,f,f,t,f,f,f,f,f,f,f,f], 22 [t,f,f,f,f,t,f,f,t,f,f,f,f,f,f,f], 23 [f,t,f,f,t,f,t,f,f,t,f,f,f,f,f,f], 24 [f,f,t,f,f,t,f,t,f,f,t,f,f,f,f,f], 25 [f,f,f,t,f,f,t,f,f,f,f,t,f,f,f,f], 26 [f,f,f,f,t,f,f,f,f,t,f,f,t,f,f,f], 27 [f,f,f,f,f,t,f,f,t,f,t,f,f,t,f,f], 28 [f,f,f,f,f,f,t,f,f,t,f,t,f,f,t,f], 29 [f,f,f,f,f,f,f,t,f,f,t,f,f,f,f,t], 30 [f,f,f,f,f,f,f,f,t,f,f,f,f,t,f,f], 31 [f,f,f,f,f,f,f,f,f,t,f,f,t,f,t,f], 32 [f,f,f,f,f,f,f,f,f,f,t,f,f,t,f,t], 33 [f,f,f,f,f,f,f,f,f,f,f,t,f,f,t,f]]; 34 35node oracle( 36 p0_c:int;p1_c:int;p2_c:int;p3_c:int;p4_c:int;p5_c:int;p6_c:int;p7_c:int;p8_c:int;p9_c:int;p10_c:int;p11_c:int;p12_c:int;p13_c:int;p14_c:int;p15_c:int 37 Enab_p0_conflict,Enab_p1_conflict,Enab_p2_conflict,Enab_p3_conflict,Enab_p4_conflict,Enab_p5_conflict,Enab_p6_conflict,Enab_p7_conflict,Enab_p8_conflict,Enab_p9_conflict,Enab_p10_conflict,Enab_p11_conflict,Enab_p12_conflict,Enab_p13_conflict,Enab_p14_conflict,Enab_p15_conflict:bool; 38 p0_conflict,p1_conflict,p2_conflict,p3_conflict,p4_conflict,p5_conflict,p6_conflict,p7_conflict,p8_conflict,p9_conflict,p10_conflict,p11_conflict,p12_conflict,p13_conflict,p14_conflict,p15_conflict:bool; 39returns (ok:bool); 40var 41 Acti:bool^an^pn; 42 Enab:bool^an^pn; 43let 44 Acti = [[p0_conflict],[p1_conflict],[p2_conflict],[p3_conflict],[p4_conflict],[p5_conflict],[p6_conflict],[p7_conflict],[p8_conflict],[p9_conflict],[p10_conflict],[p11_conflict],[p12_conflict],[p13_conflict],[p14_conflict],[p15_conflict]]; 45 Enab = [[Enab_p0_conflict],[Enab_p1_conflict],[Enab_p2_conflict],[Enab_p3_conflict],[Enab_p4_conflict],[Enab_p5_conflict],[Enab_p6_conflict],[Enab_p7_conflict],[Enab_p8_conflict],[Enab_p9_conflict],[Enab_p10_conflict],[Enab_p11_conflict],[Enab_p12_conflict],[Enab_p13_conflict],[Enab_p14_conflict],[Enab_p15_conflict]]; 46 47 ok = coloring_oracle<<an,pn>>(Enab,Acti); 48tel
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 to
1on Line 6)
- the number of processes (
pn, which is bound to
16on 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
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
rdbg as follows:
ledit rdbg -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.
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