Library mcertikos.multicore.refins.AsmEnvSemtoEnvSem
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 EnvSemImpl.
Require Import FutureTactic.
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_sep.
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 env_step_single_aux_ge´ :=
@env_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
(s_set current_CPU_ID) single_oracle ge sten M Hmakege.
Definition env_step_full_aux_ge´ :=
@env_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
core_set hw_oracle ge sten M Hmakege.
Lemma env_step_aux_eq :
∀ zs o s t s´,
env_step_aux_ge zs o ge sten M (Hmakege:=Hmakege) ge s t s´ ↔
env_step_aux zs o ge sten M (Hmakege:=Hmakege) s t s´.
Proof.
intros; split; intros.
inversion H; auto.
constructor; auto.
Qed.
Existing Instance op_general.
Definition match_eestate_link := @match_eestate zset_op hdseting op_general pmap single_oracle current_CPU_ID.
Hint Unfold match_eestate_link.
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.
Lemma one_step_env_refines_env_concrete:
∀ st t st´ st0
(Hone: env_step_single_aux_ge´ ge st t st´)
(Hmatch: match_eestate_link st st0),
(∃ st0´,
(plus env_step_full_aux_ge´) ge st0 t st0´ ∧
match_eestate_link st´ st0´) ∨
((state_measure (s_set current_CPU_ID) st´ < state_measure (s_set current_CPU_ID) st)%nat ∧ t = E0 ∧
match_eestate_link st´ st0).
Proof.
simpl in ×.
unfold env_step_single_aux_ge´.
unfold env_step_full_aux_ge´.
intros.
rewrite env_step_aux_eq in Hone.
unfold env_step_aux in Hone; simpl in ×.
unfold match_eestate_link in ×.
assert (Hcore_el: core_set current_CPU_ID = true).
{ simpl.
apply current_CPU_ID_in_core_set. }
assert (Hvalid_oracle: valid_oracle current_CPU_ID (s_set current_CPU_ID) single_oracle).
{ inv mc_oracle_cond; auto. }
eapply single_env_step_refines_full_env_step in Hone; eauto.
{ destruct Hone as [Hone | Hone].
- destruct Hone as (s0´ & Hone1 & Hone2).
left.
∃ s0´.
split; auto.
inv Hone1.
eapply plus_star_trans.
eapply plus_one.
rewrite env_step_aux_eq.
unfold env_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 env_step_aux_eq.
unfold env_step_aux.
exact H.
eauto.
eauto. }
eauto.
- right; auto. }
{ intros; inv mc_oracle_cond; intros; eauto. }
{ intros; inv mc_oracle_cond.
unfold relate_single_oracle_concrete_step_def in relate_single_oracle_concrete_step.
unfold hardware_local_step_aux in relate_single_oracle_concrete_step.
eapply relate_single_oracle_concrete_step; eauto. }
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
(env_semantics
(s_set current_CPU_ID) single_oracle
(Hmakege := make_program_globalenv (make_program_ops := make_program_ops) _ _ _ _ Hmakep)
(Genv.globalenv ph) s CTXT ph)
(env_semantics
core_set hw_oracle
(Hmakege := make_program_globalenv (make_program_ops := make_program_ops) _ _ _ _ Hmakep)
(Genv.globalenv ph) s CTXT ph).
Proof.
intros. apply forward_to_backward_simulation; eauto.
- eapply forward_simulation_star with
(match_states := match_eestate_link)
(measure := @state_measure hdseting pmap (s_set current_CPU_ID));
unfold match_eestate_link; simpl in *; intros; eauto.
+ inv H.
∃(EState 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.
× eapply MATCH_EESTATE_S.
{ simpl; auto. }
{ generalize current_CPU_ID_in_core_set; eauto. }
{ constructor.
- generalize current_CPU_ID_in_core_set; eauto.
- simpl; auto. }
{ simpl; auto. }
{ rewrite pgss.
rewrite pgss.
auto.
simpl.
apply current_CPU_ID_in_core_set.
apply s_set_in; auto. }
{ intros.
subst.
rewrite pgss in H1; auto; [ inv H1 | ].
generalize current_CPU_ID_in_core_set; eauto. }
{ intros.
rewrite pgso in H1; auto.
assert (core_set tid = true).
{ eapply pget_some_domain in H1.
auto. }
rewrite pinit_gi in H1; auto.
inv H1; auto. }
{ intros.
simpl in H1; inv H1. }
{ intros; auto. }
+ generalize one_step_env_refines_env_concrete.
unfold env_step_single_aux_ge´.
unfold env_step_full_aux_ge´.
unfold match_eestate_link.
intros Htemp.
exploit Htemp; eauto.
-
eapply env_semantics_receptive.
-
eapply env_semantics_determinate; eauto.
Qed.
End LinkSim.