Library mcertikos.conlib.conmtlib.AsmT2IIE
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.compcertx.MemWithData.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compat.CompatData.
Require Import liblayers.compat.CompatPrimSem.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatExternalCalls.
Require Import Decision.
Require Import GlobIdent.
Require Import CommonTactic.
Require Import Constant.
Require Import PrimSemantics.
Require Import LRegSet.
Require Import AuxStateDataType.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobalOracle.
Require Import liblayers.compat.CompatGenSem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Require Import SingleConfiguration.
Require Import LAsm.
Require Export TAsm.
Require Import IIEAsm.
Section Refinement.
Context `{single_link_c: SingleLinkConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil}.
Context `{L: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined L}.
Context `{lasmops: !LAsmAbsDataProp}.
Local Instance ec_ops : ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance lcfg_ops : LayerConfigurationOps := compatlayer_configuration_ops L.
Lemma star_step_get_env_log:
∀ ge rs d m curid l l´,
get_env_log limit curid l = Some l´ →
star iestep ge
(IEState (proc_id (uRData l))
(ZMap.set curid (Running rs) (ZMap.init Environment))
m
(ZMap.set curid (Some d) (ZMap.init None)) l) E0
(IEState curid
(ZMap.set curid (Running rs) (ZMap.init Environment))
m
(ZMap.set curid (Some d) (ZMap.init None)) l´).
Proof.
induction limit; intros.
- simpl in H; inv H.
- simpl in H.
destruct (zeq (proc_id (uRData l)) curid).
+ simpl in H; inv H; constructor.
+ eapply star_trans.
× eapply star_one.
eapply ieexec_step_external_empty; eauto.
rewrite ZMap.gso; auto.
rewrite ZMap.gi; trivial.
rewrite ZMap.gso; eauto.
rewrite ZMap.gi; trivial.
× eapply IHn in H.
repeat rewrite ZMap.gss in H.
eauto.
× trivial.
Qed.
Lemma get_env_log_same:
∀ curid l l´,
get_env_log limit curid l = Some l´ →
proc_id (uRData l´) = curid.
Proof.
induction limit; intros.
- inv H.
- simpl in H.
destruct (zeq (proc_id (uRData l)) curid).
{
inv H; trivial.
}
{
eapply IHn; eauto.
}
Qed.
Section CURID.
Definition P_CURID st st´ :=
∀ curid curid´ rs rs´ (m m´: mem) d d´ l l´
(ST: st = TState curid rs m d l)
(ST´: st´ = TState curid´ rs´ m´ d´ l´),
curid´ = curid.
Lemma one_TAsm_same_curid´:
∀ ge st st´ t,
tstep ge st t st´ →
P_CURID st st´.
Proof.
intros. unfold P_CURID. intros; subst.
inv H; trivial.
Qed.
Lemma star_TAsm_same_curid´:
∀ ge st st´,
star tstep ge st E0 st´ →
P_CURID st st´.
Proof.
intros ge.
eapply star_E0_ind.
- unfold P_CURID; intros. subst. inv ST´. trivial.
- intros. eapply one_TAsm_same_curid´ in H.
unfold P_CURID in *; intros; subst.
destruct s2.
exploit H; eauto. intros; subst.
exploit H0; eauto.
Qed.
Lemma star_TAsm_same_curid:
∀ ge curid curid´ rs rs´ m m´ d d´ l l´,
star tstep ge (TState curid rs m d l) E0
(TState curid´ rs´ m´ d´ l´) →
curid´ = curid.
Proof.
intros. exploit star_TAsm_same_curid´; eauto.
Qed.
End CURID.
Inductive match_tstate_iestate: (ZMap.t ThreadState) → (mem × mem) → (ZMap.t (option dproc)) →
regset → mem → dproc → Log → Z → Prop :=
| MATCH_TSTATE_IESTATE:
∀ (rs: regset) rsm (m: mem) (mp : mem × mem) (d: dproc) (dp : ZMap.t (option dproc)) curid l
(RSM: rsm = ZMap.set curid (Running rs) (ZMap.init Environment))
(Hcurid: proc_id (uRData l) = current_thread)
(MP: m = fst mp)
(DP: dp = ZMap.set curid (Some d) (ZMap.init None)),
match_tstate_iestate rsm mp dp rs m d l curid.
Theorem one_step_Asm_T2E:
∀ ge mp m m´ curid curid´ rsm rs rs´ l l´ dp d d´ t
(TStep: TAsm.tstep ge (TState curid rs m d l) t (TState curid´ rs´ m´ d´ l´))
(Match: match_tstate_iestate rsm mp dp rs m d l curid),
∃ rsm´ mp´ dp´,
plus IIEAsm.iestep ge (IEState curid rsm mp dp l) t
(IEState curid´ rsm´ mp´ dp´ l´)
∧ match_tstate_iestate rsm´ mp´ dp´ rs´ m´ d´ l´ curid´.
Proof.
intros. inv TStep.
-
inv Match.
refine_split´.
+ apply plus_one.
eapply ieexec_step_internal with (mset := mp) (mset´ := (m´, snd mp)); eauto.
× case_eq (decide (proc_id (uRData l´) = current_thread)); intros; subst; auto.
elim n; auto.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
× case_eq (decide (proc_id (uRData l´) = current_thread)); intros; subst; auto.
elim n; auto.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
+ econstructor; eauto.
rewrite ZMap.set2; trivial.
rewrite ZMap.set2; trivial.
-
inv Match.
refine_split´.
+ apply plus_one.
eapply ieexec_step_builtin; eauto.
× case_eq (decide (proc_id (uRData l´) = current_thread)); intros; subst; auto.
elim n; auto.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
× case_eq (decide (proc_id (uRData l´) = current_thread)); intros; subst; auto.
elim n; auto.
+ econstructor; eauto.
rewrite ZMap.set2; trivial.
rewrite ZMap.set2; trivial.
-
inv Match.
refine_split´.
+ apply plus_one.
eapply ieexec_step_annot; eauto.
× case_eq (decide (proc_id (uRData l´) = current_thread)); intros; subst; auto.
elim n; auto.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
× case_eq (decide (proc_id (uRData l´) = current_thread)); intros; subst; auto.
elim n; auto.
+ econstructor; eauto.
rewrite ZMap.set2; trivial.
rewrite ZMap.set2; trivial.
-
inv Match.
refine_split´.
+ apply plus_one.
eapply ieexec_step_external; eauto.
× case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
× case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto.
+ econstructor; eauto.
rewrite ZMap.set2; trivial.
subdestruct; try (inv NON_YIELD; simpl; auto; fail).
destruct NON_YIELD as (? & ? & ? & ? & ?); subst.
rewrite <- Hcurid.
apply uRData_proc_id_eq.
eauto.
rewrite ZMap.set2; trivial.
-
inv Match.
refine_split´.
+ apply plus_one.
eapply ieexec_step_prim_call; eauto.
× case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
× rewrite Hcurid; simpl; auto.
rewrite ZMap.gss; trivial.
× case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto.
+ econstructor; eauto.
rewrite ZMap.set2; trivial.
subdestruct; try (inv NON_YIELD; simpl; auto; fail).
inv NON_YIELD.
rewrite <- Hcurid.
apply uRData_proc_id_eq.
eauto.
rewrite ZMap.set2; trivial.
-
inv Match.
refine_split´.
+ eapply plus_left.
{
eapply ieexec_step_external_yield; eauto.
- case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto.
- rewrite ZMap.gss; trivial.
- rewrite ZMap.gss; reflexivity.
- unfold state_checks.
rewrite ZMap.gss; eauto.
}
eapply star_trans.
{
eapply star_step_get_env_log; eauto.
}
{
eapply star_one.
eapply ieexec_step_external_yield_back; eauto.
{ case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto. }
{ rewrite ZMap.gss. eauto. }
{ rewrite ZMap.gss; reflexivity. }
{ eapply get_env_log_same; eauto. }
{ case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto. }
}
{ trivial. }
{ trivial. }
+ econstructor; eauto.
× rewrite ZMap.set2; trivial.
× apply get_env_log_same in H16.
rewrite <- Hcurid.
rewrite <- H16.
apply uRData_proc_id_eq; eauto.
-
inv Match.
refine_split´.
+ eapply plus_left.
{
eapply ieexec_step_external_sleep; eauto.
- case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto.
- rewrite ZMap.gss; trivial.
- rewrite ZMap.gss; reflexivity.
- unfold state_checks.
rewrite ZMap.gss; eauto.
}
eapply star_trans.
{
eapply star_step_get_env_log; eauto.
}
{
eapply star_one.
eapply ieexec_step_external_yield_back; eauto.
{ case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto. }
{ rewrite ZMap.gss. eauto. }
{ rewrite ZMap.gss; reflexivity. }
{ eapply get_env_log_same; eauto. }
{ case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; auto.
elim n; auto. }
}
{ trivial. }
{ trivial. }
+ econstructor; eauto.
× rewrite ZMap.set2; trivial.
× apply get_env_log_same in H16.
rewrite <- Hcurid.
rewrite <- H16.
apply uRData_proc_id_eq; eauto.
Qed.
Before we can start the lockstep simulation between the TAsm and
EAsm machines, the EAsm machine has to "catch up" to the initial
state of the TAsm machine and replay the init_log with
environment steps.
Lemma initial_Asm_T2E ge rs rsm rsm0 m m´ mp mp´ dp d:
initial_thread_state ge current_thread init_log = Some rs →
init_mem_lift_nextblock m = m´ →
rsm = ZMap.set current_thread (Running rs) (ZMap.init Environment) →
rsm0 = ZMap.set current_thread (init_regset ge current_thread) (ZMap.init Environment) →
mp = (m, m) →
mp´ = (m´, m) →
dp = ZMap.set current_thread (Some d) (ZMap.init None) →
(star IIEAsm.iestep ge)
(IEState (proc_id (uRData nil)) rsm0 mp dp nil)
E0
(IEState current_thread rsm mp´ dp init_log) ∧
match_tstate_iestate rsm mp´ dp rs m´ d init_log current_thread.
Proof.
intros Hrs Hm´ Hrsm Hrsm0 Hmp Hmp´ Hdp.
split; try (constructor; eauto).
destruct init_log_structure as [Hil | (l & e & Hil & Hnm & He & Hnb & Hnc)].
-
rewrite Hil in ×.
unfold initial_thread_state in Hrs.
simpl in Hrs.
unfold init_regset in Hrsm0.
destruct (decide _) as [Hcid | ]; [ | discriminate].
rewrite null_log_proc_id.
rewrite Hcid.
inversion Hrs; subst.
unfold init_mem_lift_nextblock.
rewrite Hil.
apply star_refl.
-
rewrite Hil in Hrs |- ×.
rewrite null_log_proc_id in Hnm.
rewrite init_log_proc_id in Hnc.
assert (Hl_proc_id: proc_id (uRData l) = current_thread).
{
rewrite <- init_log_proc_id.
rewrite Hil.
symmetry.
apply uRData_proc_id_eq.
reflexivity.
}
unfold initial_thread_state in Hrs; simpl in Hrs.
unfold thread_init_pc_of in Hrs; simpl in Hrs.
destruct (initial_thread_pc ge current_thread l) as [pc|] eqn:Hpcl;
[|discriminate].
unfold initial_regset_state in Hrs.
inversion Hrs; clear Hrs; subst rs.
unfold init_regset in Hrsm0.
destruct (decide _) as [ | Hmc]; [congruence | ].
assert (HE0: E0 = E0 ** E0) by reflexivity.
eapply star_trans; eauto.
{
instantiate (1 := IEState current_thread rsm0 mp dp l).
rewrite <- Hl_proc_id.
assert
(Hl: ∀ l1 e l2,
l = l1 ++ e :: l2 →
proc_id (uRData l2) ≠ current_thread ∧
Single_Oracle l2 = e).
{
intros.
split; eauto.
eapply oracle_init_log; eauto.
subst l.
rewrite app_comm_cons in Hil.
eassumption.
}
revert Hl.
subst mp.
subst mp´.
subst rsm0.
subst dp.
clear.
induction l.
- intros.
eapply star_refl.
- intros.
eapply star_trans.
+ eapply IHl; eauto.
intros l1 e l2 Hle.
eapply Hl; eauto.
rewrite Hle.
eapply app_comm_cons.
+ eapply star_one; eauto.
specialize (Hl nil a l eq_refl).
destruct Hl as [Hproc_id Horacle].
eapply ieexec_step_external_empty; eauto.
× rewrite ZMap.gso; eauto.
apply ZMap.gi.
× rewrite ZMap.gso; eauto.
apply ZMap.gi.
× congruence.
+ reflexivity.
}
eapply star_one.
{
unfold init_mem_lift_nextblock in Hm´.
rewrite Hil in Hm´.
subst rsm rsm0.
erewrite <- (ZMap.set2 _ _ (Running (_ # _ <- _))).
rewrite Hmp´.
eapply ieexec_step_external_yield_back; eauto.
case_eq (decide (current_thread = current_thread)); intros; subst; auto.
- left.
split.
+ apply ZMap.gss.
+ unfold initial_thread_kctxt.
rewrite Hpcl.
reflexivity.
- rewrite Hdp.
rewrite ZMap.gss; reflexivity.
- congruence.
- apply FunctionalExtensionality.functional_extensionality.
intros [ | [] | [] | | [] | ]; reflexivity.
- destruct e as [? [ ]]; simpl in Hnb |- *; try congruence;
destruct l; simpl in He |- *; try congruence;
inversion He; reflexivity.
- case_eq (decide (current_thread = current_thread)); intros; subst; auto.
elim n; auto.
}
- apply init_log_proc_id.
- inv Hmp´; simpl; auto.
Qed.
End Refinement.
Section Link.
Require Import AuxFunctions.
Require Import liblayers.compat.CompatLayers.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import CompatExternalCalls.
Require Import MakeProgram.
Require Import LAsmModuleSem.
Require Import I64Layer.
Require Import Soundness.
Require Import LinkTactic.
Require Import LAsmModuleSemAux.
Require Import LAsm.
Require Import MakeProgramImpl.
Require Import LAsmAbsDataProperty.
Context `{s_config_link : SingleLinkConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Context `{LH: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined (LH ⊕ L64)}.
Context `{lasmops: !LAsmAbsDataProp}.
Context `{extcallsx: !ExternalCallsXDefined (LH ⊕ L64)}.
Context `{primcall_props: !PrimcallProperties IIEAsm.sprimitive_call}.
Inductive match_testate (ge: genv): tstate (mem:=mem) → iestate (mem:=mem) → Prop :=
| match_testate_init rs m m´ mp d rsm dp:
initial_thread_state ge current_thread init_log = Some rs →
init_mem_lift_nextblock m = m´ →
mp = (m, m) →
rsm = ZMap.set current_thread (init_regset ge current_thread) (ZMap.init Environment) →
dp = ZMap.set current_thread (Some d) (ZMap.init None) →
match_testate ge
(TState current_thread rs m´ d init_log)
(IEState main_thread rsm mp dp nil)
| match_testate_running curid rs mp m d l rsm dp:
match_tstate_iestate rsm mp dp rs m d l curid →
match_testate ge
(TState curid rs m d l)
(IEState curid rsm mp dp l).
Theorem cl_backward_simulation:
∀ (s: StencilImpl.stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
(Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (LH ⊕ L64) = OK ph),
backward_simulation
(TAsm.tsemantics ph)
(IIEAsm.iesemantics (current_thread::nil) ph).
Proof.
intros. apply forward_to_backward_simulation; eauto.
- eapply forward_simulation_plus with
(match_states:= match_testate (Genv.globalenv ph));
simpl; intros; trivial.
+
destruct H.
eexists.
split.
× constructor; eauto.
× simpl.
eapply match_testate_init; eauto.
+ destruct s1´ as [curid´ rs´ m´ d´ l´].
destruct H0.
× rewrite <- null_log_proc_id.
edestruct initial_Asm_T2E as [Hinit_step Hinit_match]; eauto.
edestruct one_step_Asm_T2E as (rsm´ & mp´ & dp´ & Hstep & Hmatch); eauto.
eexists.
split; [ | constructor; eauto].
eapply star_plus_trans; eauto.
× edestruct one_step_Asm_T2E as (rsm´ & mp´ & dp´ & Hstep & Hmatch); eauto.
eexists.
split; [ | constructor; eauto].
eauto.
- apply tasm_semantics_receptive.
- apply ieasm_semantics_determinate; eauto.
Qed.
End Link.