A Framework for Certified Self-Stabilization
PADEC Coq Library

• Feb 2016 - updated April 2018

Global imports

Local imports

Distributed Algorithm:

In this section we provide the main definitions of

• Channels
• Network
• Algorithm
  Usage: prove a specification of a distributed algorithm
  forall Channels,
  exists an Algorithm (the one to be proven) (uses Channels)
  forall Network using Channels,
  the Algorithm meets its specification
  defined on Network and Channels
  (provided some assumption on Network and Channels).

Class Channels:

Channels are used to model the access of a node to its neighbors. A channel (Type Channel) c connects a node n to its neighbor n': n --c--> n' The type Channel is endowed with a decidable equivalence relation (equiv, notation '==') to express equality between channels. Specifies the interface between an algorithm and a given network.

Class Network:

A network is described by its nodes (Type Node) and links between nodes. A link is defined through a channel from one node to another. The type Node is endowed with a decidable equivalence relation (equiv, notation '==') to express equality between nodes. Network is defined w.r.t given channels.

link: (link n n') is

• either None when n and n' are not neighbors
• either Some c when n --c--> n', i.e. n' is the neighbor of n through channel c.

peer: (peer n c) is

• either None when c is not a channel from n
• either Some n' when n --c--> n', i.e. n' is the neighbor of n through channel c.

is_channel: is_channel n c n' holds when n --c--> n'.

peer and link cover the same edges of the network

The number of nodes is finite: this is modeled using a (finite) list of nodes and with the predicate: every node is in this list.

From a node a given channel points to at most one node. Namely, each node has a local referential given by its outgoing channels

For a given network and a given node n, (peers n) is the list of outgoing channels from n

peers characterization using the function peer: every channel in (peer n) is actually a channel from n in the network

peers characterization using the function link

Symmetric Network: Bidirectionnal channels

reverse: if c is a channel outgoing from n, then (reverse n c) is the channel corresponding to c in the other direction

specification of reverse: n1 --c12--> n2 and n1 <--c21-- n2

reverse_spec': same as reverse_spec, maybe easier to use

reverse is "involutive" (using adequate parameters for nodes)

A symmetric network (as we defined it) allows no multi-edge

Note on compatibility: Let consider the above function f: Node -> A The assumption Proper fequiv f means that when taking to equivalent nodes n1 and n2, i.e., s.t. n1 == n2 (in this model, this means that n1 and n2 are equal and represent the same node in the network), we expect that (f n1) and (f n2) produce the same result. Again "same result" is expressed using relation: (f n1) == (f n2) when A is a setoid or (f n1) =~= (f n2) when A is a partial setoid. We say in this case that f is compatible (implicitely: f is compatible with respect to the (partial) equivalence relations on its parameter(s) and result). The explanation applies to hardly every function in PADEC (eg. peer, reverse and peers above).

Class Algorithm:

States are attached to nodes: an algorithm describes step by step the way the state of a node evolves. In the locally shared memory model, this evolution depends on the state itself but also on the state of neighbors of the node. The class Algorithm describes the algorithm of a node. It contains the type State (which should be endowed with a decidable equivalence relation to express equality), and the function run which is actually the local algorithm of the node. The function run has 2 parameters: the current state s of the node (let call it n) and a function sn from Channel to (option State). A call to run: run s sn For sn, we have the following convention (implemented in the semantics, see RelModel, function RUN): For a channel c, (sn c) provides the state of the neightbor pointed by c. Otherwise it is None. Now, if the node can access, from its current state, some of its outgoing channels c, it will be able to access to the states of the pointed neighbors using sn, and so to use their values in run. The call to run s sn returns a new state for node n. If this new state is actually different from s, then the node was enabled and did compute. Otherwise the run function has no effect and this means that either the node was disabled or that the statement of the algorithm has no effect.

Type State: state of a node

run: see above

Stable Variable

Some part of the state of the node cannot be changed by the algorithm, we call them stable or read-only variables. The class (Stable_Variable GetVar) expresses the fact that the part of the state (usually a projection) computed using GetVar is constant, i.e. cannot be changed using run; The type of the result of GetVar should be endowed with a partial equivalence relation that represents equality (stability). We also require GetVar to be compatible.

VarType: type of the projection

projection is compatible

GetVar projection is preserved by run

Networks

The signature of the run function assumes that the state of the node contains some information about the neighborhood and in particular some outgoing channels, to be able to use the second parameters that contains the neighbor states. In the following, we provide tools to check that the elements stored in the state of a node about the topology actually represents the network. See SubNetwork_assumption, Network_assumption and Symmetric_Network_assumption. Similar definition will be given for particular topologies (ring, tree...). We comment Network_assumption (others are similar): given a network, we check that the function tested_peers exactly contains the peers represented in the network. The idea is that, from a node and its state in the algorithm, if their exists a projection that represents the peers of the node then we can instantiate tested_peers using the result of the projection and check the assumption.

Subnetwork: inclusion of the peers

Network: same set of peers

Symmetric Networks:

• same set of peers
• for element in peers, same reverse channel

(i.e. for every outgoing channel, we check that they have the same reverse channel)

General network (without reverse) To ensure Network_Assumption, we assume ROState is built as follows Record ROState := mkROState { ... lpeers: list Channel }. and provide the function build_links that ensures Network_Assumption

triviality :)

Symmetric network (with reverse) To ensure Symmetric_Network_Assumption, we assume ROState is built as follows Record ROState := mkROState { ... lpeers_reverse: list (Channel * Channel); pr_assume: lpeers_reverse_assume lpeers_reverse }. and provide functions that build links and reverse links each peer has a unique reverse channel

• existence is ensured by construction (list)
• uniqueness is enforced by the following assumption: