Library mcertikos.conlib.conmtlib.AsmIIE2E
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 FutureTactic.
Require Import SingleConfiguration.
Require Import LAsm.
Require Import IIEAsm.
Require Import EAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Require Import EAsmPropLib.
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 disjoint_union_next_block_left_or_right:
∀ ml mr m next_block_val,
mem_disjoint_union ml mr m →
Mem.nextblock m = next_block_val →
Mem.nextblock ml = next_block_val ∨ Mem.nextblock mr = next_block_val.
Proof.
intros.
eapply mem_disjoint_union_nextblock_max in H.
rewrite H in H0.
unfold Pos.max in H0.
subdestruct.
- subst.
apply Pos.compare_eq in Hdestruct.
rewrite Hdestruct.
auto.
- subst.
right; auto.
- subst.
left; auto.
Qed.
Lemma disjoint_union_next_block_cond:
∀ ml mr m next_block_val,
mem_disjoint_union ml mr m →
Mem.nextblock m = next_block_val →
(Mem.nextblock ml = next_block_val → (Mem.nextblock mr ≤ Mem.nextblock ml)%positive) ∧
(Mem.nextblock mr = next_block_val → (Mem.nextblock ml ≤ Mem.nextblock mr)%positive).
Proof.
intros.
eapply mem_disjoint_union_nextblock_max in H.
rewrite H in H0.
unfold Pos.max in H0.
subdestruct.
- subst.
apply Pos.compare_eq in Hdestruct.
rewrite Hdestruct.
split; intros; apply Pos.le_refl.
- subst.
split.
+ intros.
rewrite Pos.compare_lt_iff in Hdestruct.
rewrite H0 in Hdestruct.
eapply Pos2Nat.inj_lt in Hdestruct.
omega.
+ intros.
rewrite Pos.compare_lt_iff in Hdestruct; auto.
eapply Pos.lt_le_incl; auto.
- subst.
split.
+ intros.
rewrite Pos.compare_gt_iff in Hdestruct; auto.
eapply Pos.lt_le_incl; auto.
+ intros.
rewrite Pos.compare_gt_iff in Hdestruct.
rewrite H0 in Hdestruct.
eapply Pos2Nat.inj_lt in Hdestruct.
omega.
Qed.
Lemma active_condition_disjoint:
∀ l,
active_condition current_thread l →
∀ i, i ≠ current_thread → ¬active_condition i l.
Proof.
intros.
unfold active_condition in ×.
intros contra.
destruct H.
destruct contra.
destruct H.
destruct H1.
rewrite H in H1.
elim H0; auto.
destruct H.
unfold yield_condition in H1.
destruct H1 as (a & l´ & H1a & H1b & H1c).
subst.
unfold getLogEventType in H1c; destruct a.
unfold getLogEventUnitType in H1c.
destruct l; inv H1c.
unfold lastEvType in H2; simpl in H2; elim H2; auto.
unfold lastEvType in H2; simpl in H2; elim H2; auto.
destruct contra.
destruct H1.
unfold yield_condition in H.
destruct H as (a & l´ & H1a & H1b & H1c).
subst.
unfold getLogEventType in H1c; destruct a.
unfold getLogEventUnitType in H1c.
destruct l; inv H1c.
unfold lastEvType in H2; simpl in H2; elim H2; auto.
unfold lastEvType in H2; simpl in H2; elim H2; auto.
unfold yield_condition in H, H1.
destruct H as (a & l´ & H1a & H1b & H1c).
destruct H1 as (a1 & l1´ & H2a & H2b & H2c).
subst.
inv H2a.
rewrite H1b in H0.
elim H0.
auto.
Qed.
Definition mem_block_conditions (mp_h: (mem × mem)) (m_l : mem) (l : Log) : Prop :=
(mem_disjoint_union (fst mp_h) (snd mp_h) m_l) ∧
(active_condition current_thread l →
(Mem.nextblock (snd mp_h) ≤ Mem.nextblock (fst mp_h)) % positive) ∧
(∀ i, i ≠ current_thread → active_condition i l →
(Mem.nextblock (fst mp_h) ≤ Mem.nextblock (snd mp_h)) % positive) ∧
(∀ i, yield_condition i l → Mem.nextblock m_l = last_nb l).
Definition total_machine_regset (i : Z) rsm :=
∃ rs, ZMap.get i rsm = Running rs ∨ ZMap.get i rsm = Available.
Inductive match_iestate_estate (ge : genv) : (iestate (mem := mem)) →
(estate (mem := mem)) → Prop :=
| MATCH_IESTATE_ESTATE:
∀ curid rsm_h rsm_l (dp_h dp_l : ZMap.t (option dproc)) (mp_h: (mem × mem)) m_l l
(HCurID : proc_id (uRData l) = curid)
(HRsmDom3 : ∀ i, In i full_thread_list → total_machine_regset i rsm_h)
(HRsmDom3 : ∀ i, In i full_thread_list → total_machine_regset i rsm_l)
(HRsmRel: ∀ i, In i full_thread_list →
ts_lessdef (ZMap.get i rsm_h) (ZMap.get i rsm_l))
(HDprocDom3: ∀ i, In i full_thread_list → ZMap.get i dp_h ≠ None)
(HDprocDom3: ∀ i, In i full_thread_list → ZMap.get i dp_l ≠ None)
(HDprocRel: ∀ i, In i full_thread_list → ZMap.get i dp_h = ZMap.get i dp_l)
(HMemRel: mem_block_conditions mp_h m_l l),
match_iestate_estate ge (IEState curid rsm_h mp_h dp_h l) (EState curid rsm_l m_l dp_l l).
Theorem one_step_Asm_E2E:
∀ ge curid curid´ mp_h mp_h´ m_l rsm_h rsm_l rsm_h´ l l´ (dp_h dp_l dp_h´ : ZMap.t (option dproc)) t
(HEStep: IIEAsm.iestep ge (IEState curid rsm_h mp_h dp_h l) t (IEState curid´ rsm_h´ mp_h´ dp_h´ l´))
(HMatch: match_iestate_estate ge (IEState curid rsm_h mp_h dp_h l) (EState curid rsm_l m_l dp_l l)),
∃ rsm_l´ m_l´ dp_l´,
(plus EAsm.estep) ge (EState curid rsm_l m_l dp_l l) t (EState curid´ rsm_l´ m_l´ dp_l´ l´)
∧ match_iestate_estate ge (IEState curid´ rsm_h´ mp_h´ dp_h´ l´) (EState curid´ rsm_l´ m_l´ dp_l´ l´).
Proof.
intros.
inversion HEStep; substx.
-
rename l´ into l.
assert (HCond: (mem_block_conditions mp_h m_l l) ∧
ts_lessdef (ZMap.get (proc_id (uRData l)) rsm_h)
(ZMap.get (proc_id (uRData l)) rsm_l)).
{ inv HMatch.
split; auto.
exploit (HRsmRel (proc_id (uRData l))).
{ apply all_cid_in_full_thread_list; auto. }
intros; auto. }
destruct HCond as (Hmem & Hlessdef).
assert (Htemp: ∃ rs_l, ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧
regset_lessdef rs rs_l).
{ inv Hlessdef; try (rewrite H8 in H0; inv H0).
rewrite <- H in H8.
inv H8.
∃ rs´0; auto. }
assert (Hactive: active_condition (proc_id (uRData l)) l).
{ unfold active_condition.
left.
split; auto. }
destruct Htemp as (rs_l & Hrs_cond1 & Hrs_cond2).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; subst.
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mother ≤ Mem.nextblock mcur)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
rewrite Hdec in Hactive; intros; subst.
simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
exploit exec_instr_disjoint_union; eauto.
intros H.
destruct H as (m_l´ & rs_l´ & Hexec & Hmem_l1 & Hmem_l2 & Hrs_l).
∃ (ZMap.set (proc_id (uRData l)) (Running rs_l´) rsm_l).
∃ m_l´.
∃ (ZMap.set (proc_id (uRData l)) (Some d´) dp_l).
split.
×
eapply plus_one.
eapply eexec_step_internal; eauto.
eapply regset_lessdef_eq; eauto. congruence.
inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto.
×
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; ∃ rs´; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; ∃ rs_l´; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ rewrite Hdec in Hactive.
generalize (active_condition_disjoint l Hactive i0 H); auto.
intros contra; elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´ & Hlval & Hproc_id & Hty).
rewrite Hlval in H15.
elim H15.
unfold lastEvType; simpl; f_equal; auto. }
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mcur ≤ Mem.nextblock mother)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
generalize (H1 (proc_id (uRData l)) Hdec Hactive); intros; simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
apply mem_disjoint_union_commutativity in Hmem2.
exploit exec_instr_disjoint_union; eauto.
intros H.
destruct H as (m_l´ & rs_l´ & Hexec & Hmem_l1 & Hmem_l2 & Hrs_l).
∃ (ZMap.set (proc_id (uRData l)) (Running rs_l´) rsm_l).
∃ m_l´.
∃ (ZMap.set (proc_id (uRData l)) (Some d´) dp_l).
split.
×
eapply plus_one.
eapply eexec_step_internal; eauto.
eapply regset_lessdef_eq; eauto. congruence.
inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto.
×
apply mem_disjoint_union_commutativity in Hmem_l1.
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; ∃ rs´; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; ∃ rs_l´; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ generalize (active_condition_disjoint l H (proc_id (uRData l)) Hdec); intro contra;
elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´ & Hlval & Hproc_id & Hty).
rewrite Hlval in H15.
elim H15.
unfold lastEvType; simpl; f_equal; auto. }
-
rename l´ into l.
assert (HCond: (mem_block_conditions mp_h m_l l) ∧
ts_lessdef (ZMap.get (proc_id (uRData l)) rsm_h)
(ZMap.get (proc_id (uRData l)) rsm_l)).
{ inv HMatch.
split; auto.
exploit (HRsmRel (proc_id (uRData l))).
{ apply all_cid_in_full_thread_list; auto. }
intros; auto. }
destruct HCond as (Hmem & Hlessdef).
assert (Htemp: ∃ rs_l, ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧
regset_lessdef rs rs_l).
{ inv Hlessdef; try (rewrite H9 in H0; inv H0).
rewrite <- H in H9.
inv H9.
∃ rs´; auto. }
assert (Hactive: active_condition (proc_id (uRData l)) l).
{ unfold active_condition.
left.
split; auto. }
destruct Htemp as (rs_l & Hrs_cond1 & Hrs_cond2).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; subst.
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mother ≤ Mem.nextblock mcur)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
rewrite Hdec in Hactive; intros; subst.
simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
exploit (exec_external_disjoint_union_regset (L:= L)); eauto.
intros (m_l´ & vl´ & Hexec & HMem_l1 & HMem_l2 & Hrs_rel).
refine_split´.
×
apply plus_one.
eapply eexec_step_builtin; eauto.
eapply regset_lessdef_eq; eauto. congruence.
inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto.
×
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
regset_lessdef_solve_tac.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ rewrite Hdec in Hactive.
generalize (active_condition_disjoint l Hactive i H); auto.
intros contra; elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´ & Hlval & Hproc_id & Hty).
rewrite Hlval in H15.
elim H15.
unfold lastEvType; simpl; f_equal; auto. }
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mcur ≤ Mem.nextblock mother)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
generalize (H1 (proc_id (uRData l)) Hdec Hactive); intros; simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
apply mem_disjoint_union_commutativity in Hmem2.
exploit (exec_external_disjoint_union_regset (L:= L)); eauto.
intros (m_l´ & vl´ & Hexec & HMem_l1 & HMem_l2 & Hrs_rel).
refine_split´.
×
apply plus_one.
eapply eexec_step_builtin; eauto.
eapply regset_lessdef_eq; eauto. congruence.
inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto.
×
apply mem_disjoint_union_commutativity in HMem_l1.
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
regset_lessdef_solve_tac.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ generalize (active_condition_disjoint l H (proc_id (uRData l)) Hdec); intro contra;
elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´ & Hlval & Hproc_id & Hty).
rewrite Hlval in H15.
elim H15.
unfold lastEvType; simpl; f_equal; auto. }
-
rename l´ into l.
assert (HCond: (mem_block_conditions mp_h m_l l) ∧
ts_lessdef (ZMap.get (proc_id (uRData l)) rsm_h)
(ZMap.get (proc_id (uRData l)) rsm_l)).
{ inv HMatch.
split; auto.
exploit (HRsmRel (proc_id (uRData l))).
{ apply all_cid_in_full_thread_list; auto. }
intros; auto. }
destruct HCond as (Hmem & Hlessdef).
assert (Htemp: ∃ rs_l, ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧
regset_lessdef rs rs_l).
{ inv Hlessdef; try (rewrite H9 in H0; inv H0).
rewrite <- H in H9.
inv H9.
∃ rs´; auto. }
assert (Hactive: active_condition (proc_id (uRData l)) l).
{ unfold active_condition.
left.
split; auto. }
destruct Htemp as (rs_l & Hrs_cond1 & Hrs_cond2).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; subst.
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mother ≤ Mem.nextblock mcur)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
rewrite Hdec in Hactive; intros; subst.
simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
exploit annot_arguments_disjoint_union; eauto.
intros (vargs´ & Hargs & Hless).
exploit (exec_external_disjoint_union (L:=L)); eauto.
intros (m_l´ & vl´ & Hexec & HMem_l1 & HMem_l2 & Hrs_rel).
refine_split´.
×
apply plus_one.
eapply eexec_step_annot; eauto.
eapply regset_lessdef_eq; eauto. congruence.
inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto.
×
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
regset_lessdef_solve_tac.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ rewrite Hdec in Hactive.
generalize (active_condition_disjoint l Hactive i H); auto.
intros contra; elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´ & Hlval & Hproc_id & Hty).
rewrite Hlval in H16.
elim H16.
unfold lastEvType; simpl; f_equal; auto. }
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mcur ≤ Mem.nextblock mother)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
generalize (H1 (proc_id (uRData l)) Hdec Hactive); intros; simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
apply mem_disjoint_union_commutativity in Hmem2.
exploit annot_arguments_disjoint_union; eauto.
intros (vargs´ & Hargs & Hless).
exploit (exec_external_disjoint_union (L:=L)); eauto.
intros (m_l´ & vl´ & Hexec & HMem_l1 & HMem_l2 & Hrs_rel).
refine_split´.
×
apply plus_one.
eapply eexec_step_annot; eauto.
eapply regset_lessdef_eq; eauto. congruence.
inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto.
×
apply mem_disjoint_union_commutativity in HMem_l1.
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
regset_lessdef_solve_tac.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ generalize (active_condition_disjoint l H (proc_id (uRData l)) Hdec); intro contra;
elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´ & Hlval & Hproc_id & Hty).
rewrite Hlval in H16.
elim H16.
unfold lastEvType; simpl; f_equal; auto. }
-
assert (Hproc_id_same: proc_id (uRData l) = proc_id (uRData l´)).
{ destruct ef; try (subst; auto).
subdestruct.
- contradiction.
- contradiction.
- destruct NON_YIELD as (largs & choice & Ha & Hb & Hc); subst.
symmetry.
eapply uRData_proc_id_eq.
simpl; auto.
- subst; auto.
- contradiction.
- contradiction.
- destruct NON_YIELD as (largs & choice & Ha & Hb & Hc); subst.
symmetry.
eapply uRData_proc_id_eq.
simpl; auto.
- subst; auto. }
assert (HCond: (mem_block_conditions mp_h m_l l) ∧
ts_lessdef (ZMap.get (proc_id (uRData l)) rsm_h)
(ZMap.get (proc_id (uRData l)) rsm_l)).
{ inv HMatch.
split; auto.
exploit (HRsmRel (proc_id (uRData l))).
{ apply all_cid_in_full_thread_list; auto. }
intros; auto. }
destruct HCond as (Hmem & Hlessdef).
assert (Htemp: ∃ rs_l, ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧
regset_lessdef rs rs_l).
{ inv Hlessdef; try (rewrite H9 in H0; inv H0).
rewrite <- H in H9.
inv H9.
∃ rs´; auto. }
assert (Hactive: active_condition (proc_id (uRData l)) l).
{ unfold active_condition.
left.
split; auto. }
assert (Hactive´: active_condition (proc_id (uRData l)) l´).
{ destruct ef; try (subst; auto).
subdestruct.
- contradiction.
- contradiction.
- destruct NON_YIELD as (largs & choice & Ha & Hb & Hc); subst.
unfold active_condition.
left.
rewrite <- Hproc_id_same; split ;auto.
unfold lastEvType; simpl; intro contra.
inv contra.
- subst; auto.
- contradiction.
- contradiction.
- destruct NON_YIELD as (largs & choice & Ha & Hb & Hc); subst.
unfold active_condition.
left.
rewrite <- Hproc_id_same; split ;auto.
unfold lastEvType; simpl; intro contra.
inv contra.
- subst; auto. }
destruct Htemp as (rs_l & Hrs_cond1 & Hrs_cond2).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; subst.
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mother ≤ Mem.nextblock mcur)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
rewrite Hdec in Hactive; intros; subst.
simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
exploit extcall_arguments_disjoint_union; eauto.
intros (vargs´ & Hargs & Hless).
exploit exec_external_disjoint_union´; eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & vl´ & Hexe & Hunion & Hnb & Hless´).
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. }
{ inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto. }
×
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
regset_lessdef_solve_tac.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ rewrite Hdec in Hactive´.
generalize (active_condition_disjoint l´ Hactive´ i); auto.
intros contra; elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´´ & Hlval & Hproc_id & Hty).
destruct ef; subst; try (rewrite Hlval in H15; elim H15;
unfold lastEvType; simpl; f_equal; auto; fail).
subdestruct.
- contradiction.
- contradiction.
- destruct NON_YIELD as (? & ? & ? & ? & ?).
inv H1.
subst.
simpl in Hty; inv Hty.
- subst; elim H15; unfold lastEvType; simpl; simpl in Hty.
f_equal; auto. }
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mcur ≤ Mem.nextblock mother)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
generalize (H1 (proc_id (uRData l)) Hdec Hactive); intros; simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
apply mem_disjoint_union_commutativity in Hmem2.
exploit extcall_arguments_disjoint_union; eauto.
intros (vargs´ & Hargs & Hless).
exploit exec_external_disjoint_union´; eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & vl´ & Hexe & Hunion & Hnb & Hless´).
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. }
{ inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto. }
×
apply mem_disjoint_union_commutativity in Hunion.
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
regset_lessdef_solve_tac.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ generalize (active_condition_disjoint l´ H (proc_id (uRData l)) Hdec); intro contra;
elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´´ & Hlval & Hproc_id & Hty).
destruct ef; subst; try (rewrite Hlval in H15; elim H15;
unfold lastEvType; simpl; f_equal; auto; fail).
subdestruct.
- contradiction.
- contradiction.
- destruct NON_YIELD as (? & ? & ? & ? & ?).
inv H1.
subst.
simpl in Hty; inv Hty.
- subst; elim H15; unfold lastEvType; simpl; simpl in Hty.
f_equal; auto. }
-
assert (Hproc_id_same: proc_id (uRData l) = proc_id (uRData l´)).
{ destruct ef; try (subst; auto).
subdestruct.
- contradiction.
- contradiction.
- symmetry; subst.
eapply uRData_proc_id_eq.
simpl; auto.
- subst; auto.
- contradiction.
- contradiction.
- symmetry; subst.
eapply uRData_proc_id_eq.
simpl; auto.
- subst; auto. }
assert (HCond: (mem_block_conditions mp_h m_l l) ∧
ts_lessdef (ZMap.get (proc_id (uRData l)) rsm_h)
(ZMap.get (proc_id (uRData l)) rsm_l)).
{ inv HMatch.
split; auto.
exploit (HRsmRel (proc_id (uRData l))).
{ apply all_cid_in_full_thread_list; auto. }
intros; auto. }
destruct HCond as (Hmem & Hlessdef).
assert (Htemp: ∃ rs_l, ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧
regset_lessdef rs rs_l).
{ inv Hlessdef; try (rewrite H7 in H0; inv H0).
rewrite <- H in H7.
inv H7.
∃ rs´0; auto. }
assert (Hactive: active_condition (proc_id (uRData l)) l).
{ unfold active_condition.
left.
split; auto. }
assert (Hactive´: active_condition (proc_id (uRData l)) l´).
{ destruct ef; try (subst; auto).
subdestruct.
- contradiction.
- contradiction.
- inv NON_YIELD.
unfold active_condition.
left.
rewrite <- Hproc_id_same; split ;auto.
unfold lastEvType; simpl; intro contra.
inv contra.
- subst; auto.
- contradiction.
- contradiction.
- inv NON_YIELD.
unfold active_condition.
left.
rewrite <- Hproc_id_same; split ;auto.
unfold lastEvType; simpl; intro contra.
inv contra.
- subst; auto. }
destruct Htemp as (rs_l & Hrs_cond1 & Hrs_cond2).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; subst.
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mother ≤ Mem.nextblock mcur)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
rewrite Hdec in Hactive; intros; subst.
simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
exploit exec_primitive_disjoint_union; eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & vl´ & Hexe & Hunion & Hnb & Hless´).
refine_split´.
×
apply plus_one.
eapply eexec_step_prim_call; eauto.
{ eapply regset_lessdef_eq; eauto. congruence. }
{ inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto. }
×
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ rewrite Hdec in Hactive´.
generalize (active_condition_disjoint l´ Hactive´ i H); auto.
intros contra; elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´´ & Hlval & Hproc_id & Hty); subst.
destruct ef; try (subst; elim H14; unfold lastEvType; simpl; simpl in Hty;
f_equal; auto; fail).
subdestruct.
+ contradiction.
+ contradiction.
+ inv NON_YIELD.
simpl in Hty; inv Hty.
+ subst; elim H14; unfold lastEvType; simpl; simpl in Hty.
f_equal; auto. }
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mcur ≤ Mem.nextblock mother)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
generalize (H1 (proc_id (uRData l)) Hdec Hactive); intros; simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
apply mem_disjoint_union_commutativity in Hmem2.
exploit exec_primitive_disjoint_union; eauto.
{ eapply ef_id_imply; eapply NON_YIELD. }
intros (gm´ & vl´ & Hexe & Hunion & Hnb & Hless´).
refine_split´.
×
apply plus_one.
eapply eexec_step_prim_call; eauto.
{ eapply regset_lessdef_eq; eauto. congruence. }
{ inv HMatch.
exploit (HDprocRel (proc_id (uRData l))); auto.
apply all_cid_in_full_thread_list; auto.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto. }
×
apply mem_disjoint_union_commutativity in Hunion.
inv HMatch; constructor; intros; try auto.
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; eexists; auto.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss.
constructor; auto.
- rewrite ?ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; intros contra; inv contra.
- intros; rewrite ZMap.gso; auto. }
{ case_eq (zeq i (proc_id (uRData l))); intros; subst.
- rewrite ?ZMap.gss; auto.
- rewrite ?ZMap.gso; auto. }
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
unfold mem_block_conditions; refine_split´; simpl; auto; intros.
{ generalize (active_condition_disjoint l´ H (proc_id (uRData l)) Hdec); intro contra;
elim contra; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´´ & Hlval & Hproc_id & Hty); subst.
destruct ef; try (subst; elim H14; unfold lastEvType; simpl; simpl in Hty;
f_equal; auto; fail).
subdestruct.
+ contradiction.
+ contradiction.
+ inv NON_YIELD.
simpl in Hty; inv Hty.
+ subst; elim H14; unfold lastEvType; simpl; simpl in Hty.
f_equal; auto. }
-
rename rsm_h´ into rsm_h.
rename mp_h´ into mp_h.
rename dp_h´ into dp_h.
assert (HCond: (mem_block_conditions mp_h m_l l) ∧
ts_lessdef (ZMap.get (proc_id (uRData l)) rsm_h)
(ZMap.get (proc_id (uRData l)) rsm_l)).
{ inv HMatch.
split; auto.
exploit (HRsmRel (proc_id (uRData l))).
{ apply all_cid_in_full_thread_list; auto. }
intros; auto. }
destruct HCond as (Hmem & Hlessdef).
assert (Htemp: ∃ rs_l, ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧
regset_lessdef rs rs_l).
{ inv Hlessdef; try (rewrite H9 in H0; inv H0).
rewrite <- H in H9.
inv H9.
∃ rs´; auto. }
assert (Hactive: active_condition (proc_id (uRData l)) l).
{ unfold active_condition.
left.
split; auto. }
destruct Htemp as (rs_l & Hrs_cond1 & Hrs_cond2).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; subst.
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mother ≤ Mem.nextblock mcur)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
rewrite Hdec in Hactive; intros; subst.
simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
assert (Htemp1: (ZMap.get (proc_id (uRData l)) (ZMap.set (proc_id (uRData l)) (Running rs) rsm_h)) =
ZMap.get (proc_id (uRData l)) rsm_h).
{ rewrite ZMap.gss.
rewrite H9; auto. }
assert (Htemp2: ZMap.get (proc_id (uRData l)) dp_h = ZMap.get (proc_id (uRData l)) dp_l).
{ inv HMatch.
eapply HDprocRel; auto.
apply all_cid_in_full_thread_list. }
rewrite H11 in Htemp2.
symmetry in Htemp2.
inv Hlessdef; try (rewrite H9 in H0; inv H0; fail).
symmetry in H, H0.
rewrite H9 in H; inv H.
rewrite Hrs_cond1 in H0.
inv H0.
rename rs´ into rs_l.
rename rs0 into rs_h.
generalize (mem_disjoint_union_nextblock_eq mcur m_l mother Hmem2 Hmem3); intros Htemp3.
refine_split´.
×
apply plus_one.
eapply eexec_step_external_yield; eauto.
{ eapply regset_lessdef_eq; eauto.
congruence. }
{ rewrite Htemp3; reflexivity. }
{ unfold state_checks in ×.
rewrite Htemp2.
rewrite H11 in H18.
auto. }
×
inv HMatch.
constructor; intros; auto.
unfold mem_block_conditions in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
refine_split´; simpl; auto; intros.
unfold active_condition in H0.
destruct H0.
{ unfold lastEvType in H0; simpl in H0.
destruct H0 as (_ & H0); elim H0; auto. }
{ unfold yield_condition in H0.
destruct H0 as (a & l´´ & Hlval & Hproc_id & Hty).
inv Hlval.
elim H; auto. }
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mcur ≤ Mem.nextblock mother)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
generalize (H1 (proc_id (uRData l)) Hdec Hactive); intros; simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
assert (Htemp1: (ZMap.get (proc_id (uRData l)) (ZMap.set (proc_id (uRData l)) (Running rs) rsm_h)) =
ZMap.get (proc_id (uRData l)) rsm_h).
{ rewrite ZMap.gss.
rewrite H9; auto. }
assert (Htemp2: ZMap.get (proc_id (uRData l)) dp_h = ZMap.get (proc_id (uRData l)) dp_l).
{ inv HMatch.
eapply HDprocRel; auto.
apply all_cid_in_full_thread_list. }
rewrite H11 in Htemp2.
symmetry in Htemp2.
inv Hlessdef; try (rewrite H9 in H0; inv H0; fail).
symmetry in H, H0.
rewrite H9 in H; inv H.
rewrite Hrs_cond1 in H0.
inv H0.
rename rs´ into rs_l.
rename rs0 into rs_h.
apply mem_disjoint_union_commutativity in Hmem2.
generalize (mem_disjoint_union_nextblock_eq mother m_l mcur Hmem2 Hmem3); intros Htemp3.
refine_split´.
×
apply plus_one.
eapply eexec_step_external_yield; eauto.
{ eapply regset_lessdef_eq; eauto.
congruence. }
{ rewrite Htemp3; reflexivity. }
{ unfold state_checks in ×.
rewrite Htemp2.
rewrite H11 in H18.
auto. }
×
inv HMatch.
constructor; intros; auto.
unfold mem_block_conditions in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
refine_split´; simpl; auto; intros.
unfold active_condition in H.
destruct H.
{ unfold lastEvType in H; simpl in H.
destruct H as (_ & H); elim H; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´´ & Hlval & Hproc_id & Hty).
inv Hlval.
elim Hdec; auto. }
-
rename rsm_h´ into rsm_h.
rename mp_h´ into mp_h.
rename dp_h´ into dp_h.
assert (HCond: (mem_block_conditions mp_h m_l l) ∧
ts_lessdef (ZMap.get (proc_id (uRData l)) rsm_h)
(ZMap.get (proc_id (uRData l)) rsm_l)).
{ inv HMatch.
split; auto.
exploit (HRsmRel (proc_id (uRData l))).
{ apply all_cid_in_full_thread_list; auto. }
intros; auto. }
destruct HCond as (Hmem & Hlessdef).
assert (Htemp: ∃ rs_l, ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧
regset_lessdef rs rs_l).
{ inv Hlessdef; try (rewrite H9 in H0; inv H0).
rewrite <- H in H9.
inv H9.
∃ rs´; auto. }
assert (Hactive: active_condition (proc_id (uRData l)) l).
{ unfold active_condition.
left.
split; auto. }
destruct Htemp as (rs_l & Hrs_cond1 & Hrs_cond2).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; subst.
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mother ≤ Mem.nextblock mcur)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
rewrite Hdec in Hactive; intros; subst.
simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
assert (Htemp1: (ZMap.get (proc_id (uRData l)) (ZMap.set (proc_id (uRData l)) (Running rs) rsm_h)) =
ZMap.get (proc_id (uRData l)) rsm_h).
{ rewrite ZMap.gss.
rewrite H9; auto. }
assert (Htemp2: ZMap.get (proc_id (uRData l)) dp_h = ZMap.get (proc_id (uRData l)) dp_l).
{ inv HMatch.
eapply HDprocRel; auto.
apply all_cid_in_full_thread_list. }
rewrite H11 in Htemp2.
symmetry in Htemp2.
inv Hlessdef; try (rewrite H9 in H0; inv H0; fail).
symmetry in H, H0.
rewrite H9 in H; inv H.
rewrite Hrs_cond1 in H0.
inv H0.
rename rs´ into rs_l.
rename rs0 into rs_h.
exploit extcall_arguments_disjoint_union; eauto.
intros (vargs´ & Hargs_l & Hless_l).
inv Hless_l.
inv H2.
inv H4.
generalize (mem_disjoint_union_nextblock_eq mcur m_l mother Hmem2 Hmem3); intros Htemp3.
refine_split´.
×
apply plus_one.
eapply eexec_step_external_sleep; eauto.
{ eapply regset_lessdef_eq; eauto.
congruence. }
{ rewrite Htemp3; reflexivity. }
{ unfold state_checks in ×.
rewrite Htemp2.
rewrite H11 in H18.
auto. }
×
inv HMatch.
constructor; intros; auto.
unfold mem_block_conditions in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
refine_split´; simpl; auto; intros.
unfold active_condition in H0.
destruct H0.
{ unfold lastEvType in H0; simpl in H0.
destruct H0 as (_ & H0); elim H0; auto. }
{ unfold yield_condition in H0.
destruct H0 as (a & l´´ & Hlval & Hproc_id & Hty).
inv Hlval.
elim H; auto. }
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin; inv MOrigin; subst.
assert (Hmem2: mem_disjoint_union mcur mother m_l ∧
(Mem.nextblock mcur ≤ Mem.nextblock mother)%positive).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?).
generalize (H1 (proc_id (uRData l)) Hdec Hactive); intros; simpl in *; auto. }
destruct Hmem2 as (Hmem2 & Hmem3).
assert (Htemp1: (ZMap.get (proc_id (uRData l)) (ZMap.set (proc_id (uRData l)) (Running rs) rsm_h)) =
ZMap.get (proc_id (uRData l)) rsm_h).
{ rewrite ZMap.gss.
rewrite H9; auto. }
assert (Htemp2: ZMap.get (proc_id (uRData l)) dp_h = ZMap.get (proc_id (uRData l)) dp_l).
{ inv HMatch.
eapply HDprocRel; auto.
apply all_cid_in_full_thread_list. }
rewrite H11 in Htemp2.
symmetry in Htemp2.
inv Hlessdef; try (rewrite H9 in H0; inv H0; fail).
symmetry in H, H0.
rewrite H9 in H; inv H.
rewrite Hrs_cond1 in H0.
inv H0.
rename rs´ into rs_l.
rename rs0 into rs_h.
apply mem_disjoint_union_commutativity in Hmem2.
exploit extcall_arguments_disjoint_union; eauto.
intros (vargs´ & Hargs_l & Hless_l).
inv Hless_l.
inv H2.
inv H4.
generalize (mem_disjoint_union_nextblock_eq mother m_l mcur Hmem2 Hmem3); intros Htemp3.
refine_split´.
×
apply plus_one.
eapply eexec_step_external_sleep; eauto.
{ eapply regset_lessdef_eq; eauto.
congruence. }
{ rewrite Htemp3; reflexivity. }
{ unfold state_checks in ×.
rewrite Htemp2.
rewrite H11 in H18.
auto. }
×
inv HMatch.
constructor; intros; auto.
unfold mem_block_conditions in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4); simpl in ×.
refine_split´; simpl; auto; intros.
unfold active_condition in H.
destruct H.
{ unfold lastEvType in H; simpl in H.
destruct H as (_ & H); elim H; auto. }
{ unfold yield_condition in H.
destruct H as (a & l´´ & Hlval & Hproc_id & Hty).
inv Hlval.
elim Hdec; auto. }
-
inv HMatch.
generalize (HDprocDom3 (proc_id (uRData l))); intros Htemp; exploit Htemp.
apply all_cid_in_full_thread_list; auto.
simpl; auto.
auto.
intros; inv H.
-
assert (Hproc_id_same: proc_id (uRData l) =
proc_id (uRData (LEvent (proc_id (uRData l)) LogYieldBack :: l))).
{ symmetry.
eapply uRData_proc_id_eq.
simpl; auto. }
assert (HCond: (mem_block_conditions mp_h m_l l) ∧
ts_lessdef (ZMap.get (proc_id (uRData l)) rsm_h)
(ZMap.get (proc_id (uRData l)) rsm_l)).
{ inv HMatch.
split; auto.
exploit (HRsmRel (proc_id (uRData l))).
{ apply all_cid_in_full_thread_list; auto. }
intros; auto. }
destruct HCond as (Hmem & Hlessdef).
assert (Hnbeq: nb = last_nb l).
{ destruct l; inv H13. simpl.
rewrite Hnextblock. trivial. }
assert (Mem.nextblock m_l = nb).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (_ & _ & _ & Hmem).
destruct l.
- simpl in H13; inv H13.
- simpl in H13; inv H13.
generalize (Hmem (proc_id (uRData l0))); intros.
unfold yield_condition in H.
exploit H.
∃ e, l0; refine_split; auto.
unfold getLogEventNB in Hnextblock.
destruct e.
unfold getLogEventUnitNB in Hnextblock.
destruct l; try (inv Hnextblock).
simpl; auto.
simpl; auto.
intros; auto. }
intros.
assert (Hdproc_l: ZMap.get (proc_id (uRData l)) dp_l = Some d).
{ inv HMatch.
rewrite <- HDprocRel; auto.
apply all_cid_in_full_thread_list; auto. }
rename dp_h´ into dp_h.
assert (Hmem2: mem_disjoint_union (fst mp_h) (snd mp_h) m_l).
{ unfold mem_block_conditions in Hmem.
destruct Hmem as (? & ? & ? & ?); auto. }
exploit disjoint_union_next_block_left_or_right; eauto; intros.
exploit disjoint_union_next_block_cond; eauto; intros.
Opaque full_thread_list.
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; subst.
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst; simpl in ×.
destruct H0.
×
destruct H1 as (H1 & _).
generalize (H1 H0); clear H1; intro H1.
destruct H7.
{ destruct H2.
assert (Hnewrsm: ZMap.get (proc_id (uRData l)) rsm_l = Available).
{ rewrite H2 in Hlessdef.
inversion Hlessdef; split; auto. }
set (rs´ := (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).
assert (Hnewrsm´: regset_lessdef rs´ rs´).
{ eapply regset_lessdef_refl; auto. }
∃ (ZMap.set (proc_id (uRData l)) (Running rs´) rsm_l).
set (m_l´ := mem_lift_nextblock m_l (Pos.to_nat (last_nb l) -
Pos.to_nat (Mem.nextblock m_l) % nat)).
∃ m_l´.
∃ dp_l.
refine_split.
-
apply plus_one.
exploit (eexec_step_external_yield_back ge rs´ rs0 m_l m_l´ (proc_id (uRData l)) rsm_l l
(LEvent (proc_id (uRData l)) LogYieldBack::l)
(last_nb l) dp_l d e); eauto.
-
inversion HMatch; substx.
constructor; simpl; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
× rewrite ?ZMap.gss.
constructor.
auto.
× rewrite ?ZMap.gso; auto.
+ unfold mem_block_conditions in *; simpl in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4).
refine_split´.
× rewrite H0.
rewrite H.
eapply mem_disjoint_union_lift_nextblock_left; auto.
× intros.
rewrite H0.
rewrite minus_diag.
assert (mem_lift_nextblock mcur 0 = mcur).
{ eapply mem_lift_nextblock_source_eq.
reflexivity. }
rewrite H5; auto.
× intros.
unfold active_condition in H5.
destruct H5.
{ destruct H5.
rewrite uRData_proc_id_eq in H5; simpl; auto.
rewrite Hdec in H5.
elim H4; auto. }
{ unfold yield_condition in H5.
destruct H5 as (a & l´ & H5a & H5b & H5c); inv H5a.
elim H4; auto. }
× intros.
unfold yield_condition in H4.
destruct H4 as (a & l´ & H4a & H4b & H4c).
inv H4a.
simpl in H4c.
inv H4c. }
{ assert (Hnewrsm: ∃ rs_l,
ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧ regset_lessdef rs0 rs_l).
{ rewrite H2 in Hlessdef.
inv Hlessdef.
∃ rs´; auto. }
destruct Hnewrsm as (rs_l & Hnewrsm_a & Hnewrsm_b).
set (rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs_l))
# EAX <- Vundef #PC <- (rs_l RA) #RA <- Vundef).
∃ (ZMap.set (proc_id (uRData l)) (Running rs´) rsm_l).
set (m_l´ := mem_lift_nextblock m_l (Pos.to_nat (last_nb l)
- Pos.to_nat (Mem.nextblock m_l) % nat)).
∃ m_l´.
∃ dp_l.
refine_split.
-
apply plus_one.
exploit (eexec_step_external_yield_back ge rs´ rs_l m_l m_l´ (proc_id (uRData l)) rsm_l l
(LEvent (proc_id (uRData l)) LogYieldBack::l)
(last_nb l) dp_l d e); auto.
-
inversion HMatch; substx.
constructor; simpl; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
× rewrite ?ZMap.gss.
constructor.
auto.
regset_lessdef_solve_tac.
× rewrite ?ZMap.gso; auto.
+ unfold mem_block_conditions in *; simpl in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4).
refine_split´.
× rewrite H0.
rewrite H.
eapply mem_disjoint_union_lift_nextblock_left; auto.
× intros.
rewrite H0.
rewrite minus_diag.
assert (mem_lift_nextblock mcur 0 = mcur).
{ eapply mem_lift_nextblock_source_eq.
reflexivity. }
rewrite H4; auto.
× intros.
unfold active_condition in H4.
destruct H4.
{ destruct H4.
rewrite uRData_proc_id_eq in H4; simpl; auto.
rewrite Hdec in H4.
elim H3; auto. }
{ unfold yield_condition in H4.
destruct H4 as (a & l´ & H5a & H5b & H5c); inv H5a.
elim H3; auto. }
× intros.
unfold yield_condition in H3.
destruct H3 as (a & l´ & H4a & H4b & H4c).
inv H4a.
simpl in H4c.
inv H4c. }
×
destruct H1 as (_ & H1).
generalize (H1 H0); clear H1; intro H1.
destruct H7.
{ destruct H2.
assert (Hnewrsm: ZMap.get (proc_id (uRData l)) rsm_l = Available).
{ rewrite H2 in Hlessdef.
inversion Hlessdef; split; auto. }
set (rs´ := (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).
assert (Hnewrsm´: regset_lessdef rs´ rs´).
{ eapply regset_lessdef_refl; auto. }
∃ (ZMap.set (proc_id (uRData l)) (Running rs´) rsm_l).
set (m_l´ := mem_lift_nextblock m_l (Pos.to_nat (last_nb l)
- Pos.to_nat (Mem.nextblock m_l) % nat)).
∃ m_l´.
∃ dp_l.
refine_split.
-
apply plus_one.
exploit (eexec_step_external_yield_back ge rs´ rs0 m_l m_l´ (proc_id (uRData l)) rsm_l l
(LEvent (proc_id (uRData l)) LogYieldBack::l)
(last_nb l) dp_l d e); eauto.
-
inversion HMatch; substx.
constructor; simpl; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
× rewrite ?ZMap.gss.
constructor.
auto.
× rewrite ?ZMap.gso; auto.
+ unfold mem_block_conditions in *; simpl in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4).
refine_split´.
× erewrite (mem_disjoint_union_nextblock_eq mother m_l mcur); eauto.
eapply mem_disjoint_union_lift_nextblock_left´; eauto.
xomega.
eapply mem_disjoint_union_commutativity; eauto.
× intros.
rewrite H0.
rewrite H0 in H1.
eapply (lift_nextblock_le mcur (last_nb l)) in H1.
rewrite H1.
xomega.
× intros.
unfold active_condition in H5.
destruct H5.
{ destruct H5.
rewrite uRData_proc_id_eq in H5; simpl; auto.
rewrite Hdec in H5.
elim H4; auto. }
{ unfold yield_condition in H5.
destruct H5 as (a & l´ & H5a & H5b & H5c); inv H5a.
elim H4; auto. }
× intros.
unfold yield_condition in H4.
destruct H4 as (a & l´ & H4a & H4b & H4c).
inv H4a.
simpl in H4c.
inv H4c. }
{ assert (Hnewrsm: ∃ rs_l,
ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧ regset_lessdef rs0 rs_l).
{ rewrite H2 in Hlessdef.
inv Hlessdef.
∃ rs´; auto. }
destruct Hnewrsm as (rs_l & Hnewrsm_a & Hnewrsm_b).
set (rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs_l))
# EAX <- Vundef #PC <- (rs_l RA) #RA <- Vundef).
∃ (ZMap.set (proc_id (uRData l)) (Running rs´) rsm_l).
set (m_l´ := mem_lift_nextblock m_l (Pos.to_nat (last_nb l)
- Pos.to_nat (Mem.nextblock m_l) % nat)).
∃ m_l´.
∃ dp_l.
refine_split.
-
apply plus_one.
exploit (eexec_step_external_yield_back ge rs´ rs_l m_l m_l´ (proc_id (uRData l)) rsm_l l
(LEvent (proc_id (uRData l)) LogYieldBack::l)
(last_nb l) dp_l d e); eauto.
-
inversion HMatch; substx.
constructor; simpl; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
× rewrite ?ZMap.gss.
constructor.
auto.
regset_lessdef_solve_tac.
× rewrite ?ZMap.gso; auto.
+ unfold mem_block_conditions in *; simpl in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4).
refine_split´.
× erewrite (mem_disjoint_union_nextblock_eq mother m_l mcur); eauto.
eapply mem_disjoint_union_lift_nextblock_left´; eauto.
xomega.
eapply mem_disjoint_union_commutativity; eauto.
× intros.
rewrite H0.
rewrite H0 in H1.
eapply (lift_nextblock_le mcur (last_nb l)) in H1.
rewrite H1.
xomega.
× intros.
unfold active_condition in H4.
destruct H4.
{ destruct H4.
rewrite uRData_proc_id_eq in H4; simpl; auto.
rewrite Hdec in H4.
elim H3; auto. }
{ unfold yield_condition in H4.
destruct H4 as (a & l´ & H5a & H5b & H5c); inv H5a.
elim H3; auto. }
× intros.
unfold yield_condition in H3.
destruct H3 as (a & l´ & H4a & H4b & H4c).
inv H4a.
simpl in H4c.
inv H4c. }
+
destruct mp_h as (mcur & mother).
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; subst; simpl in ×.
destruct H0.
×
destruct H1 as (H1 & _).
generalize (H1 H0); clear H1; intro H1.
destruct H7.
{ destruct H2.
assert (Hnewrsm: ZMap.get (proc_id (uRData l)) rsm_l = Available).
{ rewrite H2 in Hlessdef.
inversion Hlessdef; split; auto. }
set (rs´ := (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).
assert (Hnewrsm´: regset_lessdef rs´ rs´).
{ eapply regset_lessdef_refl; auto. }
∃ (ZMap.set (proc_id (uRData l)) (Running rs´) rsm_l).
set (m_l´ := mem_lift_nextblock m_l (Pos.to_nat (last_nb l) -
Pos.to_nat (Mem.nextblock m_l) % nat)).
∃ m_l´.
∃ dp_l.
refine_split.
-
apply plus_one.
exploit (eexec_step_external_yield_back ge rs´ rs0 m_l m_l´ (proc_id (uRData l)) rsm_l l
(LEvent (proc_id (uRData l)) LogYieldBack::l)
(last_nb l) dp_l d e); eauto.
-
inversion HMatch; substx.
constructor; simpl; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
× rewrite ?ZMap.gss.
constructor.
auto.
× rewrite ?ZMap.gso; auto.
+ unfold mem_block_conditions in *; simpl in ×.
apply mem_disjoint_union_commutativity in Hmem2.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4).
refine_split´.
× apply mem_disjoint_union_commutativity.
erewrite (mem_disjoint_union_nextblock_eq mcur m_l mother); eauto.
eapply mem_disjoint_union_lift_nextblock_left´; eauto.
xomega.
× intros.
unfold active_condition in H4.
destruct H4.
{ destruct H4.
rewrite uRData_proc_id_eq in H4; simpl; auto.
elim Hdec.
auto. }
{ unfold yield_condition in H4.
destruct H4 as (a & l´ & H5a & H5b & H5c); inv H5a.
simpl in H5c.
inv H5c. }
× intros.
rewrite H0.
rewrite H0 in H1.
eapply (lift_nextblock_le mother (last_nb l)) in H1.
rewrite H1.
xomega.
× intros.
unfold yield_condition in H4.
destruct H4 as (a & l´ & H4a & H4b & H4c).
inv H4a.
simpl in H4c.
inv H4c. }
{ assert (Hnewrsm: ∃ rs_l,
ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧ regset_lessdef rs0 rs_l).
{ rewrite H2 in Hlessdef.
inv Hlessdef.
∃ rs´; auto. }
destruct Hnewrsm as (rs_l & Hnewrsm_a & Hnewrsm_b).
set (rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs_l))
# EAX <- Vundef #PC <- (rs_l RA) #RA <- Vundef).
∃ (ZMap.set (proc_id (uRData l)) (Running rs´) rsm_l).
set (m_l´ := mem_lift_nextblock m_l (Pos.to_nat (last_nb l)
- Pos.to_nat (Mem.nextblock m_l) % nat)).
∃ m_l´.
∃ dp_l.
refine_split.
-
apply plus_one.
exploit (eexec_step_external_yield_back ge rs´ rs_l m_l m_l´ (proc_id (uRData l)) rsm_l l
(LEvent (proc_id (uRData l)) LogYieldBack::l)
(last_nb l) dp_l d e); eauto.
-
inversion HMatch; substx.
constructor; simpl; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
× rewrite ?ZMap.gss.
constructor.
auto.
regset_lessdef_solve_tac.
× rewrite ?ZMap.gso; auto.
+ unfold mem_block_conditions in *; simpl in ×.
apply mem_disjoint_union_commutativity in Hmem2.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4).
refine_split´.
× apply mem_disjoint_union_commutativity.
erewrite (mem_disjoint_union_nextblock_eq mcur m_l mother); eauto.
eapply mem_disjoint_union_lift_nextblock_left´; eauto.
xomega.
× intros.
unfold active_condition in H3.
destruct H3.
{ destruct H3.
rewrite uRData_proc_id_eq in H3; simpl; auto.
elim Hdec.
auto. }
{ unfold yield_condition in H3.
destruct H3 as (a & l´ & H5a & H5b & H5c); inv H5a.
simpl in H5c.
inv H5c. }
× intros.
rewrite H0.
rewrite H0 in H1.
eapply (lift_nextblock_le mother (last_nb l)) in H1.
rewrite H1.
xomega.
× intros.
unfold yield_condition in H3.
destruct H3 as (a & l´ & H4a & H4b & H4c).
inv H4a.
simpl in H4c.
inv H4c. }
×
destruct H1 as (_ & H1).
generalize (H1 H0); clear H1; intro H1.
destruct H7.
{ destruct H2.
assert (Hnewrsm: ZMap.get (proc_id (uRData l)) rsm_l = Available).
{ rewrite H2 in Hlessdef.
inversion Hlessdef; split; auto. }
set (rs´ := (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).
assert (Hnewrsm´: regset_lessdef rs´ rs´).
{ eapply regset_lessdef_refl; auto. }
∃ (ZMap.set (proc_id (uRData l)) (Running rs´) rsm_l).
set (m_l´ := mem_lift_nextblock m_l (Pos.to_nat (last_nb l)
- Pos.to_nat (Mem.nextblock m_l) % nat)).
∃ m_l´.
∃ dp_l.
refine_split.
-
apply plus_one.
exploit (eexec_step_external_yield_back ge rs´ rs0 m_l m_l´ (proc_id (uRData l)) rsm_l l
(LEvent (proc_id (uRData l)) LogYieldBack::l)
(last_nb l) dp_l d e); eauto.
-
inversion HMatch; substx.
constructor; simpl; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
× rewrite ?ZMap.gss.
constructor.
auto.
× rewrite ?ZMap.gso; auto.
+ unfold mem_block_conditions in *; simpl in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4).
apply mem_disjoint_union_commutativity in Hmem2.
refine_split´.
× apply mem_disjoint_union_commutativity.
rewrite H0.
rewrite H.
eapply mem_disjoint_union_lift_nextblock_left; auto.
× intros.
unfold active_condition in H4.
destruct H4.
{ destruct H4.
rewrite uRData_proc_id_eq in H4; simpl; auto.
elim Hdec.
auto. }
{ unfold yield_condition in H4.
destruct H4 as (a & l´ & H5a & H5b & H5c); inv H5a.
simpl in H5c.
inv H5c. }
× intros.
rewrite H0.
rewrite minus_diag.
assert (mem_lift_nextblock mother 0 = mother).
{ eapply mem_lift_nextblock_source_eq.
reflexivity. }
rewrite H6; auto.
× intros.
unfold yield_condition in H4.
destruct H4 as (a & l´ & H4a & H4b & H4c).
inv H4a.
simpl in H4c.
inv H4c. }
{ assert (Hnewrsm: ∃ rs_l,
ZMap.get (proc_id (uRData l)) rsm_l = Running rs_l ∧ regset_lessdef rs0 rs_l).
{ rewrite H2 in Hlessdef.
inv Hlessdef.
∃ rs´; auto. }
destruct Hnewrsm as (rs_l & Hnewrsm_a & Hnewrsm_b).
set (rs´ := (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs_l))
# EAX <- Vundef #PC <- (rs_l RA) #RA <- Vundef).
∃ (ZMap.set (proc_id (uRData l)) (Running rs´) rsm_l).
set (m_l´ := mem_lift_nextblock m_l (Pos.to_nat (last_nb l)
- Pos.to_nat (Mem.nextblock m_l) % nat)).
∃ m_l´.
∃ dp_l.
refine_split.
-
apply plus_one.
exploit (eexec_step_external_yield_back ge rs´ rs_l m_l m_l´ (proc_id (uRData l)) rsm_l l
(LEvent (proc_id (uRData l)) LogYieldBack::l)
(last_nb l) dp_l d e); eauto.
-
inversion HMatch; substx.
constructor; simpl; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
unfold total_machine_regset in ×.
case_eq (zeq i (proc_id (uRData l))).
× intros.
subst.
rewrite ZMap.gss.
esplit; eauto.
× intros.
rewrite ZMap.gso; auto.
+ intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
× rewrite ?ZMap.gss.
constructor.
auto.
regset_lessdef_solve_tac.
× rewrite ?ZMap.gso; auto.
+ unfold mem_block_conditions in *; simpl in ×.
destruct HMemRel as (HMemRel1 & HMemRel2 & HMemRel3 & HMemRel4).
apply mem_disjoint_union_commutativity in Hmem2.
refine_split´.
× apply mem_disjoint_union_commutativity.
rewrite H0.
rewrite H.
eapply mem_disjoint_union_lift_nextblock_left; auto.
× intros.
unfold active_condition in H3.
destruct H3.
{ destruct H3.
rewrite uRData_proc_id_eq in H3; simpl; auto.
elim Hdec.
auto. }
{ unfold yield_condition in H3.
destruct H3 as (a & l´ & H5a & H5b & H5c); inv H5a.
simpl in H5c.
inv H5c. }
× intros.
rewrite H0.
rewrite minus_diag.
assert (mem_lift_nextblock mother 0 = mother).
{ eapply mem_lift_nextblock_source_eq.
reflexivity. }
rewrite H5; auto.
× intros.
unfold yield_condition in H3.
destruct H3 as (a & l´ & H4a & H4b & H4c).
inv H4a.
simpl in H4c.
inv H4c. }
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)}.
Lemma init_state_total_machine_regset :
∀ i rsm (ph: AST.program fundef unit),
In i full_thread_list →
rsm = initial_map Environment (init_regset (Genv.globalenv ph)) full_thread_list →
total_machine_regset i rsm.
Proof.
induction full_thread_list; intros; try (inv H; fail).
simpl in H.
destruct H.
- simpl in H0; subst.
unfold total_machine_regset.
rewrite ZMap.gss.
unfold init_regset.
case_eq (decide (i = main_thread)); intros; subst.
+ esplit; left; auto.
+ ∃ (Pregmap.init Vundef); right; auto.
- case_eq (zeq i a); intros.
+ subst.
unfold total_machine_regset; subst; simpl.
rewrite ZMap.gss.
unfold init_regset.
case_eq (decide (a = main_thread)); intros; subst.
× esplit; left; auto.
× ∃ (Pregmap.init Vundef); right; auto.
+ simpl in H0.
subst.
unfold total_machine_regset.
rewrite ZMap.gso; auto.
unfold total_machine_regset in IHl; subst.
eapply IHl; eauto.
Qed.
Lemma init_state_regset_eq:
∀ i rsm (ph: AST.program fundef unit),
In i full_thread_list →
rsm = initial_map Environment (init_regset (Genv.globalenv ph)) full_thread_list →
ts_lessdef (ZMap.get i rsm) (ZMap.get i rsm).
Proof.
induction full_thread_list; intros; try (inv H; fail).
simpl in H.
destruct H.
- simpl in H0; subst.
rewrite ?ZMap.gss; auto.
unfold init_regset.
case_eq (decide (i = main_thread)).
+ intros; subst.
constructor.
apply regset_lessdef_refl.
+ intros.
constructor.
- subst; simpl; subst.
case_eq (decide (i = a)); intros; subst.
+ rewrite ?ZMap.gss; auto.
unfold init_regset.
case_eq (decide (a = main_thread)).
× intros; subst.
constructor.
apply regset_lessdef_refl.
× intros.
constructor.
+ rewrite ZMap.gso; auto.
exploit IHl; eauto.
Qed.
Lemma init_state_total_dproc:
∀ i dm,
In i full_thread_list →
dm = (initial_map None (fun i : Z ⇒ Some (thread_init_dproc i)) full_thread_list) →
ZMap.get i dm ≠ None.
Proof.
induction full_thread_list; intros; try (inv H; fail).
simpl in H.
destruct H.
- simpl in H0; subst.
rewrite ZMap.gss.
intro contra; inv contra.
- case_eq (zeq i a); intros.
+ subst; simpl; subst.
rewrite ZMap.gss.
intro contra; inv contra.
+ simpl in H0.
subst.
rewrite ZMap.gso; auto.
Qed.
Lemma init_state_dproc_eq:
∀ i dm,
In i full_thread_list →
dm = (initial_map None (fun i : Z ⇒ Some (thread_init_dproc i)) full_thread_list) →
ZMap.get i dm =ZMap.get i dm.
Proof.
induction full_thread_list; intros; try (inv H; fail).
simpl in H.
destruct H.
- simpl in H0; subst.
rewrite ?ZMap.gss; auto.
- case_eq (zeq i a); intros.
+ subst; simpl; subst.
rewrite ?ZMap.gss; auto.
+ simpl in H0.
subst.
rewrite ZMap.gso; auto.
Qed.
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
(IIEAsm.iesemantics (full_thread_list) ph)
(EAsm.esemantics (full_thread_list) ph).
Proof.
intros. apply forward_to_backward_simulation; eauto.
- eapply forward_simulation_plus
with (match_states:= match_iestate_estate (Genv.globalenv ph));
simpl; intros; trivial.
+
inv H.
refine_split.
econstructor; eauto.
assert (Hproc_id : proc_id (uRData nil) = main_thread).
{ apply null_log_proc_id. }
set (rsm´ := (initial_map Environment (init_regset (Genv.globalenv ph)) full_thread_list)).
set (dm´ := (initial_map None (fun i : Z ⇒ Some (thread_init_dproc i)) full_thread_list)).
assert (Hmem_nextblock: Mem.nextblock m0 = init_nb).
{
erewrite <- Genv.init_mem_genv_next; eauto.
rewrite <- Hs.
eapply make_globalenv_genv_next.
unfold make_globalenv.
setoid_rewrite Hmakep.
reflexivity.
}
assert (Hmem_other: mem_disjoint_union m0 m0 m0).
{ eapply init_mem_disjoint_union; eauto. }
constructor; eauto.
× intros.
unfold rsm.
eapply init_state_total_machine_regset; eauto.
× intros.
unfold rsm´.
eapply init_state_total_machine_regset; eauto.
× intros.
unfold rsm, rsm´.
eapply init_state_regset_eq; eauto.
× intros.
unfold dm.
eapply init_state_total_dproc; eauto.
× intros.
unfold dm´.
eapply init_state_total_dproc; eauto.
× unfold mem_block_conditions.
refine_split´; simpl; auto; intros; xomega.
+
destruct s2 as [curid_l rsm_l m_l d_l l_l].
destruct s1 as [curid_h rsm_h m_h d_h l_h].
destruct s1´ as [curid_h´ rsm_h´ m_h´ d_h´ l_h´]; inv H0.
edestruct one_step_Asm_E2E with (ge:=(Genv.globalenv ph))
(rsm_l := rsm_l)
(dp_l := d_l)
as (rsm_l´ & dp_l´ & Hl_step & Hl_match); eauto.
econstructor; eauto.
- apply ieasm_semantics_receptive; eauto.
- apply easm_semantics_determinate; eauto.
Qed.
End Link.