Library mcertikos.conlib.conmtlib.EAsmCompose
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 SingleConfiguration.
Require Import LAsm.
Require Import EAsmCommon.
Require Import EAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Require Import EAsmPropLib.
Section Refinement.
Context `{single_link_config: 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 : ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance : LayerConfigurationOps := compatlayer_configuration_ops L.
Opaque Z.to_nat.
Ltac list_append_neq_tac:=
match goal with
| H: ?l = _ ++ ?e :: ?l |- _ ⇒
eapply ListLemma2.list_append_neq in H; inversion H
| H: ?l = ?e :: ?l |- _ ⇒
eapply ListLemma2.list_append_neq0 in H; inversion H
| H: ?e :: ?l = ?l |- _ ⇒
symmetry in H; eapply ListLemma2.list_append_neq0 in H; inversion H
| H: ?l = ?e :: _ ++ ?l |- _ ⇒
eapply list_head_neq in H; inversion H
| _ ⇒ idtac
end.
Inductive match_estate_state: (ZMap.t ThreadState) → mem → (ZMap.t (option dproc)) →
(ZMap.t ThreadState) → mem → (ZMap.t (option dproc)) →
ThreadState → mem → dproc → Z → Log → Z → Prop :=
| MATCH_ESTATE_STATE:
∀ ts rsm rsm´ (d: dproc) (dp dp´ : ZMap.t (option dproc)) m m´ m0 tid curid l
(NotEnv: ts ≠ Environment)
(MapEq: (∀ i,
ts_lessdef (ZMap.get i (ZMap.set tid ts rsm´))
(ZMap.get i rsm)))
(DMapEq: (∀ i,
ZMap.get i (ZMap.set tid (Some d) dp´) = ZMap.get i dp))
(NoneReg: ZMap.get tid rsm´ = Environment)
(Nextblock0: active_condition tid l→ (Mem.nextblock m0 ≤ Mem.nextblock m´) % positive)
(Nextblock1: inactive_condition l rsm´ → (Mem.nextblock m´ ≤ Mem.nextblock m0) % positive)
(Hyield: yield_condition tid l → Mem.nextblock m´ = last_nb l)
(Hinyield: inyield_condition l rsm´ → Mem.nextblock m0 = last_nb l)
(Hnbbig: let lnb := last_nb l in
∀ (Hnac: ¬ active_condition tid l)
(Hninac: ¬ inactive_condition l rsm´),
(Mem.nextblock m´ ≤ lnb ∧ Mem.nextblock m0 ≤ lnb)%positive),
mem_disjoint_union m´ m0 m →
match_estate_state rsm m dp rsm´ m´ dp´ ts m0 d tid l curid.
Theorem one_step_EAsm_compose:
∀ ge m m´ m0 m0´ gm curid curid´ rsm rsm´ rsm0 rsm0´ grsm ts ts´ tid l l´ gdp dp dp´ d d´ dp0 dp0´ t
(EStep: EAsm.estep ge (EState curid rsm0 m dp0 l) t (EState curid´ rsm0´ m´ dp0´ l´))
(RSM: rsm0 = ZMap.set tid ts (ZMap.init Environment))
(RSM0: rsm0´= ZMap.set tid ts´ (ZMap.init Environment))
(DP: dp0 = ZMap.set tid (Some d) (ZMap.init None))
(DP0: dp0´= ZMap.set tid (Some d´) (ZMap.init None))
(SEStep: star EAsm.estep ge (EState curid rsm m0 dp l) t (EState curid´ rsm´ m0´ dp´ l´))
(Match: match_estate_state grsm gm gdp rsm m dp ts m0 d tid l curid),
∃ gm´ grsm´ gdp´,
plus EAsm.estep ge (EState curid grsm gm gdp l) t
(EState curid´ grsm´ gm´ gdp´ l´)
∧ match_estate_state grsm´ gm´ gdp´ rsm´ m´ dp´ ts´ m0´ d´ tid l´ curid´.
Proof.
intros. inv EStep.
-
inv Match.
eapply regmap_None_Some in H8. destruct H8 as [? ?]; subst.
exploit skip_step_same_log; eauto.
intros (_ & ? & ? & ?); subst.
exploit regset_lessdef_exists_eq; eauto.
intros (rs0´ & Hrs0´ & Hless).
assert (Hactive: active_condition (proc_id (uRData l´)) l´).
{
eapply active_condition_same_neq; eauto.
}
exploit exec_instr_disjoint_union; eauto.
intros (gm´ & rs0´0 & Hexe & Hunion & Hnb & Hlessdef_option).
refine_split´.
+ apply plus_one.
eapply eexec_step_internal; eauto.
eapply regset_lessdef_eq; eauto. congruence.
erewrite <- DMapEq. rewrite ZMap.gss in *; auto.
+ econstructor; eauto.
{
apply ZMap_gss_eq in H5.
congruence.
}
{
rewrite <- (ZMap.set2 (proc_id (uRData l´)) (Running rs)).
eapply ts_lessdef_gss; eauto.
rewrite ZMap.set2 in H5.
eapply set_init_eq in H5. inv H5.
constructor; assumption.
}
{
eapply ZMap_gss_eq in H9. inv H9.
rewrite <- (ZMap.set2 (proc_id (uRData l´)) (Some d)).
eapply ZMap_gss_forall. eauto.
}
{
intros HF. eapply inactive_condition_diff_neq in HF; eauto. inv HF.
}
{
intro HY.
eapply yield_condition_false2 in HY; eauto. inv HY.
}
{
intros. elim Hnac; trivial.
}
-
inv Match.
eapply regmap_None_Some in H9. destruct H9 as [? ?]; subst.
exploit skip_step_same_log; eauto.
intros (_ & ? & ? & ?); subst.
exploit regset_lessdef_exists_eq; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
assert (Hactive: active_condition (proc_id (uRData l´)) l´).
{
eapply active_condition_same_neq; eauto.
}
exploit (exec_external_disjoint_union_regset (L:= L)); eauto.
intros (gm´ & vl´ & Hexe & Hunion & Hnb & Hless).
refine_split´.
+ apply plus_one.
eapply eexec_step_builtin; eauto.
eapply regset_lessdef_eq; eauto. congruence.
erewrite <- DMapEq. rewrite ZMap.gss in *; auto.
+ econstructor; eauto.
{
apply ZMap_gss_eq in H5.
congruence.
}
{
rewrite <- (ZMap.set2 (proc_id (uRData l´)) (Running rs)).
eapply ts_lessdef_gss; eauto.
rewrite ZMap.set2 in H5.
eapply set_init_eq in H5. inv H5.
constructor.
regset_lessdef_solve_tac.
}
{
eapply ZMap_gss_eq in H7. inv H7.
rewrite <- (ZMap.set2 (proc_id (uRData l´)) (Some d)).
eapply ZMap_gss_forall. eauto.
}
{
intros HF. eapply inactive_condition_diff_neq in HF; eauto. inv HF.
}
{
intro HY.
eapply yield_condition_false2 in HY; eauto. inv HY.
}
{
intros. elim Hnac; trivial.
}
-
inv Match.
eapply regmap_None_Some in H9. destruct H9 as [? ?]; subst.
exploit skip_step_same_log; eauto.
intros (_ & ? & ? & ?); subst.
exploit regset_lessdef_exists_eq; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
exploit annot_arguments_disjoint_union; eauto.
intros (vargs´ & Hargs & Hless).
assert (Hactive: active_condition (proc_id (uRData l´)) l´).
{
eapply active_condition_same_neq; eauto.
}
exploit (exec_external_disjoint_union (L:=L)); eauto.
intros (gm´ & vl´ & Hexe & Hunion & Hnb & Hless´).
refine_split´.
+ apply plus_one.
eapply eexec_step_annot; eauto.
{ eapply regset_lessdef_eq; eauto. congruence. }
{
erewrite <- DMapEq. rewrite ZMap.gss in *; auto.
}
+ econstructor; eauto.
{
apply ZMap_gss_eq in H5.
congruence.
}
{
rewrite <- (ZMap.set2 (proc_id (uRData l´)) (Running rs)).
eapply ts_lessdef_gss; eauto.
rewrite ZMap.set2 in H5.
eapply set_init_eq in H5. inv H5.
constructor.
regset_lessdef_solve_tac.
}
{
eapply ZMap_gss_eq in H7. inv H7.
rewrite <- (ZMap.set2 (proc_id (uRData l´)) (Some d)).
eapply ZMap_gss_forall. eauto.
}
{
intros HF. eapply inactive_condition_diff_neq in HF; eauto. inv HF.
}
{
intro HY.
eapply yield_condition_false2 in HY; eauto. inv HY.
}
{
intros. elim Hnac; trivial.
}
-
inv Match.
eapply regmap_None_Some in H9. destruct H9 as [? ?]; subst.
exploit regset_lessdef_exists_eq; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
exploit extcall_arguments_disjoint_union; eauto.
intros (args´ & Hargs & Hless).
assert (Hactive: active_condition (proc_id (uRData l)) l).
{
eapply active_condition_same_neq; eauto.
}
exploit exec_external_disjoint_union´; eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & vl´ & Hexe & Hunion & Hnb & Hless´).
assert (HT: rsm´ = rsm ∧ m0´ = m0
∧ dp´ = dp).
{
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2].
- subst. eapply skip_step_same_log; eauto.
- destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id).
{
destruct Hl as (largs & choice & Hlargs & Hch & Hl).
inversion SEStep.
{
rewrite H8 in Hl.
list_append_neq_tac.
}
{
subst.
inv H0; try decompose [and or] H9; try congruence.
exploit star_step_log_incr; eauto.
intros Ha. eapply list_append_e_impl in Ha; eauto.
rewrite Ha in ×.
erewrite uRData_proc_id_eq in H1; [| reflexivity].
subst. eapply skip_step_same_log; eauto.
}
}
{
subst. eapply skip_step_same_log; eauto.
}
}
destruct HT as (? & ? & ?); subst.
refine_split´.
+ apply plus_one.
eapply eexec_step_external; eauto.
{ eapply regset_lessdef_eq; eauto. congruence. }
{ destruct ef; eauto.
case_eq (peq name thread_yield); intros; [subst; rewrite peq_true in NON_YIELD; contradiction |].
case_eq (peq name thread_sleep); intros; [subst; rewrite peq_true in NON_YIELD; contradiction |].
case_eq (has_event name); intros Hhas_event; rewrite peq_false in NON_YIELD; auto;
rewrite peq_false in NON_YIELD; auto; rewrite Hhas_event in NON_YIELD; auto.
destruct NON_YIELD as (largs & choice & Hlargs & Hch & Hl);
∃ largs; ∃ choice; eauto; split.
eapply val2Lval_list_lessdef; eauto.
split; auto. }
{
intros. exploit STACK; eauto.
eapply regset_lessdef_eq´; eauto.
intros (Hst1 & Hst2).
split; trivial.
erewrite mem_disjoint_union_nextblock_eq; eauto.
}
{ eapply regset_lessdef_neq; eauto. }
{ eapply regset_lessdef_neq; eauto. }
{
erewrite <- DMapEq. rewrite ZMap.gss in *; auto.
}
+ econstructor; eauto.
{
apply ZMap_gss_eq in H5.
congruence.
}
{
rewrite <- (ZMap.set2 (proc_id (uRData l)) (Running rs)).
eapply ts_lessdef_gss; eauto.
rewrite ZMap.set2 in H5.
eapply set_init_eq in H5. inv H5.
constructor.
regset_lessdef_solve_tac.
}
{
eapply ZMap_gss_eq in H7. inv H7.
rewrite <- (ZMap.set2 (proc_id (uRData l)) (Some d)).
eapply ZMap_gss_forall. eauto.
}
{
intros HF. eapply inactive_condition_diff_neq in HF; eauto. inv HF.
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; subst; auto.
destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); subst; eauto.
destruct Hl as (largs & choice & Hlargs & Hch & Hl); subst.
rewrite lastEvType_tail.
erewrite uRData_proc_id_eq; eauto.
split; eauto. simpl; congruence.
}
{
intros.
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; subst; auto.
- eapply yield_condition_false2 in H0; eauto. inv H0.
- destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); subst; eauto.
+ eapply yield_condition_false2 in H0; eauto. inv H0.
destruct Hl as (largs & choice & Hlargs & Hch & Hl); subst.
unfold lastEvType; simpl. congruence.
+ eapply yield_condition_false2 in H0; eauto. inv H0.
}
{
intros.
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; subst; auto.
destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); subst; eauto.
eapply inyield_condition_false2 in H0; eauto. inv H0.
destruct Hl as (largs & choice & Hlargs & Hch & Hl); subst.
unfold lastEvType; simpl.
congruence.
}
{
intros. elim Hnac.
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; subst; auto.
destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); subst; eauto.
destruct Hl as (largs & choice & Hlargs & Hch & Hl); subst.
eapply active_condition_same_neq; eauto.
- erewrite uRData_proc_id_eq; trivial.
- unfold lastEvType. simpl. congruence.
}
-
inv Match.
eapply regmap_None_Some in H7. destruct H7 as [? ?]; subst.
exploit regset_lessdef_exists_eq; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
assert (Hactive: active_condition (proc_id (uRData l)) l).
{
eapply active_condition_same_neq; eauto.
}
exploit exec_primitive_disjoint_union; eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & rs0´0 & Hexe & Hunion & Hnb & Hregset_less).
assert (HT: rsm´ = rsm ∧ m0´ = m0 ∧ dp´ = dp).
{
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2].
- subst. eapply skip_step_same_log; eauto.
- destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id).
{
inversion SEStep.
{ rewrite H7 in Hl. list_append_neq_tac. }
subst.
inv H0; try decompose [and or] H8; try congruence.
exploit star_step_log_incr; eauto.
intros Ha. eapply list_append_e_impl in Ha; eauto.
rewrite Ha in ×.
erewrite uRData_proc_id_eq in H1; [| reflexivity].
eapply skip_step_same_log; eauto.
}
{
subst. eapply skip_step_same_log; eauto.
}
}
destruct HT as (? & ? & ?); subst.
refine_split´.
+ apply plus_one.
eapply eexec_step_prim_call; eauto.
eapply regset_lessdef_eq; eauto. congruence.
{
erewrite <- DMapEq. rewrite ZMap.gss in *; auto.
}
+ econstructor; eauto.
{
apply ZMap_gss_eq in H5.
congruence.
}
{
rewrite <- (ZMap.set2 (proc_id (uRData l)) (Running rs)).
eapply ts_lessdef_gss; eauto.
rewrite ZMap.set2 in H5.
eapply set_init_eq in H5. inv H5.
constructor. assumption.
}
{
eapply ZMap_gss_eq in H9. inv H9.
rewrite <- (ZMap.set2 (proc_id (uRData l)) (Some d)).
eapply ZMap_gss_forall. eauto.
}
{
intros HF. eapply inactive_condition_diff_neq in HF; eauto. inv HF.
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; subst; auto.
destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); subst; eauto.
rewrite lastEvType_tail.
erewrite uRData_proc_id_eq; eauto.
split; eauto. simpl; congruence.
}
{
intros.
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; subst; auto.
- eapply yield_condition_false2 in H0; eauto. inv H0.
- destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); subst; eauto.
+ eapply yield_condition_false2 in H0; eauto. inv H0.
unfold lastEvType; simpl. congruence.
+ eapply yield_condition_false2 in H0; eauto. inv H0.
}
{
intros.
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; subst; auto.
destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); subst; eauto.
eapply inyield_condition_false2 in H0; eauto. inv H0.
unfold lastEvType; simpl. congruence.
}
{
intros. elim Hnac.
exploit ef_id_imply_or; try eapply NON_YIELD.
intros HT.
destruct HT as [HT2 | HT2]; subst; auto.
destruct HT2 as (id & sg & Hef & Hl); subst.
destruct (has_event id); subst; eauto.
eapply active_condition_same_neq; eauto.
- erewrite uRData_proc_id_eq; trivial.
- unfold lastEvType. simpl. congruence.
}
-
inv Match.
eapply regmap_None_Some in H9. destruct H9 as [? ?]; subst.
exploit regset_lessdef_exists_eq´´; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
assert (Hactive: active_condition (proc_id (uRData l)) l).
{
eapply active_condition_same_neq; eauto.
}
assert (Hmem0: (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive) by eauto.
inversion SEStep; clear SEStep.
{ list_append_neq_tac. }
subst.
inv H0; try decompose [and or] H10; try congruence.
assert (Heq: Single_Oracle l = LEvent (proc_id (uRData l)) (LogYield (Mem.nextblock m´))).
{
exploit star_step_log_incr; eauto.
intros Ha. eapply list_append_e_impl in Ha; eauto.
}
rewrite Heq in ×.
eapply set_init_eq in H5. inv H5.
inv H1.
+
refine_split´.
× apply plus_one.
erewrite <- (mem_disjoint_union_nextblock_eq m´ gm) in Heq |- *; eauto.
eapply eexec_step_external_yield; eauto.
{ generalize (DMapEq (proc_id (uRData l))); intros.
rewrite ZMap.gss in H0; eauto. }
{ eapply regset_lessdef_eq; eauto. congruence. }
{ unfold state_checks in ×.
rewrite <- DMapEq; rewrite ZMap.gss; eauto.
rewrite ZMap.gss in H18.
eapply set_init_eq in H7; inv H7.
assumption. }
× econstructor; eauto.
{
eapply ZMap_gss_eq in H7. inv H7. auto.
}
{
intros HF.
eapply inactive_condition_false in HF; eauto. inv HF.
}
{
intros HF.
eapply inyield_condition_false in HF; eauto. inv HF.
}
{
intros. elim Hnac.
eapply active_condition_true; eauto.
}
+
inv H0;
match goal with
| HG: _ ≠ Some LogYieldTy |- _ ⇒
rewrite lastEvType_tail in HG; simpl in HG; congruence
| _ ⇒ idtac
end.
×
eapply star_log_incr_nil´ in H3.
inv H3.
×
eapply star_log_incr_nil´ in H3.
inv H3.
-
inv Match.
eapply regmap_None_Some in H9. destruct H9 as [? ?]; subst.
exploit regset_lessdef_exists_eq´´; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
assert (Hactive: active_condition (proc_id (uRData l)) l).
{
eapply active_condition_same_neq; eauto.
}
assert (Hmem0: (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive) by eauto.
inversion SEStep; clear SEStep.
{ list_append_neq_tac. }
subst.
inv H0; try decompose [and or] H10; try congruence.
eapply set_init_eq in H5. inv H5.
eapply set_init_eq in H7. inv H7.
exploit extcall_arguments_disjoint_union; eauto.
intros (args´ & Hargs´ & Hless).
assert (Heq: Single_Oracle l = LEvent (proc_id (uRData l)) (LogSleep (Int.unsigned i) (Mem.nextblock m´) (sync_chpool_check thread_sleep (Lint i :: nil) (uRData l) d0))).
{
exploit star_step_log_incr; eauto.
intros Ha. eapply list_append_e_impl in Ha; eauto.
}
rewrite Heq in ×.
inv H1.
+
refine_split´.
× apply plus_one.
erewrite <- (mem_disjoint_union_nextblock_eq m´ gm) in Heq |- *; eauto.
eapply eexec_step_external_sleep; eauto.
{ generalize (DMapEq (proc_id (uRData l))); intros.
rewrite ZMap.gss in H0.
rewrite <- H0.
rewrite ZMap.gss in H11; inv H11; auto. }
{ eapply regset_lessdef_eq; eauto. congruence. }
{ inv Hless. inv H3. inv H5. trivial.
unfold state_checks in ×.
rewrite <- DMapEq.
rewrite ZMap.gss.
rewrite ZMap.gss in H18.
auto. }
{ inv Hless. inv H3. inv H5. trivial. }
× econstructor; eauto.
{
intros HF.
eapply inactive_condition_false in HF; eauto. inv HF.
}
{
intros HF.
eapply inyield_condition_false in HF; eauto. inv HF.
}
{
intros. elim Hnac.
eapply active_condition_true; eauto.
}
+
inv H0;
match goal with
| HG: _ ≠ Some LogYieldTy |- _ ⇒
rewrite lastEvType_tail in HG; simpl in HG; congruence
| _ ⇒ idtac
end.
×
eapply star_log_incr_nil´ in H3.
inv H3.
×
eapply star_log_incr_nil´ in H3.
inv H3.
-
inv Match.
eapply set_init_eq in H7. inv H7.
eapply set_init_eq in H9. inv H9.
eapply regmap_None_None in H6.
destruct (regsetmap_dec (proc_id (uRData l)) rsm) as [HT | HT].
+ inversion SEStep.
{ list_append_neq_tac. }
subst.
inv H0; try decompose [and or] H9; try congruence.
assert (Heq: rsm´ = rsm ∧ m0´ = m0 ∧ dp´ = dp).
{
destruct (regsetmap_dec (proc_id (uRData (Single_Oracle l :: l))) rsm) as [HT´ | [HT´ | HT´]].
- exploit skip_step_same_log; eauto.
intros (_ & ? & ? & ?); subst. eauto.
- exploit skip_step_same_log; eauto.
intros (_ & ? & ? & ?); subst. eauto.
- destruct HT´ as (rs & HT´).
assert (Hlast: lastEvType (Single_Oracle l :: l) = Some LogYieldTy).
{
rewrite lastEvType_tail; simpl.
destruct (getLogEventType (Single_Oracle l)) eqn: Htype; trivial.
rewrite uRData_proc_id_eq in HT´; eauto. congruence.
}
inv H1; eauto.
inv H0; try congruence.
eapply star_step_log_incr in H3.
destruct H3 as (l0 & HF).
eapply ListLemma2.list_append_neq in HF.
inv HF.
}
destruct Heq as (? & ? & ?); subst.
refine_split´.
× eapply plus_left.
eapply eexec_step_external_empty; eauto.
specialize (MapEq (proc_id (uRData l))).
rewrite ZMap.gso in MapEq; auto.
rewrite HT in MapEq. inv MapEq. trivial.
rewrite <- DMapEq.
rewrite ZMap.gso; auto.
econstructor; eauto. trivial.
× econstructor; eauto.
{
intro HF. eapply active_condition_false in HF; trivial. inv HF.
}
{
intro HF. eapply inactive_condition_false in HF; trivial. inv HF.
}
{
intro HF. eapply yield_condition_false in HF; trivial. inv HF.
}
{
intro HF. eapply inyield_condition_false in HF; trivial. inv HF.
}
{
intros.
assert (Hac: (¬ active_condition tid l ∧ ¬ inactive_condition l rsm)
∨ yield_condition tid l ∨ inyield_condition l rsm).
{
destruct (getLogEventType (Single_Oracle l)) eqn:Htype.
- left. eapply oracle_event_yield in Htype; eauto.
split. eapply active_condition_false2; eauto.
eapply inactive_condition_diff_neq; eauto.
- eapply active_condition_imply_neg in Hnac; eauto.
eapply inactive_condition_imply_neg in Hninac; eauto.
destruct Hnac; destruct Hninac.
+ left; auto.
+ right. right. trivial.
+ right. left. trivial.
+ right. left. trivial.
}
pose proof (Oracle_le_nb l) as Hole.
eapply le_and_trans; eauto.
destruct Hac as [HF |[HF|HF]].
- destruct HF as (? & ?); eauto.
- rewrite <- Hyield; eauto.
split. reflexivity.
eapply Nextblock0. right; trivial.
- rewrite <- Hinyield; eauto.
split. eapply Nextblock1. right; trivial.
reflexivity.
}
+ assert (Hdec: lastEvType l = Some LogYieldTy ∨ lastEvType l ≠ Some LogYieldTy).
{
destruct (lastEvType l). destruct l0.
- left; trivial.
- right. congruence.
- right. congruence.
}
destruct Hdec as [Hlast | Hlast].
{
inversion SEStep.
{ list_append_neq_tac. }
subst.
inv H0;
try (try decompose [and or] H10; congruence);
try (decompose [or ex] HT; congruence).
exploit star_step_log_incr; eauto.
intros (l0 & Heq).
eapply list_append_e_or´ in Heq.
destruct Heq as (Heq & ?); subst.
rewrite Heq in ×.
rewrite uRData_proc_id_eq in H1; trivial.
exploit regset_lessdef_exists_neq´´; eauto.
intros (grs0 & Hgrsm & Hless).
assert (Hless_opt:
∀ i,
ts_lessdef
(ZMap.get i
(ZMap.set tid ts´
(ZMap.set (proc_id (uRData l))
(Running
(((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs0))
# EAX <- Vundef) # PC <- (rs0 RA)) # RA <- Vundef) rsm)))
(ZMap.get i (ZMap.set (proc_id (uRData l))
(Running
(((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) grs0))
# EAX <- Vundef) # PC <- (grs0 RA)) # RA <- Vundef) grsm))).
{
eapply regset_map_neq´´; eauto.
constructor.
regset_lessdef_solve_tac.
}
assert (Hac: (¬ active_condition tid l ∧ ¬ inactive_condition l rsm)
∨ yield_condition tid l ∨ inyield_condition l rsm).
{
destruct l; inv H15.
destruct (zeq (proc_id (uRData l0)) tid); subst.
- right. left. unfold yield_condition.
refine_split´; trivial.
unfold lastEvType in Hlast; simpl in Hlast. congruence.
- destruct (ZMap.get (proc_id (uRData l0)) rsm) eqn: Heq´.
+ left. split. eapply active_condition_false; auto.
eapply inactive_condition_false; auto.
+ right. right. unfold inyield_condition.
refine_split´; trivial.
rewrite Heq´. congruence.
unfold lastEvType in Hlast; simpl in Hlast. congruence.
+ right. right. unfold inyield_condition.
refine_split´; trivial.
rewrite Heq´. congruence.
unfold lastEvType in Hlast; simpl in Hlast. congruence.
}
assert (Hnbeq: nb = last_nb l).
{
destruct l; inv H15. simpl.
rewrite Hnextblock. trivial.
}
eapply (star_step_disjoint_union ge _ _ m´ (mem_lift_nextblock gm (Pos.to_nat (nb) - Pos.to_nat(Mem.nextblock gm)))) in H1; eauto.
{
destruct H1 as (gm´ & rsm0´ & dp0´ & Hstar & Hdis & Hreg & Hdp & Hnb & Hrsm´).
refine_split´; eauto.
× eapply plus_left.
{
eapply eexec_step_external_yield_back; eauto.
rewrite <- DMapEq.
rewrite ZMap.gso; eassumption.
}
{
rewrite uRData_proc_id_eq; trivial.
eapply Hstar.
}
{ trivial. }
× rewrite uRData_proc_id_eq; trivial.
econstructor; eauto.
{
intro HF. eapply active_condition_false in HF; trivial. inv HF.
}
{
intro HF. eapply yield_condition_false in HF; trivial. inv HF.
}
{
intro HF. eapply inyield_condition_false2 in HF; trivial. inv HF.
unfold lastEvType. simpl. congruence.
}
{
intros. elim Hninac.
left. erewrite uRData_proc_id_eq; trivial.
eapply star_step_rsm in SEStep.
destruct SEStep as (_ & SEStep & _). exploit SEStep; eauto.
unfold lastEvType; simpl.
intros [Hav | (rs1 & ->)];
split; congruence.
}
}
{
subst.
destruct Hac as [HF | [HF|HF]].
- exploit Hnbbig; try eapply HF.
intros (Hle1 & Hle2).
destruct (plt (Mem.nextblock m0) (Mem.nextblock m´)).
{
assert (Hle: (Mem.nextblock m0 ≤ Mem.nextblock m´)%positive) by xomega.
erewrite (mem_disjoint_union_nextblock_eq m´ gm m0); eauto.
eapply mem_disjoint_union_lift_nextblock_right´; eauto.
xomega.
}
{
assert (Hle: (Mem.nextblock m´ ≤ Mem.nextblock m0)%positive) by xomega.
erewrite (mem_disjoint_union_nextblock_eq m0 gm m´); eauto.
eapply mem_disjoint_union_lift_nextblock_right; eauto.
eapply mem_disjoint_union_commutativity; eauto.
}
- rewrite <- Hyield; auto.
assert (Ha: active_condition tid l) by (right; trivial).
specialize (Nextblock0 Ha).
eapply mem_disjoint_union_lift_nextblock_right´; eauto.
erewrite (mem_disjoint_union_nextblock_eq m´ gm m0); eauto.
omega.
- rewrite <- Hinyield; auto.
assert (Ha: inactive_condition l rsm) by (right; trivial).
specialize (Nextblock1 Ha).
erewrite (mem_disjoint_union_nextblock_eq m0 gm m´); eauto.
eapply mem_disjoint_union_lift_nextblock_right; eauto.
eapply mem_disjoint_union_commutativity; eauto.
}
{
subst.
destruct Hac as [HF | [HF|HF]].
- exploit Hnbbig; try eapply HF.
intros (Hle1 & Hle2).
rewrite lift_nextblock_le; eauto.
- rewrite <- Hyield; auto.
assert (Ha: active_condition tid l) by (right; trivial).
specialize (Nextblock0 Ha).
rewrite lift_nextblock_le; eauto.
reflexivity.
- rewrite <- Hinyield; auto.
assert (Ha: inactive_condition l rsm) by (right; trivial).
specialize (Nextblock1 Ha).
rewrite lift_nextblock_le; eauto.
reflexivity.
}
{ rewrite ZMap.gso; auto. }
}
{
eapply star_log_append_split in SEStep.
destruct SEStep as (rsm0 & m1 & dp0 & rsm1 & m2 & dp1 & Hstar & Hone & Hstar2).
pose proof Hstar as Hstar´.
pose proof Hone as Hone´.
pose proof Hstar2 as Hstar2´.
exploit (star_step_rsm ge rsm); eauto. intros (HrsmN & HrsmS & HrsmR).
exploit (one_step_rsm ge rsm0); eauto; intros (HrsmN1 & _).
assert (Hle: (Mem.nextblock m´ ≤ Mem.nextblock m0)%positive).
{
eapply Nextblock1.
left. split; try congruence.
destruct HT as [HT | (rs & HT)]; congruence.
}
eapply star_step_disjoint_union in Hstar; eauto.
destruct Hstar as (gm´ & rsm0´ & dp0´ & Hstar & Hdis & Hreg & Hdp & Hnb & _).
specialize (HrsmN _ NoneReg).
eapply one_step_disjoint_union_log in Hone; eauto.
destruct Hone as (gm´0 & rsm0´0 & dp0´0 & Hone & Hdis1 & Hreg1 & Hdp1 & Hnb1).
eapply star_step_disjoint_union in Hstar2; eauto.
destruct Hstar2 as (gm´1 & rsm0´1 & dp0´1 & Hstar2 & Hdis2 & Hreg2 & Hdp2 & Hnb2 & Hnone).
refine_split´; eauto.
× eapply star_plus_trans; eauto.
eapply plus_left; eauto.
{ reflexivity. }
× econstructor; eauto.
{
intro HF. eapply active_condition_false in HF; trivial. inv HF.
}
{
intro HF. eapply yield_condition_false in HF; trivial. inv HF.
}
{
intro HF.
destruct (getLogEventType (Single_Oracle l)) eqn:Htype.
- assert (ZMap.get (proc_id (uRData l)) rsm0 ≠ Environment).
{
eapply HrsmS in HT.
destruct HT as [HT | (rs & HT)]; try congruence.
}
eapply one_step_last_nb in Hone´; eauto.
rewrite <- Hone´.
eapply star_step_last_yield in Hstar2´; subst; eauto.
unfold lastEvType; simpl; congruence.
- eapply inyield_condition_false2 in HF. inv HF.
unfold lastEvType; simpl. congruence.
}
{
intros.
assert (HT´: ZMap.get (proc_id (uRData l)) rsm´ = Available ∨ ∃ rs, ZMap.get (proc_id (uRData l)) rsm´ = Running rs).
{
apply HrsmS in HT.
eapply one_step_rsm in Hone´. destruct Hone´ as (_ & Hone´).
eapply Hone´ in HT.
eapply star_step_rsm in Hstar2´. destruct Hstar2´ as (_ & Hstar2´).
eapply Hstar2´ in HT. trivial.
}
destruct (getLogEventType (Single_Oracle l)) eqn:Htype.
- elim Hninac. right. unfold inyield_condition.
refine_split´; trivial.
destruct HT´ as [HT´ | (rs & HT´)]; congruence.
- elim Hninac.
left. erewrite uRData_proc_id_eq; trivial.
split.
+ destruct HT´ as [HT´ | (rs & HT´)]; congruence.
+ unfold lastEvType; simpl.
congruence.
}
}
+ assumption.
-
inv Match.
eapply regmap_None_Some´ in H7. destruct H7 as [? Hrs0]; subst.
exploit regset_lessdef_exists_eq´´´; eauto.
intros (rs´1 & Hrs´1 & Hregset_lessdef).
inversion SEStep.
{ list_append_neq_tac. }
subst.
inv H0; try decompose [and or] H10; try congruence.
assert (Heq: Single_Oracle l = LEvent (proc_id (uRData l)) LogYieldBack).
{
exploit star_step_log_incr; eauto.
intros Ha. eapply list_append_e_impl in Ha; eauto.
}
rewrite Heq in ×.
erewrite uRData_proc_id_eq in H1; [| reflexivity].
exploit skip_step_same_log; eauto.
intros (_ & ? & ? & ?); subst.
assert (Hac: (¬ active_condition (proc_id (uRData l)) l ∧ ¬ inactive_condition l rsm)
∨ yield_condition (proc_id (uRData l)) l ∨ inyield_condition l rsm).
{
destruct l; inv H13.
destruct (zeq (proc_id (uRData l0)) (proc_id (uRData (e::l0)))).
- right. left. unfold yield_condition.
refine_split´; trivial.
functional inversion Hnextblock.
functional inversion H0; trivial.
- destruct (ZMap.get (proc_id (uRData l0)) rsm) eqn: Heq´.
+ left. split. eapply active_condition_false; auto.
eapply inactive_condition_false; auto.
+ right. right. unfold inyield_condition.
refine_split´; trivial.
rewrite Heq´. congruence.
functional inversion Hnextblock.
functional inversion H0; trivial.
+ right. right. unfold inyield_condition.
refine_split´; trivial.
rewrite Heq´. congruence.
functional inversion Hnextblock.
functional inversion H0; trivial.
}
assert (Hnbeq: nb = last_nb l).
{
destruct l; inv H13. simpl.
rewrite Hnextblock. trivial.
}
refine_split´.
+ apply plus_one.
eapply eexec_step_external_yield_back; eauto.
rewrite <- DMapEq.
rewrite ZMap.gss; auto.
+ apply ZMap_gss_eq in H5.
econstructor; eauto.
× congruence.
× rewrite <- (ZMap.set2 (proc_id (uRData l)) ts).
eapply ts_lessdef_gss; eauto.
subst ts´.
constructor.
regset_lessdef_solve_tac.
× eapply ZMap_gss_eq in H9. inv H9. trivial.
× intros HF.
subst.
destruct Hac as [HF´|[HF´|HF´]].
{
exploit Hnbbig; try eapply HF´.
intros (Hle1 & Hle2).
erewrite lift_nextblock_le; eauto.
}
{
rewrite <- Hyield; auto.
assert (Ha: active_condition (proc_id (uRData l)) l) by (right; trivial).
specialize (Nextblock0 Ha).
erewrite lift_nextblock_le; eauto.
reflexivity.
}
{
rewrite <- Hinyield; auto.
assert (Ha: inactive_condition l rsm) by (right; trivial).
specialize (Nextblock1 Ha).
erewrite lift_nextblock_le; eauto.
reflexivity.
}
× intros HF.
eapply inactive_condition_diff_neq in HF; eauto. inv HF.
rewrite lastEvType_tail; simpl.
erewrite uRData_proc_id_eq; eauto.
split; eauto. congruence.
× intro HF. eapply yield_condition_false2 in HF. inv HF.
unfold lastEvType; simpl. congruence.
× intro HF. eapply inyield_condition_false2 in HF. inv HF.
unfold lastEvType; simpl. congruence.
× intros. elim Hnac. left.
erewrite uRData_proc_id_eq; trivial.
split; trivial.
unfold lastEvType; simpl. congruence.
× subst.
destruct Hac as [HF´|[HF´|HF´]].
{
exploit Hnbbig; try eapply HF´.
intros (Hle1 & Hle2).
destruct (plt (Mem.nextblock m0) (Mem.nextblock m)).
{
assert (Hle: (Mem.nextblock m0 ≤ Mem.nextblock m)%positive) by xomega.
erewrite (mem_disjoint_union_nextblock_eq m gm m0); eauto.
eapply mem_disjoint_union_lift_nextblock_left; eauto.
}
{
assert (Hle: (Mem.nextblock m ≤ Mem.nextblock m0)%positive) by xomega.
erewrite (mem_disjoint_union_nextblock_eq m0 gm m); eauto.
eapply mem_disjoint_union_lift_nextblock_left´; eauto.
xomega.
eapply mem_disjoint_union_commutativity; eauto.
}
}
{
rewrite <- Hyield; auto.
assert (Ha: active_condition (proc_id (uRData l)) l) by (right; trivial).
specialize (Nextblock0 Ha).
erewrite (mem_disjoint_union_nextblock_eq m gm m0); eauto.
eapply mem_disjoint_union_lift_nextblock_left; eauto.
}
{
rewrite <- Hinyield; auto.
assert (Ha: inactive_condition l rsm) by (right; trivial).
specialize (Nextblock1 Ha).
erewrite (mem_disjoint_union_nextblock_eq m0 gm m); eauto.
eapply mem_disjoint_union_lift_nextblock_left´; eauto.
xomega.
eapply mem_disjoint_union_commutativity; eauto.
}
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.
Context `{s_oracle_link : SingleLinkConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil}.
Context `{real_params: RealParams}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Context `{LH: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined (LH ⊕ L64)}.
Context `{lasmops: !LAsmAbsDataProp}.
Context (left_thread : Z) (right_thread : Z).
Class EAsmComposeConfiguration :=
{
left_valid: In left_thread full_thread_list;
right_valid: In right_thread full_thread_list;
disjoint_valid: left_thread ≠ right_thread
}.
Context`{compose_thread_config: EAsmComposeConfiguration}.
Definition compose_estate := prod (estate (mem:= mem)) (estate (mem:= mem)).
Inductive compose_estep (ge: genv) : compose_estate → trace → compose_estate → Prop :=
| eexec_step_left:
∀ curid curid´ l l´ rsm0 rsm1 m0 m1 dp0 dp1 rsm0´ rsm1´ m0´ m1´ dp0´ dp1´
(Hleft: estep ge (EState curid rsm0 m0 dp0 l) E0 (EState curid´ rsm0´ m0´ dp0´ l´))
(Hright: star estep ge (EState curid rsm1 m1 dp1 l)
E0 (EState curid´ rsm1´ m1´ dp1´ l´)),
compose_estep ge ((EState curid rsm0 m0 dp0 l), (EState curid rsm1 m1 dp1 l)) E0
((EState curid´ rsm0´ m0´ dp0´ l´), (EState curid´ rsm1´ m1´ dp1´ l´))
| eexec_step_right:
∀ curid curid´ l l´ rsm0 rsm1 m0 m1 dp0 dp1 rsm0´ rsm1´ m0´ m1´ dp0´ dp1´
(Hleft: star estep ge (EState curid rsm0 m0 dp0 l) E0 (EState curid´ rsm0´ m0´ dp0´ l´))
(Hright: estep ge (EState curid rsm1 m1 dp1 l)
E0 (EState curid´ rsm1´ m1´ dp1´ l´)),
compose_estep ge ((EState curid rsm0 m0 dp0 l), (EState curid rsm1 m1 dp1 l)) E0
((EState curid´ rsm0´ m0´ dp0´ l´), (EState curid´ rsm1´ m1´ dp1´ l´)).
Inductive compose_einitial{F V} (p: AST.program F V) : compose_estate → Prop :=
| compose_einitial_intro:
∀ s1 s2 (Hleft: einitial_state (left_thread::nil) p s1)
(Hright: einitial_state (right_thread::nil) p s2),
compose_einitial p (s1, s2).
Inductive compose_efinal: compose_estate → int → Prop :=
| compose_efinal_intro:
∀ s1 s2 r (Hleft: efinal_state s1 r)
(Hright: efinal_state s2 r),
compose_efinal (s1, s2) r.
Definition compose_esemantics (p: program) :=
Smallstep.Semantics compose_estep (compose_einitial p) compose_efinal (Genv.globalenv p).
Lemma compose_esemantics_single_events:
∀ p, single_events (compose_esemantics p).
Proof.
intros p s t s´ Hstep; inv Hstep; auto.
Qed.
Lemma compose_esemantics_receptive:
∀ p, receptive (compose_esemantics p).
Proof.
intros; constructor.
- intros s t1 s1 t2 Hstep Hmatch; inv Hstep; inv Hmatch.
+ eexists; eapply eexec_step_left; eauto.
+ eexists; eapply eexec_step_right; eauto.
- apply compose_esemantics_single_events.
Qed.
Inductive match_data: (ZMap.t ThreadState) → mem → (ZMap.t (option dproc)) →
ThreadState → mem → dproc → Z →
ThreadState → mem → dproc → Z → Log → Z → Prop :=
| MATCH_DATA:
∀ ts0 ts1 rsm rsm1 (d0 d1: dproc) (dp dp1: ZMap.t (option dproc))
m m0 m1 tid0 tid1 curid l
(Hts0: ts0 ≠ Environment)
(Hts1: ts1 ≠ Environment)
(Hrsm1: rsm1 = ZMap.set tid1 ts1 (ZMap.init Environment))
(Hdp1: dp1 = ZMap.set tid1 (Some d1) (ZMap.init None))
(MapEq: (∀ i,
ts_lessdef (ZMap.get i (ZMap.set tid0 ts0 rsm1))
(ZMap.get i rsm)))
(DMapEq: (∀ i,
ZMap.get i (ZMap.set tid0 (Some d0) dp1) = ZMap.get i dp))
(NoneReg: tid0 ≠ tid1)
(Nextblock0: active_condition tid0 l→ (Mem.nextblock m1 ≤ Mem.nextblock m0) % positive)
(Nextblock1: inactive_condition l rsm1 → (Mem.nextblock m0 ≤ Mem.nextblock m1) % positive)
(Hyield: yield_condition tid0 l → Mem.nextblock m0 = last_nb l)
(Hinyield: inyield_condition l rsm1 → Mem.nextblock m1 = last_nb l)
(Hnbbig: let lnb := last_nb l in
∀ (Hnac: ¬ active_condition tid0 l)
(Hninac: ¬ inactive_condition l rsm1),
(Mem.nextblock m0 ≤ lnb ∧ Mem.nextblock m1 ≤ lnb)%positive),
mem_disjoint_union m0 m1 m →
match_data rsm m dp ts0 m0 d0 tid0 ts1 m1 d1 tid1 l curid.
Inductive match_compose_estate: compose_estate → (estate (mem:= mem)) → Prop :=
| MATCH_COMPOSE_ESTATE:
∀ grsm gm gdp l curid rsm0 m0 dp0 ts0 d0 rsm1 m1 dp1 ts1 d1
(RSM0: rsm0 = ZMap.set left_thread ts0 (ZMap.init Environment))
(DP0: dp0 = ZMap.set left_thread (Some d0) (ZMap.init None))
(RSM1: rsm1 = ZMap.set right_thread ts1 (ZMap.init Environment))
(DP1: dp1 = ZMap.set right_thread (Some d1) (ZMap.init None))
(Match: match_data grsm gm gdp ts0 m0 d0 left_thread ts1 m1 d1 right_thread l curid),
match_compose_estate ((EState curid rsm0 m0 dp0 l), (EState curid rsm1 m1 dp1 l)) (EState curid grsm gm gdp l).
Lemma match_data_imply:
∀ grsm gm gdp ts0 m0 d0 tid0 ts1 m1 d1 tid1 l curid rsm1 dp1
(Hrsm1: rsm1 = ZMap.set tid1 ts1 (ZMap.init Environment))
(Hdp1: dp1 = ZMap.set tid1 (Some d1) (ZMap.init None))
(Match: match_data grsm gm gdp ts0 m0 d0 tid0 ts1 m1 d1 tid1 l curid),
match_estate_state grsm gm gdp rsm1 m0 dp1 ts0 m1 d0 tid0 l curid.
Proof.
intros. inv Match. econstructor; eauto.
rewrite ZMap.gso; eauto. rewrite ZMap.gi; eauto.
Qed.
Lemma match_data_imply_reverse:
∀ grsm gm gdp ts0 m0 d0 tid0 ts1 m1 d1 tid1 l curid rsm1 dp1
(Hts1: ts1 ≠ Environment)
(Hrsm1: rsm1 = ZMap.set tid1 ts1 (ZMap.init Environment))
(Hdp1: dp1 = ZMap.set tid1 (Some d1) (ZMap.init None))
(Match: match_estate_state grsm gm gdp rsm1 m0 dp1 ts0 m1 d0 tid0 l curid),
match_data grsm gm gdp ts0 m0 d0 tid0 ts1 m1 d1 tid1 l curid.
Proof.
intros. inv Match. econstructor; eauto.
intro HF; subst.
rewrite ZMap.gss in NoneReg.
congruence.
Qed.
Lemma yield_condition_imply:
∀ tid1 l ts1
(Hts1: ts1 ≠ Environment)
(Hcon: yield_condition tid1 l),
inyield_condition l (ZMap.set tid1 ts1 (ZMap.init Environment)).
Proof.
intros. inv Hcon.
destruct H as (l´ & Hl & HT1 & HT2).
unfold inyield_condition.
∃ x, l´.
rewrite HT1. rewrite ZMap.gss.
refine_split´; eauto.
Qed.
Lemma active_condition_imply:
∀ tid1 l ts1
(Hts1: ts1 ≠ Environment)
(Hcon: active_condition tid1 l),
inactive_condition l (ZMap.set tid1 ts1 (ZMap.init Environment)).
Proof.
intros. inv Hcon.
- econstructor.
destruct H as (HT1 & HT2).
rewrite HT1. rewrite ZMap.gss.
split; eauto.
- right. eapply yield_condition_imply; eauto.
Qed.
Lemma inyield_condition_imply:
∀ tid1 l ts1
(Hts1: ts1 ≠ Environment)
(Hcon: inyield_condition l (ZMap.set tid1 ts1 (ZMap.init Environment))),
yield_condition tid1 l.
Proof.
intros. inv Hcon.
destruct H as (l´ & Hl & HT1 & HT2).
unfold yield_condition.
∃ x, l´.
refine_split´; eauto.
destruct (zeq tid1 (proc_id (uRData l´))); subst; trivial.
rewrite ZMap.gso in HT1; eauto.
rewrite ZMap.gi in HT1. congruence.
Qed.
Lemma inactive_condition_imply:
∀ tid1 l ts1
(Hts1: ts1 ≠ Environment)
(Hcon: inactive_condition l (ZMap.set tid1 ts1 (ZMap.init Environment))),
active_condition tid1 l.
Proof.
intros. inv Hcon.
- econstructor.
destruct H as (HT1 & HT2).
split; eauto.
destruct (zeq tid1 (proc_id (uRData l))); subst; trivial.
rewrite ZMap.gso in HT1; eauto.
rewrite ZMap.gi in HT1. congruence.
- right. eapply inyield_condition_imply; eauto.
Qed.
Lemma match_data_commu:
∀ grsm gm gdp rs0 m0 d0 tid0 rs1 m1 d1 tid1 l curid
(Match: match_data grsm gm gdp rs0 m0 d0 tid0 rs1 m1 d1 tid1 l curid),
match_data grsm gm gdp rs1 m1 d1 tid1 rs0 m0 d0 tid0 l curid.
Proof.
intros. inv Match. econstructor; eauto.
- intros. destruct (zeq i tid1); subst.
+ rewrite ZMap.gss. specialize (MapEq tid1).
rewrite ZMap.gso in MapEq; eauto.
rewrite ZMap.gss in MapEq; eauto.
+ rewrite ZMap.gso; eauto. specialize (MapEq i).
destruct (zeq i tid0); subst.
× rewrite ZMap.gss in ×. eauto.
× rewrite ZMap.gso; eauto.
rewrite ZMap.gso in MapEq; eauto.
rewrite ZMap.gso in MapEq; eauto.
- intros. destruct (zeq i tid1); subst.
+ rewrite ZMap.gss. specialize (DMapEq tid1).
rewrite ZMap.gso in DMapEq; eauto.
rewrite ZMap.gss in DMapEq; eauto.
+ rewrite ZMap.gso; eauto. specialize (DMapEq i).
destruct (zeq i tid0); subst.
× rewrite ZMap.gss in ×. eauto.
× rewrite ZMap.gso; eauto.
rewrite ZMap.gso in DMapEq; eauto.
rewrite ZMap.gso in DMapEq; eauto.
- intros. eapply Nextblock1.
eapply active_condition_imply; eauto.
- intros. eapply Nextblock0.
eapply (inactive_condition_imply _ _ rs0); eauto.
- intros. eapply Hinyield.
eapply yield_condition_imply; eauto.
- intros. eapply Hyield.
eapply (inyield_condition_imply _ _ rs0); eauto.
- intros. exploit Hnbbig; eauto.
+ intro HF. elim Hninac.
eapply active_condition_imply; eauto.
+ intro HF. elim Hnac.
eapply inactive_condition_imply; eauto.
+ intros (HT1 & HT2). split; trivial.
- eapply mem_disjoint_union_commutativity; eauto.
Qed.
Context `{extcallsx: !ExternalCallsXDefined (LH ⊕ L64)}.
Context `{primcall_props: !PrimcallProperties EAsm.sprimitive_call}.
Theorem cl_backward_simulation:
∀ (s: StencilImpl.stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
(Hs: genv_next s = init_nb)
(Hph: noglobvar ph)
(Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (LH ⊕ L64) = OK ph),
backward_simulation
(compose_esemantics ph)
(EAsm.esemantics (left_thread::right_thread::nil) ph).
Proof.
intros. apply forward_to_backward_simulation; eauto.
- eapply forward_simulation_plus with (match_states:= match_compose_estate);
simpl; intros; trivial.
+
destruct H.
destruct Hleft as [m0l Hm0l curidl rsml].
destruct Hright as [m0r Hm0r curidr rsmr].
econstructor; split.
× econstructor; eauto.
× assert (m0r = m0l) by congruence; subst.
assert (Mem.nextblock m0l = init_nb).
{
erewrite <- Genv.init_mem_genv_next; eauto.
rewrite <- Hs.
eapply make_globalenv_genv_next.
unfold make_globalenv.
setoid_rewrite Hmakep.
reflexivity.
}
econstructor; [reflexivity .. | ].
econstructor; try reflexivity; eauto.
{ unfold init_regset. destruct (decide _); congruence. }
{ unfold init_regset. destruct (decide _); congruence. }
{ intros. apply ts_lessdef_refl. }
{ apply disjoint_valid. }
{
intros lnb _ _.
subst lnb.
rewrite H.
split; reflexivity.
}
{
eapply init_mem_disjoint_union; eauto.
}
+
destruct H0.
destruct Hleft.
+
destruct s2. inv H0.
assert (Hts0: ts0 ≠ Environment) by (destruct Match; eauto).
assert (Hts1: ts1 ≠ Environment) by (destruct Match; eauto).
inv H; subst.
× exploit one_step_init; eauto.
intros (rs0´ & d0´ & Hrsm0´ & Hdp0´ & Hrs0´).
exploit star_step_init; eauto.
intros (rs1´ & d1´ & Hrsm1´ & Hdp1´ & Hrs1´).
subst. eapply match_data_imply in Match; eauto.
eapply one_step_EAsm_compose in Hleft; eauto.
destruct Hleft as (gm´ & grsm´ & gdp´ & Hplus & Hme).
refine_split´; eauto.
econstructor; eauto.
eapply match_data_imply_reverse; eauto.
× exploit one_step_init; eauto.
intros (rs1´ & d1´ & Hrsm1´ & Hdp1´ & Hrs1´).
exploit star_step_init; eauto.
intros (rs0´ & d0´ & Hrsm0´ & Hdp0´ & Hrs0´).
subst. eapply match_data_commu in Match.
eapply match_data_imply in Match; eauto.
eapply one_step_EAsm_compose in Hright; eauto.
destruct Hright as (gm´ & grsm´ & gdp´ & Hplus & Hme).
refine_split´; eauto.
econstructor; eauto.
eapply match_data_commu; eauto.
eapply match_data_imply_reverse; eauto.
- apply compose_esemantics_receptive.
- apply easm_semantics_determinate; eauto.
Qed.
End Link.