PADEC
Coq Library
Tools
PADEC - Coq Library

Library Padec.Model.Algorithm

A Framework for Certified Self-Stabilization
PADEC Coq Library

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
Section Distributed_Algorithm.

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 Channels :=
    mkChannels {
        Channel: Type;
        Channel_setoid:> Setoid Channel;
        Channel_dec: Decider (equiv (A := Channel))
      }.

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.
  Class Network {Chans: Channels} :=
    mkNet {

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

        
link: (link n n') is
        link: Node -> Node -> option Channel;
        
        
peer: (peer n c) is
        peer: Node -> Channel -> option Node;

        
is_channel: is_channel n c n' holds when n --c--> n'.
        is_channel n1 c12 n2 := peer n1 c12 == Some n2;

        
peer and link cover the same edges of the network
        link_peer_spec: forall n1 n2 c12,
            link n1 n2 == Some c12 <-> is_channel n1 c12 n2;
        
        link_compat: Proper fequiv link;
        peer_compat: Proper fequiv peer;

        
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_channel_compat {Chans: Channels} {Net: Network}:
    Proper fequiv is_channel.

From a node a given channel points to at most one node. Namely, each node has a local referential given by its outgoing channels
  Lemma is_channel_unique {Chans: Channels} {Net: Network}:
    forall n c m m', is_channel n c m -> is_channel n c m' ->
                     m == m'.

For a given network and a given node n, (peers n) is the list of outgoing channels from n
  Definition peers {Chans: Channels} {Net: Network} (n: Node): list Channel :=
    map_filter (fun nn => link n nn) all_nodes.

  Global Instance peers_compat {Chans: Channels} {Net: Network}:
    Proper fequiv peers.

  Global Instance peers_compat_equiv {Chans: Channels} {Net: Network}:
    Proper (equiv ==> equivlistA equiv) peers.

peers characterization using the function peer: every channel in (peer n) is actually a channel from n in the network
  Lemma peers_spec_peer {Chans: Channels} {Net: Network}:
    forall n1 c12, InA equiv c12 (peers n1)
                   <->
                   exists n2, is_channel n1 c12 n2.

peers characterization using the function link
  Lemma peers_spec_link {Chans: Channels} {Net: Network}:
    forall n1 c12, InA equiv c12 (peers n1)
                   <->
                   exists n2, link n1 n2 == Some c12.

Symmetric Network: Bidirectionnal channels

  Class Symmetric_Network {Chans: Channels} :=
    mkSymNet {
        net:> Network;

        sym_net: forall n1 n2,
            (exists c12, is_channel n1 c12 n2) <->
            (exists c21, is_channel n2 c21 n1);
        
        
reverse: if c is a channel outgoing from n, then (reverse n c) is the channel corresponding to c in the other direction
        reverse: Node -> Channel -> Channel;

        
specification of reverse: n1 --c12--> n2 and n1 <--c21-- n2
        reverse_spec: forall n1 n2 c12 c21,
            is_channel n1 c12 n2 /\ is_channel n2 c21 n1 ->
            reverse n1 c12 == c21;
        
        reverse_compat:> Proper fequiv reverse
      }.


reverse_spec': same as reverse_spec, maybe easier to use
  Lemma reverse_spec' {Chans: Channels} {Net: Symmetric_Network}:
    forall n1 c n2, is_channel n1 c n2 ->
                    is_channel n2 (reverse n1 c) n1.

reverse is "involutive" (using adequate parameters for nodes)
  Lemma reverse_involutive {Chans: Channels} {Net: Symmetric_Network}:
    forall n c m, is_channel n c m ->
                  reverse m (reverse n c) == c.

A symmetric network (as we defined it) allows no multi-edge
  Lemma no_multi_edge {Chans: Channels} {Net: Symmetric_Network}:
    forall n c c' m, is_channel n c m -> is_channel n c' m
                     -> c == c'.


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.

  Class Algorithm {Chans: Channels} :=
    {
      
Type State: state of a node
      State: Type;
      State_setoid:> Setoid State;
      State_dec: Decider (equiv (A := State));

      
run: see above
      run: State -> (Channel -> option State) -> State;
      
      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 {Chans: Channels}
        (Algo: Algorithm) (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 sn, GetVar (run s sn) =~= 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

  Definition SubNetwork_assumption {Chans: Channels} (Net: Network)
             (tested_peers: Node -> list Channel) :=
    forall n c, InA equiv c (tested_peers n) -> InA equiv c (peers n).

  Global Instance SubNetwork_assumption_compat
         {Chans: Channels} (Net: Network):
    Proper ((equiv ==> equivlistA equiv) ==> equiv)
           (SubNetwork_assumption Net).

Network: same set of peers

  Definition Network_assumption {Chans: Channels} (Net: Network)
             (tested_peers: Node -> list Channel) :=
    forall n, equivlistA equiv (tested_peers n) (peers n).

  Global Instance Network_assumption_compat
         {Chans: Channels} (Net: Network):
    Proper ((equiv ==> equivlistA equiv) ==> equiv)
           (Network_assumption Net).

  Lemma Network_is_SubNetwork:
    forall {Chans: Channels} (Net: Network)
           (tested_peers: Node -> list Channel),
      Network_assumption Net tested_peers ->
      SubNetwork_assumption Net tested_peers.

Symmetric Networks:

(i.e. for every outgoing channel, we check that they have the same reverse channel)
  Definition Symmetric_Network_assumption {Chans: Channels}
             (Net: Symmetric_Network)
             (tested_peers: Node -> list Channel)
             (tested_reverse: Node -> Channel -> Channel): Prop :=
    Network_assumption net tested_peers /\
    forall n c, InA equiv c (peers n) ->
                tested_reverse n c == reverse n c.

  Global Instance Symmetric_Network_assumption_compat
         {Chans: Channels} (Net: Symmetric_Network):
    Proper ((equiv ==> equivlistA equiv) ==> fequiv ==> equiv)
           (Symmetric_Network_assumption Net).

  Lemma Symmetric_Network_assumption_compat_equiv
        {Chans: Channels} (Net: Symmetric_Network):
    forall t1 t2 (et: (equiv ==> equivlistA equiv) t1 t2)
           r1 r2
           (er: forall n c, InA equiv c (t1 n) -> r1 n c == r2 n c),
      Symmetric_Network_assumption Net t1 r1 ==
      Symmetric_Network_assumption Net t2 r2.

  Section Net_Algorithm_mapping.

    Context {Chans: Channels}.

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

    Definition build_links (Net: Network) (n: Node): list Channel :=
      peers n.

triviality :)
    Lemma build_links_ensures_Network_Assumption:
      forall (Net: Network),
        Network_assumption Net (fun n => build_links Net n).

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
    Definition lpeers_reverse_assume (lp: list (Channel * Channel)) :=
      forall x1 y1 x2 y2, InA equiv (x1, y1) lp ->
                          InA equiv (x2, y2) lp ->
                          x1 == x2 -> y1 == y2.

    Instance lpeers_reverse_assume_compat:
      Proper (equivlistA equiv ==> equiv) lpeers_reverse_assume.

    Definition llpeers (lr: list (Channel * Channel)): list Channel :=
      map (fun xy => fst xy) lr.

    Definition llreverse (lr: list (Channel * Channel)) (c: Channel): Channel :=
      let lf := filter (fun xy => if Channel_dec (fst xy) c
                                  then true else false) lr in
      match lf with nil => c | (_,y)::_ => y end.

    Instance llpeers_compat: Proper fequiv llpeers.

    Instance llpeers_compat_equivlist:
      Proper (equivlistA equiv ==> equivlistA equiv) llpeers.

    Instance llreverse_compat: Proper fequiv llreverse.

    Lemma llreverse_compat_equivlist:
      forall l1 l2, lpeers_reverse_assume l1 ->
                    equivlistA equiv l1 l2 ->
                    fequiv (llreverse l1) (llreverse l2).

    Definition build_symlinks (Net: Symmetric_Network) (n: Node):
      list (Channel * Channel) :=
      map (fun c => (c, reverse n c)) (peers n).

    Instance build_symlinks_compat
             {Net: Symmetric_Network}: Proper fequiv (build_symlinks Net).

    Instance build_symlinks_compat_equiv
             {Net: Symmetric_Network}:
      Proper (equiv ==> equivlistA equiv) (build_symlinks Net).

    Lemma build_symlinks_ensures_lpeers_reverse_assume:
      forall Net n, lpeers_reverse_assume (build_symlinks Net n).

    Lemma build_links_ensures_Symmetric_Network_Assumption:
      forall (Net: Symmetric_Network),
        Symmetric_Network_assumption
          Net (fun n => llpeers (build_symlinks Net n))
          (fun n => llreverse (build_symlinks Net n)).

    Lemma build_links_ensures_Symmetric_Network_Assumption_equivlist:
      forall Net (pr: Node -> list (Channel * Channel)),
        (forall n, equivlistA equiv (pr n)
                              (build_symlinks Net n)) ->
        Symmetric_Network_assumption
          Net (fun n => llpeers (pr n))
          (fun n => llreverse (pr n)).

  End Net_Algorithm_mapping.

End Distributed_Algorithm.

Unset Implicit Arguments.
Close Scope signature_scope.