PADEC - Coq Library

Library Padec.KClustering.KClustering_alpha_termination

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 ZArith.
From Coq Require Import Lia.
From Coq Require Import Bool.
From Coq Require Import Inclusion.
From Coq Require Import RelationPairs.

Local Imports

From Padec Require Import SetoidUtil.
From Padec Require Import OptionUtil.
From Padec Require Import ZUtils.
From Padec Require Import ListUtils.
From Padec Require Import RelationA.
From Padec Require Import FoldRight.
From Padec Require Import Algorithm.
From Padec Require Import RelModel.
From Padec Require Import Spanning_Tree.
From Padec Require Import KClustering_specification.
From Padec Require Import KClustering_algo.
From Padec Require Import KClustering_def_termination.
From Padec Require Import P_Q_Termination.

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

Termination for KClustering Algorithm: Alpha Steps Only

This part shows termination of the algorithm when considering alpha safe steps only. Actually, it shows safe inclusion required by the rest of the proof:

alpha_safe_incl := (forall g g', Alpha_SafeStep g' g -> ltM (Pot_alpha g') (Pot_alpha g)

Roadmap of the proof:

1) Define Potential of a node: 0 if not enabled, else tree depth signature: node->env -> nat

NB: depth for root == 1

2) Proof: if a node becomes enabled, one of its direct child has moved

3) Proof (down path induction + 2)): if a node becomes enabled, one of its descedant has become disabled

assumption: downpaths are finite (to be proved elsewhere)

4) Proof: there is always a node whose activation has changed (potential of this node passed from >0 to 0) (induction on down path)

5) Using 3) and multiset theorem (P_Q_Termination.v) conclude that the algorithm terminates

=> Use results from P_Q_Termination

proof of local criterion: see 3)
proof of global criterion: see 4)

Section KClustering_Alpha_Termination.

Channel and network

  Context {Chans: Channels} {Net: Symmetric_Network}
          {KCP: KClustering_parameters} {KCT: KC_algo_tools}.

  Existing Instance KC_Stable.

  Notation Env := (Env (Algo := KC_algo)).

  Let k_pos := k_pos.

  Variable (root: Node).

  Section Potential_Definition.

Potential of a node:

0 if not enabled, else depth of the node in the spanning tree.

Note that this definition requires that the spanning tree exists. This is the reason why termination cannot be shown without the assumption on safe configurations.

    Variable (g: Env) (pg: Proper pequiv g)
             (span_tree: spanning_tree root (Par_part g) /\
                         Symmetric_Network_assumption Net (fun n => KCpeers (g n)) (fun n => KCreverse (g n))).

Local (of a node) alpha-potential is defined using the depth of the node in the spanning tree Note that this definition requires that the spanning tree exists indeed. This is the reason why termination can not be shown without the assumption of a safe environment.

depth in the tree

    Program Fixpoint depth (env: Env) (n: N)
            (W: Acc (is_tree_parent_of env) n) {struct W}: nat :=
      Datatypes.S
        match W with
            Acc_intro h =>
            match (tree_parent env n) as op return 
                  (eqoptionA eqN op (tree_parent env n)) -> nat
            with
              | None   => fun _ => 0%nat
              | Some p => fun e => (@depth env p (h p e))
            end (Equivalence_Reflexive (tree_parent env n))
        end.

    Definition depth_ (par:Node -> option Channel) (n: Node)
               (W: Acc (is_tree_parent_of par) n): nat :=
      @Fix_F Node (is_tree_parent_of par) (fun _ => nat)
             (fun (x: Node)
                  (f_rec: forall y: Node, is_tree_parent_of par y x -> nat) =>
                Datatypes.S
                  (match (tree_parent par x) as op return
                         (op == tree_parent par x ) -> nat
                   with
                   | None => fun _ => 0%nat
                   | Some y => fun e => (f_rec y e)
                   end (Equivalence_Reflexive (tree_parent par x)))
             ) n W.

    Definition depth (n: Node): nat := depth_ (WF_par (Par_part_compat pg) (proj1 span_tree) n).

