Library mcertikos.multicore.semantics.ConcurrentOracle

Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Events.
Require Import Globalenvs.
Require Import Conventions.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import Smallstep.
Require Import CommonTactic.
Require Import Coq.Logic.FunctionalExtensionality.

Require Import AuxFunctions.
Require Import LAsm.
Require Import GlobalOracle.
Require Import liblayers.compat.CompatLayers.
Require Import MBoot.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import LAsmModuleSem.
Require Import Soundness.
Require Import CompatExternalCalls.
Require Import LinkTactic.
Require Import I64Layer.
Require Import StencilImpl.
Require Import MakeProgram.
Require Import MakeProgramImpl.
Require Import LAsmModuleSemAux.

Require Import Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
Require Import Concurrent_Linking_Prop.

Require Import HWSemImpl.

Section ORACLEPROPINSTANCES.

  Section ORACLEPROPSEPINSTANCE.

    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.
    Context `{multi_oracle_prop: MultiOracleProp}.
    Context `{zset_op: ZSet_operation}.

    Definition SepOracleType := (Z × separate_log_type × ident) → option (Z × separate_log_type).

    Definition separate_log_len (l: Z × separate_log_type × ident) :=
      match l with
      | (_, l0, _) ⇒ list_Len l0
      end.

    Global Instance op_sep :
      OracleProp (ret:= separate_log_type)
                 (log:= Z × separate_log_type × ident) (log_len:= separate_log_len)
                 (hdset := hdseting) :=
      {
        Oracle := SepOracleType;
        oget A l o := match o l with
                       | Some (i, g) ⇒ if A i then Some g else None
                       | _ ⇒ None
                       end;
        append_o o1 o2 l :=
          match o1 l with
          | Some l´ ⇒ Some l´
          | _ ⇒ o2 l
          end;
        uoracle i l e l´:=
          if separate_log_dec l l´ then
            Some (i, e) else None;
        empty_o l := None
      }.
    Proof.
      - eapply separate_log_dec.
      - unfold separate_log_len; simpl. intros. destruct l1, l2.
        destruct p, p0. red; intros HF. inv HF.
        elim Hneq; trivial.
      - intros. eapply functional_extensionality_dep; intros.
        destruct (o1 x) eqn: Hx1; destruct (o2 x) eqn: Hx2.
        + destruct p, p0.
          specialize (Heq (s_set z) x).
          rewrite Hx1, Hx2 in Heq.
          destruct (zeq z z0); subst.
          × rewrite s_set_in in Heq. inv Heq. trivial.
          × rewrite s_set_in in Heq.
            rewrite s_set_not_in in Heq; auto. inv Heq.
        + destruct p.
          specialize (Heq (s_set z) x).
          rewrite Hx1, Hx2 in Heq.
          rewrite s_set_in in Heq. inv Heq.
        + destruct p.
          specialize (Heq (s_set z) x).
          rewrite Hx1, Hx2 in Heq.
          rewrite s_set_in in Heq. inv Heq.
        + trivial.

      - intros. destruct (o1 l); trivial. inv H.
      - intros. destruct (o1 l) eqn: Ho1; trivial.
        destruct p. destruct (A z) eqn: HA. inv H.
        destruct (o2 l) eqn: Ho2; trivial.
        destruct p. destruct (A z0) eqn: HA0; trivial.
        destruct Hdis as (A0 & B0 & HI1 & HI2 & HD).
        specialize (HI1 l).
        specialize (HI2 l).
        specialize (HD (separate_log_len l)).
        destruct HD as (HD1 & HD2).
        destruct (A0 (separate_log_len l)).
        + specialize (HD1 eq_refl).
          specialize (HI2 HD1 A). rewrite Ho2, HA0 in HI2. inv HI2.
        + specialize (HI1 eq_refl (s_set z)).
          rewrite Ho1, s_set_in in HI1. inv HI1.

      - intros. destruct (o1 l) eqn: Ho1; trivial.
        destruct p. left; trivial. right. split; trivial.
      - intros. eapply functional_extensionality_dep.
        intros. destruct (o1 x); trivial.
      - intros.
        destruct (separate_log_dec l l); trivial. rewrite H. trivial. congruence.
      - intros. destruct (separate_log_dec l l´); subst; trivial.
        destruct H.
        + congruence.
        + rewrite H. trivial.
      - trivial.
      - intros. eapply functional_extensionality_dep.
        intros.
        destruct (o x); trivial.
      - intros. destruct (o l); trivial.
        destruct p. destruct (A1 z) eqn: HA1; try congruence.
        inv H. eapply H0 in HA1. rewrite HA1. trivial.
    Defined.

  End ORACLEPROPSEPINSTANCE.

  Section ORACLEPROPREORDERINSTANCE.

    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.
    Context `{multi_oracle_prop: MultiOracleProp}.
    Context `{zset_op: ZSet_operation}.

    Definition ReorderOracleType := Log → option (Z × Log).

    Global Instance op_reorder :
      OracleProp (ret:= Log)
                 (log:= Log) (log_len:= list_Len)
                 (hdset := hdseting) :=
      {
        Oracle := ReorderOracleType;
        oget A l o := match o l with
                      | Some (i, g) ⇒ if A i then Some g else None
                      | _ ⇒ None
                      end;
        append_o o1 o2 l :=
          match o1 l with
          | Some l´ ⇒ Some l´
          | _ ⇒ o2 l
          end;
        uoracle i l e l´:=
          if Log_dec l l´ then
            Some (i, e) else None;
        empty_o l := None
      }.
    Proof.
      - eapply Log_dec.
      - unfold list_Len; simpl.
        destruct l1, l2; simpl; intros.
        + elim Hneq; auto.
        + intros HF; inv HF.
        + intros HF; inv HF.
        + intros HF.
          inv HF.
          elim Hneq.
          reflexivity.
      - intros. eapply functional_extensionality_dep; intros.
        destruct (o1 x) eqn: Hx1; destruct (o2 x) eqn: Hx2.
        + destruct p, p0.
          specialize (Heq (s_set z) x).
          rewrite Hx1, Hx2 in Heq.
          destruct (zeq z z0); subst.
          × rewrite s_set_in in Heq. inv Heq. trivial.
          × rewrite s_set_in in Heq.
            rewrite s_set_not_in in Heq; auto. inv Heq.
        + destruct p.
          specialize (Heq (s_set z) x).
          rewrite Hx1, Hx2 in Heq.
          rewrite s_set_in in Heq. inv Heq.
        + destruct p.
          specialize (Heq (s_set z) x).
          rewrite Hx1, Hx2 in Heq.
          rewrite s_set_in in Heq. inv Heq.
        + trivial.

      - intros. destruct (o1 l); trivial. inv H.
      - intros. destruct (o1 l) eqn: Ho1; trivial.
        destruct p. destruct (A z) eqn: HA. inv H.
        destruct (o2 l) eqn: Ho2; trivial.
        destruct p. destruct (A z0) eqn: HA0; trivial.
        destruct Hdis as (A0 & B0 & HI1 & HI2 & HD).
        specialize (HI1 l).
        specialize (HI2 l).
        specialize (HD (list_Len l)).
        destruct HD as (HD1 & HD2).
        destruct (A0 (list_Len l)).
        + specialize (HD1 eq_refl).
          specialize (HI2 HD1 A). rewrite Ho2, HA0 in HI2. inv HI2.
        + specialize (HI1 eq_refl (s_set z)).
          rewrite Ho1, s_set_in in HI1. inv HI1.

      - intros. destruct (o1 l) eqn: Ho1; trivial.
        destruct p. left; trivial. right. split; trivial.
      - intros. eapply functional_extensionality_dep.
        intros. destruct (o1 x); trivial.
      - intros.
        destruct (Log_dec l l); trivial. rewrite H. trivial. congruence.
      - intros. destruct (Log_dec l l´); subst; trivial.
        destruct H.
        + congruence.
        + rewrite H. trivial.
      - trivial.
      - intros. eapply functional_extensionality_dep.
        intros.
        destruct (o x); trivial.
      - intros. destruct (o l); trivial.
        destruct p. destruct (A1 z) eqn: HA1; try congruence.
        inv H. eapply H0 in HA1. rewrite HA1. trivial.
    Defined.

  End ORACLEPROPREORDERINSTANCE.

  Section ORACLEPROPGENERALINSTANCE.

    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.
    Context `{multi_oracle_prop: MultiOracleProp}.
    Context `{zset_op: ZSet_operation}.

    Definition GeneralOracleType := Log → option (Z × event).

    Global Instance op_general :
      OracleProp (ret:= event)
                 (log:= Log) (log_len:= list_Len)
                 (hdset := hdseting) :=
      {
        Oracle := GeneralOracleType;
        oget A l o := match o l with
                      | Some (i, g) ⇒ if A i then Some g else None
                      | _ ⇒ None
                      end;
        append_o o1 o2 l :=
          match o1 l with
          | Some l´ ⇒ Some l´
          | _ ⇒ o2 l
          end;
        uoracle i l e l´:=
          if Log_dec l l´ then
            Some (i, e) else None;
        empty_o l := None
      }.
    Proof.
      - eapply Log_dec.
      - unfold list_Len; simpl.
        destruct l1, l2; simpl; intros.
        + elim Hneq; auto.
        + intros HF; inv HF.
        + intros HF; inv HF.
        + intros HF.
          inv HF.
          elim Hneq.
          reflexivity.
      - intros. eapply functional_extensionality_dep; intros.
        destruct (o1 x) eqn: Hx1; destruct (o2 x) eqn: Hx2.
        + destruct p, p0.
          specialize (Heq (s_set z) x).
          rewrite Hx1, Hx2 in Heq.
          destruct (zeq z z0); subst.
          × rewrite s_set_in in Heq. inv Heq. trivial.
          × rewrite s_set_in in Heq.
            rewrite s_set_not_in in Heq; auto. inv Heq.
        + destruct p.
          specialize (Heq (s_set z) x).
          rewrite Hx1, Hx2 in Heq.
          rewrite s_set_in in Heq. inv Heq.
        + destruct p.
          specialize (Heq (s_set z) x).
          rewrite Hx1, Hx2 in Heq.
          rewrite s_set_in in Heq. inv Heq.
        + trivial.

      - intros. destruct (o1 l); trivial. inv H.
      - intros. destruct (o1 l) eqn: Ho1; trivial.
        destruct p. destruct (A z) eqn: HA. inv H.
        destruct (o2 l) eqn: Ho2; trivial.
        destruct p. destruct (A z0) eqn: HA0; trivial.
        destruct Hdis as (A0 & B0 & HI1 & HI2 & HD).
        specialize (HI1 l).
        specialize (HI2 l).
        specialize (HD (list_Len l)).
        destruct HD as (HD1 & HD2).
        destruct (A0 (list_Len l)).
        + specialize (HD1 eq_refl).
          specialize (HI2 HD1 A). rewrite Ho2, HA0 in HI2. inv HI2.
        + specialize (HI1 eq_refl (s_set z)).
          rewrite Ho1, s_set_in in HI1. inv HI1.

      - intros. destruct (o1 l) eqn: Ho1; trivial.
        destruct p. left; trivial. right. split; trivial.
      - intros. eapply functional_extensionality_dep.
        intros. destruct (o1 x); trivial.
      - intros.
        destruct (Log_dec l l); trivial. rewrite H. trivial. congruence.
      - intros. destruct (Log_dec l l´); subst; trivial.
        destruct H.
        + congruence.
        + rewrite H. trivial.
      - trivial.
      - intros. eapply functional_extensionality_dep.
        intros.
        destruct (o x); trivial.
      - intros. destruct (o l); trivial.
        destruct p. destruct (A1 z) eqn: HA1; try congruence.
        inv H. eapply H0 in HA1. rewrite HA1. trivial.
    Defined.

  End ORACLEPROPGENERALINSTANCE.

