Auxiliary lemmas for the soundness proof


Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 permission fslassn fslassnsem fslmodel fslassnlemmas.

Set Implicit Arguments.

Various helper lemmas


Hint Unfold imm_happens_before.

Lemma hupds A h l (y : A) : hupd h l y l = y.

Lemma hist_closed_trans :
   sb rf V (HC: hist_closed sb rf V)
    a b (TR: clos_refl_trans _ sb a b) (IN: In b V), In a V.

Lemma hist_closedD :
   sb rf V (HC: hist_closed sb rf V)
    a b (TR: happens_before_union_rf sb rf a b) (IN: In b V), In a V.

Lemma happens_before_trans lab sb rf mo a b c :
  happens_before lab sb rf mo a b
  happens_before lab sb rf mo b c
  happens_before lab sb rf mo a c.

Lemma happens_before_union_rf_trans sb rf a b c :
  happens_before_union_rf sb rf a b
  happens_before_union_rf sb rf b c
  happens_before_union_rf sb rf a c.

Lemma happens_before_sb lab (sb : relation actid) rf mo a b :
  sb a b happens_before lab sb rf mo a b.

Lemma happens_before_sw lab sb rf mo a b :
  synchronizes_with lab sb rf mo a b happens_before lab sb rf mo a b.

Lemma happens_before_union_rf_sb (sb : relation actid) rf a b :
  sb a b happens_before_union_rf sb rf a b.

Lemma happens_before_union_rf_rf (sb : relation actid) rf a b :
  rf b = Some a happens_before_union_rf sb rf a b.

Lemma clos_trans_hbE :
   lab sb rf mo a b (HB: clos_trans actid (happens_before lab sb rf mo) a b),
    happens_before lab sb rf mo a b.

Lemma clos_trans_hbUrfE :
   sb rf a b (HB: clos_trans actid (happens_before_union_rf sb rf) a b),
    happens_before_union_rf sb rf a b.

Hint Immediate clos_trans_hbE : hb.
Hint Immediate clos_trans_hbUrfE : hb.

Hint Resolve
  happens_before_sb happens_before_sw happens_before_union_rf_sb happens_before_union_rf_rf
  happens_before_trans happens_before_union_rf_trans t_step hist_closedD : hb.

Lemma count_implies :
   (T: eqType) (f1 f2 : T bool) (IMP : x, f1 x f2 x) l,
  count f1 l count f2 l.

Lemma hasP' :
   (T : eqType) (a : pred T) (l : list_predType T),
    reflect ( x : T, In x l a x) (has a l).

Lemma clos_refl_transE X rel a b :
    clos_refl_trans X rel a b a = b clos_trans X rel a b.

Lemma clos_refl_trans_hbE :
   lab sb rf mo a b,
    clos_refl_trans actid (happens_before lab sb rf mo) a b
    happens_before lab sb rf mo a b a = b.

Lemma clos_refl_trans_hbUrfE :
   sb rf a b,
    clos_refl_trans actid (happens_before_union_rf sb rf) a b
    happens_before_union_rf sb rf a b a = b.

Lemma release_seq_implies_hbUrf lab sb rf mo a b:
  release_seq lab sb rf mo a b
  clos_refl_trans _ (happens_before_union_rf sb rf) a b.

Lemma hb_implies_hbUrf lab sb rf mo a b:
  happens_before lab sb rf mo a b happens_before_union_rf sb rf a b.

Lemma helper_perm_filter_post :
   e T,
     posts_sb posts_rf,
      Permutation T (filter (fun x : hbcase(hb_fst x != e) || (x == hb_sink e)) T ++
                     map (hb_sb e) posts_sb ++
                     map (hb_rf e) posts_rf).

Lemma helper_filter_decide_sink: a T (ND: NoDup T),
      Permutation (filter (fun x : hbcase(hb_fst x != a) || (x == hb_sink a)) T)
        (if excluded_middle_informative (In (hb_sink a) T)
          then hb_sink a :: (filter (fun x : hbcasehb_fst x != a) T)
          else (filter (fun x : hbcasehb_fst x != a) T)).

