Module RTLinjectlow

Require Import
  Utf8 Classical
  Coqlib Ast Maps Mem Op
  Globalenvs Events Values.

Require Import
  Utils Emem Permissions TSOMemoryMachine
  INJECT RTLinject.

Require Import
  TSOmachine Simulations.

Section TSOSEM.

  Definition te_of_me (me: mem_event) : Events.thread_event :=
    match me with
      | MEwrite _ _ p v => Events.TEmem (Events.MEwrite p Mint32 v)
      | MEread _ _ p v => Events.TEmem (Events.MEread p Mint32 v)
      | MErmw _ p v i => Events.TEmem (Events.MErmw p Mint32 v i)
      | MEalloc p i k => Events.TEmem (Events.MEalloc p i k)
      | MEfree p k => Events.TEmem (Events.MEfree p k)
      | MEperm _ => Events.TEtau
    end.

  Definition te_of_te (ev: thread_event) : option Events.thread_event :=
    match ev with
      | TEext e => Some (Events.TEext e)
      | TEtso (INJECT.TSOmem e) => Some (te_of_me e)
      | TEend ReturnVoid
      | TEend FailEvent => Some (Events.TEext Events.Efail)
      | TEstart fp v => Some (Events.TEstart fp (v::nil))
      | TEexit => Some Events.TEexit
      | TEtso TSOfence => Some (Events.TEmem Events.MEfence)
      | TEtso (INJECT.TSOunbuf _)
      | TEbegin BeginLow
      | TEend (ReturnEvent _)
      | TEtau => Some Events.TEtau
      | TEtso (INJECT.TSObeginatomic)
      | TEtso (INJECT.TSOendatomic _)
      | TEtso (INJECT.TSOstart _)
      | TEato _
      | TEbegin BeginHigh => None
    end.

  Definition not_a_high_state (st: intra_state) : bool :=
    match st with
      | RIInjectState _ _ _ _ _ _ (INJECT.NormalState _ is k) =>
        match is with
          | Satomic _ _
          | Sloop _ | Sbranch _ _ => false
          | _ => match in_atomic k with
                   | Some _ => false
                   | None => true
                 end
        end
      | _ => true
    end.

  Inductive rtl_step' (ge:genv) : intra_state → Events.thread_event → intra_state → Prop :=
  | Rtl_step s e s' te
    (STEP:rtli_step ge s e s')
    (LOW: not_a_high_state s)
    (TE: Some te = te_of_te e) :
    rtl_step' ge s te s'.

  Ltac inv_step :=
    match goal with
      | H : step _ _ _ _ _ |- _ => inversion H; try (subst; clear H)
    end.

  Ltac sktau :=
    match goal with
      | [H: te_samekind ?t Events.TEtau |- _] =>
        rewrite (te_tau_samekind t H) in *; clear H
      | [H: te_samekind ?t ?q |- _] =>
        let p := fresh in
        destruct t as [p|p| | |? ?|? ?|? ? ?|]; try destruct p; inversion H; subst; clear H
    end.

  Lemma rtli_receptive : forall ge : genv, receptive(@mklts thread_labels intra_state (rtl_step' ge)).

  Ltac hpc :=
    match goal with
      | H: _ = _, K: _ = _ |- _ => rewrite H in K; inversion K; subst; clear K
      | H: _ = _, K: _ = _ |- _ => rewrite <- H in K; inversion K; subst; clear K
    end.

  Lemma map_vint_inj : forall {u v},
                         map Vint u = map Vint v →
                         u = v.

  Lemma rtli_determinate : forall ge : genv,
                             determinate (@mklts thread_labels intra_state (rtl_step' ge)).

  Definition rtl_ge_init (p: program) (ge:genv) (m: Mem.mem) : Prop :=
    Genv.globalenv_initmem p ge Ast.low_mem_restr m.

  Definition RtlInjectSem : SEM.

End TSOSEM.

Section TRACES.

  Require Traces.

  Variable p : program.
  Variable args : list val.
  Variable t : Traces.trace event.
  Definition rtli_lts ge := mklts event_labels (TSO.step RtlInjectSem ge).
  Definition rtli_traces : Prop :=
    exists ge : genv,
      exists s : TSO.state RtlInjectSem,
        TSO.init RtlInjectSem p args ge s /\
        Traces.traces (rtli_lts ge) s t.

End TRACES.

Section LOWSIM.

  Variable ge : genv.

  Definition can_unbuffer (tso: tsomem) : Prop :=
    ∀ tid bi buf,
      tso.(TSOMemoryMachine.buffers) tid = buf ++ bi :: nil →
      ∃m', ∃e',
        TSOMemoryMachine.buf_step tid tso.(shared_mem) bi e' m'.

  Definition progress (s: state) : Prop :=
    ∀ tid st,
      (snd s) ! tid = Some st →
      ∃e, ∃s',
        astep ge s (tid, e::nil) s'
      ∧ (∀ bi, e ≠ TEtso (TSOunbuf bi))
      ∧ not_a_high_state st.

  Definition wf_load (s: state) : Prop :=
    ∀ tid, match (snd s) ! tid with
             | Some (RIInjectState _ _ sp _ _ _ (NormalState irs
                    (Sload _ addr args _) _)) =>
    ∀ p m v, eval_addressing ge sp addr (map irs args) = Some (Vptr p) →
           flush tid ((fst s).(TSOMemoryMachine.buffers) tid) (fst s) m →
           load_ptr Mint32 m.(MemoryMachine.mem_rtl) p = Some v →
           wf_val v
             | _ => True
           end.

  Definition reachable (i: state) : state → Prop :=
    fun s => ∃tr, trace ge i tr s.

  Remark reachable_refl : reflexive _ reachable.
  Remark reachable_trans: transitive _ reachable.

  Definition can_write_and_free (s: state) : Prop :=
      ∀ tid, match (snd s) ! tid with
               | Some (RIInjectState _ _ sp _ _ _ (NormalState irs
                      (Sstore _ _ addr args src) k)) =>
    ∀ p, eval_addressing ge sp addr (map irs args) = Some (Vptr p) →
    (fst s).(TSOMemoryMachine.buffers) tid = empty_buffer →
    load_ptr Mint32 (fst s).(MemoryMachine.mem_rtl) p ≠ None
               | Some (RIState _ c (Some sp) pc _) =>
    ∀ res, c ! pc = Some (Ireturn res) →
    (fst s).(TSOMemoryMachine.buffers) tid = empty_buffer →
    ∃ m', free_ptr sp MObjStack (fst s).(MemoryMachine.mem_rtl) = Some m'
        ∧ forall tid' p v b,
          (fst s).(TSOMemoryMachine.buffers) tid' = b ++ WBufItem p v :: nil → store_ptr Mint32 m' p v ≠ None
               | _ => True
             end.

  Lemma may_store_may_load : ∀ m p v m',
                               store_ptr Mint32 m p v = Some m' →
                               load_ptr Mint32 m p ≠ None.

  Lemma can_unbuffer_can_write_and_free i :
    (∀ s, reachable i s → can_unbuffer (fst s)) →
    ∀ s, reachable i s → progress s → can_write_and_free s.

  Inductive safe_buf t : buffer → MemoryMachine.mem → Prop :=
  | SBnil m : safe_buf t nil m
  | SBsnoc m buf bi m' e
      (UNB: TSOMemoryMachine.buf_step t m bi e m')
      (SB: safe_buf t buf m')
    : safe_buf t (buf ++ bi :: nil) m.

  Lemma can_unbuffer_safe' {i tid} :
    (∀ s, reachable i s → can_unbuffer (fst s)) →
    ∀ buf,
    ∀m t, reachable i (m,t) →
        m.(TSOMemoryMachine.buffers) tid = buf →
        safe_buf tid buf m.(shared_mem).
  Corollary can_unbuffer_safe i :
    (∀ s, reachable i s → can_unbuffer (fst s)) →
    ∀ s t, reachable i (s,t) →
         ∀ tid, safe_buf tid (s.(TSOMemoryMachine.buffers) tid) s.(shared_mem).

  Definition l_state : Type := (tso_state * PTree.t intra_state)%type.
  Definition l_step : l_state → fullevent → l_state → Prop := TSO.step RtlInjectSem ge.

  Inductive match_bi : buf_item → buffer_item → Prop :=
  | MBIW p v
    : match_bi (WBufItem p v) (BufferedWrite p Mint32 v)
  | MBIA p i k
    : match_bi (ABufItem p i k) (BufferedAlloc p i k)
  | MBIF p k
    : match_bi (FBufItem p k) (BufferedFree p k)
  .

  Definition match_buf : (thread_id → buffer) → buffers → Prop :=
    fun x y => ∀ t, lift_forall_list match_bi (rev (x t)) (y t).

  Definition match_mem : MemoryMachine.mem → mem → Prop :=
    fun x y => MemoryMachine.mem_rtl x = y.

  Remark match_bi_abi {a b m n t buf} :
    match_bi a b →
    match_mem m n →
    safe_buf t (buf ++ a :: nil) m →
    forall {n'}, apply_buffer_item b n = Some n' →
    ∃ m', unbuffer t (m, buf ++ a :: nil) (m', buf)
    ∧ match_mem m' n'
    ∧ safe_buf t buf m'
  .

  Definition safe_tsomem : tsomem → Prop :=
    fun M => ∀ t, safe_buf t (M.(TSOMemoryMachine.buffers) t) M.(shared_mem).

  Definition safe_state : state → Prop :=
    fun Mts => safe_tsomem (fst Mts) ∧ progress Mts ∧ wf_load Mts ∧ can_write_and_free Mts.

  Remark flush_ab {a b t} :
    match_buf a b →
    forall {m n}, match_mem m n →
    safe_tsomem (TSOMEM m a) →
    forall {n'}, apply_buffer (b t) n = Some n' →
    ∃ m',
      flush t (a t) m m'
    ∧ match_mem m' n'
  .

  Inductive match_state : state → l_state → Prop :=
  | MS m m' buf buf' ts
       (MEM: match_mem m m')
       (BUF: match_buf buf buf')
    : match_state (TSOMEM m buf, ts) (mktsostate buf' m', ts)
  .

  Definition match_ev : thread_event → fullevent → Prop :=
    fun te e =>
      match te with
        | TEext f => e = Evisible f
        | TEend ReturnVoid
        | TEend FailEvent => e = Evisible Efail
        | TEbegin BeginHigh => False
        | _ => e = Etau
      end.

  Definition progress' (s: state) : Prop :=
    ∀ tid,
      match (snd s) ! tid with
        | Some (RIInjectState stk c sp pc rs dst
               (NormalState irs (Sload ap addr args res) k)) =>
      ∀ p, eval_addressing ge sp addr (map irs args) = Some (Vptr p) →
        wf_ptr p
      ∧ ∀ m' perms, flush tid ((fst s).(TSOMemoryMachine.buffers) tid) (fst s).(shared_mem) (MemoryMachine.MEM m' perms) →
       (match ap with Local => readable_perm perms p tid
                   | Global => ∀ t, perms p = HiddenBy t → tid = t end)
     ∧ (∃v, wf_val v ∧
            if addr_in_buf p ((fst s).(TSOMemoryMachine.buffers) tid)
            then buf_load p ((fst s).(TSOMemoryMachine.buffers) tid) = Some v
            else MemoryMachine.mem_step tid (fst s) (MEread ap false p v) (fst s))
     ∧ (∀ x k, ¬ In (FBufItem x k) ((fst s).(TSOMemoryMachine.buffers) tid))
        | Some (RIInjectState _ _ _ _ _ _
               (NormalState irs (Satomicmem r cas args dst) k)) =>
       ∃ instr, ∃ p, ∃ v, atomic_statement_mem_event r cas (map irs args) v (MErmw r p v instr)
       ∧ wf_rmw instr
       ∧ wf_ptr p
       ∧ load_ptr Mint32 (fst s).(MemoryMachine.mem_rtl) p = Some v ∧ wf_val v
       ∧ ∃m', store_ptr Mint32 (fst s).(MemoryMachine.mem_rtl) p (rmw_instr_semantics instr v) = Some m'
       ∧ ∃d', (if r then release tid (fst s).(MemoryMachine.perms) d' else (fst s).(MemoryMachine.perms)=d') ∧ d' p = empty_perm
        | Some (RIInjectState stk c sp pc rs dst
               (NormalState irs (Srequestperm rp addr args) k)) =>
      ∀ p, eval_addressing ge sp addr (map irs args) = Some (Vptr p) →
      ∃ perm',
        perm_step tid (fst s).(MemoryMachine.perms) (PErequest rp p) perm'
        | Some (RIInjectState stk c sp pc rs dst
               (NormalState irs Srelease k)) =>
      ∃ perm',
        perm_step tid (fst s).(MemoryMachine.perms) PErelease perm'
        | Some (RIInjectState stk c sp pc rs dst
               (NormalState irs (Sstore released ap addr args src) k)) =>
      (∀ p, eval_addressing ge sp addr (map irs args) = Some (Vptr p) →
            check_perm_store tid (fst s).(MemoryMachine.perms) ap p ∧ wf_ptr p)
      ∧
      if released then ∃ perm',
        perm_step tid (fst s).(MemoryMachine.perms) PErelease perm'
      else True
        | Some (RIInjectState stk c sp pc rs dst
               (NormalState irs Sfreeperm k)) =>
      ∃ perm',
        perm_step tid (fst s).(MemoryMachine.perms) PEfreeperm perm'
        | _ => True
      end.

  Remark progress_progress' (s: state) :
    progress s → progress' s.

  Lemma safe_not_stuck s tso st tid ts :
    safe_state s →
    match_state s (tso, st) →
    st ! tid = Some ts →
    ¬ ∀ ts' ev, ¬ rtl_step' ge ts ev ts'.

  Definition bw_step_spec : Prop :=
    ∀ s t ev t',
      ev ≠ Eoutofmemory →
      safe_state s →
      match_state s t →
      l_step t ev t' →
      ∃tid, ∃e, ∃s',
        astep ge s (tid, e::nil) s'
      ∧ match_ev e ev
      ∧ match_state s' t'
  .

  Lemma bw_step : bw_step_spec.

  Lemma bw_taustar :
      ∀ j j',
        taustar (rtli_lts ge) j j' →
        ∀ i,
          match_state i j →
          (∀ s, reachable i s → can_unbuffer (fst s) ∧ progress s ∧ wf_load s) →
        ∃ tr, ∃ i',
           low_trace ge i tr i' ∧ filter_fullevent tr = nil ∧ match_state i' j'.

  Lemma bw_fintrace :
    ∀ j trace j',
      Traces.fintrace (rtli_lts ge) j trace j' →
      ∀ i,
        match_state i j →
        (∀ s, reachable i s → can_unbuffer (fst s) ∧ progress s ∧ wf_load s) →
        ∃ tr, ∃ i',
           low_trace ge i tr i' ∧ filter_fullevent tr = rev trace ∧ match_state i' j'.

End LOWSIM.

Definition init (p: program) (ge: genv) (s: state) : Prop :=
  (∀ p, (fst s).(MemoryMachine.perms) p = empty_perm)
∧ (∀ tid, (fst s).(TSOMemoryMachine.buffers) tid = nil)
∧ (TSO.init RtlInjectSem p nil ge (mktsostate (fun _ => nil) (fst s).(MemoryMachine.mem_rtl), snd s)).

Definition safe_program (p: program) : Prop :=
  ∀ ge s,
    init p ge s →
    ∀ s', reachable ge s s' → can_unbuffer (fst s') ∧ progress ge s' ∧ wf_load ge s'.

Inductive low_traces (p: program) : Traces.trace event → Prop :=
| LTr ge i f tr trf t
      (INIT: init p ge i)
      (TRACE: low_trace ge i tr f)
      (FILTER: trf = rev (filter_fullevent tr))
      (NOFAIL: ¬In Efail trf)
      (TEQ: Traces.appt trf Traces.Send = t)
  : low_traces p t
| LTrF ge i f f' tr trf t t' x fe
      (INIT: init p ge i)
      (TRACE: low_trace ge i tr f)
      (FILTER: trf = rev (filter_fullevent tr))
      (NOFAIL: ¬In Efail trf)
      (FAILSTEP: astep ge f (x, (fe::nil)) f')
      (FAIL: fe = TEext Efail ∨ fe = TEend FailEvent ∨ fe = TEend ReturnVoid)
      (TEQ: Traces.appt trf t' = t)
  : low_traces p t
.

Lemma init_ex p ge s :
  TSO.init RtlInjectSem p nil ge s →
  ∃ s', init p ge s' ∧ match_state s' s.

Inductive tfin : Traces.trace event -> Prop :=
  | tfin_end: tfin Traces.Send
  | tfin_cons x t:
      tfin t → tfin (Traces.Scons x t)
.

Lemma fintrace_no_fail {ge j trace j'} :
  Traces.fintrace (rtli_lts ge) j trace j' →
  ¬ In Efail trace.

Lemma bw_sim p :
  safe_program p →
  ∀ trace, rtli_traces p nil trace →
           tfin trace →
           low_traces p trace.