PADEC - Coq Library

Library Padec.MessagePassing.AlgorithmMP

A Framework for Certified Self-Stabilization
PADEC Coq Library

Jan 2019 (Description of the network and the algorithm)

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.

Classes *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 DirNetwork:

A network is described by its nodes (Type Node) and links (arcs) between nodes. A directed connection (arc) linking two nodes has two channels: one InChannel (at the destination) and one OutChannel (at the source).

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));

inLink: inLink (n,c) is

either None when c is not a outChannel from n
either Some (n',c') when n -c---c'-> n', i.e. n is linked to n' through an arc with outChannel c at n and inchannel c' at n'.

outLink is defined similarly.

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

inLink and outLink are inverse of each other

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

inLink and outLink are compatible

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

is_valid_dest checks whether the provided (dest : Node * InChannel) is an actual arc of the network

is_valid_dest dest := ~(outLink dest == None );

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;
      }.

Global Instance is_valid_dest_compat {InChans: InChannels} {OutChans: OutChannels} {DNet: DirNetwork}:
Proper fequiv is_valid_dest.

Note on compatibility: Let us consider the above function f: Node -> A

The assumption Proper fequiv f means that when taking two 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. inLink and outLink above).

Extend decidability to destinations, of type Node*InChannel

Lemma dest_dec {InChans: InChannels} {OutChans: OutChannels} {DNet: DirNetwork}:
Decider (equiv (A := (Node * InChannel))).

Class MPAlgorithm: TO BE UPDATED

States are attached to nodes: an algorithm describes step by step the way the state of a node evolves. In the message passing model, this evolution depends on the state itself but also possibly on some incoming message.

The class Algorithm describes the algorithm of a node. It contains the types State and Msg (which should both 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 and a possible incoming message om (option (InChannel * Msg)). A call to run: run s om

The call to run s om returns a new state for the node and a (possibly empty) list of messages that the node wants to send. Each element of the list specifies what and where to send.

  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: 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 om, GetVar (fst (run s om)) =~= GetVar s
}.

End MP_Distributed_Algorithm.

Unset Implicit Arguments.
Close Scope signature_scope.