Lemma has_rf_succs acts lab sb rf mo (a: actid) :
  ExecutionFinite acts lab sb
  ConsistentRF_basic lab sb rf mo
   (rfs: list actid),
    << NDrfs: NoDup rfs >>
    << INrfs: x, In x rfs rf x = Some a >>.

Lemma has_rf_pres acts lab sb rf mo a :
  ExecutionFinite acts lab sb
  ConsistentRF_basic lab sb rf mo
   rfs,
    << NDrfs: NoDup rfs >>
    << INrfs: x, In x rfs rf a = Some x >>.

Definition wf_ltof A (f : A nat) :
  well_founded (fun x yf x < f y).

A few lemmas about Permutations

Lemma In_implies_perm A (x : A) l (IN: In x l) :
   l', Permutation l (x :: l').

Lemma Permutation_count A l l' (P : Permutation (A:=A) l l') f :
  count f l = count f l'.

Lemma count_eq_0: A f (lst: list A), count f lst = 0 x (IN: In x lst), ¬ f x.

Lemma Permutation_hmap_valids PS PSg :
   l l' (P : Permutation l l') lab sb rf hmap,
    @hmap_valids PS PSg lab sb rf hmap l
    hmap_valids lab sb rf hmap l'.

Lemma Permutation_hmap_valids_strong PS PSg:
   l l' (P : Permutation l l') lab sb rf hmap,
    @hmap_valids_strong PS PSg lab sb rf hmap l
    hmap_valids_strong lab sb rf hmap l'.

Lemma Permutation_hist_closed :
   l l' (P : Permutation l l') sb rf,
    hist_closed sb rf l
    hist_closed sb rf l'.

Lemma Consistent_perm :
   acts lab sb rf mo sc mt (CONS : Consistent acts lab sb rf mo sc mt)
         acts' (EQ: perm_eq acts acts'),
    Consistent acts' lab sb rf mo sc mt.

Lemma weakConsistent_perm :
   acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts' (EQ: perm_eq acts acts'),
    weakConsistent acts' lab sb rf mo sc mt.

Lemma weakConsistent_Permutation :
   acts lab sb rf mo sc mt (CONS : weakConsistent acts lab sb rf mo sc mt)
         acts' (EQ: Permutation acts acts'),
    weakConsistent acts' lab sb rf mo sc mt.

Lemma Permutation_flatten A l l' (P : Permutation l l') :
  Permutation (A:=A) (flatten l) (flatten l').

Lemma AcyclicStrong_implies_IrreflexiveHBuRF:
   lab sb rf mo, AcyclicStrong lab sb rf mo IrreflexiveHBuRF sb rf.

Hint Resolve AcyclicStrong_implies_IrreflexiveHBuRF.

Depth metric


Definition is_pred A (rel : A A Prop) B a :=
  has (fun bmydec (clos_refl_trans A rel a b)) B.

Definition depth_metric A (rel: A A Prop) V a :=
  count (is_pred rel a) V.

Lemma clos_transK T (rel: relation T) x y :
  clos_trans _ (clos_trans _ rel) x y
  clos_trans _ rel x y.

Lemma clos_refl_transD T rel a b :
  clos_refl_trans T rel a b a = b clos_trans T rel a b.

Lemma depth_lt (rel : relation actid) V A B
  (HB : a, In a A ¬ In a B
         b, In b B rel a b)
  b (IN : In b B) (NIN: ¬ In b A)
  (NHB: a, In a A ¬ clos_trans _ rel b a)
  (SUB: b, In b B In b V) :
  depth_metric rel V A < depth_metric rel V B.

A useful induction principle for happens-before graphs.

Lemma edge_depth_ind lab sb rf V
  (ACYCLIC: IrreflexiveHBuRF sb rf)
  (HC: hist_closed sb rf V) (P : hbcase Prop) :
  ( edge
    (IH: edge' (EV : edge_valid lab sb rf edge')
            (LT: happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)),
      P edge')
    (EV : edge_valid lab sb rf edge)
    (IN : In (hb_fst edge) V),
    P edge)
   edge (EV : edge_valid lab sb rf edge), In (hb_fst edge) V P edge.

