ihc

Independent heap compatibility

Require Import Vbase Varith.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslmodel fslassnlemmas fslhmap.
Set Implicit Arguments.

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 mo hmap edge h l
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (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)
    (NAr: ∀ x h, rf (hb_fst edge) = Some x →
                      hmap (hb_rf 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 :
  ∀ lab sb rf mo hmap V
    (ACYCLIC: IrreflexiveHBuRF sb rf )
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf 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_union_rf sb rf) c (hb_fst edge).

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 sb rf T :=
  ∀ edge1 (IN1: In edge1 T) edge2 (IN2: In edge2 T)
      (HB: ∃ e, hb_snd edge1 = Some e ∧
           (e = hb_fst edge2 ∨ happens_before_union_rf sb rf e (hb_fst edge2))),
    False.

Lemma go_back_one :
  ∀ acts lab sb rf mo
    (FIN: ExecutionFinite acts lab sb)
    (CONS_RF: ConsistentRF_basic 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_rf posts_sb posts_rf,
     NoDup pres_sb ∧
     NoDup pres_rf ∧
     NoDup posts_sb ∧
     NoDup posts_rf ∧
     (∀ x : actid, In x pres_sb ↔ sb x e ) ∧
     (∀ x : actid, In x pres_rf ↔ rf e = Some x ) ∧
     (∀ x : actid, In x posts_sb ↔ sb e x ) ∧
     (∀ x : actid, In x posts_rf ↔ rf x = Some e ) ∧
     (∀ h
       (EQ: hsum (map hmap (map (hb_sb ^~ e) pres_sb)) +!+
            hsum (map hmap (map (hb_rf ^~ e) pres_rf)) +!+ hFR =
            Hdef h),
      let hS := if excluded_middle_informative (ann_sink lab e) then hmap (hb_sink e) else hemp in
      ∃ h0 : val → HeapVal ,
        hsum (map hmap (map (hb_sb e) posts_sb)) +!+
        hsum (map hmap (map (hb_rf e) posts_rf)) +!+ hS +!+ hFR =
        Hdef h0 ).
Lemma get_pres_aux :
  ∀ sb rf V a
    (HC : hist_closed sb rf V)
    (IN : In a V),
   ∃ pres_sb pres_rf,
     << NDb : NoDup pres_sb >> ∧
     << NDr : NoDup pres_rf >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x a >> ∧
     << Pr : ∀ x, In x pres_rf ↔ rf a = Some x >>.

Lemma get_pres :
  ∀ lab sb rf V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (HC : hist_closed sb rf 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_union_rf sb rf (hb_fst edge) (hb_fst edge´) → False)
    (IND: independent sb rf T),
   ∃ pres_sb pres_rf,
     let res := map (fun x ⇒ hb_sb x (hb_fst edge)) pres_sb ++
                map (fun x ⇒ hb_rf x (hb_fst edge)) pres_rf ++
                filter (fun x : hbcase ⇒ hb_fst x != hb_fst edge) T in
     << NDb : NoDup pres_sb >> ∧
     << NDr : NoDup pres_rf >> ∧
     << Pb : ∀ x, In x pres_sb ↔ sb x (hb_fst edge) >> ∧
     << Pr : ∀ x, In x pres_rf ↔ rf (hb_fst edge) = Some x >> ∧
     << ND´ : NoDup res >> ∧
     << METR: (depth_metric (happens_before_union_rf sb rf) V (map hb_fst res) <
               depth_metric (happens_before_union_rf sb rf) 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 sb rf res >>.

The main independent heap compatibility lemma.

Theorem independent_heap_compat :
  ∀ acts lab sb rf mo
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab) hmap V
    (HC: hist_closed sb rf 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_rf a b) T), In a V)
      (Ssink: ∀ a (IN: In (hb_sink a) T), In a V)
      (TSB: ∀ a b (IN: In (hb_sb a b) T), sb a b)
      (TSW: ∀ a b (IN: In (hb_rf a b) T), rf b = Some a)
      (Tsink: ∀ a (IN: In (hb_sink a) T), ann_sink lab a)
    (INDEP: independent sb rf T),
    ∃ h, hsum (map hmap T) = Hdef h.

A helper lemma for showing that two edges are independent

Lemma independent_two :
  ∀ lab sb rf edge edge´,
    IrreflexiveHBuRF sb rf →
    edge_valid lab sb rf edge →
    edge_valid lab sb rf edge´ →
    hb_snd edge ≠ Some (hb_fst edge´) →
    hb_snd edge´ ≠ Some (hb_fst edge) →
    (¬ ∃ b, hb_snd edge = Some b ∧ happens_before_union_rf sb rf b (hb_fst edge´)) →
    (¬ ∃ b´, hb_snd edge´ = Some b´ ∧ happens_before_union_rf sb rf b´ (hb_fst edge )) →
    independent sb rf (edge :: edge´ :: nil).

A helper lemma for showing that two edges are not independent

Lemma not_independent_two:
  ∀ acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf V) (VALID: hmap_valids lab sb rf hmap V)
    edge1 edge2 (DIF: edge1 ≠ edge2) (IN1: In (hb_fst edge1) V) (IN1: In (hb_fst edge2) V)
    (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
    hf1 hf2 (MAP1: hmap edge1 = Hdef hf1) (MAP2: hmap edge2 = Hdef hf2)
    l (ALL1: hf1 l ≠ HVnone) (ALL2: hf2 l ≠ HVnone) (NA: is_nonatomic (hf1 l) ∨ is_nonatomic (hf2 l)),
  ¬ independent sb rf (edge1 :: edge2 :: nil).

Edges that are dependent are connected trough HBuRF

Lemma destruct_not_independent_two:
  ∀ lab sb rf (ACYCLIC: IrreflexiveHBuRF sb rf)
  edge1 edge2 (EV1: edge_valid lab sb rf edge1) (EV2: edge_valid lab sb rf edge2)
  (DEP: ¬ independent sb rf (edge1 :: edge2 :: nil)),
  (∃ b1, hb_snd edge1 = Some b1 ∧ clos_refl_trans _ (happens_before_union_rf sb rf) b1 (hb_fst edge2)) ∨
  (∃ b2, hb_snd edge2 = Some b2 ∧ clos_refl_trans _ (happens_before_union_rf sb rf) b2 (hb_fst edge1)).

This page has been generated by coqdoc