Module Algo

The Algorithm programming Interface

A SASA process is an instance of an algorithm defined via this module.

To be provided by users

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.

type 's neighbor
type action = string
type 's enable_fun = 's -> 's neighbor list -> action list
type 's step_fun = 's -> 's neighbor list -> action -> 's

enable_fun and step_fun have the same arguments in input:

  • The first argument holds the current state of the process. As it is polymorphic ('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.
  • The second argument holds the process neighbors it can read the state of (i.e., its predecessors in the graph). Note that SASA processes, that live in graph nodes, can only access to their immediate neighbors. From each neighbor, a process can access to various information (cf 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.

type 's state_init_fun = int -> string -> 's

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.

To be provided optionally

Potential function

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)

type pid = string
type 's potential_fun = pid list -> (pid -> 's * ('s neighbor * pid) list) -> float

Legitimate Configurations

type 's legitimate_fun = pid list -> (pid -> 's * ('s neighbor * pid) list) -> bool

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.

Fault Injection

type 's fault_fun = int -> string -> 's -> 's

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.

Can be used in algorithms

Process (local) Information

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

Topological Information

When writing algorithms, one can also have access to topological information (i.e., information that are relative to the graph)

val card : unit -> int
val min_degree : unit -> int
val mean_degree : unit -> float
val max_degree : unit -> int
val is_directed : unit -> bool
val is_cyclic : unit -> bool
val is_connected : unit -> bool
val diameter : unit -> int
val is_tree : unit -> bool

Trees

a tree is an a-cyclic and connected graph (directed or not)

val is_in_tree : unit -> bool

an in-tree is a _directed_ tree where all nodes have at most one _predecessor_

val is_out_tree : unit -> bool

an out-tree is a _directed_ tree where all nodes have at most one _successor_

Rooted Trees

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

val sub_tree_size : string -> int

maps each node to the size of the corresponding sub-tree

val height : string -> int

maps each node to its height in the tree

val level : string -> int

maps each node to its level in the tree

val parent : string -> int option

maps each node to the channel number of its parent, and to None for the tree root.

val is_rooted_tree : unit -> bool

returns true iff is_tree returns true, and exactly one node name contains the string "root" or "Root"

val get_graph_attribute : string -> string

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.

val get_graph_attribute_opt : string -> string option

Get the value of a graph attribute. Returns None if the attribute doesn't exist.

type value =
  1. | F of float * float * float
  2. | I of int * int * int
  3. | B of bool

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 values. 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).

type 's state_to_values_fun = ('s -> value list) * (value list -> 's -> 's)

Code Registration

The register: 's to_register -> unit function must be called once in the user code.

type 's algo_to_register = {
  1. algo_id : string;
  2. init_state : 's state_init_fun;
  3. enab : 's enable_fun;
  4. step : 's step_fun;
}
type 's to_register = {
  1. algo : 's algo_to_register list;
  2. state_to_string : 's -> string;
  3. state_of_string : (string -> 's) option;
  4. copy_state : 's -> 's;
  5. actions : action list;
    (*

    Mandatory in custom daemon mode, or to use oracles

    *)
  6. legitimate_function : 's legitimate_fun option;
  7. fault_function : 's fault_fun option;
    (*

    called at legitimate configuration

    *)
  8. potential_function : 's potential_fun option;
    (*

    Mandatory with Evil daemons

    *)
  9. init_search_utils : 's state_to_values_fun option;
    (*

    for sasa --init-search

    *)
}
  • For the 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.
  • For the 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

Automatic Code Registration

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