Library RobustReconfiguration

Modelisation of robust reconfiguration protocols

Require Import Common.

Modelisation: architectures, invariants, algorithms

possible states for components

Inductive Status :=
| Started
| Stopped
| Failed.

Section s.

we assume a set of components, a set of import names, and a function indicating which import is mandatory for each component

Variable Component: FSet.
Variable Imports: FSet.
Variable is_mandatory: Component -> Imports -> bool.

Notation mandatory c i := (is_mandatory c i = true).
Notation optional c i := (is_mandatory c i = false).

an architecture is represented by:

a function associating a status to all components
a partial function representing existing wires

Record arch := mk_arch {
status: Component -> Status;
wires: Component * Imports -> option Component
}.

the empty architecture: no wires, all components stopped

Definition empty_arch := {|
status := fun _ => Stopped;
wires := fun _ => None
|}.

the five kinds of reconfiguration operations

Inductive down_op :=
| Unwire(c: Component)(i: Imports)
| Stop(c: Component)
| Fail(c: Component).

Inductive up_op :=
| Wire(c: Component)(i: Imports)(d: Component)
| Start(c: Component).

Inductive op :=
| down(o: down_op)
| up(o: up_op).

Coercion down: down_op >-> op.
Coercion up: up_op >-> op.

Section d.

  Variable s: arch.

  Notation started c := (status s c = Started).
  Notation stopped c := (status s c = Stopped).
  Notation failed c := (status s c = Failed).

  Notation wired c i d := (wires s (c,i) = Some d).
  Notation notwired c i := (wires s (c,i) = None).

  Definition needs c d := exists_ (fun i => is_mandatory c i && (wires s (c,i) ?= Some d)).
  Definition acyclic := acyclic needs.
  Definition rank := rank needs.

architectural invariants, to be preserved

  Record consistent := {
    AI1: forall c i, started c -> mandatory c i -> exists d, wired c i d;
    AI2: forall c i d, started c -> wired c i d -> started d;
    AI3: forall c i d, wired c i d -> ~failed c /\ ~failed d;
    AI4: forall c i d, stopped c -> wired c i d -> mandatory c i;
    AI5:> acyclic
  }.

  Lemma AI4': consistent -> forall c i d, wired c i d -> optional c i -> started c.

lifecycle FSM

the following predicate specifies when an operation is allowed; it corresponds to the lifecycle FSM of the paper.

  Inductive allowed: op -> Prop :=
  | wire_m: forall c i d, notwired c i -> mandatory c i -> stopped c -> allowed (Wire c i d)
  | wire_o: forall c i d, notwired c i -> optional c i -> started c -> allowed (Wire c i d)
  | unwire_m: forall c i, ~notwired c i -> mandatory c i -> stopped c -> allowed (Unwire c i)
  | unwire_o: forall c i, ~notwired c i -> optional c i -> started c -> allowed (Unwire c i)
  | start: forall c, stopped c -> allowed (Start c)
  | stop: forall c, started c -> allowed (Stop c)
  | fail: forall c, allowed (Fail c).

applying atomic reconfiguration operations to an architecture

  Definition down_apply (o: down_op): arch :=
    match o with
      | Unwire c i => mk_arch (status s) (set (c,i) None (wires s))
      | Stop c => mk_arch (set c Stopped (status s)) (wires s)
      | Fail c => mk_arch (set c Failed (status s)) (wires s)
    end.

  Definition up_apply (o: up_op): arch :=
    match o with
      | Wire c i d => mk_arch (status s) (set (c,i) (Some d) (wires s))
      | Start c => mk_arch (set c Started (status s)) (wires s)
    end.

  Definition apply (o: op): arch :=
    match o with
      | down o => down_apply o
      | up o => up_apply o
    end.

comparison functions for operations

V-ordering of reconfiguration operations

auxiliary functions