Fixpoint find_max A (curr : A) f l :=
  match l with
    | nilcurr
    | x :: xs
      if f curr f x then find_max x f xs else find_max curr f xs
  end.

Lemma find_max_range :
   A (curr: A) f l,
    In (find_max curr f l) (curr :: l).

Lemma find_max_greatest :
   A (x curr: A) f l (IN: In x (curr :: l)),
    f x f (find_max curr f l).

Given a non-empty set of edges, T, there is always an edge whose source node does not happen before any of the sources of the other edges.

Lemma get_deepest :
   sb rf (ACYCLIC: IrreflexiveHBuRF sb rf)
         V (HC: hist_closed sb rf V)
         T (NNIL: T nil)
         (INCL: edge (IN: In edge T), In (hb_fst edge) V),
   edge,
    << IN: In edge T >>
    << INe: In (hb_fst edge) V >>
    << DEEP: edge' (IN': In edge' T)
                 (HB': happens_before_union_rf sb rf (hb_fst edge) (hb_fst edge')),
               False >>.

Fixpoint find_min A (curr : A) f l :=
  match l with
    | nilcurr
    | x :: xs
      if f x f curr then find_min x f xs else find_min curr f xs
  end.

Lemma find_min_range :
   A (curr: A) f l,
    In (find_min curr f l) (curr :: l).

Lemma find_min_greatest :
   A (x curr: A) f l (IN: In x (curr :: l)),
    f (find_min curr f l) f x.

