PADEC - Coq Library

Library Padec.Dijkstra.Dijkstra_algo

A Framework for Certified Self-Stabilization
PADEC Coq Library

March 2017

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.

Local Imports

From Padec Require Import OptionUtil.
From Padec Require Import SetoidUtil.
From Padec Require Import Algorithm.
From Padec Require Import Ring_topology.

Open Scope nat_scope.
Open Scope signature_scope.
Set Implicit Arguments.

Diskstra's first token ring algorithm

Proof of self-stabilization and specification
Proof of a complexity bound in steps
Proof that this complexity bound is exact (by building a worst case prefix of execution)

The Algorithm

/contains:/ Dijkstra first algorithm for token circulation on a rooted ring

/assume:/ Parameter k>1

Definition of the state of a process (ROState and State, equivalence, decidability, getter, compatibility)
Definition of the algorithm:
- > function *simple_run* contains the algorithm as written in the original paper, using two arguments (the current state of the node and the current state of its predecessor);
- > function *run* calls simple_run with the proper arguments, as awaited by PADEC in class Algorithm.

Section Dijkstra_algo.

  Context {Chans: Channels}.

  Class Dijkstra_parameters :=
    {

Parameter k of the algoritm: node values are incremented

modulo k

      k: nat;
      H_k: k > 0
    }.

Assuming the Dijkstra parameter and hypothesis:

Context {DP: Dijkstra_parameters}.
Let H_k := H_k.

State of a Node in the Algorithm

Read Only Part of a State; local topology information

It is made of

the channel to the predecessor node and
a Boolean value meaning that the node is a root in the ring

    Record Dijkstra_ROState := mkROState {
                                   predc: Channel;
                                   root: bool
                                 }.

    Notation eqROS := (fun (x y: Dijkstra_ROState) =>
                         predc x == predc y /\ root x = root y).

    Instance eqROS_equiv: Equivalence eqROS.

    Global Instance Dijkstra_ROState_setoid: Setoid Dijkstra_ROState :=
      {|equiv := eqROS|}.

State of a node

a natural counter, v, smaller than k
the local topology read-only part as defined above

    Record Dijkstra_State := mkState {
                                 vltk: { n : nat | n <= k -1};
                                 Dijkstra_ROpart :> Dijkstra_ROState
                               }.

    Notation eqS := (fun (x y: Dijkstra_State) =>
      vltk x == vltk y /\ Dijkstra_ROpart x == Dijkstra_ROpart y).

    Instance eqS_equiv: Equivalence eqS.

    Global Instance State_setoid :Setoid Dijkstra_State := {|equiv := eqS|}.

Getter for vltk

    Definition v (s: Dijkstra_State): nat := proj1_sig (vltk s).

    Lemma v_ltk: forall (s: Dijkstra_State), v s < k.

    Lemma v_plus_0: forall (s: Dijkstra_State), (v s + 0) mod k = v s.

Equality and Compatibility properties on State

    Lemma Dijkstra_ROState_dec: Decider (equiv (A := Dijkstra_ROState)).

    Lemma Dijkstra_State_dec: Decider (equiv (A := Dijkstra_State)).

    Instance v_compat: Proper fequiv v.

    Instance predc_compat_RO: Proper fequiv predc.

    Instance root_compat_RO: Proper fequiv root.

    Instance Dijkstra_ROpart_compat: Proper fequiv Dijkstra_ROpart.

    Instance predc_compat: Proper (equiv (A:=Dijkstra_State) ==> equiv) predc.

    Instance root_compat: Proper (equiv (A:=Dijkstra_State) ==> equiv) root.

    Section Run_definition.

"+1" on natural modulo k

      Program Definition Smod (nltk: {n : nat | n <= k -1}):
        {n : nat | n <= k -1} := (S (proj1_sig nltk) mod k).

      Global Instance Smod_compat: Proper fequiv Smod.

      Lemma Smod_neq:
        k > 1 -> forall (v: {n : nat | n <= k -1}), ~v == (Smod v ).

      Lemma Smod_neq_degenerated:
        k = 1 -> forall (v: {n : nat | n <= k -1}), v == (Smod v ).

Run Function for the Algorithm

when the root value is equal to the value of its predecessor, its value increments modulo k
when the value of a non-root node is different from that of its predecessor, the node gets the value of its predecessor

Function simple_run contains the algorithm as written in papers, using two arguments (the current state of the node and the current state of its predecessor).

Function run_algorithm calls simple_run with the arguments, as awaited by PADEC in class Algorithm.

      Definition simple_run (s s_pred: Dijkstra_State): Dijkstra_State :=
         if root s then
           if Nat.eq_dec (v s) (v s_pred) then
             {| vltk := Smod (vltk s); Dijkstra_ROpart := s |}
           else
             s
         else
           if Nat.eq_dec (v s) (v s_pred) then
             s
           else
             {| vltk := vltk s_pred; Dijkstra_ROpart := s |}.

      Definition run_algorithm
                 (s: Dijkstra_State)
                 (peer_state: Channel -> option Dijkstra_State)
        : Dijkstra_State :=
        match peer_state (predc s) with
          None => s
        | Some s_pred => simple_run s s_pred
        end.

    End Run_definition.

Properties of the Algorithm

Compatibility of the Run Function

    Instance simple_run_compat:
      Proper fequiv simple_run.

    Instance run_algorithm_compat: Proper fequiv run_algorithm.

Definition of The Algorithm

Instance Dijkstra_algo: Algorithm :=
{| State := Dijkstra_State; State_dec:= Dijkstra_State_dec; run := run_algorithm; |}.

Stability for the Read-Only Part of the Run Function

    Lemma ROpart_stable:
      forall s sn, Dijkstra_ROpart (run_algorithm s sn) =~= Dijkstra_ROpart s.

    Global Instance Dijkstra_Stable:
      Stable_Variable Dijkstra_algo Dijkstra_ROpart.

End Dijkstra_algo.

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