Independent heap compatibility


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

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 PS PSg:
  ∀ lab sb rf mo hmap ga edge h g l
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (VAL: hmap_valid lab sb rf hmap ga (hb_fst edge))
    (EV : edge_valid lab sb rf edge)
    (HM : hmap edge = Hdef h g)
    (ALL: h l ≠ @HVnone PS PSg)
    (NAb: ∀ x h g, sb x (hb_fst edge) →
                      hmap (hb_sb x (hb_fst edge)) = Hdef h g → h l = @HVnone PS PSg)
    (NAr: ∀ x h g, rf (hb_fst edge) = Some x →
                      hmap (hb_rf x (hb_fst edge)) = Hdef h g → h l = @HVnone PS PSg),
    lab (hb_fst edge) = Aalloc l.

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 PS PSg :
  ∀ 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 g (GET: hmap edge = Hdef h g) l (LA: h l ≠ @HVnone PS PSg),
  ∃ 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.

Allocating new ghosts cannot destroy compatibility.

Lemma new_ghosts_are_ok PS PSg:
  ∀ h h' g hfs gs
    (DEF: h +!+ gheap _ _ g ≠ @Hundef PS PSg ) (DEF': h +!+ h' = Hdef hfs gs)
    (GHOSTS: ∀ hf' g' loc, h' = Hdef hf' g' → g' loc ≠ None → g loc = None),
  h +!+ gheap _ _ g +!+ h' = Hdef hfs (gres_plus_total g gs).

Lemma hsingl_with_ghosts_is_ok PS PSg:
  ∀ l hv h g hfs gs (DEF: h +!+ gheap _ _ g ≠ @Hundef PS PSg) (DEF': hsingl _ _ l hv +!+ h = Hdef hfs gs),
  hsingl _ _ l hv +!+ h +!+ gheap _ _ g = Hdef hfs (gres_plus_total g gs).

Lemma go_back_one PS PSg :
  ∀ acts lab sb rf mo ga
    (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 ga e) hFR
    (ALLOC : ∀ hf g loc,
               hFR = Hdef hf g → hf loc ≠ @HVnone PS PSg →
               ∃ c, lab c = Aalloc loc ∧ c ≠ e)
    (GHOSTS: ∀ hf g loc,
               hFR = Hdef hf g → g loc ≠ None →
               ga loc ≠ Some 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 g
      (EQ: hsum (map hmap (map (hb_sb^~ e) pres_sb)) +!+
           hsum (map hmap (map (hb_rf^~ e) pres_rf)) +!+ hFR =
           Hdef h g),
     let hS := if excluded_middle_informative (ann_sink lab e) then hmap (hb_sink e) else hemp in
     ∃ h0 g0,
       hsum (map hmap (map (hb_sb e) posts_sb)) +!+
       hsum (map hmap (map (hb_rf e) posts_rf)) +!+ hS +!+ hFR =
       Hdef h0 g0).

Lemma step_back_ghost PS PSg:
  ∀ lab sb rf mo (CONS_RF: ConsistentRF_basic lab sb rf mo)
    edge (EV: edge_valid lab sb rf edge)
    hmap ga (VALID: hmap_valid lab sb rf hmap ga (hb_fst edge))
    hf g (MAP: hmap edge = Hdef hf g) l (GALL: g l ≠ None),
  << GA: ga l = Some (hb_fst edge) >> ∨
  ∃ edge' hf' g', << CON: hb_snd edge' = Some (hb_fst edge) >> ∧
                       << EV': edge_valid lab sb rf edge' >> ∧
                       << MAP': hmap edge' = @Hdef PS PSg hf' g' >> ∧
                       << GALL': g' l ≠ None >>.

Lemma ghost_allocated PS PSg :
  ∀ lab sb rf mo hmap ga V
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (HC: hist_closed sb rf V)
    (VALID: ∀ e : actid, In e V → hmap_valid lab sb rf hmap ga e)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h g (GET: hmap edge = @Hdef PS PSg h g) l
    (GL: g l ≠ None),
  ∃ edge',
    edge_valid lab sb rf edge' ∧
    ga l = Some (hb_fst edge') ∧
    (edge' = edge ∨ happens_before_union_rf sb rf (hb_fst edge') (hb_fst edge)).

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 PS PSg :
  ∀ 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 g, hsum (map hmap T) = @Hdef PS PSg h g.

Helper lemmas 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).

Lemma independent_when_sharing_first_node:
  ∀ lab sb rf (ACYCLIC: IrreflexiveHBuRF sb rf)
    edge1 (EV1: edge_valid lab sb rf edge1)
    edge2 (EV2: edge_valid lab sb rf edge2)
    (FST: hb_fst edge1 = hb_fst edge2),
  independent sb rf (edge1 :: edge2 :: nil).

Lemma independent_when_sharing_second_node:
  ∀ lab sb rf (ACYCLIC: IrreflexiveHBuRF sb rf)
    edge1 (EV1: edge_valid lab sb rf edge1)
    edge2 (EV2: edge_valid lab sb rf edge2)
    (FST: hb_snd edge1 = hb_snd edge2),
  independent sb rf (edge1 :: edge2 :: nil).

A helper lemma for showing that two edges are not independent
Lemma not_independent_two PS PSg:
  ∀ 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 g1 hf2 g2 (MAP1: hmap edge1 = Hdef hf1 g1 ) (MAP2: hmap edge2 = Hdef hf2 g2)
    l (ALL1: hf1 l ≠ @HVnone PS PSg) (ALL2: hf2 l ≠ @HVnone PS PSg) (NA: is_lvalue (hf1 l) ∨ is_lvalue (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