PADEC - Coq Library

Library Padec.BFS.BFS_algo

*Certified Round Complexity of Self-Stabilizing Algorithms*

Global Imports

From Coq Require Import SetoidList.
From Coq Require Import Bool.
From Coq Require Import ZArith.

From Coq Require Import SetoidClass.
From Coq Require Import Lia.

Local Imports

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

From Padec Require Import Graph_Diameter.
Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

BFS Spanning Tree: the Algoritm

nb: Two algorithms are given, one for the root, the other for other processes. We merge them, using conditional structure.

Algorithm for a process p: Global Input (shared by every process): D natural number assumption: the diameter of the network is upper bounded by D Input: p.N contains channels assumption: p.N is the list of channels of every neighbor towards p in the network Input: p.root Boolean assumption: True for a unique process, represents the root of the rooted network Variables: p.d natural number, p.par channel nb: p.par has no meaning if root

Section BFS_algo.

Context {Chans: Channels}.

D is an upper bound on the network diameter

Variable (D: nat).

State of node for the algorithm

  Record BFSROState :=
    mkROState {

is the process considered as the root?

root: bool;

neighbors of the process, implemented as a list. The order in the list represents the local on those channels (required in the algorithm)

        neighbors: list Channel
      }.

  Notation eqROS :=
    (fun (x y: BFSROState) => root x == root y /\
                              neighbors x == neighbors y).

  Global Instance eqROS_equiv: Equivalence eqROS.

  Global Instance BFSROState_setoid: Setoid BFSROState :=
    {| equiv := eqROS |}.

  Record BFSState :=
    mkState {

distance to the root; should be <= D after the first step of the algorithm

d: nat;

parent pointer; meaningless if root; should be in neighbors (InA equiv par neighbors) after the first step of action CP

par: Channel;

read-only part of the state

        BFSROpart:> BFSROState
      }.

  Notation eqS :=
    (fun (x y: BFSState) =>
       d x == d y /\ par x == par y /\ BFSROpart x == BFSROpart y).

  Global Instance eqS_equiv: Equivalence eqS.

  Global Instance BFSState_setoid: Setoid BFSState :=
    {| equiv := eqS |}.

  Lemma BFSROState_dec: Decider (equiv (A := BFSROState)).

  Lemma BFSState_dec: Decider (equiv (A := BFSState)).

Compatibility on states

  Global Instance d_compat: Proper fequiv d.

  Global Instance par_compat: Proper fequiv par.

  Global Instance root_compat: Proper fequiv root.

  Global Instance neighbors_compat: Proper fequiv neighbors.

  Global Instance BFSROpart_compat: Proper fequiv BFSROpart.

Function run

Definition Dist_p (dists: list nat): nat :=
match min_list dists with None => 0 | Some m => m end.

Par_dist = q s.t. q in p.Neigh and q.d + 1 = p.d

  Definition Par_dist (pd: nat) (dum: Channel)
             (neigh_dist: list (Channel * nat)): Channel :=
    fst (hd (dum , 0)
            (filter (fun cn => if Nat.eq_dec (S (snd cn)) pd
                               then true else false) neigh_dist)).

  Global Instance Par_dist_compat: Proper pequiv Par_dist.

Root Algorithm

Definition simple_run_Root (s: BFSState): BFSState :=
{| d := 0; par := par s; BFSROpart := BFSROpart s |}.

Non-Root Algorithm: guard for CD: p.d <> DistpD guard for CP: p.d = DistpD /\ p.d = Distp /\ p.par.d + 1 <> p.d

  Definition simple_run (d: nat) (par: Channel) (par_d: nat)
             (ro: BFSROState)
             (neigh: list (Channel * nat)): BFSState :=
    if Nat.eq_dec d (Dist_p (D :: (map S (map snd neigh)))) then

      if Nat.eq_dec d (Dist_p (map S (map snd neigh))) then

        if Nat.eq_dec d (S par_d) then

Do Nothing

{| d := d; par := par; BFSROpart := ro |}
        else

CP Action

          {| d := d; par := Par_dist d par neigh; BFSROpart := ro |}
      else

Do Nothing

{| d := d; par := par; BFSROpart := ro |}
    else

      {|

CD Action

        d := Dist_p (D :: (map S (map snd neigh)));
        par := par;
        BFSROpart := ro |}.

  Definition neighbor_list
             (state: BFSState)
             (peer_state: Channel -> option BFSState):
    list (Channel * nat) :=
    map_filter (fun c =>
                  match peer_state c with
                  | None => None
                  | Some s => Some (c , d s) end)
               (neighbors state).

  Definition run (state: BFSState)
             (peer_state: Channel -> option BFSState): BFSState :=
    if root state then simple_run_Root state
    else simple_run (d state)
                    (par state)
                    (match peer_state (par state) with
                     | None => d state
                     | Some s => d s end)
                    (BFSROpart state)
                    (neighbor_list state peer_state).

Compatibility of definitions used in run_algorithm

  Global Instance Dist_p_compat: Proper pequiv Dist_p.

  Global Instance simple_run_Root_compat: Proper pequiv simple_run_Root.

  Global Instance simple_run_compat: Proper pequiv simple_run.

  Global Instance neighbor_list_compat: Proper pequiv neighbor_list.
  Global Instance run_compat: Proper pequiv run.

  Lemma ROpart_stable: forall s sn, BFSROpart (run s sn) =~= BFSROpart s.

The Algorihtm

  Global Instance BFS_algo: Algorithm.

  Global Instance BFS_Stable:
    Stable_Variable BFS_algo BFSROpart.

End BFS_algo.

Close Scope signature_scope.
Close Scope nat_scope.
Unset Implicit Arguments.