PADEC - Coq Library

Library Padec.MessagePassing.AlgorithmMPold

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016 - updated April 2018
Jan 2019 (Fork by David Ilcinkas for message-passing systems)

Global imports

From Coq Require Import SetoidList.
From Coq Require Import SetoidClass.

Local imports

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ListUtils.

Open Scope signature_scope.
Set Implicit Arguments.

Distributed Algorithm:

In this section we provide the main definitions of

Channels (In and Out)
Network
Algorithm

Usage: prove a specification of a distributed algorithm

forall InChannels, OutChannels,
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).

Section MP_Distributed_Algorithm.

Class Channels:

Channels are used to model the access of a node to its neighbors. An incoming channel (Type InChannel) cin connects a node n to its neighbor n': n <-cin---- n' An outgoing channel (Type OutChannel) cout connects a node n to its neighbor n': n -cout----> n'

The types *Channel are endowed with a decidable equivalence relation (equiv, notation '==') to express equality between *channels.

They specify the interface between an algorithm and a given network.

    Class InChannels :=
      mkInChannels {
          InChannel: Type;
          InChannel_setoid :> Setoid InChannel;
          InChannel_dec: Decider (equiv (A:=InChannel))
        }.
    Class OutChannels :=
      mkOutChannels {
          OutChannel: Type;
          OutChannel_setoid :> Setoid OutChannel;
          OutChannel_dec: Decider (equiv (A:=OutChannel))
        }.

Class Network:

A network is described by its nodes (Type Node) and links (arcs) between nodes. A directed connection is defined through two channels (one InChannel and one OutChannel) linking two nodes.

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.

  Class DirNetwork {InChans: InChannels} {OutChans: OutChannels} :=
    mkNet {

        Node: Type;
        Node_setoid :> Setoid Node;
        Node_dec: Decider (equiv (A := Node));

XLink: (XLink n n') is

either None when n' is not an X-neighbor of n;
either Some c when n ?-c----? n', i.e. n' is the X-neighbor of n through XChannel c, with X being either In or Out.

        inLink: Node * OutChannel -> option (Node * InChannel);
        outLink: Node * InChannel -> option (Node * OutChannel);

peer and link cover the same arcs of the network

        Link_spec: forall n1 n2 c1 c2,
            inLink (n1 ,c1 ) == Some (n2 ,c2 ) <-> outLink (n2 ,c2 ) == Some (n1 ,c1 );

        inLink_compat: Proper fequiv inLink;
        outLink_compat: Proper fequiv outLink;

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.

        all_nodes: list Node;
        all_nodes_prop: forall n, InA equiv n all_nodes;

The number of arcs is also finite: this is modeled using a (finite) list of incomming channels and with the predicate: every incoming channel is in this list.

all_inChannels: list InChannel; all_inChannels_prop: forall n1 cin n2 cout, is_InChannel n1 cin n2 -> InA equiv cin all_inChannels;

fromIntoOutChannel and fromOuttoInChannel are inverse of each other (first version)

For a given network and a given node n, (XPeers n) is the list of XChannels from n

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

Symmetric DirNetwork: Bidirectionnal channels

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.

  Class MPAlgorithm {InChans: InChannels} {OutChans: OutChannels} :=
    {

Type State: state of a node

      State: Type;
      State_setoid:> Setoid State;
      State_dec: Decider (equiv (A := State));

Type Msg: state of a message

      Msg: Type;
      Msg_setoid:> Setoid Msg;
      Msg_dec: Decider (equiv (A := Msg));

run: see above

      run: State -> option (InChannel * Msg) -> (State * (list (OutChannel *Msg)));

      run_compat :> Proper fequiv run;
    }.

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.

  Class Stable_Variable {InChans: InChannels} {OutChans: OutChannels}
        (Algo: MPAlgorithm) (VarType: Type) (GetVar: State -> VarType) :=
    {

VarType: type of the projection

VarType_setoid :> PartialSetoid VarType;

projection is compatible

GetVar_compat :> Proper fequiv GetVar;

GetVar projection is preserved by run

GetVar_stable: forall s lm, GetVar (fst (run s lm)) =~= GetVar s
}.

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

End MP_Distributed_Algorithm.

Unset Implicit Arguments.
Close Scope signature_scope.