Algo
A SASA process is an instance of an algorithm defined via this module.
In order to define a SASA algorithm, one need to provide an enable and a step function:
The enable and the step functions should be of the type 's enable_fun
and 's step_fun
respectively.
enable_fun
and step_fun
have the same arguments in input:
's
), algorithms designers can put anything they need into this state (an integer, a structure, etc.). The only constraint is that all algorithms should use the same type.state
, reply
, and weight
functions below).enable_fun
returns the list of enable actions.
step_fun
, which also takes an action in input, returns the new value of the local state resulting from the execution of the action.
The initial value of the local state can be set using an initialization function that takes as input 2 arguments: the number of node neighbors, and the pid. Anonymous algorithms are not supposed to use the pid.
Let the user define what the potential of a configuration is. Used to explore best/worst case daemons (e.g., --greedy-daemon, or --exhaustive-daemon)
By default, legitimate configurations (i.e., global states) are silent ones. But this is not true for all algorithms. Predicates of this type are used to redefine what's a legitimate configuration is.
The fault function is called on each node to update their state each time a legitimate configuration is reached. It takes 3 arguments: the number of node neighbors, the pid, and the value of the current state.
val state : 's neighbor -> 's
Returns the neighbor processes local state
val reply : 's neighbor -> int
Returns the neighbor channel number, that let this neighbor access to the content of the current process, if its neighbor can access it. The channel number is the rank, starting at 0, in the neighbors' list, which are sorted alphabetically. Returns -1 if the neighbor can not access to the process, which may happen in directed graphs.
An algorithm that uses reply, and not the pid, is called semi-anonymous. It is called anonymous if it can access none.
val weight : 's neighbor -> int
Returns the weight of the edge from the current node to the neighbor. Note that "weight" is an edge (dot) attribute. 1 is returned if not weight is set in the graph.
val print_neighbor : 's neighbor -> unit
For debugging
val fmt_print_neighbor : Stdlib.Format.formatter -> 's neighbor -> unit
When writing algorithms, one can also have access to topological information (i.e., information that are relative to the graph)
an in-tree is a _directed_ tree where all nodes have at most one _predecessor_
an out-tree is a _directed_ tree where all nodes have at most one _successor_
A rooted tree in a tree where one vertex is distinguished.
By convention, sasa considers a tree to be rooted if exactly one node id contains the string "root" or "Root".
The following 4 functions only work on rooted trees
maps each node to the channel number of its parent, and to None for the tree root.
returns true
iff is_tree
returns true
, and exactly one node name contains the string "root" or "Root"
It is possible to set some global parameters in the dot file using graph attributes. This function allows one the get their values. Throws an error if the attribute doesn't exist.
Get the value of a graph attribute. Returns None if the attribute doesn't exist.
Finding bad initial states
The --init-search sasa performs a local search for finding the worst possible initial configuration. More precisely, it mutates the initial configuration and observes (by simulation) if this mutated leads to a longer path to a legitimate configuration.
In order to perform this mutation, the user needs to provide functions to translate (local) state 's
to/from list of value
s. Each value
also holds the minimum and the maximum value it could have after a mutation.
Note that it is not necessary to expose the whole state to the optimization process. To do that, one just needs to filter some of the state value in the 's -> value list
function. This is the reason the state reconstruction function (value list -> 's -> 's
) takes a state as argument (to be able to fill the previously filtered values, that will therefore never change during the search).
The register: 's to_register -> unit
function must be called once in the user code.
type 's algo_to_register = {
algo_id : string;
init_state : 's state_init_fun;
enab : 's enable_fun;
step : 's step_fun;
}
type 's to_register = {
algo : 's algo_to_register list;
state_to_string : 's -> string;
state_of_string : (string -> 's) option;
copy_state : 's -> 's;
actions : action list;
Mandatory in custom daemon mode, or to use oracles
*)legitimate_function : 's legitimate_fun option;
fault_function : 's fault_fun option;
called at legitimate configuration
*)potential_function : 's potential_fun option;
Mandatory with Evil daemons
*)init_search_utils : 's state_to_values_fun option;
for sasa --init-search
*)}
state_to_string
field, the idea is to print the raw values contained in 's
. If a value is omitted, one won't see it in the simulation outputs. If one prepend a value with "some_id", some_id will we used in the simulation outputs. Otherwise, an id will be invented by sasa.state_of_string
field, if some function is provided, sasa should be able to parse state init values in the dot.val register : 's to_register -> unit
To be called once
Once enable and step functions are defined, they need to be registered by calling the register function.
An alternative to writing this registration code is to let sasa generate it with the "--gen-register" (or "-reg") option. In this case, one needs to follow some naming conventions (w.r.t file and function names):
(1) The internal state (i.e. the 's shared by all algos) should be defined in a file named "state.ml" that defines the following 5 entities:
type t = define_me
let (to_string: t -> string) = fun _ -> "define_me"
let (of_string: string -> t option) = fun _ -> None
let (copy : t -> t) = fun x -> x
let actions = ["action1";"action2"];
If one does not want/need to provide the of_string state parser, returning None is fine. This is mandatory only if one wants to define initial values in the dot file.
Defining a copy that is not the identity is necessary if the state is opaque (e.g., if it contains an array or an Hashtbl).
In the file "state.ml" does not exist in the current directory, a skeleton is generated.
(2) The optional functions relative to the global configuration should be defined in a file named "config.ml" that defines the following 5 entities:
let potential_function = None (** Mandatory with --worst-daemon (-wd) *);
let legitimate_function = None (** if different from silent ones *);
let fault_function = None (** called when a legitimate configuration is
reached *)
(3) All the algos mentioned in the dot file should define the following functions:
let (init_state: int -> string -> State.t) = xxx finishme
let (enable_f: State.t neighbor list -> State.t -> action list) = xxx
let (step_f : State.t neighbor list -> State.t -> action -> State.t) = xxx