final V-ordering functions

  Definition order_down_op o1 o2 := lex (cmp_down_kop (kind_of_down_op o1) (kind_of_down_op o2)) (cmp_down_op o1 o2).
  Definition order_up_op o1 o2 := lex (cmp_up_kop (kind_of_up_op o1) (kind_of_up_op o2)) (cmp_up_op o1 o2).

  Instance Cmp_order_down_op: Cmp order_down_op.

  Instance Cmp_order_up_op: Cmp order_up_op.

End d.

applying sequences of operations

Definition apply_down_seq s (l: list down_op) := fold_left down_apply l s.
Definition apply_up_seq s (l: list up_op) := fold_left up_apply l s.
Definition apply_seq s (l: list op) := fold_left apply l s.

Incrementally Consistent Sequences (ICS)

Inductive ics: arch -> list op -> Prop :=
| as_nil: forall s, consistent s -> ics s nil
| as_cons: forall s o q, allowed s o -> consistent s -> ics (apply s o) q -> ics s (o::q).

Lemma apply_ics_consistent: forall s l, ics s l -> consistent (apply_seq s l).

Lemma ics_comp: forall s h k, ics s h -> ics (apply_seq s h) k -> ics s (h++k).

Lemma ics_prefix s h k: ics s (h++k) -> ics s h.

Lemma ics_suffix s h k: ics s (h++k) -> ics (apply_seq s h) k.

propagation algorithm, to saturate "apply down sets"

auxiliary functions to fold through wires

Definition fold_wires s A c (f: Imports -> list A) :=
   fold (fun i a =>
     match wires s (c,i) with
       | Some _ => f i ++ a
       | None => a
     end) nil.

Definition fold_optional_wires s A c (f: Imports -> list A) :=
   fold_wires s c (fun i => if is_mandatory c i then nil else f i).

Definition fold_pointing_wires s A c (f: Component -> Imports -> list A) :=
   fold (fun di a => if wires s di ?= Some c then f (fst di) (snd di) ++ a else a) nil.

Definition fold_optional_pointing_wires s A c (f: Component -> Imports -> list A) :=
   fold_pointing_wires s c (fun d i => if is_mandatory d i then nil else f d i).

Definition fold_mandatory_pointing_components s A c (f: Component -> list A) :=
   fold_pointing_wires s c (fun d i => if is_mandatory d i then f d else nil).

propagating stopped goals (unlike in the paper, we unfold the recursive calls to unwire optional imports: this allows us to get a simply recursive function rather than mutually recursive functions)

Fixpoint xpropagate_stop n s c :=
   match status s c with
     | Started =>
       (match n with O => nil | S n => fold_mandatory_pointing_components s c (xpropagate_stop n s) end) ++
       (fold_optional_pointing_wires s c (fun d i => Unwire d i::nil)) ++
       (fold_optional_wires s c (fun i => Unwire c i::nil)) ++
       (Stop c) :: nil
     | _ => nil
   end.
Definition propagate_stop := xpropagate_stop (cardinal Component).

propagating unwired goals

Definition propagate_unwire s c i :=
   match wires s (c,i) with
     | Some _ =>
       if is_mandatory c i then propagate_stop s c ++ Unwire c i :: nil
       else Unwire c i :: nil
     | _ => nil
   end.

propagating failed goals

Definition propagate_fail s c :=
   match status s c with
     | Failed => nil
     | _ =>
       fold_pointing_wires s c (propagate_unwire s) ++
       fold_wires s c (propagate_unwire s c) ++
       Fail c :: nil
   end.

architectural diff to generate apply up/down sets

generating saturated apply down sets by architectural diff and propagation (we assume that the source does not contain more failed components than the target)

Definition needs_unwire c d :=
   match c,d with
     | Some _,None => true
     | Some c, Some d => negb (c?=d)
     | _,_ => false
   end.

Definition down_diff e t :=
   fold (fun c l =>
     match status e c, status t c with
       | _, Failed => propagate_fail e c ++ l
       | Started, Stopped => propagate_stop e c ++ l
       | _,_ => l
     end) nil
   ++
   fold (fun di l =>
     if needs_unwire (wires e di) (wires t di)
       then propagate_unwire e (fst di) (snd di) ++ l
       else l)
   nil.

