Lemmas about non-atomic accesses


Require Import Vbase.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 rslassn rslassnlemmas rslmodel rslhmap.

Set Implicit Arguments.

Lemma go_back_one_val :
   lab sb rf hmap edge
    (VALID : hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET : hmap edge = Hdef hf) l v
    (LA : hf l = HVval v)
    (NW: ¬ is_writeLV (lab (hb_fst edge)) l v),
   edge',
    edge_valid lab sb rf edge'
    hb_snd edge' = hb_fst edge
    ¬ is_writeL (lab (hb_fst edge)) l
     hf', hmap edge' = Hdef hf'
                hf' l = HVval v.

Lemma heap_loc_na_initialized2 :
   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)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l v (LA: h l = HVval v),
   cpre c hf,
    sb cpre c
    is_writeLV (lab c) l v
    hmap (hb_sb cpre c) = Hdef hf
    is_val (hf l)
    (c = hb_fst edge happens_before lab sb rf mo c (hb_fst edge))
    ( d
      (HB1: d = hb_fst edge happens_before lab sb rf mo d (hb_fst edge))
      (HB2: happens_before lab sb rf mo c d),
      ¬ is_writeL (lab d) l).
Lemma hc_edge_hb mt lab sb rf mo a b :
  happens_before lab sb rf mo a b
  clos_trans _ (hc_edge mt lab sb rf mo) a b.

Lemma heap_loc_na_initialized :
   mt acts lab sb rf mo hmap V
    (FIN: ExecutionFinite acts lab sb)
    (IRR: IrreflexiveHB lab sb rf mo)
    (ACYCLIC: acyclic (hc_edge mt 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)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l v (LA: h l = HVval v),
   cpre c hf,
    sb cpre c
    is_writeLV (lab c) l v
    hmap (hb_sb cpre c) = Hdef hf
    is_val (hf l)
    (c = hb_fst edge happens_before lab sb rf mo c (hb_fst edge))
    
    ( d
      (HB1: clos_refl_trans _ (hc_edge mt lab sb rf mo) d (hb_fst edge))
      (HB2: clos_trans _ (hc_edge mt lab sb rf mo) c d),
      ¬ is_writeL (lab d) l).
Lemma is_write_weaken typ l v : is_writeLV typ l v is_writeL typ l.

Lemma is_access_weaken typ l v : is_writeLV typ l v is_access typ.

Hint Resolve is_write_weaken is_access_weaken.

Lemma two_access_cases :
   mt pre a b acts lab sb rf mo hmap V hf
    (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)
    (INa : In a V)
    (INb : In b V)
    (SB : sb pre a) (HD: hmap (hb_sb pre a) = Hdef hf) (IV: is_val (hf (loc (lab a))))
    (B : is_access (lab b)) (LOC : loc (lab a) = loc (lab b)),
  a = b happens_before lab sb rf mo a b happens_before lab sb rf mo b a.

Lemma hb_prev :
   lab sb rf mo a p n,
    happens_before lab sb rf mo a n
    ( x, sb x n x = p)
    ( x, synchronizes_with lab sb rf mo x n x = p)
    a = p happens_before lab sb rf mo a p.

Lemma go_back_one_na :
   lab sb rf hmap edge
    (VALID : hmap_valid lab sb rf hmap (hb_fst edge))
    (EV : edge_valid lab sb rf edge) hf
    (GET : hmap edge = Hdef hf) l
    (LA : is_val (hf l))
    (NW: lab (hb_fst edge) Aalloc l),
   edge',
    edge_valid lab sb rf edge'
    hb_snd edge' = hb_fst edge
     hf', hmap edge' = Hdef hf'
                is_val (hf' l).

Lemma heap_loc_na_allocated :
   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)
    edge (EV: edge_valid lab sb rf edge) (IN: In (hb_fst edge) V)
    h (GET: hmap edge = Hdef h) l (LA: is_val (h l)),
   cpre c hf,
    sb cpre c
    lab cpre = Aalloc l
    hmap (hb_sb cpre c) = Hdef hf
    hf l = HVuval
    (cpre = hb_fst edge happens_before lab sb rf mo cpre (hb_fst edge)).


This page has been generated by coqdoc Imprint | Data protection