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 rslassn rslmodel rslassnlemmas.

Set Implicit Arguments.

Lemmas about view shifts

Lemma vshift_refl h : vshift h h.

Lemma vshift_eqI x y : x = y → vshift x y.

Lemma vshift_trans h1 h2 h3: vshift h1 h2 → vshift h2 h3 → vshift h1 h3.

Lemma vshift_star_l :
  ∀ h h1 h1' (V1: vshift h1 h1'),
    vshift (hplus h1 h) (hplus h1' h).

Lemma vshift_star :
  ∀ h1 h1' (V1: vshift h1 h1') h2 h2' (V1: vshift h2 h2'),
    vshift (hplus h1 h2) (hplus h1' h2').

Lemma vshift_star_def :
  ∀ h1 h1' (V1: vshift h1 h1') h (D: hplus h1 h ≠ Hundef),
    hplus h1' h ≠ Hundef.

Lemma vshift_def :
  ∀ hf y,
    vshift (Hdef hf) y →
    ∃ hf', y = Hdef hf'.

Lemma vshift_nalloc :
  ∀ hf hf' l,
    vshift (Hdef hf) (Hdef hf') →
    hf l = HVnone →
    hf' l = HVnone.

Lemma vshift_val :
  ∀ hf hf' l,
    vshift (Hdef hf) (Hdef hf') →
    is_val (hf' l) →
    hf' l = hf l.

Lemma vshift_ra :
  ∀ hf hf' l PP QQ isrmw init,
    vshift (Hdef hf) (Hdef hf') →
    hf' l = HVra PP QQ isrmw init →

    ∃ PP' QQ' isrmw' init',
      hf l = HVra PP' (fun v ⇒ mk_assn_mod (Astar (sval (QQ v)) (QQ' v))) isrmw' init'
      ∧ (∀ v, implies (sval (PP v)) (sval (PP' v)))
      ∧ (isrmw → isrmw')
      ∧ (init → init').

Lemma vshift_hack:
  ∀ x y, vshift x y ↔ x = y.

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 :
  ∀ mt lab sb rf mo V (HC: hist_closed mt lab sb rf mo V)
    a b (TR: clos_refl_trans _ sb a b) (IN: In b V), In a V.

Lemma hist_closedD :
  ∀ mt lab sb rf mo V (HC: hist_closed mt lab sb rf mo V)
    a b (TR: happens_before lab sb rf mo 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_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_ann_sw lab sb rf mo a b :
  ann_sw lab rf a b → happens_before lab sb rf mo 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.

Hint Immediate clos_trans_hbE : hb.

Hint Resolve
  happens_before_sb happens_before_sw happens_before_ann_sw
  happens_before_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 helper_perm_filter_post :
  ∀ e T,
    ∃ posts_sb posts_sw,
      Permutation T (filter (fun x : hbcase ⇒ hb_fst x != e) T ++
                     map (hb_sb e) posts_sb ++
                     map (hb_sw e) posts_sw).

Lemma has_sw_succs acts lab sb rf a :
  ExecutionFinite acts lab sb →
  ∃ sws,
    << NDsws: NoDup sws >> ∧
    << INsws: ∀ x, In x sws ↔ ann_sw lab rf a x >>.

Lemma has_sw_pres acts lab sb rf a :
  ExecutionFinite acts lab sb →
  ∃ sws,
    << NDsws: NoDup sws >> ∧
    << INsws: ∀ x, In x sws ↔ ann_sw lab rf x a >>.

Definition wf_ltof A (f : A → nat) :
  well_founded (fun x y ⇒ f 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 Permutation_hmap_valids :
  ∀ l l' (P : Permutation l l') lab sb rf hmap,
    hmap_valids lab sb rf hmap l →
    hmap_valids lab sb rf hmap l'.

Lemma Permutation_hist_closed :
  ∀ l l' (P : Permutation l l') mt lab sb rf mo,
    hist_closed mt lab sb rf mo l →
    hist_closed mt lab sb rf mo 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 hc_edge_irr acts lab sb rf mo sc mt :
  weakConsistent acts lab sb rf mo sc mt →
  irreflexive (hc_edge mt lab sb rf mo).

Depth metric

Definition is_pred A (rel : A → A → Prop) B a :=
  has (fun b ⇒ mydec (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 mt lab sb rf mo V
  (ACYCLIC: IrreflexiveHB lab sb rf mo)
  (HC: hist_closed mt lab sb rf mo V) (P : hbcase → Prop) :
  (∀ edge
    (IH: ∀ edge' (EV : edge_valid lab sb rf edge')
            (LT: happens_before lab sb rf mo (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.

Lemma edge_depth_ind2 mt lab sb rf mo V
  (ACYCLIC: acyclic (hc_edge mt lab sb rf mo))
  (HC: hist_closed mt lab sb rf mo V) (P : hbcase → Prop) :
  (∀ edge
    (IH: ∀ edge' (EV : edge_valid lab sb rf edge')
            (LT: clos_trans _ (hc_edge mt lab sb rf mo) (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
    | nil ⇒ curr
    | 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 :
  ∀ lab sb rf mo (ACYCLIC: IrreflexiveHB lab sb rf mo)
         mt V (HC: hist_closed mt lab sb rf mo 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 lab sb rf mo (hb_fst edge) (hb_fst edge')),
               False >>.

Fixpoint find_min A (curr : A) f l :=
  match l with
    | nil ⇒ curr
    | 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 :
  ∀ mt lab sb rf mo (ACYCLIC: with_mt mt AcyclicMedium AcyclicStrong lab sb rf mo)
         V (HC: hist_closed mt lab sb rf mo V)
         T (HC': hist_closed mt lab sb rf mo (V ++ T)) (NNIL: T ≠ nil),
  ∃ e,
    << IN: In e T >> ∧
    << HC: hist_closed mt lab sb rf mo (e :: V) >>.

Memory safety

In order to prove memory safety, we need two auxiliary lemmas.

1. If a location, l, is not in the domain of any of the annotated heap on the incoming edges of a validly allocated node, and it is in the domain of the heap annotated on some outgoing edge, then that node must be an allocation node.

Lemma only_alloc_allocates:
  ∀ lab sb rf hmap edge h l
    (VAL: hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge)
    (HM : hmap edge = Hdef h)
    (ALL: h l ≠ HVnone)
    (NAb: ∀ x h, sb x (hb_fst edge) →
                      hmap (hb_sb x (hb_fst edge)) = Hdef h → h l = HVnone)
    (NAw: ∀ x h, ann_sw lab rf x (hb_fst edge) →
                      hmap (hb_sw x (hb_fst edge)) = Hdef h → h l = HVnone),
    lab (hb_fst edge) = Aalloc l.

2. If a location, l, is in the domain of some validly annotated edge, then there must be a node before that edge that allocated l.

Lemma heap_loc_allocated :
  ∀ mt lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l (LA: h l ≠ HVnone),
  ∃ c,
    lab c = Aalloc l ∧
    clos_refl_trans _ (happens_before lab sb rf mo) c (hb_fst edge).

Memory safety follows from the previous lemma.

Theorem valid_implies_mem_safe :
  ∀ mt lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V),
  mem_safe V lab sb rf mo.

Independent heap compatibitity

A list of edges, T, is independent iff there are no two edges in T such that the one happens before the other.

Definition independent lab sb rf mo T :=
  ∀ edge1 (IN1: In edge1 T) edge2 (IN2: In edge2 T)
      (HB: hb_snd edge1 = hb_fst edge2 ∨
           happens_before lab sb rf mo (hb_snd edge1) (hb_fst edge2)),
    False.

Lemma go_back_one :
  ∀ acts lab sb rf mo
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A : ConsistentAlloc lab) hmap e
    (VALID : hmap_valid lab sb rf hmap e) hFR
    (ALLOC : ∀ hf loc,
               hFR = Hdef hf → hf loc ≠ HVnone →
               ∃ c, lab c = Aalloc loc ∧ c ≠ e),
   ∃ pres_sb pres_sw posts_sb posts_sw,
     NoDup pres_sb ∧
     NoDup pres_sw ∧
     NoDup posts_sb ∧
     NoDup posts_sw ∧
     (∀ x : actid, In x pres_sb ↔ sb x e ) ∧
     (∀ x : actid, In x pres_sw ↔ ann_sw lab rf x e ) ∧
     (∀ x : actid, In x posts_sb ↔ sb e x ) ∧
     (∀ x : actid, In x posts_sw ↔ ann_sw lab rf e x ) ∧
     (∀ h
       (EQ: hsum (map hmap (map (hb_sb ^~ e) pres_sb)) +!+
            hsum (map hmap (map (hb_sw ^~ e) pres_sw)) +!+ hFR =
            Hdef h),
      ∃ h0 : val → HeapVal ,
        hsum (map hmap (map (hb_sb e) posts_sb)) +!+
        hsum (map hmap (map (hb_sw e) posts_sw)) +!+ hFR =
        Hdef h0 ).

Lemma get_pres_aux :
  ∀ mt lab sb rf mo V a
    (HC : hist_closed mt lab sb rf mo V)
    (IN : In a V),
   ∃ pres_sb pres_sw,
     << NDb : NoDup pres_sb >> ∧
     << NDw : NoDup pres_sw >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x a >> ∧
     << Pw : ∀ x, In x pres_sw ↔ ann_sw lab rf x a >>.

Lemma get_pres :
  ∀ mt lab sb rf mo V
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (HC : hist_closed mt lab sb rf mo V) edge T
    (ND : NoDup T)
    (IN : In edge T)
    (INCL : ∀ edge, In edge T → In (hb_fst edge) V)
    (EVS : ∀ edge, In edge T → edge_valid lab sb rf edge)
    (DEEP : ∀ edge', In edge' T →
              happens_before lab sb rf mo (hb_fst edge) (hb_fst edge') → False)
    (IND: independent lab sb rf mo T),
   ∃ pres_sb pres_sw,
     let res := map (fun x ⇒ hb_sb x (hb_fst edge)) pres_sb ++
                map (fun x ⇒ hb_sw x (hb_fst edge)) pres_sw ++
                filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T in
     << NDb : NoDup pres_sb >> ∧
     << NDw : NoDup pres_sw >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x (hb_fst edge) >> ∧
     << Pw : ∀ x, In x pres_sw ↔ ann_sw lab rf x (hb_fst edge) >> ∧
     << ND' : NoDup res >> ∧
     << METR: (depth_metric (happens_before lab sb rf mo) V (map hb_fst res) <
               depth_metric (happens_before lab sb rf mo) V (map hb_fst T) : Prop) >> ∧
     << INCL': ∀ edge, In edge res → In (hb_fst edge) V >> ∧
     << EVS' : ∀ edge, In edge res → edge_valid lab sb rf edge >> ∧
     << IND' : independent lab sb rf mo res >>.

The main independent heap compatibility lemma.

Theorem independent_heap_compat :
  ∀ acts lab sb rf mo
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab) mt hmap V
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V)
    T (ND: NoDup T)
      (SSB: ∀ a b (IN: In (hb_sb a b) T), In a V)
      (SSW: ∀ a b (IN: In (hb_sw a b) T), In a V)
      (TSB: ∀ a b (IN: In (hb_sb a b) T), sb a b)
      (TSW: ∀ a b (IN: In (hb_sw a b) T), ann_sw lab rf a b)
    (INDEP: independent lab sb rf mo T),
    ∃ h, hsum (map hmap T) = Hdef h.

A helper lemma for showing that two edges are independent

Lemma independent_two :
  ∀ lab sb rf mo e e',
    IrreflexiveHB lab sb rf mo →
    edge_valid lab sb rf e →
    edge_valid lab sb rf e' →
    hb_snd e ≠ hb_fst e' →
    hb_snd e' ≠ hb_fst e →
    ¬ happens_before lab sb rf mo (hb_snd e) (hb_fst e') →
    ¬ happens_before lab sb rf mo (hb_snd e') (hb_fst e) →
    independent lab sb rf mo (e :: e' :: nil).

Race freedom

In order to establish race freedom, we need two auxliary lemmas.

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

Lemma valid_accessD :
  ∀ lab sb rf hmap a
         (VALID : hmap_valid lab sb rf hmap a)
         (Aa : is_access (lab a)),
  ∃ pre hf,
    sb pre a ∧ hmap (hb_sb pre a) = Hdef hf
    ∧ hf (loc (lab a)) ≠ HVnone.

2. The heap of every validly annotated non-atomic memory access maps the accessed location to some value.

Lemma valid_na_accessD :
  ∀ lab sb rf hmap a
         (VALID : hmap_valid lab sb rf hmap a)
         (NA : is_na (lab a)) pre
         (SB : sb pre a) hf
         (HM : hmap (hb_sb pre a) = Hdef hf),
  is_val (hf (loc (lab a))).

Race-freedom follows from these two lemmas and independent heap compatibility.

Theorem valid_implies_race_free :
  ∀ mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHB lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed mt lab sb rf mo V)
    (VALID: hmap_valids lab sb rf hmap V),
  race_free V lab sb rf mo.

This page has been generated by coqdoc Imprint | Data protection