generating up sets: just architectural diff (we assume that the target is reachable by up operations only, i.e., that the down phase succeeded)

Definition up_diff e t :=
   fold (fun c l =>
     match status e c, status t c with
       | Stopped, Started => Start c :: l
       | _,_ => l
     end) nil
   ++
   fold (fun di l =>
     match wires e di, wires t di with
       | None, Some c => Wire (fst di) (snd di) c :: l
       | _,_ => l
     end) nil.

final commit session algorithm, without considering failures

(returns the sequence of operations to apply)

Definition commit_seq e t :=
   let d := sort (order_down_op (rank e)) (down_diff e t) in
   let e := apply_down_seq e d in
   let u := sort (order_up_op (rank t)) (up_diff e t) in
     map down d ++ map up u.

Proofs

comparing architecures

Inductive les: relation Status :=
| les_refl: forall x, les x x
| les_ur: les Stopped Started
| les_f: forall x, les Failed x.
Lemma les_r: forall x, les x Started.

Hint Constructors les. Hint Resolve les_r.

e<=t holds when e is less functional than t, and when wires from e are wired like in t

Record le (e t: arch): Prop := mk_le {
le_status: forall c, les (status e c) (status t c);
le_wires: forall ci, wires e ci = None \/ wires t ci = wires e ci
}.
Infix "<=" := le.

isomorphism of architectures

Record isomorph (e t: arch): Prop := mk_eq {
iso_status: forall c, status e c = status t c;
iso_wires: forall ci, wires t ci = wires e ci
}.
Infix "==" := isomorph (at level 80).

Lemma ge_wires e t: e <= t -> forall ci, wires t ci = None -> wires e ci = None.

Instance les_preorder: PreOrder les.

Instance le_preorder: PreOrder le.
Hint Extern 0 (?x <= ?x) => apply le_preorder.

Instance eq_equivalence: Equivalence isomorph.

Instance le_PartialOrder: PartialOrder isomorph le.

has an architecture less failed components than another one ?

Definition less_failures e t := forall c, status e c = Failed -> status t c = Failed.
Infix "<<" := less_failures (at level 80).

Instance less_failures_preorder: PreOrder less_failures.

conjunction of <= and <<

Definition le_and_less_failures e t :=
(forall c, status e c = status t c \/ status e c = Stopped /\ status t c = Started ) /\
(forall ci, wires e ci = None \/ wires t ci = wires e ci).
Infix "<<=" := le_and_less_failures (at level 80).

Lemma leless_le_less e t: e <<= t <-> (e<=t /\ e<<t).

miscellaneous lemmas

Lemma consistent_empty: consistent empty_arch.

Lemma apply_down_seq_map s l: apply_down_seq s l = apply_seq s (map down l).

Lemma apply_up_seq_map s l: apply_up_seq s l = apply_seq s (map up l).

Lemma apply_seq_app s h k: apply_seq s (h++k) = apply_seq (apply_seq s h) k.

Lemma le_acyclic s t: acyclic t -> s <= t -> acyclic s.

Lemma wires_rank s (Hs: acyclic s) d i c: mandatory d i -> wires s (d,i) = Some c -> rank s d < rank s c.

Lemma apply_allowed_down_op_le s (o: down_op): allowed s o -> apply s o <= s.

Lemma apply_down_ics_le s l: ics s (map down l) -> apply_down_seq s l <= s.

Lemma apply_allowed_less_failures s o: allowed s o -> s << apply s o.

Lemma apply_ics_less_failures s l: ics s l -> s << apply_seq s l.

Lemma nofail_less_failures s o: (forall c, o<>down (Fail c)) -> apply s o << s.

Lemma nofail_seq_less_failures s l: (forall c, ~In (down (Fail c)) l) -> apply_seq s l << s.

sufficient conditions for operations to preserve consistency

