Library mcertikos.multicore.refins.AsmOracleSemtoHWStepSem
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 liblayers.compat.CompatGenSem.
Require Import TacticsForTesting.
Require Import Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
Require Import Concurrent_Linking_Prop.
Require Import HWSemImpl.
Require Import ConcurrentOracle.
Require Import OracleSemImpl.
Require Import HWStepSemImpl.
Section LinkwithLAsm.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).
Local Open Scope Z_scope.
Context `{pmap: PartialMap}.
Context `{zset_op: ZSet_operation}.
Existing Instance hdseting.
Existing Instance op_general.
Existing Instance hdsem.
Context `{mc_oracle_cond: MCLinkOracleCond (mem := mem) (memory_model_ops := memory_model_ops) (Hmwd := Hmwd)
(Hmem := Hmem) (real_params_ops := real_params_ops)
(oracle_ops0 := oracle_ops0) (oracle_ops := oracle_ops) (big_ops := big_ops)
(builtin_idents_norepet_prf := builtin_idents_norepet_prf)
(zset_op := zset_op) (pmap := pmap)}.
Section WITH_GE.
Variables (ge: genv) (sten: stencil) (M: module).
Context {Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
sten M (mboot ⊕ L64) = ret ge}.
Definition hdsem_instance := @hdsem mem memory_model_ops Hmem Hmwd real_params_ops oracle_ops0
oracle_ops big_ops builtin_idents_norepet_prf ge sten M Hmakege.
Definition oracle_step_aux_ge´ :=
@oracle_step_aux_ge mem memory_model_ops Hmem Hmwd
real_params_ops oracle_ops0 oracle_ops big_ops
builtin_idents_norepet_prf pmap zset_op mc_oracle
ge sten M Hmakege.
Definition hw_step_aux_ge´ :=
@hw_step_aux_ge mem memory_model_ops Hmem Hmwd
real_params_ops oracle_ops0 oracle_ops big_ops
builtin_idents_norepet_prf pmap
ge sten M Hmakege.
Lemma oracle_step_aux_eq :
∀ s t s´,
oracle_step_aux_ge ge sten M (Hmakege:=Hmakege) ge s t s´ ↔
oracle_step_aux ge sten M (Hmakege:=Hmakege) s t s´.
Proof.
intros; split; intros.
inversion H; auto.
constructor; auto.
Qed.
Lemma hw_step_aux_eq :
∀ s t s´,
hw_step_aux_ge ge sten M (Hmakege:=Hmakege) ge s t s´ ↔
hw_step_aux ge sten M (Hmakege:=Hmakege) s t s´.
Proof.
intros; split; intros.
inversion H; auto.
constructor; auto.
Qed.
Definition match_state_link := match_state (hdset := hdseting) (pmap := pmap) current_CPU_ID.
Hint Unfold match_state_link.
Existing Instance op_general.
Lemma one_step_hw_refines_oracle_concrete:
∀ s s0 s´ t
(Hone: hw_step_aux_ge´ ge s t s´)
(Hmatch: match_state_link s0 s),
∃ s0´,
plus oracle_step_aux_ge´ ge s0 t s0´
∧ match_state_link s0´ s´.
Proof.
simpl in ×.
unfold hw_step_aux_ge´.
unfold oracle_step_aux_ge´.
intros.
rewrite hw_step_aux_eq in Hone.
unfold hw_step_aux in Hone; simpl in ×.
eapply one_step_hw_refines_oracle with (hw_o := hw_oracle) in Hone; eauto.
{ destruct Hone as (s0´ & Hone1 & Hone2).
∃ s0´.
split; auto.
inv Hone1.
eapply plus_star_trans.
eapply plus_one.
rewrite oracle_step_aux_eq.
unfold oracle_step_aux; simpl; eauto.
instantiate (1:= t2).
simpl.
generalize dependent H0.
clear H Hmatch Hone2.
{ induction 1.
constructor.
eapply star_trans.
eapply star_one.
rewrite oracle_step_aux_eq.
unfold oracle_step_aux.
exact H.
eauto.
eauto. }
eauto. }
{ generalize current_CPU_ID_in_core_set; intros; auto. }
{ inv mc_oracle_cond; auto. }
{ inv mc_oracle_cond.
unfold relate_hw_step_hw_oracle_def in ×.
unfold hardware_local_step_aux in *; simpl in ×.
intros.
eapply relate_hw_step_hw_oracle; eauto.
inv H.
constructor; simpl; auto.
generalize current_CPU_ID_in_core_set; intros; simpl in *; auto.
}
Qed.
Lemma match_state_implies_one_step_concrete:
∀ curid lsp l curid´ hsp l´,
match_state_link (State curid lsp l) (HState curid´ hsp l´) →
∃ curid´´ lsp´ l´, star oracle_step_aux_ge´ ge (State curid lsp l) E0 (State curid´´ lsp´ l´) ∧
l´ = (EBACK curid´´)::(EYIELD curid)::l ∧
(∀ ps, pget curid lsp = Some (LState ps true) →
lsp´ = pset curid (LState ps false) lsp).
Proof.
intros.
unfold match_state_link in H.
simpl in H.
eapply match_state_implies_one_step with (hw_o:= hw_oracle) in H; eauto.
{ instantiate (1:= hdsem_instance) in H.
destruct H as (curid´´ & lsp´ & l´´ & H1 & H2 & H3).
∃ curid´´, lsp´, l´´.
refine_split; auto.
clear H2 H3.
generalize dependent H1.
clear.
induction 1.
- eapply star_refl.
- eapply star_trans; eauto.
eapply star_one.
unfold oracle_step_aux_ge´ in ×.
rewrite oracle_step_aux_eq; auto. }
{ generalize current_CPU_ID_in_core_set; intros; auto. }
{ inv mc_oracle_cond; eauto. }
{ inv mc_oracle_cond.
unfold relate_hw_step_hw_oracle_def in ×.
unfold hardware_local_step_aux in *; simpl in ×.
intros.
eapply relate_hw_step_hw_oracle; eauto.
inv H0.
constructor; simpl; auto.
generalize current_CPU_ID_in_core_set; intros; simpl in *; auto. }
Qed.
Lemma one_step_hw_refines_oracle_progress_concrete´:
∀ s1 s2,
match_state_link s1 s2 →
(∀ s´ : state, star oracle_step_aux_ge´ ge s1 E0 s´ →
(∃ (t : trace) (s´´ : state), oracle_step_aux_ge´ ge s´ t s´´)) →
∃ (t : trace) (s2´ : hstate), hw_step_aux_ge´ ge s2 t s2´.
Proof.
intros.
pose proof H as Hmatch.
destruct s1; destruct s2.
assert (z = z0) by (inv H; auto); subst.
assert (l = l0) by (inv H; auto); subst.
rename p into lsp_o.
rename p0 into lsp_h.
rename l0 into l.
rename z0 into curid.
eapply match_state_implies_one_step_concrete in H.
destruct H as (curid´´ & lsp´´ & l´´ & Ha & Hb & Hc).
eapply H0 in Ha; subst.
assert (∃ ps, pget curid lsp_o = Some ps).
{ inv Hmatch.
eapply pget_some; eauto. }
assert (∃ ps´, pget curid lsp_h = Some ps´).
{ inv Hmatch.
eapply pget_some; eauto. }
destruct H as (ps & H).
destruct H1 as (ps´ & H1).
destruct ps as (ps & b).
assert (ps´ = ps ∧ b = true).
{ inv Hmatch.
exploit Hlsp; eauto.
intros Hlocal.
inv Hlocal; auto. }
destruct H2; subst.
rename lsp´´ into lsp_o´.
assert (lsp_o´ = pset curid (LState ps false) lsp_o).
{ eapply Hc; eauto. }
clear Hc.
destruct Ha as (t & s´´ & Ha).
clear H0.
inv Ha.
inv H0.
-
inv Hmatch.
assert (pget curid´´ lsp_h = Some ps0).
{ case_eq (zeq curid´´ (get_curid_from_log current_CPU_ID l)); intros; subst.
+ rewrite pgss in Hget_local; auto.
inv Hget_local; auto.
+ rewrite pgso in Hget_local; auto.
assert (core_set curid´´ = true).
{ eapply pget_some_domain in Hget_local; auto. }
assert (∃ ps´´, pget curid´´ lsp_h = Some ps´´).
{ eapply pget_some; eauto. }
destruct H4 as (ps´´ & H4).
exploit Hlsp; eauto.
intros.
inv H5; auto. }
∃ E0.
∃ (HState curid´´ (pset curid´´ ps´ lsp_h) (l´ ++ (EBACK curid´´ :: EYIELD (get_curid_from_log current_CPU_ID l) :: l))).
unfold hw_step_aux_ge´.
rewrite hw_step_aux_eq.
eapply hardware_exec_step_progress; eauto.
- inv Hmatch.
case_eq (zeq (get_curid_from_log current_CPU_ID l) curid´´).
+ intros; subst.
rewrite pgss in Hget_local; auto.
inv Hget_local.
+ intros.
rewrite pgso in Hget_local; auto.
assert (core_set curid´´ = true).
{ eapply pget_some_domain in Hget_local; auto. }
assert (∃ ps´´, pget curid´´ lsp_h = Some ps´´).
{ eapply pget_some; eauto. }
destruct H4 as (ps´´ & H4).
exploit (Hlsp curid´´); eauto; intros.
inv H5.
exploit Hmatch_program_neq; eauto; intros contra; inv contra.
Qed.
End WITH_GE.
End LinkwithLAsm.
Section LinkSim.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).
Local Open Scope Z_scope.
Context `{pmap: PartialMap}.
Context `{zset_op: ZSet_operation}.
Context `{mc_oracle_cond: MCLinkOracleCond (mem := mem) (memory_model_ops := memory_model_ops) (Hmwd := Hmwd)
(Hmem := Hmem) (real_params_ops := real_params_ops)
(oracle_ops0 := oracle_ops0) (oracle_ops := oracle_ops) (big_ops := big_ops)
(builtin_idents_norepet_prf := builtin_idents_norepet_prf)
(zset_op := zset_op) (pmap := pmap)}.
Theorem cl_backward_simulation:
∀ (s: stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
(Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (mboot ⊕ L64) = OK ph),
backward_simulation
(oracle_semantics
(Hmakege := make_program_globalenv (make_program_ops := make_program_ops) _ _ _ _ Hmakep)
(Genv.globalenv ph) s CTXT ph)
(hwstep_semantics
(Hmakege := make_program_globalenv (make_program_ops := make_program_ops) _ _ _ _ Hmakep)
(Genv.globalenv ph) s CTXT ph).
Proof.
intros.
eapply backward_simulation_plus
with (match_states := match_state_link); simpl; unfold match_state_link; eauto.
-
intros; inv H.
∃ (@HState hdseting pmap current_CPU_ID (pinit (B := core_set) (Asm.State rs0 m0)) nil).
constructor; auto.
-
intros; inv H.
∃ (State current_CPU_ID
(pset current_CPU_ID (LState (hdset := hdseting) (Asm.State rs0 m0) true)
(pinit (B := core_set) (LState (hdset := hdseting) (Asm.State rs0 m0) false)))
nil).
split.
+ constructor; auto.
+ unfold match_state_link.
inv H0.
constructor; simpl; auto; intros.
× rewrite pinit_gi in H2; auto.
assert (m1 = m0).
{ rewrite H in H1; inv H1; auto. }
unfold rs0, rs1; subst.
case_eq (zeq i current_CPU_ID); intros; subst.
{ rewrite pgss in H3; auto.
inv H3; inv H2.
assert (current_CPU_ID = current_CPU_ID → true = true) by auto.
assert (current_CPU_ID ≠ current_CPU_ID → true = false).
{ intros Htemp; elim Htemp; auto. }
eapply MATCH_LOCAL_NEQ; eauto. }
{ rewrite pgso in H3; auto.
rewrite pinit_gi in H3; auto.
inv H2; inv H3; constructor; eauto. }
× intro contra; inv contra.
× generalize current_CPU_ID_in_core_set; simpl; intros; auto.
× constructor; auto.
generalize current_CPU_ID_in_core_set; intros; auto.
simpl; auto.
-
unfold safe in *; intros.
simpl in ×.
generalize one_step_hw_refines_oracle_progress_concrete´.
unfold match_state_link.
unfold oracle_step_aux_ge´.
intros Htemp.
exploit Htemp; eauto.
intros.
apply H0 in H1.
destruct H1.
+ destruct H1; inv H1.
+ auto.
-
intros; simpl in ×.
generalize one_step_hw_refines_oracle_concrete.
unfold hw_step_aux_ge´.
unfold oracle_step_aux_ge´.
unfold match_state_link.
intros Htemp.
exploit Htemp; eauto.
Qed.
End LinkSim.