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 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.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 sasa oracle skeleton generator (using sasa --gen-lustre-oracle-skeleton, or sasa -glos for 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):

 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 1 on Line 6)
  • the number of processes (pn, which is bound to 16 on 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 -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.