Lemma consistent_unwire_notstarted s c i: consistent s ->
   status s c <> Started -> consistent (apply s (Unwire c i)).

Lemma consistent_unwire_optional s c i: consistent s ->
   optional c i -> consistent (apply s (Unwire c i)).

Lemma consistent_stop s c: consistent s ->
   (forall i, optional c i -> wires s (c,i) = None) ->
   (forall d i, wires s (d,i) = Some c -> status s d <> Started) ->
   consistent (apply s (Stop c)).

Lemma consistent_fail s c: consistent s ->
   (forall i, wires s (c,i) = None) ->
   (forall d i, wires s (d,i) <> Some c) ->
   consistent (apply s (Fail c)).

Lemma consistent_start s c: consistent s ->
   status s c <> Failed ->
   (forall i, mandatory c i -> exists d, wires s (c,i) = Some d /\ status s d = Started) ->
   (forall i, optional c i -> wires s (c,i) = None) ->
   consistent (apply s (Start c)).

Lemma consistent_wire_mandatory s c i d t: consistent s ->
   status s c = Stopped -> status s d <> Failed -> mandatory c i ->
   acyclic t -> s <= t -> wires t (c,i) = Some d ->
   consistent (apply s (Wire c i d)).

Lemma consistent_wire_optional s c i d t: consistent s ->
   status s c = Started -> status s d = Started -> optional c i ->
   acyclic t -> s <= t -> wires t (c,i) = Some d ->
   consistent (apply s (Wire c i d)).

applying consistent down sequences containing particular operations actually perform these operations

Lemma apply_down_ics_unwires s l c i: In (Unwire c i) l -> ics s (map down l) ->
   wires (apply_down_seq s l) (c,i) = None.
Lemma apply_down_ics_fails s l c: In (Fail c) l -> ics s (map down l) ->
   status (apply_down_seq s l) c = Failed.

Lemma apply_down_ics_nofail s l c: status s c <> Failed -> ~In (Fail c) l -> ics s (map down l) ->
   status (apply_down_seq s l) c <> Failed.

Lemma apply_down_ics_stops s l c: In (Stop c) l -> ~In (Fail c) l -> ics s (map down l) ->
   status (apply_down_seq s l) c = Stopped.

abstract characterisation of saturated down sets

(generated by the propagation algorithms, represented by unsorted lists, with possible duplicates)

Definition xsaturated_down_set s l l' :=
   (forall c, In (Stop c) l ->
     (forall d i, mandatory d i -> wires s (d,i) = Some c -> status s d = Started -> In (Stop d) l') /\
     (forall d i, optional d i -> wires s (d,i) = Some c -> In (Unwire d i) l') /\
     (forall i, optional c i -> wires s (c,i) <> None -> In (Unwire c i) l') /\
     (status s c = Started )) /\
   (forall c i, In (Unwire c i) l ->
     (mandatory c i -> status s c = Started -> In (Stop c) l') /\
     wires s (c,i) <> None ) /\
   (forall c, In (Fail c) l ->
     (forall d i, wires s (d,i) = Some c -> In (Unwire d i) l') /\
     (forall i, wires s (c,i) <> None -> In (Unwire c i) l')
   ).
Definition saturated_down_set s l := xsaturated_down_set s l l.

auxiliary lemmas about saturated down sets

Lemma xsaturated_down_set_app s l1 l2 l':
   xsaturated_down_set s l1 l' ->
   xsaturated_down_set s l2 l' ->
   xsaturated_down_set s (l1++l2) l'.

Lemma xsaturated_down_set_incr s l l' l'':
   (forall o, In o l' -> In o l'') ->
   xsaturated_down_set s l l' ->
   xsaturated_down_set s l l''.

Lemma saturated_down_set_compat s h k: (forall o, In o h <-> In o k) ->
   (saturated_down_set s h <-> saturated_down_set s k).

merging two saturated down sets gives a saturated down set

Lemma merge_saturated_down_sets s h k:
saturated_down_set s h -> saturated_down_set s k -> saturated_down_set s (h++k).

the empty set is saturated

Lemma saturated_down_set_empty s: saturated_down_set s nil.

key lemma: sorting a saturated down set results in an incrementally consistent sequence

Lemma sorted_saturated_down_set_ics s l: consistent s ->
sorted (order_down_op (rank s)) l -> saturated_down_set s l -> ics s (map down l).

the propagation algorithms produce saturated down sets

auxiliary lemmas to reason about wires folding functions

Lemma fold_wires_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), wires s (c,i) = Some d -> P l -> P (f i++l)) ->
   P nil -> P (fold_wires s c f).

Lemma fold_optional_wires_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), optional c i -> wires s (c,i) = Some d -> P l -> P (f i++l)) ->
   P nil -> P (fold_optional_wires s c f).

