About Legitimate Configurations in sasa Interactive Simulations

nb: now that a legitimate function had been added into the lib/algo/algo.mli API, defining it in rdbg is less useful. Nevertheless, this post is still interesting as it illustrates how new features can easily be added in during interactive simulations.

In this tutorial, we suppose that you are already familiar with interactive sasa simulations and that you are able to read straightforward ocaml programs.

Let’s first download an example from the git repository

If you haven’t already done this clone in previous vtt posts.

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

In the remaining of this tutorial, we suppose that you have launched an interactive session (for at most 1000 steps) with the test/unison algorithm under a synchronous daemon on a ring network.

rdbg --sasa -sut  "sasa -l 1000 ring.dot --synchronous-daemon"

The default behavior of the legitimate command

From rdbg, when using sasa, it is possible to move forward until a legitimate configuration is reached by using the legitimate command.

help legitimate

which outputs:

(rdbg) help legitimate
legitimate : unit -> unit [sasa] (sasa-rdbg-cmds.ml)
  Move forward until a legitimate configuration is reached (uses 'silence' by default)

As the online help hints, by default, a legitimate configuration is a silent one (i.e., when no node is enabled). Its also says that this command is defined in the test/sasa-rdbg-cmds.ml file. This file contains the definition of several rdbg commands that are meant to be used when running sasa simulations under the control of rdbg. You don’t need to read it to understand the following, but just note that it may be a source of inspiration if you wish to define your own commands.

But let’s come back to the topic. The legitimate command calls the silence command.

h silence
(rdbg) h silence
silence : unit -> unit [sasa] (sasa-rdbg-cmds.ml)
Move forward until is_silent returns true
h is_silent
(rdbg) h is_silent
is_silent : RdbgEvent.t -> bool [sasa] (sasa-rdbg-cmds.ml)
is the event correspond to a silent configuration? (i.e., no enable node)

This default behavior is suitable for the majority of self-stabilizing algorithms, but not all.

For example, consider the test/unison/unison.ml algorithm. A configuration is legitimate when all local clocks have the same value. But in such configurations, all nodes are enabled – to increment their local clock. This algorithm actually never becomes silent.

(rdbg) legitimate
Maximum step number reached
Terminating all processes
Exception: RdbgEvent.End 1001.

Redefining Legitimacy

Let’s overwrite the default legitimate function. The values of node states are available in the data field of the current event:

(rdbg) !e.data;;
- : Data.subst list =
[("p1_c", I 2); ("p2_c", I 2); ("p3_c", I 5); ("p4_c", I 1); ("p5_c", I 3);
 ("p6_c", I 3); ("p7_c", I 4); ("Enab_p1_g", B true); ("Enab_p2_g", B true);
 ("Enab_p3_g", B true); ("Enab_p4_g", B true); ("Enab_p5_g", B true);
 ("Enab_p6_g", B true); ("Enab_p7_g", B true); ("p1_g", B true);
 ("p2_g", B true); ("p3_g", B true); ("p4_g", B false); ("p5_g", B false);
 ("p6_g", B true); ("p7_g", B false)]

This list actually contains more information that we need: some variables concern the process status: enabled (e.g., Enab_p1_g states that node p1 is enabled) or active (p1_g states that node p1 is active), but we don’t care about them in this context. So let’s remove them from this list:

let get_states e =
  let is_state_var vname = String.sub vname ((String.length vname)-2 ) 2 = "_c" in
  List.partition (fun (n,v) -> is_state_var n) e.data ;;
let clocks = fst (get_states !e);;
(rdbg) let get_states e =
  let is_state_var vname = String.sub vname ((String.length vname)-2 ) 2 = "_c" in
  List.partition (fun (n,v) -> is_state_var n) e.data ;;
let clocks = fst (get_states !e);;
val clocks : Data.subst list =
  [("p1_c", I 2); ("p2_c", I 2); ("p3_c", I 5); ("p4_c", I 1); ("p5_c", I 3);
   ("p6_c", I 3); ("p7_c", I 4)]

the get_states function above splits the input list into:

  • variables which names end with “_c”
  • and the others

The code snippet above illustrates how to use this get_states function to compute a list of pairs (clocks) holding the clock names and their values for the current event (!e).

A configuration is legitimate if and only if all the values in this list are equals:

let is_legitimate e =
  let clocks = fst (get_states e) in (* fst returns the first  value of a pair *)
  let clk1 = snd (List.hd clocks) in (* snd returns the second value of a pair *)
  (* List.hd and List.tl resp. returns the head and the tail of a list *)
  List.for_all (fun (_,clk) -> clk=clk1) (List.tl clocks) ;;

So now that we have a predicate that states if an event corresponds to a legitimate configuration, we can redefine the legitimate command. rdbg moving commands are of type unit -> unit, and work by modifying the current event reference e.

let rec legitimate () =
   e := next !e;
   if is_legitimate !e then () else legitimate ();;

or equivalently, using the next_cond function (invoke help next, or help next_event if you don’t know what that functions do):

let legitimate () = e:= next_cond !e is_legitimate;;

If you want to count the number of rounds necessary to reach a legitimate configuration, you can also define legitimate as follows:

let legitimate () =
  let rec aux rn =
   e := next_round !e;
   if is_legitimate !e then rn else aux (rn+1)
  let rn = aux 1 in
  Printf.printf "A legitimate configuration has been reached after %i round%s\n%!" rn
    (if rn > 1 then "s" else "")
(rdbg) legitimate
Round 2 - Step 2
Active node states: p1_c=3 p3_c=2 p4_c=2 p5_c=2 p6_c=4 p7_c=3
Round 3 - Step 3
Active node states: p2_c=3 p3_c=3 p4_c=3 p5_c=3 p6_c=3
Round 4 - Step 4
Active node states: p1_c=4 p2_c=4 p3_c=4 p4_c=4 p5_c=4 p6_c=4 p7_c=4
A legitimate configuration has been reached after 3 rounds

Make this work Persistent across Sessions

When you are happy with your brand new legitimate definition, you can put it into the .my-rdbg-tuning.ml file, as it is loaded by rdbg at startup. Note that it is necessary to name it legitimate if you want it to used by the rdbgui4sasa GUI.

For another example of legitimate configuration tuning, cf