Module TSOMemoryMachine


Require Import Coqlib Utf8.
Require Import Maps.
Require Import Ast.
Require Import Integers.
Require Import Pointers.
Require Import Values.
Require Import Mem.
Require Import Events.
Require Import Globalenvs.
Require Import Op.
Require Import Registers.
Require Import Libtactics.
Require Import INJECT.
Require Import Utils.
Require Import Classical.
Require Import Relations.
Require Import Permissions Emem.
Require Import MemoryMachine.

Definition buffer := list buf_item.

Definition empty_buffer : buffer := nil.

Definition push_item (b:buf_item) (buf:buffer) : buffer := b::buf.

Record tsomem : Type := TSOMEM {
  shared_mem :> mem;
  buffers : thread_id -> buffer
}.

Definition m2bi (me:mem_event) : option buf_item :=
  match me with
    | MEwrite _ _ p v => Some (WBufItem p v)
    | MEalloc p i k => Some (ABufItem p i k)
    | MEfree p k => Some (FBufItem p k)
    | _ => None
  end.


Fixpoint addr_in_buf (addr:pointer) (l:list buf_item) : bool :=
  match l with
    | nil => false
    | (WBufItem p _)::q => (eq_dec addr p) || addr_in_buf addr q
    | _::q => addr_in_buf addr q
  end.

Lemma addr_in_buf_app p b1 :
  ∀ b2,
    match addr_in_buf p (b1 ++ b2) with
      | true => addr_in_buf p b1 = true ∨ addr_in_buf p b2 = true
      | false => addr_in_buf p b1 = false ∧ addr_in_buf p b2 = false
    end.
Proof.
  induction b1; intros b2. simpl. destruct addr_in_buf; auto.
  rewrite <- app_comm_cons.
  destruct a.
  red. fold addr_in_buf. eq_case. intros ->. rewrite orb_true_l. left.
  unfold addr_in_buf. eq_case; intuition.
  intros n. rewrite orb_false_l.
  assert (addr_in_buf p (WBufItem p0 v :: b1) = addr_in_buf p b1) as K.
    unfold addr_in_buf. eq_case; intuition.
  rewrite K. exact (IHb1 _).
  change (addr_in_buf p (_ :: b1 ++ b2)) with (addr_in_buf p (b1 ++ b2)).
  change (addr_in_buf p (_ :: b1)) with (addr_in_buf p b1).
  exact (IHb1 _).
  change (addr_in_buf p (_ :: b1 ++ b2)) with (addr_in_buf p (b1 ++ b2)).
  change (addr_in_buf p (_ :: b1)) with (addr_in_buf p b1).
  exact (IHb1 _).
Qed.

Fixpoint buf_load (addr: pointer) (l: list buf_item) : option val :=
  match l with
    | nil => None
    | WBufItem p v::q =>
      if eq_dec addr p
      then Some v
      else buf_load addr q
    | _::q => buf_load addr q
  end.

Lemma buf_load_iff addr l :
  addr_in_buf addr l <-> buf_load addr l ≠ None.
Proof.
  induction l as [| [p v| |] q]; try now simpl; intuition.
  unfold addr_in_buf, buf_load.
  eq_case. intros ->. rewrite orb_true_l. intuition. congruence.
  intros. rewrite orb_false_l. intuition.
Qed.

Lemma buf_load_app1 {addr l v} :
  buf_load addr l = Some v →
  ∀ l', buf_load addr (l ++ l') = Some v.
Proof.
  induction l as [|bi l]. inversion 1.
  unfold buf_load. fold buf_load.
  destruct bi as [p w|? ? ?|? ?]; auto.
  eq_case. intros -> X l'; inv X. rewrite <- app_comm_cons. unfold buf_load. eq_case; congruence.
  intros. rewrite <- app_comm_cons. unfold buf_load. eq_case. congruence. intros _.
  intuition.
Qed.

Lemma buf_load_app2 {addr l} :
  addr_in_buf addr l = false →
  ∀ l', buf_load addr (l ++ l') = buf_load addr l'.