Alpha-Potential of a node: 0 if not alpha-enabled, else tree depth

    Definition potential (n: Node): nat :=
      if alpha_enabled_bb g n then depth n
      else 0%nat.

  End Potential_Definition.

  Section Potential_Compatibility.

    Lemma depth__compat:
      (Proper (respectful_dep_param (equiv (A:=nat))
                                    ((Node -> option Channel )::Node ::nil)
                                    (pequiv ,(equiv ,tt ))
                                    (inl (fun par n => Acc (is_tree_parent_of par) n)::nil)) depth_).

    Lemma depth_compat:
      Proper (respectful_dep_param
                (pequiv (A:=Node -> nat ))
                (Env ::nil)
                (pequiv ,tt )
                (inl (fun g => Proper fequiv g)
                     ::inl (fun g => spanning_tree root (Par_part g)
                                     /\
                                     Symmetric_Network_assumption
                                       Net (fun n => KCpeers (g n))
                                       (fun n => KCreverse (g n))
                           )
                     ::nil)) depth.

    Lemma potential_compat:
      Proper (respectful_dep_param
                (pequiv (A:=Node -> nat ))
                (Env ::nil)
                (pequiv ,tt )
                (inl (fun g => Proper fequiv g)
                     ::inl (fun g => spanning_tree root (Par_part g)
                                     /\
                                     Symmetric_Network_assumption
                                       Net (fun n => KCpeers (g n))
                                       (fun n => KCreverse (g n))
                           )
                     ::nil)) potential.

  End Potential_Compatibility.

  Section Depth_Properties.

    Variable (g: Env) (pg: Proper pequiv g)
             (span_tree: spanning_tree root (Par_part g) /\
                         Symmetric_Network_assumption
                           Net (fun n => KCpeers (g n))
                           (fun n => KCreverse (g n))).

    Lemma depth_gt_0: forall (n: Node), gt (depth pg span_tree n) 0.

Any node which is down-linked to another has smaller depth than the first one.

    Lemma deeper_depth_step:
      forall (n: Node) (child: Node),
        is_tree_parent_of (Par_part g) n child ->
        depth pg span_tree child = Datatypes.S (depth pg span_tree n).

    Lemma deeper_depth:
      forall (p: list Node) (n: Node) (d: Node),
        ~ n == d -> directed_tree_path (Par_part g) n p d ->
        (depth pg span_tree n < depth pg span_tree d)%nat.

  End Depth_Properties.

Results for one alpha step of execution

Section With_Step.

