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.
legitimate
(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:
!e.data;;
(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)]
(rdbg)
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)
in
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 "")
;;
legitimate
(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