PADEC - Coq Library

Library Padec.KDomSet.KDomSet_alpha

A Framework for Certified Self-Stabilization
PADEC Coq Library

Feb 2016

Global Imports

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

Local Imports

From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import SetoidUtil.
From Padec Require Import FoldRight.
From Padec Require Import Algorithm.
From Padec Require Import Spanning_Tree.

Open Scope Z_scope.
Open Scope signature_scope.
Set Implicit Arguments.

K Dominating Set: the Algoritm

Algorithm for a process p: Global Input (shared by every process): k positive number

Input: p.children contains a list of channels assumption: the set of every p.children (for every node p) shapes a downward tree (i.e. the tree is directed, from root to leaves).

Variables: p.alpha integer number

Algorithm in itself (for any node p) Nb: for readability, we write any channel c in p.children as a node q, namely q is the node which is pointed by c. Functions: MaxAShort(p) = max( { q.alpha | q in p.children | q.alpha < k } U { -1 } ) MinATall(p) = min ( { q.alpha | q in children | q.alpha >= k } U { 2k + 1 } ) NewAlpha(p) = if MaxAShort(p) + MinATall(p) + 2 <= 2k then MinATall(p) + 1 else MaxAShort(p) + 1 Rule: p.alpha <> NewAlpha(p) --> p.alpha(p) = NewAlpha(p)

Definition of alpha and its computation

Section KDomSet_Algo.

Context {Chans: Channels}.

Variable (k: Z).

State of node for the algorithm

  Record KDomROState :=
    mkROState {

children of the process, implemented as a list.

        _children: list Channel
      }.

  Notation eqROS :=
    (fun (x y: KDomROState) =>
       equivlistA equiv (_children x) (_children y)).

  Global Instance eqROS_equiv: Equivalence eqROS.

  Global Instance KDomROState_setoid: Setoid KDomROState :=
    {| equiv := eqROS |}.

  Record KDomState :=
    mkState {
        alpha: Z;

read-only part of the state

        KDomROpart:> KDomROState
      }.

  Notation eqS :=
    (fun (x y: KDomState) =>
       alpha x == alpha y /\ KDomROpart x == KDomROpart y).

  Global Instance eqS_equiv: Equivalence eqS.

  Global Instance KDomState_setoid: Setoid KDomState :=
    {| equiv := eqS |}.

  Lemma KDomROState_dec: Decider (equiv (A := KDomROState)).

  Lemma KDomState_dec: Decider (equiv (A := KDomState)).

Compatibility on states

  Global Instance alpha_compat: Proper fequiv alpha.

  Global Instance _children_compat:
    Proper (equiv ==> equivlistA equiv) _children.

  Global Instance KDomROpart_compat: Proper fequiv KDomROpart.

Function run

  Definition MaxAShort (children_alphas: list Z): Z :=
    List.fold_right
      Z.max (-1) (List.filter (fun a => a <? k)
                              children_alphas).

  Global Instance MaxAShort_compat:
    Proper (equivlistA equiv ==> equiv) MaxAShort.

  Definition MinATall (children_alphas: list Z): Z :=
    List.fold_right
      Z.min (2 * k + 1) (List.filter (fun a => a >=? k)
                                     children_alphas).

  Global Instance MinATall_compat:
    Proper (equivlistA equiv ==> equiv) MinATall.

    Definition NewAlpha (children_alphas: list Z): Z :=
      let short := MaxAShort children_alphas in
      let tall := MinATall children_alphas in
      if Z_le_gt_dec (short + tall + 2) (2 * k)
      then tall + 1 else short + 1.

    Global Instance NewAlpha_compat:
      Proper (equivlistA equiv ==> equiv) NewAlpha.

    Definition alpha_list
               (state: KDomState)
               (peer_state: Channel -> option KDomState):
      list Z :=
      map_filter (fun c =>
                    match peer_state c with
                    | None => None
                    | Some s => Some (alpha s) end)
                 (_children state).

    Global Instance alpha_list_compat:
      Proper (equiv ==> pequiv ==> equivlistA equiv) alpha_list.

    Definition run (state: KDomState)
               (peer_state: Channel -> option KDomState): KDomState :=
      {| alpha := NewAlpha (alpha_list state peer_state);
         KDomROpart := KDomROpart state |}.

    Global Instance run_compat: Proper fequiv run.

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

The Algorihtm

    Global Instance KDomSet_algo: Algorithm.

    Global Instance KDom_Stable:
      Stable_Variable KDomSet_algo KDomROpart.

End KDomSet_Algo.

Close Scope signature_scope.
Close Scope Z_scope.
Unset Implicit Arguments.