Lemma fold_pointing_wires_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), wires s (d,i) = Some c -> P l -> P (f d i++l)) ->
   P nil -> P (fold_pointing_wires s c f).

Lemma fold_optional_pointing_wires_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), optional d i -> wires s (d,i) = Some c -> P l -> P (f d i++l)) ->
   P nil -> P (fold_optional_pointing_wires s c f).

Lemma fold_mandatory_pointing_components_wspec A (P: list A -> Prop) f s c:
   (forall d i (l: list A), mandatory d i -> wires s (d,i) = Some c -> P l -> P (f d++l)) ->
   P nil -> P (fold_mandatory_pointing_components s c f).

Section down.
  Variable s: arch.
  Hypothesis Hs: acyclic s.

analysis of the xpropagate_stop function

  Lemma xpropagate_stop_doesnotfail n:
    forall c d, ~In (Fail d) (xpropagate_stop n s c).

  Lemma xpropagate_stop_unwire n:
    forall c, rank s c < n ->
      let l := xpropagate_stop n s c in
        forall d i, In (Unwire d i) l ->
          (mandatory d i -> status s d = Started -> In (Stop d) l) /\
          (wires s (d,i) <> None ).

  Lemma xpropagate_stop_stops n:
    forall c, status s c = Started -> In (Stop c) (xpropagate_stop n s c).

  Lemma no_stop_in_fold_optional_pwires c d:
    In (Stop d) (fold_optional_pointing_wires s c (fun d i => Unwire d i::nil)) <-> False.

  Lemma no_stop_in_fold_optional_wires c d:
    In (Stop d) (fold_optional_wires s c (fun i => Unwire c i::nil)) <-> False.

  Lemma xpropagate_stop_only_stops_started n:
    forall c d, rank s c < n -> In (Stop d) (xpropagate_stop n s c) -> status s d = Started.

  Lemma xpropagate_stop_stops_mandatory_pointing n:
    forall c, rank s c < n ->
      forall e i d, In (Stop d) (xpropagate_stop n s c) ->
        mandatory e i -> wires s (e,i) = Some d -> status s e = Started ->
        In (Stop e) (xpropagate_stop n s c).

  Lemma xpropagate_stop_unwires_optional_pointing n:
    forall c, rank s c < n ->
      forall e i d, In (Stop d) (xpropagate_stop n s c) ->
        optional e i -> wires s (e,i) = Some d -> In (Unwire e i) (xpropagate_stop n s c).

  Lemma xpropagate_stop_unwires_optional n:
    forall c, rank s c < n ->
      forall i d, In (Stop d) (xpropagate_stop n s c) ->
        optional d i -> wires s (d,i) <> None -> In (Unwire d i) (xpropagate_stop n s c).

  Lemma propagate_stop_stops c: status s c = Started -> In (Stop c) (propagate_stop s c).

  Lemma propagate_stop_doesnotfail c d: ~In (Fail d) (propagate_stop s c).

