Commit 9cb32320 authored by erwan's avatar erwan
Browse files

Fix: perform variable initiliasation once

Indeed, by using the Env.nset and Env.nget defined in
0d6575a7 a pb that was hided by the
use of Env.set and Env.get was triggered.

The bug was that variables initialisations were done several times.

In sasa.ml, the way I was updating the Env.t by iterating on the
variables was forcing to "close" expressions that were calling init
functions.
parent 14c733c0
(* Time-stamp: <modified the 05/06/2019 (at 17:23) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 16:32) by Erwan Jahier> *)
(** Process programmer API *)
type varT = It | Ft | Bt | Et of int | St | Nt | At of varT * int
......@@ -140,32 +140,40 @@ let (reg_init_vars : algo_id -> (neighbor list -> local_env) -> unit) =
flush stdout;
Hashtbl.replace tbls.init_vars algo_id x
let (get_init_vars : algo_id -> (string * varT) list ->
(neighbor list -> local_env)) =
fun algo_id vars ->
let default_env =
(fun nl v ->
match List.find_opt (fun (x,_t) -> x=v) vars with
None -> failwith (v^" unknown var")
| Some v -> init_var nl (snd v)
)
let (get_init_vars : algo_id -> (string * varT) list -> neighbor list -> local_env) =
fun algo_id vars nl ->
let lenv =
let default_env v =
match List.find_opt (fun (x,_t) -> x=v) vars with
None -> failwith (v^" unknown var")
| Some v -> init_var nl (snd v)
in
try
let user_env = Hashtbl.find tbls.init_vars algo_id in
(fun v ->
try user_env nl v
with e ->
if !verbose_level > 1 then
Printf.eprintf
"No init value for '%s' in user init function (%s).\n" v
(Printexc.to_string e);
default_env v)
with Not_found ->
if !verbose_level > 1 then
Printf.eprintf "No user init function is provided.\n";
default_env
in
try
let user_env = Hashtbl.find tbls.init_vars algo_id in
(fun nl v ->
try user_env nl v
with e ->
if !verbose_level > 1 then
Printf.eprintf
"No init value for '%s' in user init function (%s).\n" v
(Printexc.to_string e);
default_env nl v)
with Not_found ->
if !verbose_level > 1 then
Printf.eprintf "No user init function is provided.\n";
default_env
(* Make sure lenv is side-effect free (important for init variable
that are chosen at random) *)
let lassoc = List.map (fun (n,_) -> n,lenv n) vars in
let lenv v =
match List.assoc_opt v lassoc with
| None -> assert false
| Some value -> value
in
lenv
let (reg_enable : algo_id -> enable_fun -> unit) = fun algo_id x ->
if !verbose_level > 0 then Printf.printf "Registering %s enable\n" algo_id;
flush stdout;
......@@ -180,6 +188,7 @@ let (reg_step : algo_id -> step_fun -> unit) = fun algo_id x ->
if !verbose_level > 0 then Printf.printf "Registering %s step\n" algo_id;
flush stdout;
Hashtbl.replace tbls.step algo_id x
let (get_step : algo_id -> step_fun) = fun algo_id ->
try Hashtbl.find tbls.step algo_id
with Not_found ->
......
(* Time-stamp: <modified the 05/06/2019 (at 17:25) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 14:29) by Erwan Jahier> *)
(** Process programmer API *)
......@@ -79,6 +79,6 @@ val set_card : int -> unit
val get_vars : algo_id -> vars
val get_enable : algo_id -> enable_fun
val get_step : algo_id -> step_fun
val get_init_vars : algo_id -> (string * varT) list -> (neighbor list -> local_env)
val get_init_vars : algo_id -> (string * varT) list -> neighbor list -> local_env
val get_actions : algo_id -> action list
(* Time-stamp: <modified the 06/06/2019 (at 11:14) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 17:38) by Erwan Jahier> *)
module Dico = Map.Make(String)
open Algo
type t = local_env Dico.t
let (nget: t -> string -> Algo.local_env) =
fun e pid ->
Printf.printf "get pid %s\n" pid; flush stdout;
try ((Dico.find pid e) )
with Not_found -> failwith (Printf.sprintf "Unknown pid: %s" pid)
let (get: t -> string -> string -> value) =
let (get: t -> string -> Algo.local_env) =
fun e pid v ->
(* Printf.printf "get pid %s\n" pid; flush stdout; *)
try ((Dico.find pid e) v)
with _ -> failwith (Printf.sprintf "Unknown value: %s.%s" pid v)
with e ->
failwith (Printf.sprintf "Unknown value: %s.%s (%s)" pid v (Printexc.to_string e))
let (nget_copy: Algo.vars -> t -> string -> Algo.local_env) =
fun vars e pid ->
Algo.copy_local_env vars (get e pid)
let (get_copy: Algo.vars -> t -> string -> string -> value) =
let (get_copy: Algo.vars -> t -> string -> Algo.local_env) =
fun vars e pid ->
Algo.copy_local_env vars (get e pid)
let (nset: t -> string -> Algo.local_env -> t) =
let (set: t -> string -> Algo.local_env -> t) =
fun e pid lenv ->
Dico.add pid lenv e
let (set: t -> string -> string -> value -> t) =
fun e pid v value ->
Dico.add pid (fun x -> if x=v then value else Dico.find pid e x) e
let (init:unit -> t) = fun () -> Dico.empty
......@@ -4,16 +4,12 @@ type t
val init: unit -> t
(** [set env process_id var_name var_value] *)
val nset: t -> string -> Algo.local_env -> t
val set: t -> string -> string -> Algo.value -> t
val set: t -> string -> Algo.local_env -> t
(** [get env process_id var_name] *)
val nget: t -> string -> Algo.local_env
val get: t -> string -> string -> Algo.value
val get: t -> string -> Algo.local_env
(** In order to make sure that arrays ref are not shared between processes,
this function performs an array copy of the value (if it is an array)
*)
val nget_copy: Algo.vars -> t -> string -> Algo.local_env
val get_copy: Algo.vars -> t -> string -> string -> Algo.value
val get_copy: Algo.vars -> t -> string -> Algo.local_env
(* Time-stamp: <modified the 05/06/2019 (at 10:39) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 16:30) by Erwan Jahier> *)
type t = {
pid : string;
variables : Algo.vars;
actions: Algo.action list;
init : Algo.neighbor list -> Algo.local_env;
init : Algo.local_env;
enable : Algo.enable_fun;
step : Algo.step_fun ;
}
let (make: bool -> bool -> Topology.node -> t) =
fun dynlink custom_mode n ->
let (dynlink_nodes: string -> unit) =
fun ml ->
let id = Filename.chop_suffix ml ".ml" in
let cmxs = id^".cmxs" in
if !Algo.verbose_level > 0 then Printf.printf "Loading %s...\n" cmxs;
Dynlink.loadfile (Dynlink.adapt_filename cmxs)
let (make: bool -> Topology.node -> Algo.neighbor list -> t) =
fun custom_mode n nl ->
let pid = n.Topology.id in
let ml = n.Topology.file in
let id = Filename.chop_suffix ml ".ml" in
let cmxs = id^".cmxs" in
if !Algo.verbose_level > 0 then Printf.printf "Loading %s...\n" cmxs;
(* XXX TODO: should I prevent the same cmxs to be loaded twice? Not clear. *)
if dynlink then Dynlink.loadfile (Dynlink.adapt_filename cmxs);
let vars = Algo.get_vars id in
let user_init_env = Algo.get_init_vars id vars in
(* let (string_to_value: string -> Algo.value) = *)
let init_env nl v =
let user_init_env = user_init_env nl in
let init_env v =
match List.assoc_opt v n.Topology.init with
None ->
if !Algo.verbose_level > 1 then
Printf.eprintf "No init value for '%s' found in the graph.\n" v;
user_init_env nl v
user_init_env v
| Some x -> (
match List.assoc_opt v vars with
| Some(Algo.It)
......@@ -52,7 +59,7 @@ let (make: bool -> bool -> Topology.node -> t) =
let process = {
pid = pid;
variables = vars ;
init = (* user_init_env *) init_env ;
init = (* user_init_env *) init_env;
actions = actions;
enable = Algo.get_enable id;
step = Algo.get_step id;
......
(* Time-stamp: <modified the 30/04/2019 (at 16:02) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 16:23) by Erwan Jahier> *)
(** There is such a Process.t per node in the dot file. *)
type t = {
pid : string; (* unique *)
variables : Algo.vars;
actions: Algo.action list;
init : Algo.neighbor list -> Algo.local_env;
init : Algo.local_env;
enable : Algo.enable_fun;
step : Algo.step_fun;
}
(** [make dynlink_flag custom_mode_flag node] builds a process out of a dot
(* Dynamically link the algo_nodes.cmxs files (not possible from rdbg) *)
val dynlink_nodes: string -> unit
(** [make custom_mode_flag node] builds a process out of a dot
node. To do that, it retreives the registered functions by Dynamic
linking of the cmxs file specified in the "algo" field of the dot
node.
dynlink_flag: link the algo.cmxs files (not possible from rdbg)
nb: it provides variable initial values if not done in the dot
(via the init field) nor in the Algo (via Algo.reg_init_vars) *)
val make: bool -> bool -> Topology.node -> t
val make: bool -> Topology.node -> Algo.neighbor list -> t
(* Time-stamp: <modified the 06/06/2019 (at 11:20) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 17:37) by Erwan Jahier> *)
open Algo
open Sasacore
let (update_env_with_init : Env.t -> Process.t list -> Algo.neighbor list list
-> Env.t) =
fun e pl neighbors ->
let (aux: Env.t -> Process.t -> Algo.neighbor list -> Env.t) =
fun e p nl ->
Env.nset e p.pid (p.init nl)
(* List.fold_left
(fun e (n,_t) -> Env.set e p.pid n (p.init nl n))
e
p.variables *)
let (update_env_with_init : Env.t -> Process.t list -> Env.t) =
fun e pl ->
let (aux: Env.t -> Process.t -> Env.t) =
fun e p ->
Env.set e p.pid p.init
in
List.fold_left2 aux e pl neighbors
List.fold_left aux e pl
(** Returns the channel number that let [p_neighbor] access to the
content of [p], if [p] is a neighbor of [p_neighbor]. Returns -1 if
......@@ -29,9 +24,8 @@ let (reply: Topology.t -> string -> string -> int) =
in
f 0 (g.succ p_neighbor)
let (get_neighors: Topology.t -> Env.t -> Process.t -> Algo.neighbor list) =
fun g e p ->
let source_id = p.Process.pid in
let (get_neighors: Topology.t -> Env.t -> Topology.node_id -> Algo.neighbor list) =
fun g e source_id ->
let idl = g.succ source_id in
List.map
(fun neighbor_id ->
......@@ -57,7 +51,7 @@ let (dump_process: Process.t * Algo.neighbor list -> unit) =
(String.concat "\n\t\t" neighbors)
open Process
let string_of_local_env p lenv =
let _string_of_local_env p lenv =
List.fold_left
(fun acc (n,_) -> Printf.sprintf "%s %s=%s" acc n (Algo.value_to_string (lenv n)))
""
......@@ -65,17 +59,8 @@ let string_of_local_env p lenv =
let (update_env: Env.t -> Process.t * Algo.local_env -> Env.t) =
fun e (p, lenv) ->
Printf.printf "Env of %s: %s (size(lenv)=%i)\n" p.pid (string_of_local_env p lenv)
(Obj.size (Obj.repr e));
flush stdout;
(* Env.nset e p.pid lenv *)
Env.set e p.pid lenv
List.fold_left
(fun e (n,_) -> Env.set e p.pid n (lenv n))
e
p.variables
(* *)
open SasArg
let (update_neighbor_env: Env.t -> Algo.neighbor -> Algo.neighbor) =
......@@ -189,16 +174,19 @@ let (make : bool -> string array -> t) =
let dot_file = args.topo in
let g = Topology.read dot_file in
let nl = g.nodes in
let nstrl = List.map (fun n -> n.Topology.id) nl in
let nstr = String.concat "," nstrl in
let pidl = List.map (fun n -> n.Topology.id) nl in
let nstr = String.concat "," pidl in
Algo.set_card (List.length nl);
Algo.verbose_level := args.verbose;
Random.init args.seed;
if !Algo.verbose_level > 0 then Printf.eprintf "nodes: %s\nedges:\n" nstr;
let algo_files = List.map (fun n -> n.Topology.file) nl in
if dynlink then List.iter Process.dynlink_nodes (List.sort_uniq compare algo_files);
let e = Env.init () in
let pl = List.map (Process.make dynlink (args.demon=Custom)) nl in
let algo_neighors = List.map (get_neighors g e) pl in
let e = update_env_with_init e pl algo_neighors in
let algo_neighors = List.map (get_neighors g e) pidl in
let pl = List.map2 (Process.make (args.demon=Custom)) nl algo_neighors in
let e = update_env_with_init e pl in
let pl_n = List.combine pl algo_neighors in
if !Algo.verbose_level > 0 then List.iter dump_process pl_n;
if args.output_algos then (
......@@ -253,6 +241,6 @@ let (make : bool -> string array -> t) =
Printf.printf "Error: %s\n" (Dynlink.error_message e); flush stdout;
exit 2
| e ->
Printf.printf "Error: %s\n" (Printexc.to_string e);
flush stdout;
exit 2
Printf.printf "Error: %s\n" (Printexc.to_string e);
flush stdout;
exit 2
(* Time-stamp: <modified the 13/05/2019 (at 11:24) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 16:45) by Erwan Jahier> *)
open Graph
open Graph.Dot_ast
......@@ -10,7 +10,6 @@ type node = {
init: (string * string) list;
}
type edge = node_id * node_id list
type t = {
nodes: node list;
......
(* Time-stamp: <modified the 02/04/2019 (at 13:42) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 16:45) by Erwan Jahier> *)
type node_id = string
type node = {
......@@ -7,7 +7,6 @@ type node = {
init: (string * string) list; (* store the content of the init field *)
}
type edge = node_id * node_id list
type t = {
nodes: node list;
......
......@@ -56,7 +56,7 @@ let (from_sasa_env : Sasa.layout -> Env.t -> RdbgPlugin.sl) =
List.map
(fun (p,_nl) ->
List.map (fun (vn,_) ->
Printf.sprintf "%s_%s" p.pid vn, Env.nget e p.pid vn)
Printf.sprintf "%s_%s" p.pid vn, Env.get e p.pid vn)
p.variables)
p_nl_l
in
......@@ -136,9 +136,8 @@ let (make_do: string array -> SasArg.t ->
in
(* 3: Do the steps *)
let ne = Sasa.do_step pnal e in
let sasa_nenv = from_sasa_env pl_n e in
sasa_env := ne;
sasa_nenv @ (get_sl_out true pl enab_ll) @
(from_sasa_env pl_n e) @ (get_sl_out true pl enab_ll) @
(get_sl_out false pl activate_val)
in
let step = if args.demon = Demon.Custom then step else step_internal_demon in
......
- [Algos from the book](#orgec9e12f)
- [Depth First search](#org9b178aa)
- [rdbg](#org3ae5b4f)
<a id="orgec9e12f"></a>
# Algos from the book
This directory contains various examples of self-stabilizing distributed programs taken from the book \`\`Introduction to Distributed Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
- <bfs-spanning-tree> : Bread-first-search spanning tree
......@@ -5,11 +14,23 @@ This directory contains various examples of self-stabilizing distributed program
- <dijkstra-ring>: Dijkstra token ring
- <unison>:
It also contains an \`\`atomic state model'' version of a [Depth First Search algorithm proposed by Collin and Dolev in 1994 ](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf)
<a id="org9b178aa"></a>
# Depth First search
- <dfs>
contains an \`\`atomic state model'' version of a
[Depth First Search algorithm proposed by Collin and Dolev in 1994 ](http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf)
<http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf>
- <dfs>: Depth First search
<a id="org3ae5b4f"></a>
# rdbg
The following illustrate some possible use of `sasa` with `rdbg` on the examples above
......
* Algos from the book
This directory contains various examples of self-stabilizing
distributed programs taken from the book ``Introduction to Distributed
Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
......@@ -9,12 +11,17 @@ Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and Petit.
- file:dijkstra-ring: Dijkstra token ring
- file:unison:
It also contains an ``atomic state model'' version of a
* Depth First search
- file:dfs
contains an ``atomic state model'' version of a
[[http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf][Depth First Search algorithm proposed by Collin and Dolev in 1994 ]]
http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.57.1100&rep=rep1&type=pdf
- file:dfs: Depth First search
* rdbg
The following illustrate some possible use of =sasa= with =rdbg= on
the examples above
......
# Time-stamp: <modified the 23/05/2019 (at 16:18) by Erwan Jahier>
# Time-stamp: <modified the 07/06/2019 (at 17:16) by Erwan Jahier>
test: p.cmxs ring.lut
......@@ -13,15 +13,21 @@ gnuplot: ring.rif
gnuplot-rif $<
rdbg: p.cma ring.lut
rdbg: p.cma p.cmxs ring.lut
rdbg -o ring.rif \
-env "$(sasa) g.dot -cd"
-env "$(sasa) g.dot -dd"
rdbg2: p.cma ring.lut
rdbg -o ring.rif \
-env "$(sasa) ring.dot -custd -rif" \
-sut-nd "lutin ring.lut -n distributed"
rdbg3: p.cma g.lut
rdbg -o ring.rif \
-env "$(sasa) g.dot -custd" \
-sut-nd "lutin g.lut -n distributed"
lurette:cmxs ring.lut
lurette \
-env "$(sasa) ring.dot -custd " \
......
(* Time-stamp: <modified the 10/05/2019 (at 10:04) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 17:26) by Erwan Jahier> *)
(* This is algo 3.1 in the book *)
......@@ -11,13 +11,26 @@ let (init_vars: neighbor list -> local_env) =
fun _nl ->
function _ -> I (Random.int k)
let verbose = false
let (clash : neighbor list -> Algo.value list) = fun nl ->
let res = List.map (fun n -> n.lenv "c") nl in
let (neigbhors_values : neighbor list -> Algo.value list) =
fun nl ->
List.map (fun n -> n.lenv "c") nl
let (clash : Algo.value -> neighbor list -> bool) = fun v nl ->
let vnl = neigbhors_values nl in
let inl = List.map (fun n -> n.pid()) nl in
let res = List.mem v vnl in
if verbose then (
Printf.printf "%s %s in [%s] (%s)\n" (value_to_string v) (if res then "" else "not")
(String.concat "," (List.map value_to_string vnl))
(String.concat "," (inl));
flush stdout
);
res
let (free : neighbor list -> Algo.value list) = fun nl ->
let clash_list = List.sort_uniq compare (clash nl) in
let clash_list = List.sort_uniq compare (neigbhors_values nl) in
let rec aux free clash i =
if i > k then free else
(match clash with
......@@ -31,11 +44,14 @@ let (free : neighbor list -> Algo.value list) = fun nl ->
let (enable_f:neighbor list -> local_env -> action list) =
fun nl e ->
if List.mem (e "c") (clash nl) then ["conflict"] else []
if (clash (e "c") nl) then ["conflict"] else []
let (step_f : neighbor list -> local_env -> action -> local_env) =
fun nl e ->
function | _ -> (function "c" -> List.hd (free nl) | _ -> assert false)
fun nl e a ->
let f = free nl in
if f = [] then e else
match a with
| _ -> (function "c" -> List.hd f | _ -> assert false)
let () =
let algo_id = "p" in
......
# Time-stamp: <modified the 28/05/2019 (at 17:59) by Erwan Jahier>
# Time-stamp: <modified the 07/06/2019 (at 10:05) by Erwan Jahier>
test: cmxs
$(sasa) -l 30 ring.dot
$(sasa) ring.dot
cmxs: ring.cmxs ringroot.cmxs ring.cma ringroot.cma
sim2chrogtk: ring.rif
......
(* Time-stamp: <modified the 27/05/2019 (at 16:22) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 11:05) by Erwan Jahier> *)
open Algo
......@@ -15,10 +15,10 @@ let (enable_f:neighbor list -> local_env -> action list) =
if e "v" <> pred.lenv "v" then ["a"] else []
let (step_f : neighbor list -> local_env -> action -> local_env) =
fun nl e ->
function
fun nl e a ->
let pred = List.hd nl in
match a with
| _ ->
let pred = List.hd nl in
(function "v" -> pred.lenv "v" | _ -> assert false)
......
(* Time-stamp: <modified the 20/03/2019 (at 13:09) by Erwan Jahier> *)
(* Time-stamp: <modified the 07/06/2019 (at 11:06) by Erwan Jahier> *)
open Algo
......@@ -17,10 +17,10 @@ let (enable_f:neighbor list -> local_env -> action list) =
let i e v = match e v with I i -> i | _ -> failwith "type error"
let (step_f : neighbor list -> local_env -> action -> local_env) =
fun nl e ->
function
fun nl e a ->
let vv = i e "v" in
match a with
| _ ->
let vv = i e "v" in
(function "v" -> I ((vv +1) mod k) | _ -> assert false)
let () =
......
# Time-stamp: <modified the 04/04/2019 (at 21:10) by Erwan Jahier>
# Time-stamp: <modified the 07/06/2019 (at 17:36) by Erwan Jahier>
test: test1 test2 lurette0