Library mcertikos.multicore.refins.AsmEnvSemtoOracleSem
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 OracleSemImpl.
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_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.
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.
Lemma env_step_aux_eq :
∀ s t s´,
env_step_aux_ge core_set hw_oracle ge sten M (Hmakege:=Hmakege) ge s t s´ ↔
env_step_aux core_set hw_oracle ge sten M (Hmakege:=Hmakege) s t s´.
Proof.
intros; split; intros.
inversion H; auto.
constructor; auto.
Qed.
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.
Definition match_estate_link := match_estate (hdset := hdseting) current_CPU_ID.
Hint Unfold match_estate_link.
Existing Instance op_general.
Lemma one_step_env_refines_oracle_concrete:
∀ s s0 s´ t
(Hone: env_step_aux_ge´ ge s t s´)
(Hmatch: match_estate_link s s0),
∃ s0´,
plus (oracle_step_aux_ge´) ge s0 t s0´
∧ match_estate_link s´ s0´.
Proof.
simpl in ×.
unfold env_step_aux_ge´.
unfold oracle_step_aux_ge´.
intros.
rewrite env_step_aux_eq in Hone.
unfold env_step_aux in Hone; simpl in ×.
unfold match_estate_link in Hmatch.
eapply (@one_step_env_refines_oracle zset_op hdseting op_general)
in Hone; [ | inv mc_oracle_cond; eauto | exact Hmatch].
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.
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
core_set hw_oracle
(Hmakege := make_program_globalenv (make_program_ops := make_program_ops) _ _ _ _ Hmakep)
(Genv.globalenv ph) s CTXT ph)
(oracle_semantics
(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_plus with
(match_states:= match_estate_link); intros; eauto; simpl in *; unfold match_estate_link in *;
simpl in ×.
+ 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; eauto.
× constructor; eauto.
{ eapply current_CPU_ID_in_core_set. }
{ constructor.
- eapply current_CPU_ID_in_core_set.
- simpl; auto. }
{ intro contra; inversion contra. }
{ intros.
rewrite pgso in H1; auto.
assert (core_set tid = true).
{ eapply pget_some_domain in H1; auto. }
rewrite pinit_gi in H1; eauto.
inv H1; auto. }
{ intros.
rewrite pgss in H; [ | eapply current_CPU_ID_in_core_set].
inv H; inv H4. }
+ generalize one_step_env_refines_oracle_concrete; simpl.
unfold env_step_aux_ge´.
unfold oracle_step_aux_ge´.
unfold match_estate_link.
intros Hstep.
eapply Hstep in H; eauto.
-
eapply env_semantics_receptive.
-
eapply oracle_semantics_determinate; eauto.
Qed.
End LinkSim.