The alpha step

    Variable (g g': Env)
             (pg: Proper pequiv g) (pg': Proper pequiv g')
             (step: Step g' g)
             (alpha_step: alpha_step_b g' g = true)
             (span_tree: spanning_tree root (Par_part g)
                         /\
                         Symmetric_Network_assumption
                           Net (fun n => KCpeers (g n))
                           (fun n => KCreverse (g n)))
             (span_tree': spanning_tree root (Par_part g')
                          /\
                          Symmetric_Network_assumption
                            Net (fun n => KCpeers (g' n))
                            (fun n => KCreverse (g' n))).

    Lemma Local_Children_Unchanged:
      forall n,
        equivlistA equiv (Local_Children (KCpeers (g n)) (lPar (local_env g n))
                                         (KCreverse (g n)))
                   (Local_Children (KCpeers (g' n)) (lPar (local_env g' n))
                                   (KCreverse (g' n))).

Any new variables only depends on children alpha-moves

New Alphas of Children only depends on children alpha-moves

    Lemma ChildrenAlphas_only_depends_on_children:
      forall (n: Node),
        (forall (child: Node),
            is_tree_parent_of (Par_part g) n child
            ->
            alpha (g child) = alpha (g' child))
        -> equivlistA
             equiv (ChildrenAlphas (g n) (local_env g n))
             (ChildrenAlphas (g' n) (local_env g' n)).

    Lemma MinATall_only_depends_on_children:
      forall (n: Node),
        (forall (child: Node),
            is_tree_parent_of (Par_part g) n child
            -> alpha (g child) = alpha (g' child)) ->
        MinATall (g n) (local_env g n) = MinATall (g' n) (local_env g' n).

New Alphas only depends on children alpha-moves

    Lemma NewAlpha_only_depends_on_children:
      forall (n: Node),
        (forall (child: Node),
            is_tree_parent_of (Par_part g) n child
            -> alpha (g child) = alpha (g' child))
        -> NewAlpha (g n) (local_env g n) =
           NewAlpha (g' n) (local_env g' n).

The states after firing an alpha-RUN only depends on children moves

    Lemma alpha_RUN_only_depends_on_children:
      forall (n: Node),
        eqS (g n) (g' n) ->
        alpha_enabled_bb g n = true ->
        (forall (child: Node),
            is_tree_parent_of (Par_part g) n child
            -> alpha (g child) = alpha (g' child))
        ->
        (RUN g n ) == (RUN g' n ).

    Lemma alpha_step_effect:
      forall n, alpha (g' n) = NewAlpha (g n) (local_env g n)
                \/ alpha (g' n) = alpha (g n).

When a node that was disabled becomes enabled, one of its child has actually moved.

    Lemma enabled_child_has_moved:
      forall (n: Node) (H: alpha_enabled_bb g n = false)
             (H': alpha_enabled_bb g' n = true),
      exists (child: Node ),
        (is_tree_parent_of (Par_part g) n child ) /\
        (alpha (g child)) <> (alpha (g' child)).

When a node has actually moved while none of its children moved, it is no more enabled at next configuration.

    Lemma node_has_moved_but_no_child:
      forall n, alpha (g n) <> alpha (g' n)
                -> (forall child, is_tree_parent_of (Par_part g) n child
                                  -> alpha (g child) = alpha (g' child))
                -> alpha_enabled_bb g' n = false.

When a node has moved, but is still enabled at next configuration, it has a child that actually also moved.

    Lemma node_has_moved:
      forall (n: Node),
        alpha (g n) <> alpha (g' n) -> alpha_enabled_bb g' n = true ->
        exists (child: Node ),
          (is_tree_parent_of (Par_part g) n child ) /\
          (alpha (g child) <> alpha (g' child)).

When a node actually moved, it is down-linked (in the spanning tree) to a node which was enabled and became disabled.

    Lemma moving_node_has_disabled_desc:
      forall (n: Node),
        alpha (g n) <> alpha (g' n) ->
        exists (descendant: Node ),
          (exists p , directed_tree_path (Par_part g) n p descendant ) /\
          alpha_enabled_bb g descendant = true /\
          alpha_enabled_bb g' descendant = false.

When a node that was disabled becomes enabled at next configuration, it is down-linked (in the spanning tree) to a node which was enabled and becomes disabled.

    Lemma new_enabled_node_has_disabled_descendant:
      forall (n: Node),
        alpha_enabled_bb g n = false ->
        alpha_enabled_bb g' n = true ->
        exists (descendant: Node ),
          (exists p , directed_tree_path (Par_part g) n p descendant ) /\
          alpha_enabled_bb g descendant = true /\
          alpha_enabled_bb g' descendant = false.

4) Proof:

there is always a node that becomes disabled after a step (potential of this node passed from >0 to 0) (induction on down path)

Within a valid step, there exists a node that was enabled but becomes disabled

    Lemma one_disabled:
      exists (n: Node ), alpha_enabled_bb g n = true /\
                        alpha_enabled_bb g' n = false.

5) Using 3) and multiset theorem (Termination.v, Wf_Algo_Multiset)

conclude that the algorithm terminates

proof of local criterion: see 3)
proof of global criterion: see 4)

Termination Criteria

    Section Potential_termination_criteria.

      Lemma depth_preserved_step:
        forall n, depth pg span_tree n = depth pg' span_tree' n.

      Lemma diff_pot:
        forall (n: Node),
          potential pg' span_tree' n <> potential pg span_tree n
          <->
          (alpha_enabled_bb g n = false <-> alpha_enabled_bb g' n = true ).

Local Criterion

      Lemma alpha_local_criterion:
        forall (n: Node),
          gt (potential pg' span_tree' n) (potential pg span_tree n)
          -> exists (n': Node ),
            potential pg span_tree n' <> potential pg' span_tree' n'
            /\
            gt (potential pg span_tree n') (potential pg' span_tree' n).

Global Criterion

      Lemma alpha_global_criterion:
        exists n , potential pg' span_tree' n <> potential pg span_tree n.

    End Potential_termination_criteria.

  End With_Step.

Alpha-Termination Proof

  Section Alpha_Termination.

    Definition alpha_potential
               (sg: sig (Pspanning_tree root)) (n: Node): nat :=
      potential (proj1 (proj2_sig sg)) (proj2 (proj2_sig sg)) n.

    Global Instance alpha_potential_compat:
      Proper fequiv alpha_potential.

Alpha-Termination

    Notation ltM := (@MultisetNat.MSetOrd.MultisetLT gt).
    Notation Pot_alpha := (Pot alpha_potential).

    Theorem alpha_safe_inclusion:
      inclusion (Alpha_SafeStep (root := root)) (ltM @@ Pot_alpha).

  End Alpha_Termination.

End KClustering_Alpha_Termination.

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