End ORACLEPROPINSTANCES.

Section MCLink_Configure.

  Context `{multi_oracle_prop : MultiOracleProp}.

  Lemma current_CPU_ID_in_core_set: cpu_set current_CPU_ID = true.
  Proof.
    unfold cpu_set.
    generalize current_CPU_ID_range.
    intros.
    rewrite zle_lt_true; auto.
  Qed.

End MCLink_Configure.

Section SEPARATEORACLE.


  Context `{Hmem: Mem.MemoryModelX}.
  Context `{Hmwd: UseMemWithData mem}.
  Context `{multi_oracle_prop: MultiOracleProp}.

  Function fake_atomic_primitive_without_switch_points (p: ident): Prop :=
    if peq p acquire_shared then True
    else if peq p release_shared then True
         else if peq p log_incr then True
              else if peq p log_init then True
                   else if peq p log_hold then True
                        else if peq p page_copy then True
                             else False.

  Function relate_event (e: MultiOracleEvent) :=
    match e with
    | TEVENT i e0 ⇒
      match e0 with
      | TTICKET e1 ⇒
        match e1 with
        | INC_TICKET n ⇒ Some (SEATOMIC i (OINC_TICKET n))
        | INC_NOW ⇒ Some (SEATOMIC i OINC_NOW)
        | GET_NOW ⇒ Some (SEATOMIC i OGET_NOW)
        | HOLD_LOCK ⇒ Some (SEATOMIC i OHOLD_LOCK)
        | _ ⇒ None
        end
      | TSHARED (OMEME l) ⇒ Some (SEREL i l)
      | TSHARED (OPULL) ⇒ Some (SEACQ i)
      | TSHARED (OBUFFERE b) ⇒ Some (SEATOMIC i (OPAGE_COPY b))
      | _ ⇒ None
      end
    end.

  Inductive relate_log: MultiLog → separate_log_type → Prop :=
  | RELATE_LOG_INIT:
      ∀ id,
        relate_log nil (SEATOMIC id OINIT :: nil)
  | RELATE_LOG_CONS:
      ∀ e e1 l l1
             (Hrel_e: relate_event e = Some e1)
             (Hrel_l: relate_log l l1),
        relate_log (e:: l) (e1:: l1).

  Inductive relate_log_type : MultiLogType → separate_log_type → Prop :=
  | RELATE_LOG_TYPE_UNDEF:
      ∀ l,
        relate_log_type MultiUndef l
  | RELATE_LOG_TYPE_DEF:
      ∀ l l´
             (Hrel_log: relate_log l l´),
        relate_log_type (MultiDef l) l´.

  Inductive relate_log_pool : separate_log → MultiLogPool → Prop :=
  | relate_log_pool_intro:
      ∀ ml sl
             (Hrel: ∀ id,
                 relate_log_type (ZMap.get id ml) (ZMap.get id sl)),
        relate_log_pool sl ml.