Proof.
  induction l as [|bi l]. auto.
  change (bi :: l) with ((bi :: nil) ++ l) at 1. intros H.
  generalize (addr_in_buf_app addr (bi :: nil) l). rewrite H.
  intros (A & B) l'.
  rewrite <- app_comm_cons.
  destruct bi as [p v|? ? ?|? ?]; unfold buf_load; auto.
  unfold addr_in_buf in A.
  destruct @eq_dec. simpl in A. congruence.
  auto.
Qed.

Inductive buf_step t : mem -> buf_item -> mem_event -> mem -> Prop :=
  | buf_step_store: forall m p v m' d af
    (ESD: check_perm_store t (MEM m d) af p)
    (ESS: store_ptr Mint32 m p v = Some m')
    (ESWF1: wf_val v)
    (ESWF2: wf_ptr p),
    buf_step t (MEM m d) (WBufItem p v) (MEwrite false af p v) (MEM m' d)
  | buf_step_alloc: forall m p i k m' d
    (ESF: range_has_store_perm t d (p,i))
    (ESL: alloc_ptr (p,i) k m = Some m'),
    buf_step t (MEM m d) (ABufItem p i k) (MEalloc p i k) (MEM m' d)
  | buf_step_free: forall m p k m' d n
    (ESA: range_allocated (p,n) k m)
    (ESWF: range_has_store_perm t d (p,n))
    (ESL: free_ptr p k m = Some m'),
    buf_step t (MEM m d) (FBufItem p k) (MEfree p k) (MEM m' d).

Inductive unbuffer (t:thread_id) : (mem*buffer) -> (mem*buffer) -> Prop :=
| unbuffer_def: forall m b bi e b' m'
  (HU2:b = b'++bi::nil)
  (HU3:buf_step t m bi e m'),
  unbuffer t (m,b) (m',b').

Notation star := (clos_refl_trans _).

Inductive unbuffer_n (t:thread_id) : (mem*buffer) -> nat -> (mem*buffer) -> Prop :=
| unbuffer_n_0: forall mb, unbuffer_n t mb O mb
| unbuffer_n_S: forall mb1 mb2 mb3 n,
  unbuffer_n t mb1 n mb2 ->
  unbuffer t mb2 mb3 ->
  unbuffer_n t mb1 (S n) mb3.


Definition flush (t:thread_id) (b:buffer) (m m':mem) : Prop :=
  star (unbuffer t) (m,b) (m',empty_buffer).

Definition safe (t:thread_id) (b:buffer) (m:mem) : Prop := True.

Inductive mem_trace t P (m:mem) : list mem_event -> mem -> Prop :=
 | mem_trace_nil: forall (TM: P m), mem_trace t P m nil m
 | mem_trace_cons: forall l m' e m''
   (TM1: mem_trace t P m l m')
   (TM2: mem_step t m' e m'')
   (TM3: P m''),
   mem_trace t P m (e::l) m''.

Inductive tso_step t : tsomem -> tso_event -> tsomem -> Prop :=
| tso_step_fence m
  (BEMP: m.(buffers) t = empty_buffer)
  : tso_step t m TSOfence m
| tso_step_unbuf: forall b bi b' m m' bufs e
  (TM1:bufs t = b)
  (TM3:b = b'++bi::nil)
  (TM4:buf_step t m bi e m'),
  tso_step t (TSOMEM m bufs) (TSOunbuf e) (TSOMEM m' (upd bufs t b'))
| tso_step_write: forall b (r:bool) a p v b' m bufs m'
  (TM1:bufs t = b)
  (TM2:b' = push_item (WBufItem p v) b)
  (TM3:if r then mem_step t m (MEperm PErelease) m' else m=m')
  (TM4:check_perm_store t m a p)
  (ESWF1: wf_val v)
  (ESWF2: wf_ptr p),
  tso_step t (TSOMEM m bufs) (TSOmem (MEwrite r a p v)) (TSOMEM m' (upd bufs t b'))
| tso_step_alloc: forall b p i k b' m bufs
  (TM1:bufs t = b)
  (TM2:b' = push_item (ABufItem p i k) b),
  tso_step t (TSOMEM m bufs) (TSOmem (MEalloc p i k)) (TSOMEM m (upd bufs t b'))
| tso_step_free: forall b p k b' m bufs
  (TM1:bufs t = b)
  (TM2:b' = push_item (FBufItem p k) b),
  tso_step t (TSOMEM m bufs) (TSOmem (MEfree p k)) (TSOMEM m (upd bufs t b'))
| tso_step_load: forall m d p v bufs b (inbuf: bool) ap
  (TM1:bufs t = b)
  (TM2: if inbuf
        then buf_load p b = Some v
           ∧ wf_val v ∧ wf_ptr p
           ∧ match ap with
               | Global => ∀ t', d p = HiddenBy t' → t = t'
               | Local => readable_perm d p t
             end
        else mem_step t (MEM m d) (MEread ap inbuf p v) (MEM m d))
  (TM4: ∀ x k, ¬ In (FBufItem x k) b)
  (TM3:inbuf = addr_in_buf p b),
  tso_step t (TSOMEM (MEM m d) bufs) (TSOmem (MEread ap inbuf p v)) (TSOMEM (MEM m d) bufs)
 | tso_step_perm: forall m bufs m' ev
  (TM1: mem_step t m (MEperm ev) m'),
  tso_step t (TSOMEM m bufs) (TSOmem (MEperm ev)) (TSOMEM m' bufs)
| tso_step_rmw: forall m bufs m' r p v instr
  (TM1: bufs t = empty_buffer)
  (TM2: mem_step t m (MErmw r p v instr) m'),
  tso_step t (TSOMEM m bufs) (TSOmem (MErmw r p v instr)) (TSOMEM m' bufs)
| tso_step_start m bufs newtid
  : tso_step t (TSOMEM m bufs) (TSOstart newtid) (TSOMEM m (upd bufs newtid nil))
| tso_step_beginatomic m bufs
  : tso_step t (TSOMEM m bufs) TSObeginatomic (TSOMEM m bufs)
| tso_step_endatomic m bufs e
  : tso_step t (TSOMEM m bufs) (TSOendatomic e) (TSOMEM m bufs)
.

Inductive tso_trace t (m:tsomem) : list tso_event -> tsomem -> Prop :=
 | tso_trace_nil: tso_trace t m nil m
 | tso_trace_cons: forall l m' e m''
   (TM1: tso_trace t m l m')
   (TM2: tso_step t m' e m''),
   tso_trace t m (e::l) m''.


Lemma unbuffer_determinist: forall t mb mb1 mb2,
  unbuffer t mb mb1 ->
  unbuffer t mb mb2 -> mb1 = mb2.
Proof.
  intros.
  inv H; inv H0.
  exploit app_inj_tail; eauto.
  destruct 1; subst.
  f_equal; clear HU2.
  inv HU0; inv HU3; try congruence.
Qed.


Require Import Relation_Operators.
Require Import Operators_Properties.

Lemma star_unbuffer_prefix: forall t mb mb',
  clos_refl_trans_1n _ (unbuffer t) mb mb' ->
  forall m l m' l',
    mb = (m, l) ->
    mb' = (m', l') ->
    exists l'', l = l'++l''.
Proof.
  induction 1; simpl; intros.
  > assert (l = l') by congruence.
    subst; exists nil; auto with datatypes.
    rewrite app_nil_r; auto.
  > subst; inv H; simpl in *.
    subst.
    exploit IHclos_refl_trans_1n; eauto.
    intros (l'' & L); subst.
    rewrite app_ass; eauto.
Qed.

Lemma flush_unbuffer_n_aux: forall t mb mb',
   clos_refl_trans_n1 _ (unbuffer t) mb mb' ->
   let (m, b) := mb in
   let (m', b') := mb' in
   exists N,
     unbuffer_n t (m, b) N (m', b') /\ length b = (N + length b')%nat.
Proof.
  induction 1.
  > destruct mb.
    exists O.
    repeat (econstructor; eauto).
  > destruct mb; destruct y; destruct z.
    destruct IHclos_refl_trans_n1 as (N1 & HN1 & HNN1); clear H0.
    exists (S N1).
    repeat (econstructor; eauto).
    inv H; subst.
    rewrite app_length in *; simpl in *; omega.
Qed.

Lemma flush_unbuffer_n: forall b t m m',
  flush t b m m' ->
  unbuffer_n t (m,b) (length b) (m',empty_buffer).
Proof.
  unfold flush; intros.
  rewrite clos_rt_rtn1_iff in H.
  exploit flush_unbuffer_n_aux; eauto.
  simpl; intros (N & Hn & Hn2).
  replace (length b) with N by omega.
  auto.
Qed.

Lemma flush_empty : forall t m m',
  flush t empty_buffer m m' -> m' = m.
Proof.
  intros.
  apply flush_unbuffer_n in H.
  inv H; auto.
Qed.

Lemma unbuffer_n_same_buf: forall t m1 b1 N m2 b2 m1' m2' b2',
  unbuffer_n t (m1, b1) N (m2, b2) ->
  unbuffer_n t (m1', b1) N (m2', b2') -> b2' = b2.
Proof.
  induction N; intros.
  > inv H; inv H0; congruence.
  > inv H; inv H0.
    destruct mb2; destruct mb0.
    assert (b0=b) by (eapply IHN; eauto).
    subst.
    inv H4; inv H5.
    exploit app_inj_tail; eauto.
    destruct 1; congruence.
Qed.

Inductive unbuffer_n' (t:thread_id) : (mem*buffer) -> nat -> (mem*buffer) -> Prop :=
| unbuffer_n'_0: forall mb, unbuffer_n' t mb O mb
| unbuffer_n'_S: forall mb1 mb2 mb3 n,
  unbuffer t mb1 mb2 ->
  unbuffer_n' t mb2 n mb3 ->
  unbuffer_n' t mb1 (S n) mb3.

Lemma flush_unbuffer_n'_aux: forall t mb mb',
   clos_refl_trans_1n _ (unbuffer t) mb mb' ->
   let (m, b) := mb in
   let (m', b') := mb' in
   exists N,
     unbuffer_n' t (m, b) N (m', b') /\ length b = (N + length b')%nat.
Proof.
  induction 1.
  > destruct x.
    exists O.
    repeat (econstructor; eauto).
  > destruct x; destruct y; destruct z.
    destruct IHclos_refl_trans_1n as (N1 & HN1 & HNN1); clear H0.
    exists (S N1).
    repeat (econstructor; eauto).
    inv H; subst.
    rewrite app_length in *; simpl in *; omega.
Qed.

Lemma flush_unbuffer_n': forall b t m m',
  flush t b m m' ->
  unbuffer_n' t (m,b) (length b) (m',empty_buffer).
Proof.
  unfold flush; intros.
  rewrite clos_rt_rt1n_iff in H.
  exploit flush_unbuffer_n'_aux; eauto.
  simpl; intros (N & Hn & Hn2).
  replace (length b) with N by omega.
  auto.
Qed.

Lemma unbuffer_n'_func: forall t N mb0 mb mb',
  unbuffer_n' t mb0 N mb ->
  unbuffer_n' t mb0 N mb' -> mb = mb'.
Proof.
  induction N; intros.
  > inv H; inv H0; congruence.
  > inv H; inv H0.
    assert (mb2=mb3).
      inv H2; inv H1.
      exploit app_inj_tail; eauto.
      destruct 1; subst; f_equal.
      destruct bi0; inv HU0; inv HU3; congruence.
    subst; eauto.
Qed.

Lemma flush_function : ∀ t buf,
   ∀ m m' m'',
     flush t buf m m' →
     flush t buf m m'' →
       m' = m''.
Proof.
  intros t buf m m' m'' H H'.
  apply flush_unbuffer_n' in H.
  apply flush_unbuffer_n' in H'.
  generalize (unbuffer_n'_func _ _ _ _ _ H H').
  congruence.
Qed.

Lemma unbuffer_left: forall l1 t l m l0 m',
  star (unbuffer t) (m, rev l) (m', l0) ->
  star (unbuffer t) (m, l1++rev l) (m', l1++l0).
Proof.
  induction l; simpl; intros.
  > rewrite clos_rt_rt1n_iff in H; inv H.
    > constructor 2.
    > inv H0; simpl in *.
      eelim app_cons_not_nil; eauto.
  > rewrite clos_rt_rt1n_iff in H; inv H.
    > constructor 2.
    > rewrite clos_rt_rt1n_iff.
      destruct y.
      assert (b = rev l).
        inv H0; simpl in *.
        exploit app_inj_tail; eauto.
        destruct 1; congruence.
      subst.
      rewrite <- clos_rt_rt1n_iff in H1.
      generalize (IHl _ _ _ H1); clear H1 IHl; intros IH.
      rewrite <- clos_rt_rt1n_iff.
      constructor 3 with (2:=IH).
      constructor 1.
      inv H0; simpl in *; econstructor; eauto.
      simpl.
      rewrite app_ass; congruence.
Qed.

Lemma app_nil_l' : forall A (l1 l2:list A), l2 = l1 ++ l2 -> l1 = nil.
Proof.
  intros.
  assert (length l2 = length (l1++l2)) by congruence.
  rewrite app_length in *.
  assert (length l1 = 0%nat) by omega.
  destruct l1; inv H1; auto.
Qed.

Lemma unbuffer_n_app : forall t b m1 bi m2 b2,
  unbuffer_n t (m1,bi++b) (length b) (m2, b2) -> b2=bi.
Proof.
  induction b; simpl; intros.
  > inv H.
    rewrite app_nil_r; auto.
  > inv H.
    inv H3.
    replace (bi++a::b) with ((bi++a::nil)++b) in H1.
    exploit IHb; eauto; intros.
    exploit app_inj_tail; eauto; destruct 1; congruence.
    rewrite app_ass; auto.
Qed.

Lemma unbuffer_n_cons : forall t b m1 bi m2 b2,
  unbuffer_n t (m1,bi::b) (length b) (m2, b2) -> b2=bi::nil.
Proof.
  intros.
  exploit (unbuffer_n_app t b m1 (bi::nil) m2 b2); simpl; auto.
Qed.


Lemma unbuffer_n_app_inv : forall t N b1 m1 bi m2 b2,
  unbuffer_n t (m1,bi++b1) N (m2, bi++b2) ->
  unbuffer_n t (m1,b1) N (m2, b2).
Proof.
  induction N; simpl; intros.
  > inv H.
    exploit app_inv_head; eauto.
    intros; subst.
    constructor 1.
  > inv H.
    inv H3.
    rewrite app_ass in H1.
    exploit IHN; eauto; intros.
    econstructor; eauto.
    econstructor; eauto.
Qed.

Lemma unbuffer_n_cons_inv : forall t N b1 m1 bi m2 b2,
  unbuffer_n t (m1,bi::b1) N (m2, bi::b2) ->
  unbuffer_n t (m1,b1) N (m2, b2).
Proof.
  intros.
  eapply unbuffer_n_app_inv with (bi::nil); auto.
Qed.

Lemma unbuffer_n_star: forall t N mb mb',
  unbuffer_n t mb N mb' -> star (unbuffer t) mb mb'.
Proof.
  induction 1.
  > constructor 2.
  > constructor 3 with mb2; auto.
    constructor 1; auto.
Qed.

Lemma unbuffer_n'_star: forall t N mb mb',
  unbuffer_n' t mb N mb' -> star (unbuffer t) mb mb'.
Proof.
  induction 1.
  > constructor 2.
  > constructor 3 with mb2; auto.
    constructor 1; auto.
Qed.


Lemma buf_step_preserves_perm {tid m bi ev m'} :
  buf_step tid m bi ev m' →
  m'.(perms) = m.(perms).
Proof.
inversion 1; auto. Qed.

Lemma flush_preserves_perm {tid buf m m'} :
  flush tid buf m m' →
  m'.(perms) = m.(perms).
Proof.
  assert (∀ N m b, ∀ m' b', unbuffer_n' tid (m, b) N (m', b') → m'.(perms) = m.(perms)) as L.
  induction N. inversion 1; auto.
  inversion 1. subst. inv H1.
  transitivity m'1. 2: apply (buf_step_preserves_perm HU3).
  eapply IHN. eassumption.
  intros H. apply flush_unbuffer_n' in H. eapply L; eauto.
Qed.

Inductive nodef : option val → Prop :=
| NDN : nodef None
| NDU : nodef (Some Vundef)
.



Lemma load_addr_not_in_buf_undef tid :
  ∀ N b m,
    ∀ b' m' p,
      wf_ptr p →
      unbuffer_n' tid (m,b) N (m', b') →
      addr_in_buf p b = false →
      nodef (load_ptr Mint32 m p) →
      nodef (load_ptr Mint32 m' p).
Proof.
  induction N. now inversion 2.
  intros b m b' m' p H H0 H1 H2.
  inv H0. inv H4.
  generalize (addr_in_buf_app p b'0 (bi::nil)). autorw'. intros (A & B).
  exploit IHN; eauto.
  inv HU3; simpl.
  > rewrite (load_store_old _ _ _ _ _ ESWF2 ESWF1 H ESS); auto.
    unfold addr_in_buf in B. destruct @eq_dec; simpl in B; congruence.
  > destruct (wf_range_ptr_inside (proj1 ESF) H) as [X|X].
    > rewrite (load_alloc_inside ESL X). vauto. now apply wf_ptr_aligned.
    > rewrite (load_alloc_other ESL (ranges_disjoint_comm _ _ X)); auto.
  > destruct (ranges_disjoint_dec (range_of_chunk p Mint32) (p0, n)) as [X|X].
    > rewrite (load_free_other ESL ESA X). auto.
    > rewrite (load_free_overlap ESL ESA X). vauto.
Qed.


Lemma read_as_if_flush tid ap inbuf buf m m' p v :
  flush tid buf m m' →
  mem_step tid m' (MEread ap inbuf p v) m' →
  if addr_in_buf p buf
  then buf_load p buf = Some v
  else mem_step tid m (MEread ap inbuf p v) m.
Proof.
  assert (forall N b b' m m',
            unbuffer_n' tid (m, b) N (m', b') →
            N = length b →
            mem_step tid m' (MEread ap inbuf p v) m' →
            if addr_in_buf p b
            then buf_load p b = Some v
            else mem_step tid m (MEread ap inbuf p v) m
         ) as L.
  induction N; inversion 1; subst. destruct b'; clarify; simpl.
  destruct b as [|bi b]. clarify.
  inv H1. rewrite HU2 in *. clear HU2 bi b. intros H0 H1.
  assert (N = length b'0) as X. rewrite app_length in H0. simpl in H0. omega.
  generalize (IHN _ _ _ _ H3 X H1). clear IHN.
  generalize (addr_in_buf_app p b'0 (bi0::nil)).
  case (addr_in_buf p (b'0 ++ bi0::nil)).
    intros [K|K]. autorw'. intros. now apply buf_load_app1.
    case_eq (addr_in_buf p b'0). intros. now apply buf_load_app1.
    intros Q L.
    rewrite buf_load_app2; auto. destruct bi0; clarify.
    assert (p0 = p). unfold addr_in_buf in K. destruct @eq_dec; simpl in *; congruence.
    subst.
    inv HU3.
    assert (v0 = v).
    pose proof (load_store_new _ _ _ _ ESWF2 ESWF1 ESS). inv L; autorw'.
    subst.
    unfold buf_load. eq_case; congruence.
  intros (K & K'). autorw'. intros L.
  inv HU3.
  assert (p ≠ p0).
  intros ->. unfold addr_in_buf in K'. destruct @eq_dec; simpl in K'; congruence.
  inv L; econstructor; eauto; rewrite (load_store_old _ _ _ _ _ ESWF2 ESWF1 ESWF3 ESS) in ESL; auto.
  assert (wf_ptr p) as P by (inv L; auto).
  destruct (wf_range_ptr_inside (proj1 ESF) P) as [X|X].
  2: inv L; econstructor; eauto;
  rewrite (load_alloc_other ESL) in ESL0; auto using ranges_disjoint_comm.
  apply False_ind.
  pose proof (load_alloc_inside ESL X (wf_ptr_aligned _ P)) as Undef.
  pose proof (load_addr_not_in_buf_undef tid _ _ _ _ _ _ P H3 K) as Y.
  inv H1; simpl in *; autorw'; pose proof (Y NDU) as Z; inv Z; inv ESWF1.
  assert (wf_ptr p) as P by (inv L; auto).
  destruct (ranges_disjoint_dec (range_of_chunk p Mint32) (p0, n)) as [X|X].
  inv L; econstructor; eauto;
  rewrite (load_free_other ESL ESA X) in ESL0; auto.
  apply False_ind.
  pose proof (load_free_overlap ESL ESA X) as Undef.
  pose proof (load_addr_not_in_buf_undef tid _ _ _ _ _ _ P H3 K) as Y.
  inv H1; simpl in *; autorw'; pose proof (Y NDN) as Z; inv Z; inv ESWF1.
  intros H. apply flush_unbuffer_n' in H. eapply L; eauto.
Qed.

Require Import Memeq.

Section SAFE_LE.
  Definition perm_map_le t : relation perm_map :=
    fun x y => ∀ p, has_store_perm t x p → has_store_perm t y p.

  Remark perm_map_le_refl t x : perm_map_le t x x.
Proof.
now intros p. Qed.

  Record safe_le t (m m': mem) : Prop := SafeLE
  { sle_perm : perm_map_le t m.(perms) m'.(perms)
  ; sle_alloc: forall r k, range_allocated r k m <-> range_allocated r k m'
  ; sle_restr: forall b, mrestr m b = mrestr m' b
  }.

  Lemma range_has_store_perm_le {t d d'} :
    perm_map_le t d d' →
    ∀ p,
    range_has_store_perm t d p →
    range_has_store_perm t d' p.
Proof.
    intros H p (A & B). split. exact A.
    intros q Q. exact (H q (B _ Q)).
  Qed.

Lemma check_has_perm : forall t m d af p,
  check_perm_store t (MEM m d) af p ->
  has_store_perm t d p.
Proof.
  intros.
  inv H; simpl in *; perm; autorw'.
Qed.

Lemma has_check_perm : forall t d p,
  has_store_perm t d p ->
  forall m, exists af, check_perm_store t (MEM m d) af p.
Proof.
  unfold has_store_perm; intros.
  case_eq (d p); intros; rewrite H0 in *.
  subst; econstructor; econstructor; eauto.
  econstructor; econstructor 2; eauto.
Qed.

Lemma buf_step_safe_le {tid m m'} :
  safe_le tid m m' →
  forall {bi e n}, buf_step tid m bi e n → ∃n', ∃e', buf_step tid m' bi e' n' ∧ safe_le tid n n'.
Proof.
  destruct m as (m & d).
  destruct m' as (m' & d').
  intros [P A R]. simpl in *. subst.
  destruct bi; intros e n K; inv K.
  destruct (store_ptr_some_arange _ m' _ _ _ v _ ESS) as (n' & H & H').
  split. intros r k _; apply A. apply extensionality. eauto.
  assert (exists af, check_perm_store tid (MEM m' d') af p).
    apply has_check_perm.
    apply P.
    eapply check_has_perm; eauto.
  destruct H0 as (af' & ESD').
  exists (MEM n' d'); exists (MEwrite false af' p v); split.
  econstructor; eauto.
  split; auto.
  intros r k. generalize (store_preserves_allocated_ranges H r k).
  generalize (store_preserves_allocated_ranges ESS r k).
  specialize A with r k. intuition.
  simpl. intros b. rewrite (restr_of_store ESS). rewrite (R b). rewrite (restr_of_store H). reflexivity.

  destruct (alloc_ptr_some_arange _ m' _ _ _ ESL) as (n' & H & H').
  split. intros r k _; apply A. apply extensionality. exact R.
  exists (MEM n' d'); econstructor. pose proof (range_has_store_perm_le P _ ESF). split. vauto. split. auto.
  intros r k. specialize A with r k. simpl.
  etransitivity.
  apply (alloc_preserves_allocated_iff ESL r k).
  symmetry. etransitivity.
  apply (alloc_preserves_allocated_iff H r k).
  rewrite A.
  intuition.
  simpl. intros b. rewrite (restr_of_alloc ESL). rewrite (R b). rewrite (restr_of_alloc H). reflexivity.

  destruct (free_ptr_some_arange (fun _ => true) _ m' _ _ _ ESL) as (n' & H & H').
  split. intros r k _; apply A. apply extensionality. exact R.
  easy.
  exists (MEM n' d'); econstructor. pose proof (range_has_store_perm_le P _ ESWF). split. apply A in ESA. vauto. split. auto.
  intros r k. specialize A with r k. simpl.
  split. intros a. pose proof (free_preserves_allocated_back ESL _ _ a) as a'. apply A in a'.
  destruct (free_preserves_allocated H r k a') as [X|[X Y]]. easy.
  apply False_ind. subst. destruct r. apply (free_not_allocated ESL _ _ a).
 intros a. pose proof (free_preserves_allocated_back H _ _ a) as a'. apply A in a'.
  destruct (free_preserves_allocated ESL r k a') as [X|[X Y]]. easy.
  apply False_ind. subst. destruct r. apply (free_not_allocated H _ _ a).
  simpl. intros b. rewrite (restr_of_free ESL). rewrite (R b). rewrite (restr_of_free H). reflexivity.
Qed.



Lemma release_safe_le {t m d d'} :
  release t d' d →
  safe_le t (MEM m d) (MEM m d').
Proof.
  intros ESP.
  split; simpl; auto. 2: intuition.
  apply release_func in ESP. subst. intros a. perm. destruct (d' a). now destruct peq.
  intros H. apply Rset.subset_spec. intros x X.
  case (eq_dec x t). intros ->. unfold Rset.singleton. apply Rset.add_mem.
  intros. rewrite Rset.subset_spec in H. apply H. rewrite Rset.mem_rmo; auto.
Qed.

Lemma release_inv_safe_le {t m d d'} :
  release t d d' →
  safe_le t (MEM m d) (MEM m d').
Proof.
  intros ESP.
  split; simpl; auto. 2: intuition.
  apply release_func in ESP. subst. intros a. perm. destruct (d a). now destruct peq.
  intros H. apply Rset.subset_spec. intros x X.
  case (eq_dec x t). intros ->. unfold Rset.singleton. apply Rset.add_mem.
  intros. rewrite Rset.subset_spec in H. apply H. rewrite Rset.mem_rmo in X; auto.
Qed.

Lemma mem_step_le {t m1 e m2} :
  (∀ p i k, e ≠ MEalloc p i k) →
  (∀ p k, e ≠ MEfree p k) →
  mem_step t m1 e m2 →
  safe_le t m2 m1.
Proof.
  intros NEA NEF.
  intros K; inv K.
  split; simpl; auto. 2: intuition.
  intros a. inv ESD; trivial.
  case (eq_dec a p). intros ->. perm.
  intros. perm.
  inv ESD0.
  case (eq_dec a p). intros ->. perm. autorw'.
    intros K. apply Rset.subset_spec. rewrite Rset.subset_spec in K.
    intros x X. apply K. now apply Rset.mem_add.
  intros. perm.
  eapply (release_safe_le (m:=m) ESP).
  split. simpl. destruct released. 2: now subst; intros ?.
  eapply (release_safe_le (m:=m) ESP).
  simpl. intros r k. symmetry. apply (store_preserves_allocated_ranges ESS).
  simpl. intros b. now rewrite (restr_of_store ESS).
  split; simpl; intuition. apply perm_map_le_refl.
  inv ESD.
  split. simpl. destruct released. 2: now subst; intros ?.
  eapply (release_safe_le (m:=m) ESP).
  simpl. intros r k. symmetry. apply (store_preserves_allocated_ranges ESS).
  simpl. intros b. now rewrite (restr_of_store ESS).
  split; simpl; intuition. apply perm_map_le_refl.
  split. simpl. destruct r. 2: now subst; intros ?.
  eapply (release_safe_le (m:=m) ESP).
  simpl. intros r' k. symmetry. apply (store_preserves_allocated_ranges STO).
  simpl. intros b. now rewrite (restr_of_store STO).
  eelim NEA; reflexivity.
  eelim NEF; reflexivity.
Qed.


Lemma localwrite_safe_le {t m1 a v m2} :
  mem_step t m1 (MEwrite false Local a v) m2 ->
  safe_le t m2 m1.
Proof.
  intros H; inv H.
  split. simpl. intros x y. auto.
  simpl. intros r k. symmetry. apply (store_preserves_allocated_ranges ESS).
  simpl. intros b. now rewrite (restr_of_store ESS).
Qed.


Lemma release_step_safe_le {t m1 m2} :
  mem_step t m1 (MEperm PErelease) m2 ->
  safe_le t m2 m1.
Proof.
  intros H; inv H. inv ESD. now apply release_safe_le.
Qed.


Lemma release_inv_step_safe_le {t m1 m2} :
  mem_step t m1 (MEperm PErelease) m2 ->
  safe_le t m1 m2.
Proof.
  intros H; inv H. inv ESD. now apply release_inv_safe_le.
Qed.

End SAFE_LE.

Generated by coq2html