propagate_stop is correct

  Theorem propagate_stop_saturated c: saturated_down_set s (propagate_stop s c).

  Lemma propagate_unwire_unwires c i: wires s (c,i) <> None -> In (Unwire c i) (propagate_unwire s c i).

  Lemma propagate_unwire_doesnotfail c i d: ~In (Fail d) (propagate_unwire s c i).

propagate_unwire is correct

  Theorem propagate_unwire_saturated c i: saturated_down_set s (propagate_unwire s c i).

  Lemma propagate_fail_fails c: status s c <> Failed -> In (Fail c) (propagate_fail s c).

  Lemma propagate_fail_case c:
    propagate_fail s c = fold_pointing_wires s c (propagate_unwire s)++
                         fold_wires s c (propagate_unwire s c)++Fail c::nil
    \/ propagate_fail s c = nil.

  Lemma propagate_fail_fails_once c d: In (Fail d) (propagate_fail s c) -> c=d.

propagate_fail is correct

Theorem propagate_fail_saturated c: saturated_down_set s (propagate_fail s c).

analysis of the down_diff function

  Lemma down_diff_saturated t: saturated_down_set s (down_diff s t).

  Lemma down_diff_stops t c:
    status s c = Started -> status t c = Stopped -> In (Stop c) (down_diff s t).

  Lemma down_diff_fails t c:
    status s c <> Failed -> status t c = Failed -> In (Fail c) (down_diff s t).

  Lemma down_diff_doesnotfailtoomuch t c: In (Fail c) (down_diff s t) -> status t c = Failed.

  Lemma down_diff_unwires t ci:
    needs_unwire (wires s ci) (wires t ci) = true -> In (Unwire (fst ci) (snd ci)) (down_diff s t).

End down.
Implicit Arguments sorted_sort [[X] [cmp] [H]].
Implicit Arguments In_sort [[X] [cmp] [H]].

down_diff generates ICSs

Lemma down_diff_ics e t: consistent e -> ics e (map down (sort (order_down_op (rank e)) (down_diff e t))).

the ICS obtained by down_diff brings the effective system to a state where the target can be reached by up operations only

Theorem down_diff_leless e t: consistent e -> e << t -> apply_down_seq e (sort (order_down_op (rank e)) (down_diff e t)) <<= t.

correctness of the up phase

Lemma in_up_diff_wire e t c i d: In (Wire c i d) (up_diff e t) -> wires e (c,i) = None /\ wires t (c,i) = Some d.

Lemma up_diff_wire e t c i d: wires e (c,i) = None -> wires t (c,i) = Some d -> In (Wire c i d) (up_diff e t).

Lemma in_up_diff_start e t c: In (Start c) (up_diff e t) -> status e c = Stopped /\ status t c = Started.

Lemma up_diff_start e t c: status e c = Stopped -> status t c = Started -> In (Start c) (up_diff e t).

Lemma up_step_consistent e t q x:
   (forall y : up_op, In y q -> order_up_op (rank t) x y = Lt) ->
   consistent e ->
   consistent t ->
   e <<= t ->
   (forall o : up_op, In o (x :: q) <-> In o (up_diff e t)) ->
   In x (up_diff e t) -> consistent (up_apply e x).

Lemma up_step_below e t x: e <<= t -> In x (up_diff e t) -> (up_apply e x) <<= t.

Lemma up_step_diff e t q x:
   (forall y : up_op, In y q -> order_up_op (rank t) x y = Lt) ->
   (forall o : up_op, In o (x :: q) <-> In o (up_diff e t)) ->
   In x (up_diff e t) ->
   forall o : up_op, In o q <-> In o (up_diff (apply e x) t).

up_diff generates ICSs

Theorem up_diff_ics e t: consistent e -> consistent t -> e <<= t ->
ics e (map up (sort (order_up_op (rank t)) (up_diff e t))).

up_diff brings the effective system to the target architecture

Theorem up_diff_complete e t: e <<= t -> apply_up_seq e (sort (order_up_op (rank t)) (up_diff e t)) == t.

correctness of the session commit algorithm, in the failure free case

