Lemmas about non-atomic accesses


Require Import Vbase.
Require Import Relations Classical ClassicalDescription.
Require Import List Permutation Vlistbase Vlist extralib.
Require Import c11 fslassn fslassnlemmas fslmodel fslhmap ihc.

Set Implicit Arguments.

Lemma go_back_one_val :
   lab sb rf mo hmap edge
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (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 : has_value (hf l) v)
    (NW: ¬ is_writeLV (lab (hb_fst edge)) l v),
   edge´,
    edge_valid lab sb rf edge´
    hb_snd edge´ = Some (hb_fst edge)
    ¬ is_writeL (lab (hb_fst edge)) l
     hf´, hmap edge´ = Hdef hf´ has_value (hf´ l) v.
Lemma heap_loc_na_initialized2 :
   acts lab sb rf mo hmap V
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (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 v (LA: has_value (h l) 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_union_rf sb rf c (hb_fst edge))
    ( d
      (HB1: d = hb_fst edge happens_before_union_rf sb rf d (hb_fst edge))
      (HB2: happens_before_union_rf sb rf c d),
      ¬ is_writeL (lab d) l).
Lemma is_write_weaken typ l v : is_writeLV typ l vis_writeL typ l.

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

Hint Resolve is_write_weaken is_access_weaken.

Lemma two_access_cases :
   pre a b acts lab sb rf mo hmap V hf
    (CONS_RF: ConsistentRF_basic lab sb rf mo)
    (FIN: ExecutionFinite acts lab sb)
    (ACYCLIC: IrreflexiveHBuRF sb rf)
    (CONS_A: ConsistentAlloc lab)
    (HC: hist_closed sb rf 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_union_rf sb rf a b happens_before_union_rf sb rf b a.


This page has been generated by coqdoc