End SEPARATEORACLE.

Section OracleDef.

  Context `{Hmem: Mem.MemoryModelX}.
  Context `{Hmwd: UseMemWithData mem}.
  Context `{multi_oracle_prop: MultiOracleProp}.

  Class MCLinkOracle :=
    {
      hw_oracle : GeneralOracleType;
      single_oracle: GeneralOracleType;
      reorder_oracle: ReorderOracleType;
      reorder_oracle_red: ReorderOracleType;
      sep_oracle: SepOracleType
    }.

End OracleDef.

Section MCORACLEPROPCOND.


  Context `{Hmem: Mem.MemoryModelX}.
  Context `{Hmwd: UseMemWithData mem}.
  Context `{real_params: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.

  Context `{zset_op: ZSet_operation}.
  Context `{pmap: PartialMap}.
  Context `{fair: Fairness}.
  Context `{mc_oracle: !MCLinkOracle}.

  Definition hardware_local_step_aux (ge : genv) (sten : stencil) (M : module)
             (Hprog: make_globalenv sten M (mboot ⊕ L64) = ret ge) :=
    @hardware_local_step hdseting (@hdsem mem memory_model_ops Hmem Hmwd real_params_ops oracle_ops0 oracle_ops big_ops
                                          builtin_idents_norepet_prf ge sten M Hprog).

  Definition reorder_oracle´ := @reorder_oracle mem memory_model_ops Hmwd oracle_ops0 oracle_ops big_ops mc_oracle.

  Definition valid_hw_oracle_def := valid_oracle current_CPU_ID core_set hw_oracle.
  Definition valid_single_oracle_def := valid_oracle current_CPU_ID (s_set current_CPU_ID) single_oracle.
  Definition valid_reorder_reduce_oracle´_def := valid_oracle´ current_CPU_ID reorder_oracle_red.

  Definition relate_hw_step_hw_oracle_def :=
    ∀ l curid lsp psp (ge: genv) (sten :stencil) (M : module) (Hprog: make_globalenv sten M (mboot ⊕ L64) = ret ge),
      match_state (hdset := hdseting) (pmap := pmap) current_CPU_ID (State curid lsp l) (HState curid psp l) →
      valid_log current_CPU_ID (EYIELD curid::l) →
      ∃ ev,
        oget (OracleProp := op_general) core_set (EYIELD curid :: l) hw_oracle = Some ev ∧
        ∀ curid´´,
          ev = EBACK curid´´ →
          ∀ curid´ ps st,
            (hardware_local_step_aux ge sten M Hprog) curid´ (LView ps (EBACK curid´ :: EYIELD curid :: l)) st →
            curid´ = curid´´.

  Definition relate_single_oracle_hw_oracle_def :=
    ∀ l ev, valid_log current_CPU_ID l →
                 lastEvTy l = Some YIELDTY →
                 oget (hdset := hdseting) (OracleProp := op_general) (s_set current_CPU_ID) l single_oracle = Some ev →
                 oget (hdset := hdseting) (OracleProp := op_general) core_set l hw_oracle = Some ev.

  Definition relate_single_oracle_concrete_step_def :=
    ∀ curid´ curid lsp´ lsp l´ l l_res ps ev (ge: genv) (sten :stencil) (M : module) (Hprog: make_globalenv sten M (mboot ⊕ L64) = ret ge),
      match_eestate (zset_op := zset_op) (hdset := hdseting) (op := op_general)
                    (pmap := pmap) single_oracle current_CPU_ID (EState curid´ lsp´ l´) (EState curid lsp l) →
      get_curid_from_log current_CPU_ID l ≠ current_CPU_ID →
      pget (get_curid_from_log current_CPU_ID l) lsp = Some (LState ps false) →
      oget (hdset := hdseting) (OracleProp := op_general) (s_set current_CPU_ID) l single_oracle = Some ev →
      local_step_ev ev = Some l_res →
      lastEvTy l = Some EBACKTY →
      ∃ ps´ : private_state,
        (hardware_local_step_aux ge sten M Hprog) (get_curid_from_log current_CPU_ID l) (LView ps l) (LView ps´ l_res).

  Definition relate_reorder_oracle_single_oracle_def :=
    ∀ ps_h l_h ps_l l_l al,
      match_osstate (hdset := hdseting) current_CPU_ID (RState ps_h l_h) (SRState ps_l l_l al) →
      valid_log current_CPU_ID (EYIELD current_CPU_ID::al ++ l_l) →
      ∃ l1, AbsYieldBack (op := op_general) time_bound current_CPU_ID
                              (EYIELD current_CPU_ID::al ++ l_l) nil single_oracle = Some l1 ∧
                 ∀ l1´, oget (OracleProp := op_reorder) (s_set current_CPU_ID) l_h reorder_oracle´= Some l1´ →
                             l1´ = l1 ++ EYIELD current_CPU_ID :: al.

  Definition relate_reorder_oracles_def :=
    ∀ ps l l_h,
      match_rrstate (hdset := hdseting) (RState ps (reduce_log l)) (RState ps l) →
      oget (OracleProp := op_reorder) (s_set current_CPU_ID) (reduce_log l) reorder_oracle_red = Some l_h →
      ∃ l_l, oget (OracleProp := op_reorder) (s_set current_CPU_ID) l reorder_oracle = Some l_l ∧ l_h = reduce_log l_l.

  Definition relate_separate_oracle_reorder_oracle_def :=
    ∀ ps sep_l glob_l id id_l id_l´ e,
      match_spstate current_CPU_ID (SPState ps sep_l) (RState ps glob_l) →
      ZMap.get id sep_l = id_l → oget (OracleProp := op_sep) (s_set current_CPU_ID) (id, id_l, e) sep_oracle = Some id_l´ →
      ∃ glob_l´,
        oget (OracleProp := op_reorder) (s_set current_CPU_ID) glob_l reorder_oracle_red = Some glob_l´ ∧
        log_get_atomic (glob_l´ ++ glob_l) id = separate_log_type_2_log (id_l´ ++ id_l) id.

  Definition sep_oget_init_def := ∀ z l l´ i (Hget: sep_oracle (z, l, log_init) = Some (i, l´)), l = nil ∧ l´ = nil.

  Definition relate_oracle_correct_def :=
    ∀ id cid c l l´ l0´
      (Hrel_log: relate_log l l´)
      (Hfake: ¬ fake_atomic_primitive_without_switch_points c)
      (Hget: oget (OracleProp:= op_sep) (s_set cid) (id, l´, c) sep_oracle = Some l0´),
      relate_log (ZMap.get id multi_oracle_init0 cid l ++ l) (l0´ ++ l´).

  Definition fake_oracle_assumption_def :=
    ∀ id cid c l l´
      (Hrel_log: relate_log_type l´ l),
    ∃ l0, oget (OracleProp:= op_sep) (s_set cid) (id, l, c) sep_oracle = Some l0
          ∧ (∀ (Hfake: fake_atomic_primitive_without_switch_points c),
                l0 = nil).

End MCORACLEPROPCOND.

Section MCLinkOracleCondDef.

  Context `{Hmem: Mem.MemoryModelX}.
  Context `{Hmwd: UseMemWithData mem}.
  Context `{real_params: RealParams}.
  Context `{multi_oracle_prop: MultiOracleProp}.
  Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.

  Context `{zset_op: ZSet_operation}.
  Context `{pmap: PartialMap}.

  Class MCLinkOracleCond `{fair: Fairness} `{mc_oracle: !MCLinkOracle} :=
    {
      
      valid_hw_oracle: valid_hw_oracle_def;
      valid_single_oracle: valid_single_oracle_def;
      valid_reorder_reduce_oracle: valid_reorder_reduce_oracle´_def;
  
      
      
      relate_hw_step_hw_oracle: relate_hw_step_hw_oracle_def;
      
      relate_single_oracle_hw_oracle: relate_single_oracle_hw_oracle_def;
      relate_single_oracle_concrete_step: relate_single_oracle_concrete_step_def;
      
      relate_reorder_oracle_single_oracle: relate_reorder_oracle_single_oracle_def;
      
      relate_reorder_oracles : relate_reorder_oracles_def;
      
      relate_separate_oracle_reorder_oracle : relate_separate_oracle_reorder_oracle_def;

      
      
      sep_oget_init: sep_oget_init_def;
      relate_oracle_correct: relate_oracle_correct_def;
      fake_oracle_assumption: fake_oracle_assumption_def
    }.

End MCLinkOracleCondDef.