the hypothesis e << t ensures that all failed components in e remain failed in t. In other words, we do not automatically repair failed components.

Theorem commit_seq_ics e t: consistent e -> consistent t -> e << t -> ics e (commit_seq e t).

Theorem commit_seq_complete e t: consistent e -> consistent t -> e << t -> apply_seq e (commit_seq e t) == t.

Handling failures

To model failures in Coq, which is a strongly deterministic system, we assume an arbitratry eapply function, that may return an exception. This function is specified by saying that:

either it returns a new architecture, in which case this architecture should be the one returned by our deterministic and failure-free apply function,
or it returns an exception concerning a component, which should not belong to the set of "already known to be failed components".

The remaining results are parametrised by this eapply function, which means that they hold for all such functions, i.e., for arbitrary sequences of failures.

Variable eapply: arch -> op -> list Component -> arch + Component.

Inductive eapply_ind e o fs: arch + Component -> Prop :=
| ei_nofailure: eapply_ind e o fs (inl _ (apply e o))
| ei_failure: forall c, ~In c fs -> eapply_ind e o fs (inr _ c).
Hypothesis eapply_spec: forall e o fs, eapply_ind e o fs (eapply e o fs).

applying a sequence of operations, until a potential failure occurs

Fixpoint eapply_seq e l fs :=
   match l with
     | nil => (e,None )
     | o::q =>
       match eapply e o fs with
         | inl e' => eapply_seq e' q fs
         | inr c => (e,Some c)
       end
   end.

Lemma eapply_seq_nofailure e e' l fs: eapply_seq e l fs = (e',None ) -> e' = apply_seq e l.

Lemma eapply_seq_failure e e' l c fs: eapply_seq e l fs = (e',Some c) ->
   ~In c fs /\ exists h, exists k, l=h++k /\ e' = apply_seq e h.

Inductive eapply_seq_ind e l fs: arch *option Component -> Prop :=
| esi_nofailure: eapply_seq_ind e l fs (apply_seq e l, None )
| esi_failure: forall h k c, l=h++k -> ~In c fs -> eapply_seq_ind e l fs (apply_seq e h, Some c).

Lemma eapply_seq_spec: forall e l fs, eapply_seq_ind e l fs (eapply_seq e l fs).

applying an ICS always returns a consistent architecture, even when interrupted by a failure

Lemma eapply_seq_consistent e l fs: ics e l -> consistent (fst (eapply_seq e l fs)).

propagating failures and producing recovery ICSs

Definition recover_failures_set e :=
fold_right (fun c acc => propagate_fail e c ++ acc) nil.
Definition recover_failures_seq e fs :=
map down (sort (order_down_op (rank e)) (recover_failures_set e fs)).

recovering a target is a single pass process

Definition recover_target t fs := apply_seq t (recover_failures_seq t fs).

on the contrary, we need a fixpoint to recover the effective system