Lemma get_shallow :
   lab sb rf mo (ACYCLIC: AcyclicStrong lab sb rf mo)
         V (HC: hist_closed sb rf V)
         T (HC': hist_closed sb rf (V ++ T)) (NNIL: T nil),
   e,
    << IN: In e T >>
    << HC: hist_closed sb rf (e :: V) >>.

Some lemmas about validly annotated nodes

RF-edges carry only HLnabla labels

Lemma no_normals_on_rf PS PSg :
   lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    a b (RF: rf b = Some a) hmap (VALID: hmap_valid lab sb rf hmap ga a)
    hfr gr (MAP: hmap (hb_rf a b) = Hdef hfr gr) l (ALL: hfr l @HVnone PS PSg)
    (NORMAL: HVlabeled (hfr l) HLnormal),
  False.

Lemma no_normals_on_rf2 PS PSg :
   lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    a b (RF: rf b = Some a) hmap (VALID: hmap_valid lab sb rf hmap ga b)
    hfr gr (MAP: hmap (hb_rf a b) = Hdef hfr gr) l (ALL: hfr l @HVnone PS PSg)
    (NORMAL: HVlabeled (hfr l) HLnormal),
  False.

Lemma triangles_never_on_rf PS PSg:
edge lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (EV: edge_valid lab sb rf edge) hmap (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (ALL: hf l @HVnone PS PSg) (LAB: HVlabeled (hf l) HLtriangle),
  is_sb edge is_sink edge.

Lemma triangles_never_on_rf2 PS PSg:
edge lab sb rf mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (EV: edge_valid lab sb rf edge) hmap
    (VALID: b, hb_snd edge = Some b hmap_valid lab sb rf hmap ga b)
    hf g (MAP: hmap edge = Hdef hf g) l (ALL: hf l @HVnone PS PSg) (LAB: HVlabeled (hf l) HLtriangle),
  is_sb edge.

The heap on the incoming edge of a fence node is defined.

Lemma FenceInDEF PS PSg:
   hmap pre post e hF hrel hrel' hacq hacq' gnew
    (DEF: hmap (hb_sb e post) @Hundef PS PSg)
    (pEQ: hmap (hb_sb pre e) = hF +!+ hrel +!+ hacq)
    (qEQ: hmap (hb_sb e post) = hF +!+ hrel' +!+ hacq' +!+ gheap _ _ gnew)
    (RELsim: Hsim hrel hrel')
    (ACQsim: Hsim hacq hacq'),
   hf g, hmap (hb_sb pre e) = Hdef hf g.

Heaps on the incoming edges of an RMW node are compatible.

Lemma RMWinDEF PS PSg:
   hmap pre e post rfsIn rfsOut l hrel hrel' hacq hacq' ht hF P QQ v' sbg rfg
    (DEF: hmap (hb_sb e post) +!+ hsum (map hmap (map (hb_rf e) rfsOut))
          +!+ hmap (hb_sink e) @Hundef PS PSg)
    (pEQ: hmap (hb_sb pre e) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
                                +!+ hrel +!+ hF )
    (qEQ: hmap (hb_sb e post) = hsingl _ _ l (HVra (hupd Wemp v' P) QQ true (Some HLCnormal) (Some HLCnormal))
                                +!+ hacq' +!+ hF +!+ sbg)
    (rInEQ: hsum (map hmap (map (hb_rf^~ e) rfsIn)) = hacq +!+ ht)
    (rOutEQ: hsum (map hmap (map (hb_rf e) rfsOut)) +!+ hmap (hb_sink e) = hrel' +!+ ht +!+ rfg)
    (RELsim: Hsim hrel hrel') (ACQsim: Hsim hacq hacq'),
   hf g, hmap (hb_sb pre e) +!+ hsum (map hmap (map (hb_rf^~ e) rfsIn)) = Hdef hf g.

Ltac RMWin_def := exploit RMWinDEF; try eassumption; rewrite <- hdef_alt; intro DEFin; [].

Ltac RMWin_heap := exploit RMWinDEF; try eassumption; intro DEFin; desc; [].

Every validly annotated memory access contains the accessed location in the domain of the heap of its incoming sb-edge.

Lemma valid_accessD PS PSg:
   lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (Aa : is_access (lab a)),
   pre hf g,
    sb pre a hmap (hb_sb pre a) = Hdef hf g
     hf (loc (lab a)) @HVnone PS PSg HVlabeled (hf (loc (lab a))) HLnormal.

Lemma valid_na_accessD PS PSg :
   lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (NA : is_na (lab a)) pre
         (SB : sb pre a) hf g
         (HM : hmap (hb_sb pre a) = @Hdef PS PSg hf g),
  is_nonatomic (hf (loc (lab a))).

Lemma valid_readD PS PSg :
   lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (Ra : is_read (lab a)),
   pre hf g,
    sb pre a hmap (hb_sb pre a) = @Hdef PS PSg hf g
     HVlabeledR (hf (loc (lab a))) HLnormal.

Lemma valid_writeD PS PSg :
   lab sb rf hmap ga a
         (VALID : hmap_valid lab sb rf hmap ga a)
         (Wa : is_write (lab a)),
   pre hf g,
    sb pre a hmap (hb_sb pre a) = @Hdef PS PSg hf g
    (is_lvalue (hf (loc (lab a))) is_atomic (hf (loc (lab a)))).

Lemma hmap_defined_in PS PSg:
   lab sb rf hmap mo ga (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge b (VALID: hmap_valid lab sb rf hmap ga b)
    (EV: edge_valid lab sb rf edge)
    (IN: hb_snd edge = Some b),
   hf g, hmap edge = @Hdef PS PSg hf g.

Lemma hmap_defined_out PS PSg:
   lab sb rf hmap ga mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge a (VALID: hmap_valid lab sb rf hmap ga a)
    (EV: edge_valid lab sb rf edge)
    (IN: hb_fst edge = a),
   hf g, hmap edge = @Hdef PS PSg hf g.

This page has been generated by coqdoc