Fixpoint xrecover_effective n e fs :=
   match n with O => (e,fs) | S n =>
     let ics := recover_failures_seq e fs in
     match eapply_seq e ics fs with
       | (e',None ) => (e',fs)
       | (e',Some c) => xrecover_effective n e' (c::fs)
     end
   end.
Definition recover_effective := xrecover_effective (S (cardinal Component)).

robust / roll-forward / roll-back algorithms

robust commit: in case of failures, we recover the effective system and stop

Definition robust_commit e t :=
   let ics := commit_seq e t in
   match eapply_seq e ics nil with
     | (e',None ) => (e',nil )
     | (e',Some c) => recover_effective e' (c::nil)
   end.

RFP commit: in case of failures, we recover both effective system and the target architecture, and we loop

Fixpoint xrfp_commit n e t :=
   match n with O => e | S n =>
     match robust_commit e t with
       | (e',nil ) => e'
       | (e',fs) =>
         let t' := recover_target t fs in
         xrfp_commit n e' t'
     end
   end.
Definition rfp_commit := xrfp_commit (cardinal Component).

RBP commit: in case of failures, we switch to RFP with the recovered inital architecture

Definition rbp_commit e t :=
   match robust_commit e t with
     | (e',nil ) => e'
     | (e',fs) =>
       let e0 := recover_target e fs in
         rfp_commit e' e0
   end.

correctness of the recovery phase

Lemma recover_failures_saturated s fs: consistent s -> saturated_down_set s (recover_failures_set s fs).

Lemma recover_failures_ics s fs: consistent s -> ics s (recover_failures_seq s fs).

Lemma recover_failures_failed e fs: consistent e -> forall c,
status (apply_seq e (recover_failures_seq e fs)) c = Failed ->
status e c = Failed \/ In c fs.

recover target

Lemma recover_target_consistent t fs: consistent t -> consistent (recover_target t fs).

Lemma recover_target_fails t fs c: consistent t -> In c fs -> status (recover_target t fs) c = Failed.

recover effective

Lemma xrecover_effective_consistent n: forall e fs, consistent e -> consistent (fst (xrecover_effective n e fs)).

Lemma recover_effective_consistent: forall e fs, consistent e -> consistent (fst (recover_effective e fs)).

Lemma xrecover_effective_fails n e fs c: In c fs -> In c (snd (xrecover_effective n e fs)).

Lemma recover_effective_fails e fs c: In c fs -> In c (snd (recover_effective e fs)).

Lemma xrecover_effective_failed n e fs: consistent e ->
   forall c, status (fst (xrecover_effective n e fs)) c = Failed ->
     status e c = Failed \/ In c (snd (xrecover_effective n e fs)).

Lemma recover_effective_failed e fs: consistent e ->
   forall c, status (fst (recover_effective e fs)) c = Failed ->
     status e c = Failed \/ In c (snd (recover_effective e fs)).

Definition xre_size fs := fold (fun c n => if mem c fs then n else S n) O.

Lemma xre_size_cons d fs:
   xre_size fs = if mem d fs || negb (mem d Component) then xre_size (d::fs) else S (xre_size (d::fs)).

Lemma xre_size_incr d fs: ~In d fs -> xre_size fs = S (xre_size (d::fs)).

Lemma xre_size_cardinal fs: xre_size fs < S (cardinal Component).

Lemma xrecover_effective_complete n e fs: xre_size fs < n -> consistent e ->
   forall c, In c (snd (xrecover_effective n e fs)) -> status (fst (xrecover_effective n e fs)) c = Failed.

Theorem recover_effective_complete e fs: consistent e ->
   forall c, In c (snd (recover_effective e fs)) -> status (fst (recover_effective e fs)) c = Failed.

correctness of the robust commit algorithm

we always get a consistent architecture

Theorem robust_commit_consistent e t:
consistent e -> consistent t -> e << t -> consistent (fst (robust_commit e t)).

at the end, failed components are declared in the failed set unless they were already failed in the target

Theorem robust_commit_failed e t: consistent e -> consistent t -> e << t ->
forall c, status (fst (robust_commit e t)) c = Failed ->
status t c = Failed \/ In c (snd (robust_commit e t)).

moreover, all components declared in the failed set are properly accounted as failed in the architecture

Theorem robust_commit_complete e t: consistent e -> consistent t -> e << t ->
forall c, In c (snd (robust_commit e t)) -> status (fst (robust_commit e t)) c = Failed.

correctness of the RFP algorithm

Theorem rfp_commit_consistent e t:
consistent e -> consistent t -> e << t -> consistent (rfp_commit e t).

correctness of the RBP algorithm

Note the additional hypothesis t << e, which means with e << t than e and t have the same sets of failed components This is required with this policy: if t contains more failed components, then we cannot roll-back to the initial architecture if a failure occurs after these components have been marked as failed. This is not a real restriction since it seems strange to have more failed components in the target architecture.

Theorem rbp_commit_consistent e t:
consistent e -> consistent t -> e << t -> t << e -> consistent (rbp_commit e t).

End s.

This page has been generated by coqdoc