Library mcertikos.conlib.conmtlib.AsmIIE2IIE
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 IIEAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import ListLemma2.
Require Import FutureTactic.
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}.
Local Instance ec_ops : ExternalCallsOps (mwd (cdata PData))
:= CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance lcfg_ops : LayerConfigurationOps := compatlayer_configuration_ops L.
Definition total_machine_regset (i : Z) rsm :=
∃ rs, ZMap.get i rsm = Running rs ∨ ZMap.get i rsm = Available.
Section ListAppendNeqTac.
Lemma list_head_neq:
∀ {A: Type} l l´ (a: A),
l = a :: l´ ++ l → False.
Proof.
intros.
rewrite app_comm_cons in H.
eapply list_append_neq´ in H. inv H.
Qed.
Lemma list_append_e_or:
∀ {A : Type} l l1 l2 (e: A),
e :: l = l1 ++ l2 ++ l →
(l1 = nil ∧ l2 = e::nil) ∨ (l1 = e::nil ∧ l2 = nil).
Proof.
intros. destruct l1.
- left. destruct l2.
+ simpl in H. symmetry in H.
eapply list_append_neq0 in H. inv H.
+ inversion H. eapply list_append_neq´ in H2. subst. eauto.
- inversion H. right.
rewrite app_assoc in H2.
eapply list_append_neq´ in H2.
eapply app_eq_nil in H2. destruct H2 as (? & ?); subst. eauto.
Qed.
Lemma list_eq_bidirection:
∀ {A:Type} (l l´ l0 l1: list A),
l = l0 ++ l´ →
l´ = l1 ++ l →
l = l´.
Proof.
induction l; intros.
- destruct l´.
trivial. symmetry in H.
eapply list_not_e_nil in H. inv H.
- destruct l´.
+ symmetry in H0.
eapply list_not_e_nil in H0. inv H0.
+ destruct l0.
× inv H. trivial.
× inv H. destruct l1.
{
inversion H0.
eapply list_append_neq in H2. inv H2.
}
{
inversion H0.
replace (l1 ++ a1 :: l0 ++ a :: l´) with ((l1 ++ a1 :: l0) ++ a :: l´) in H2.
eapply list_append_neq in H2. inv H2.
rewrite <- app_assoc. rewrite app_comm_cons. trivial.
}
Qed.
Lemma list_contra: ∀ {A : Type} l (e : A),
e::l = l → False.
Proof.
induction l; intros.
inv H.
inversion H.
exploit (IHl a); auto.
Qed.
End ListAppendNeqTac.
Ltac list_append_neq_tac:=
match goal with
| H: ?l = _ ++ ?e :: ?l |- _ ⇒
eapply list_append_neq in H; inversion H
| H: ?l = ?e :: ?l |- _ ⇒
eapply list_append_neq0 in H; inversion H
| H: ?e :: ?l = ?l |- _ ⇒
symmetry in H; eapply list_append_neq0 in H; inversion H
| H: ?l = ?e :: _ ++ ?l |- _ ⇒
eapply list_head_neq in H; inversion H
| _ ⇒ idtac
end.
Section EF_Cond.
Lemma ef_id_imply_or:
∀ ef a b,
match ef with
| EF_external id _ ⇒
if peq id thread_yield
then False
else
if peq id thread_sleep
then False
else (a id)
| _ ⇒ b
end →
b \/(∃ id sg, ef = EF_external id sg ∧ (a id)).
Proof.
intros. destruct ef; auto.
right. refine_split´; trivial.
destruct (peq name thread_yield). inv H.
destruct (peq name thread_sleep); trivial. inv H.
Qed.
End EF_Cond.
Section STAR_PROP.
Variable step_prop: genv → (iestate (mem:= mem)) → trace → (iestate (mem:=mem)) → Prop.
Hypothesis one_step_prop:
∀ ge s1 t s2,
iestep ge s1 t s2 →
step_prop ge s1 t s2.
Hypothesis prop_refl:
∀ ge s,
step_prop ge s E0 s.
Hypothesis prop_trans:
∀ ge s0 t0 s1 t1 s2 t2,
step_prop ge s0 t0 s1 →
step_prop ge s1 t1 s2 →
t2 = (t0 ** t1) →
step_prop ge s0 t2 s2.
Lemma star_step_prop:
∀ ge s1 t s2,
star iestep ge s1 t s2 →
step_prop ge s1 t s2.
Proof.
induction 1; eauto.
Qed.
End STAR_PROP.
Section STAR_INCR.
Lemma one_step_event:
∀ ge curid curid´ rsm rsm´ mp mp´ dp dp´ l l´ t,
iestep ge (IEState curid rsm mp dp l) t (IEState curid´ rsm´ mp´ dp´ l´) →
l´ = l ∨ (∃ e, l´ = e :: l).
Proof.
intros. inv H; try apply list_append_nil; eauto.
- eapply ef_id_imply_or in NON_YIELD.
destruct NON_YIELD as [HT | HT]; subst.
+ left; trivial.
+ destruct HT as (id & sg & _ & Hl); subst.
destruct (has_event id).
× right.
destruct Hl as (largs & choice & Hla & Hlb & Hlc).
subst; eauto.
× subst; left; trivial.
- eapply ef_id_imply_or in NON_YIELD.
destruct NON_YIELD as [HT | HT]; subst.
+ left; trivial.
+ destruct HT as (id & sg & _ & Hl); subst.
destruct (has_event id).
× right. eauto.
× subst. left; trivial.
Qed.
Definition P_INCR (ge: genv) (s: iestate (mem:= mem)) (t: trace) (s´: iestate (mem:= mem)):=
∀ rsm rsm´ curid curid´ mp mp´ dp dp´ l l´,
s = IEState curid rsm mp dp l →
s´ = IEState curid´ rsm´ mp´ dp´ l´ →
∃ l0, l´ = l0 ++ l.
Lemma one_step_log_incr:
∀ ge cid cid´ rsm rsm´ mp mp´ dp dp´ l l´ t,
iestep ge (IEState cid rsm mp dp l) t (IEState cid´ rsm´ mp´ dp´ l´) →
∃ l0, l´ = l0 ++ l.
Proof.
intros. eapply one_step_event in H.
destruct H as [HT | HT].
- subst. ∃ nil. rewrite app_nil_l; trivial.
- destruct HT as (e & HT); subst. ∃ (e:: nil). eauto.
Qed.
Lemma star_step_log_incr´:
∀ ge s t s´,
star iestep ge s t s´ →
P_INCR ge s t s´.
Proof.
intros.
eapply star_step_prop; eauto; unfold P_INCR; intros; subst.
-
eapply one_step_log_incr; eauto.
-
inv H1. ∃ nil; trivial.
-
destruct s1.
exploit H0; eauto; clear H0.
intros (l1 & Hl1).
exploit H1; eauto; clear H1.
intros (l2 & Hl2). subst.
∃ (l2 ++ l1).
rewrite app_assoc. trivial.
Qed.
Lemma star_step_log_incr:
∀ ge cid cid´ rsm rsm´ mp mp´ dp dp´ l l´ t,
star iestep ge (IEState cid rsm mp dp l) t (IEState cid´ rsm´ mp´ dp´ l´) →
∃ l0, l´ = l0 ++ l.
Proof.
intros.
eapply star_step_log_incr´; eauto.
Qed.
End STAR_INCR.
Section STAR_LOG.
Definition P_LOG (ge: genv) (s: iestate (mem:= mem)) (t: trace) (s´: iestate (mem:= mem)):=
∀ rsm rsm´ curid curid´ mp mp´ dp dp´ l,
s = IEState curid rsm mp dp l →
s´ = IEState curid´ rsm´ mp´ dp´ l →
curid´ = curid.
Lemma one_step_log_same:
∀ ge curid curid´ rsm rsm´ m m´ dp dp´ l t,
iestep ge (IEState curid rsm m dp l) t
(IEState curid´ rsm´ m´ dp´ l) →
curid´ = curid.
Proof.
intros. inversion H; try reflexivity; list_append_neq_tac.
Qed.
Lemma one_step_log_same´:
∀ ge s t s´,
iestep ge s t s´ →
P_LOG ge s t s´.
Proof.
unfold P_LOG; intros. subst.
eapply one_step_log_same; eauto.
Qed.
Lemma star_step_log_same´:
∀ ge s t s´,
star iestep ge s t s´ →
P_LOG ge s t s´.
Proof.
induction 1.
- unfold P_LOG. intros; subst. inv H0. eauto.
- pose proof H as Hone.
eapply one_step_log_same´ in Hone; eauto.
unfold P_LOG in ×.
intros; subst.
destruct s2.
eapply star_step_log_incr in H0.
eapply one_step_log_incr in H.
destruct H0 as (? & Hl1).
destruct H as (? & Hl2).
exploit (list_eq_bidirection (A:= LogEvent)); eauto.
clear Hl1 Hl2.
intros; subst.
exploit Hone; eauto.
intros; subst.
exploit IHstar; eauto.
Qed.
Lemma star_step_log_same:
∀ ge curid curid´ rsm rsm´ mp mp´ dp dp´ l t,
star iestep ge (IEState curid rsm mp dp l) t
(IEState curid´ rsm´ mp´ dp´ l) →
curid´ = curid.
Proof.
intros. eapply star_step_log_same´; eauto.
Qed.
End STAR_LOG.
Section STAR_SPLIT.
Definition P_SPLIT (ge: genv) (s: iestate (mem:= mem)) (t: trace) (s´: iestate (mem:= mem)):=
∀ rsm rsm´ curid curid´ mp mp´ dp dp´ l e,
s = IEState curid rsm mp dp l →
s´ = IEState curid´ rsm´ mp´ dp´ (e :: l) →
∃ t0 t1 t2 rsm0 mp0 dp0 rsm1 mp1 dp1,
star iestep ge (IEState curid rsm mp dp l) t0 (IEState curid rsm0 mp0 dp0 l)
∧ iestep ge (IEState curid rsm0 mp0 dp0 l) t1 (IEState curid´ rsm1 mp1 dp1 (e :: l))
∧ star iestep ge (IEState curid´ rsm1 mp1 dp1 (e :: l)) t2 (IEState curid´ rsm´ mp´ dp´ (e :: l))
∧ t0 ** t1 ** t2 = t.
Lemma one_log_append_split´´:
∀ ge curid curid´ rsm rsm´ mp mp´ dp dp´ l e t,
iestep ge (IEState curid rsm mp dp l) t
(IEState curid´ rsm´ mp´ dp´ (e :: l)) →
∃ t0 t1 t2 rsm0 mp0 dp0 rsm1 mp1 dp1,
star iestep ge (IEState curid rsm mp dp l) t0 (IEState curid rsm0 mp0 dp0 l)
∧ iestep ge (IEState curid rsm0 mp0 dp0 l) t1 (IEState curid´ rsm1 mp1 dp1 (e :: l))
∧ star iestep ge (IEState curid´ rsm1 mp1 dp1 (e :: l)) t2 (IEState curid´ rsm´ mp´ dp´ (e :: l))
∧ t0 ** t1 ** t2 = t.
Proof.
intros.
refine_split´; eauto.
- eapply star_refl.
- eapply star_refl.
- rewrite E0_left. rewrite E0_right. reflexivity.
Qed.
Lemma one_log_append_split:
∀ ge curid curid´ rsm rsm´ mp mp´ dp dp´ l e,
iestep ge (IEState curid rsm mp dp l) E0
(IEState curid´ rsm´ mp´ dp´ (e :: l)) →
∃ rsm0 mp0 dp0 rsm1 mp1 dp1,
star iestep ge (IEState curid rsm mp dp l) E0 (IEState curid rsm0 mp0 dp0 l)
∧ iestep ge (IEState curid rsm0 mp0 dp0 l) E0 (IEState curid´ rsm1 mp1 dp1 (e :: l))
∧ star iestep ge (IEState curid´ rsm1 mp1 dp1 (e :: l)) E0 (IEState curid´ rsm´ mp´ dp´ (e :: l)).
Proof.
intros.
eapply one_log_append_split´´ in H.
destruct H as (t0 & t3 & t4 & rsm1 & m2 & dp1 & rsm2 & m3 & dp2 & Hstar1 & Hone1 & Hstar2 & Htrace).
apply Eapp_E0_inv in Htrace.
destruct Htrace as (? & Htrace); subst.
apply Eapp_E0_inv in Htrace.
destruct Htrace as (? & ?); subst.
refine_split´; eauto.
Qed.
Lemma one_log_append_split´:
∀ ge s t s´,
iestep ge s t s´ →
P_SPLIT ge s t s´.
Proof.
unfold P_SPLIT; intros; subst.
eapply one_log_append_split´´; eauto.
Qed.
Lemma star_log_append_split´:
∀ ge s t s´,
star iestep ge s t s´ →
P_SPLIT ge s t s´.
Proof.
induction 1.
- unfold P_SPLIT. intros; subst. inversion H0.
list_append_neq_tac.
- pose proof H as Hone.
pose proof H as Hone´.
pose proof H0 as Hstar.
eapply one_log_append_split´ in Hone´; eauto.
unfold P_SPLIT in ×.
intros; subst.
destruct s2.
eapply star_step_log_incr in H0.
eapply one_step_log_incr in H.
destruct H0 as (l1 & Hl).
destruct H as (l2 & Hl2). subst.
eapply list_append_e_or in Hl.
destruct Hl as [(Hl2 & Hl1)| (Hl2 & Hl1)]; subst.
+ clear IHstar.
simpl in ×.
edestruct Hone´ as (t0´ & t3 & t4 & rsm1 & m2 & dp1 & rsm2 & m3 & dp2 & Hstar1 & Hone1 & Hstar2 & Htrace); eauto.
clear Hone´ Hone. subst.
exploit (star_step_log_same ge z curid´); eauto.
intros; subst.
refine_split´; eauto.
× eapply star_trans; eauto.
× repeat rewrite Eapp_assoc. trivial.
+ clear Hone´.
simpl in ×.
edestruct IHstar as (t0´ & t3 & t4 & rsm1 & m2 & dp1 & rsm2 & m3 & dp2 & Hstar1 & Hone1 & Hstar2 & Htrace); eauto.
exploit one_step_log_same; eauto.
intros; subst.
refine_split´; eauto.
× eapply star_left; eauto.
× rewrite Eapp_assoc. trivial.
Qed.
Lemma star_log_append_split:
∀ ge curid curid´ rsm rsm´ mp mp´ dp dp´ l e,
star iestep ge (IEState curid rsm mp dp l) E0
(IEState curid´ rsm´ mp´ dp´ (e :: l)) →
∃ rsm0 mp0 dp0 rsm1 mp1 dp1,
star iestep ge (IEState curid rsm mp dp l) E0 (IEState curid rsm0 mp0 dp0 l)
∧ iestep ge (IEState curid rsm0 mp0 dp0 l) E0 (IEState curid´ rsm1 mp1 dp1 (e :: l))
∧ star iestep ge (IEState curid´ rsm1 mp1 dp1 (e :: l)) E0 (IEState curid´ rsm´ mp´ dp´ (e :: l)).
Proof.
intros. exploit star_log_append_split´; eauto.
intros (t0 & t3 & t4 & rsm1 & m2 & dp1 & rsm2 & m3 & dp2 & Hstar1 & Hone1 & Hstar2 & Htrace).
apply Eapp_E0_inv in Htrace.
destruct Htrace as (? & Htrace); subst.
apply Eapp_E0_inv in Htrace.
destruct Htrace as (? & ?); subst.
refine_split´; eauto.
Qed.
End STAR_SPLIT.
Ltac regset_preserve_tac i l :=
unfold total_machine_regset in *;
case_eq (zeq i (proc_id (uRData l))); intros; subst; [rewrite ZMap.gss | rewrite ZMap.gso; auto];
eexists; left; auto.
Ltac dproc_preserve_tac i l :=
case_eq (zeq i (proc_id (uRData l))); intros; subst;
[rewrite ZMap.gss; intro contra; inv contra
| rewrite ZMap.gso; auto].
Section SILENT_STAR_PRESERVE.
Definition P_PRESERVE (s: iestate (mem:= mem)) (s´: iestate (mem:= mem)):=
∀ rsm rsm´ curid curid´ mp mp´ dp dp´ l,
s = IEState curid rsm mp dp l →
s´ = IEState curid´ rsm´ mp´ dp´ l →
curid = curid´ ∧
(∀ i, i ≠ curid →
ZMap.get i rsm = ZMap.get i rsm´ ∧
ZMap.get i dp = ZMap.get i dp´) ∧
(∀ i, total_machine_regset i rsm → total_machine_regset i rsm´) ∧
(∀ i, ZMap.get i dp ≠ None → ZMap.get i dp´ ≠ None) ∧
((curid ≠ current_thread → (fst mp) = (fst mp´)) ∧
(curid = current_thread → (snd mp) = (snd mp´))).
Lemma one_step_preserve:
∀ ge st t st´,
iestep ge st t st´ →
P_PRESERVE st st´.
Proof.
unfold P_PRESERVE.
intros.
inversion H; substx; try reflexivity;
match goal with
| H: IEState _ _ _ _ _ = IEState _ _ _ _ _ |- _ ⇒ inversion H; substx; clear H
end;
match goal with
| H: IEState _ _ _ _ _ = IEState _ _ _ _ _ |- _ ⇒ inversion H; substx; clear H
end;
try list_append_neq_tac;
try refine_split; auto; intros;
intros; try (rewrite ?ZMap.gso; auto; fail);
try (regset_preserve_tac i l; fail); try (dproc_preserve_tac i l; fail);
try (case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; [elim H0; auto |];
rewrite H1 in MOrigin, MUpdate; inv MOrigin; simpl; auto; fail);
try (case_eq (decide (proc_id (uRData l) = current_thread)); intros; subst; [ | elim n; auto];
rewrite H1 in MOrigin, MUpdate; inv MOrigin; simpl; auto; fail).
- regset_preserve_tac i0 l.
- dproc_preserve_tac i0 l.
Qed.
Lemma star_step_preserve´:
∀ ge s t s´,
star iestep ge s t s´ →
P_PRESERVE s s´.
Proof.
induction 1.
- unfold P_PRESERVE.
intros; subst.
inv H0.
refine_split; intros; auto.
- pose proof H as Hone.
eapply one_step_preserve in Hone; eauto.
unfold P_PRESERVE in ×.
intros; subst.
destruct s2.
eapply star_step_log_incr in H0.
eapply one_step_log_incr in H.
destruct H0 as (? & Hl1).
destruct H as (? & Hl2).
exploit (list_eq_bidirection (A:= LogEvent)); eauto.
clear Hl1 Hl2.
intros; subst.
exploit Hone; eauto.
intros.
destruct H as (Ha & Hb & Hc & Hd & He).
exploit IHstar; eauto.
intros.
destruct H as (Ha´ & Hb´ & Hc´ & Hd´ & He´).
subst.
refine_split; intros; try reflexivity.
+ generalize (Hb i H).
intros Htemp.
destruct Htemp as (Hba & Hbb).
generalize (Hb´ i H).
intros Htemp.
destruct Htemp as (Hba´ & Hbb´).
rewrite Hba, Hbb; auto.
+ generalize (Hc i H); intros H´.
generalize (Hc´ i H´); auto.
+ generalize (Hd i H); intros H´.
generalize (Hd´ i H´); auto.
+ destruct He; destruct He´.
generalize (H2 H).
generalize (H0 H).
intros; congruence.
+ destruct He; destruct He´.
generalize (H3 H).
generalize (H1 H).
intros; congruence.
Qed.
Lemma star_step_preserve:
∀ ge curid curid´ rsm rsm´ mp mp´ dp dp´ l t,
star iestep ge (IEState curid rsm mp dp l) t
(IEState curid´ rsm´ mp´ dp´ l) →
curid = curid´ ∧
(∀ i, i ≠ curid → ZMap.get i rsm = ZMap.get i rsm´ ∧
ZMap.get i dp = ZMap.get i dp´) ∧
(∀ i, total_machine_regset i rsm → total_machine_regset i rsm´) ∧
(∀ i, ZMap.get i dp ≠ None → ZMap.get i dp´ ≠ None) ∧
((curid ≠ current_thread → (fst mp) = (fst mp´)) ∧
(curid = current_thread → (snd mp) = (snd mp´))).
Proof.
intros. eapply star_step_preserve´; eauto.
Qed.
End SILENT_STAR_PRESERVE.
Section NON_YIELD_LOG_PRESERVE.
Lemma non_yield_log_preserve:
∀ ge rsm rsm´ curid curid´ mp mp´ t dp dp´ l l´ ev,
iestep ge (IEState curid rsm mp dp l) t (IEState curid´ rsm´ mp´ dp´ l´) →
l´ = ev::l →
lastEvType l´ ≠ Some LogYieldTy →
curid = curid´ ∧
(∀ i, i ≠ curid → ZMap.get i rsm = ZMap.get i rsm´ ∧
ZMap.get i dp = ZMap.get i dp´) ∧
(∀ i, total_machine_regset i rsm → total_machine_regset i rsm´) ∧
(∀ i, ZMap.get i dp ≠ None → ZMap.get i dp´ ≠ None) ∧
((curid ≠ current_thread → (fst mp) = (fst mp´)) ∧
(curid = current_thread → (snd mp) = (snd mp´))).
Proof.
intros.
inversion H.
- rewrite H13 in H0.
symmetry in H0.
eapply list_contra in H0; inversion H0.
- rewrite H13 in H0.
symmetry in H0.
eapply list_contra in H0; inversion H0.
- rewrite H13 in H0.
symmetry in H0.
eapply list_contra in H0; inversion H0.
- subdestruct; try (inversion NON_YIELD; fail);
try (rewrite NON_YIELD in H0;
symmetry in H0;
eapply list_contra in H0; inversion H0).
+ substx.
refine_split; auto; intros.
× rewrite ?ZMap.gso; auto.
× unfold total_machine_regset in *;
case_eq (zeq i current_thread); intros; subst; [rewrite ZMap.gss | rewrite ZMap.gso; auto].
eexists; left; auto.
× case_eq (zeq i current_thread); intros; subst; [rewrite ZMap.gss; intro contra; inv contra
| rewrite ZMap.gso; auto].
× elim H0; auto.
+ substx.
refine_split; auto; intros.
× rewrite ?ZMap.gso; auto.
× unfold total_machine_regset in *;
case_eq (zeq i (proc_id (uRData l))); intros; subst; [rewrite ZMap.gss |
rewrite ZMap.gso; auto].
eexists; left; auto.
× case_eq (zeq i (proc_id (uRData l))); intros; subst; [rewrite ZMap.gss; intro contra; inv contra
| rewrite ZMap.gso; auto].
× elim n; auto.
- subdestruct; try (inversion NON_YIELD; fail);
try (rewrite NON_YIELD in H0;
symmetry in H0;
eapply list_contra in H0; inversion H0).
+ substx.
refine_split; auto; intros.
× rewrite ?ZMap.gso; auto.
× unfold total_machine_regset in *;
case_eq (zeq i current_thread); intros; subst; [rewrite ZMap.gss | rewrite ZMap.gso; auto].
eexists; left; auto.
× case_eq (zeq i current_thread); intros; subst; [rewrite ZMap.gss; intro contra; inv contra
| rewrite ZMap.gso; auto].
× elim H0; auto.
+ substx.
refine_split; auto; intros.
× rewrite ?ZMap.gso; auto.
× unfold total_machine_regset in *;
case_eq (zeq i (proc_id (uRData l))); intros; subst; [rewrite ZMap.gss |
rewrite ZMap.gso; auto].
eexists; left; auto.
× case_eq (zeq i (proc_id (uRData l))); intros; subst; [rewrite ZMap.gss; intro contra; inv contra
| rewrite ZMap.gso; auto].
× elim n; auto.
- rewrite H19 in H1.
elim H1.
unfold lastEvType; simpl; auto.
- rewrite H19 in H1.
elim H1.
unfold lastEvType; simpl; auto.
- substx.
inv H16.
remember (Single_Oracle l) as ev.
clear Heqev.
destruct ev; eauto.
destruct l0; try auto.
+ unfold lastEvType in H1; simpl in H1; elim H1; auto.
+ unfold lastEvType in H1; simpl in H1; elim H1; auto.
+ rewrite uRData_proc_id_eq; simpl; auto.
split; auto.
+ rewrite uRData_proc_id_eq; simpl; auto.
split; auto.
- substx.
inv H17.
subdestruct.
+ destruct mp, mp´; simpl in *; subst; inv MUpdate.
refine_split´; intros; auto.
× rewrite ?ZMap.gso; auto.
× unfold total_machine_regset in *;
case_eq (zeq i (proc_id (uRData l))); intros; subst; [rewrite ZMap.gss |
rewrite ZMap.gso; auto].
eexists; left; auto.
× rewrite e0 in H0.
elim H0; auto.
+ destruct mp, mp´; simpl in *; subst; inv MUpdate.
refine_split´; intros; auto.
× rewrite ?ZMap.gso; auto.
× unfold total_machine_regset in *;
case_eq (zeq i (proc_id (uRData l))); intros; subst; [rewrite ZMap.gss |
rewrite ZMap.gso; auto].
eexists; left; auto.
× elim n; auto.
Qed.
End NON_YIELD_LOG_PRESERVE.
Section YIELD_LOG_PRESERVE.
Lemma yield_log_preserve:
∀ ge rsm rsm´ curid curid´ mp mp´ t dp dp´ l l´ ev,
iestep ge (IEState curid rsm mp dp l) t (IEState curid´ rsm´ mp´ dp´ l´) →
l´ = ev::l →
lastEvType l´ = Some LogYieldTy →
(rsm = rsm´ ∧ mp = mp´ ∧ dp = dp´).
Proof.
intros.
inversion H.
- rewrite H13 in H0.
symmetry in H0.
eapply list_contra in H0; inversion H0.
- rewrite H13 in H0.
symmetry in H0.
eapply list_contra in H0; inversion H0.
- rewrite H13 in H0.
symmetry in H0.
eapply list_contra in H0; inversion H0.
- subdestruct; try (inversion NON_YIELD; fail);
try (rewrite NON_YIELD in H0;
symmetry in H0;
eapply list_contra in H0; inversion H0).
+ substx.
destruct NON_YIELD as (? & ? & ? & ? & ?).
inv H3.
unfold lastEvType in H1; simpl in H1; inv H1.
+ substx.
destruct NON_YIELD as (? & ? & ? & ? & ?).
inv H3.
unfold lastEvType in H1; simpl in H1; inv H1.
- subdestruct; try (inversion NON_YIELD; fail);
try (rewrite NON_YIELD in H0;
symmetry in H0;
eapply list_contra in H0; inversion H0).
+ substx; inv NON_YIELD.
unfold lastEvType in H1; simpl in H1; inv H1.
+ substx; inv NON_YIELD.
unfold lastEvType in H1; simpl in H1; inv H1.
- substx.
refine_split´; intros; auto.
- substx.
refine_split´; intros; auto.
- substx.
inv H16; auto.
- substx.
inv H17.
unfold lastEvType in H1; simpl in H1.
inv H1.
Qed.
End YIELD_LOG_PRESERVE.
Inductive match_iestate_state (ge : genv) : (iestate (mem := mem)) →
(iestate (mem := mem)) → Prop :=
| MATCH_IESTATE_STATE:
∀ curid rsm_h rsm_l (dp_h dp_l : ZMap.t (option dproc)) mp_h mp_l l
(HCurID : proc_id (uRData l) = curid)
(HRsmDom1: ∀ i, In i full_thread_list → i ≠ current_thread →
ZMap.get i rsm_h = Environment)
(HRsmDom2: ZMap.get current_thread rsm_h ≠ Environment)
(HRsmDom3 : ∀ i, In i full_thread_list → total_machine_regset i rsm_l)
(HRsmRel: (ZMap.get current_thread rsm_h) = (ZMap.get current_thread rsm_l))
(HDprocDom1: ∀ i, In i full_thread_list → i ≠ current_thread →
ZMap.get i dp_h = None)
(HDprocDom2: ZMap.get current_thread dp_h ≠ None)
(HDprocDom3: ∀ i, In i full_thread_list → ZMap.get i dp_l ≠ None)
(HDprocRel: ZMap.get current_thread dp_h = ZMap.get current_thread dp_l)
(HMemRel: fst mp_h = fst mp_l),
match_iestate_state ge (IEState curid rsm_h mp_h dp_h l) (IEState curid rsm_l mp_l dp_l l).
Class IE2IERel :=
{
env_step_match:
∀ (ge: genv) (mp_h mp_l: (mem × mem)) (curid curid´: Z)
(rsm_h rsm_l : ZMap.t EAsmCommon.ThreadState) dp_h dp_l (l l´ : Log)
(Hrsm: ZMap.get curid rsm_h = Environment)
(Hdproc: ZMap.get curid dp_h = None)
(Hcurid1: proc_id (uRData l) = curid)
(Hquery: l´ = (Single_Oracle l)::l)
(Hcurid2: proc_id (uRData l´) = curid´)
(HMatch: match_iestate_state ge (IEState curid rsm_h mp_h dp_h l)
(IEState curid rsm_l mp_l dp_l l)),
∃ rsm_l´ mp_l´ dp_l´ t,
(star IIEAsm.iestep) ge (IEState curid rsm_l mp_l dp_l l) t (IEState curid´ rsm_l´ mp_l´ dp_l´ l´);
function_call_cond:
∀ ef, match ef with
| EF_vload _ ⇒ False
| EF_vstore _ ⇒ False
| EF_vload_global _ _ _ ⇒ False
| EF_vstore_global _ _ _ ⇒ False
| EF_annot _ _ ⇒ False
| EF_annot_val _ _ ⇒ False
| _ ⇒ True
end
}.
Context `{ie2ie_rel: IE2IERel}.
Section NO_TRACE.
Lemma single_step_no_trace:
∀ ge st t st´, IIEAsm.iestep ge st t st´ → t = E0.
Proof.
intros.
inv H; auto.
- generalize (function_call_cond ef); eauto; intros.
destruct ef; try (inv H; fail); try (inv BUILTIN_ENABLED);
(inv H6; inv H2; auto; inv H1; auto).
- generalize (function_call_cond ef); eauto; intros.
destruct ef; try (inv H; fail); try (inv BUILTIN_ENABLED);
(inv H7; inv H2; inv H1; auto).
- generalize (function_call_cond ef); eauto; intros.
destruct ef; try (inv H; fail); try (inv NON_YIELD);
try (inv H6; inv H2; auto; inv H1; auto; fail).
+ inv H6.
inv H2.
inv H1.
inv H2.
destruct H6 as (? &? & ? & ? & ? & ? & ?); auto.
- destruct ef; try (inv NON_YIELD);
try (inv H5;
destruct H as (? & ? & ? & ? & ?);
inv H5; auto; fail).
Qed.
Lemma star_step_no_trace:
∀ ge st t st´, (star IIEAsm.iestep) ge st t st´ → t = E0.
Proof.
induction 1; intros; subst.
- auto.
- eapply single_step_no_trace in H; subst.
auto.
Qed.
End NO_TRACE.
Theorem one_step_Asm_E2E:
∀ ge curid curid´ mp_h mp_h´ mp_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_state ge (IEState curid rsm_h mp_h dp_h l) (IEState curid rsm_l mp_l dp_l l)),
∃ rsm_l´ mp_l´ dp_l´,
(plus IIEAsm.iestep) ge (IEState curid rsm_l mp_l dp_l l) t (IEState curid´ rsm_l´ mp_l´ dp_l´ l´)
∧ match_iestate_state ge (IEState curid´ rsm_h´ mp_h´ dp_h´ l´) (IEState curid´ rsm_l´ mp_l´ dp_l´ l´).
Proof.
intros.
inv HEStep.
-
rename l´ into l.
assert (Hcurid: proc_id (uRData l) = current_thread).
{ inv HMatch.
case_eq (zeq (proc_id (uRData l)) current_thread); intros; subst; auto.
clear H; eapply HRsmDom1 in n.
- rewrite n in H8; inv H8.
- apply all_cid_in_full_thread_list. }
assert (Hcond: ZMap.get (proc_id (uRData l)) rsm_l = Running rs ∧
fst mp_l = fst mp_h ∧
ZMap.get (proc_id (uRData l)) dp_l = Some d).
{ inv HMatch.
rewrite Hcurid in ×.
rewrite <- HRsmRel, <- HDprocRel; auto. }
destruct Hcond as (Hcond1 & Hcond2 & Hcond3).
destruct mp_h, mp_l, mp_h´; simpl in ×.
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; [ | elim Hdec; auto].
rewrite Hdec´ in MUpdate, MOrigin; inv MOrigin; inv MUpdate.
refine_split´.
+
eapply plus_one.
eapply ieexec_step_internal; eauto.
× rewrite Hdec´; simpl; eauto.
× rewrite Hdec´; simpl; eauto.
+
inv HMatch; constructor; intros; try auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss.
intros contra; inv contra.
× unfold total_machine_regset in ×.
rewrite Hcurid.
case_eq (zeq i0 current_thread).
{ intros; subst.
∃ rs´; left; rewrite ZMap.gss; auto. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; constructor; auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss; intros contra; inv contra.
× rewrite Hcurid.
case_eq (zeq i0 current_thread).
{ intros; subst.
rewrite ZMap.gss; intros contra; inv contra. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; auto.
-
rename l´ into l.
assert (Hcurid: proc_id (uRData l) = current_thread).
{ inv HMatch.
case_eq (zeq (proc_id (uRData l)) current_thread); intros; subst; auto.
clear H; eapply HRsmDom1 in n.
- rewrite n in H9; inv H9.
- apply all_cid_in_full_thread_list. }
assert (Hcond: ZMap.get (proc_id (uRData l)) rsm_l = Running rs ∧
fst mp_l = fst mp_h ∧
ZMap.get (proc_id (uRData l)) dp_l = Some d).
{ inv HMatch.
rewrite Hcurid in ×.
rewrite <- HRsmRel, <- HDprocRel; auto. }
destruct Hcond as (Hcond1 & Hcond2 & Hcond3).
destruct mp_h, mp_l, mp_h´; simpl in ×.
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; [ | elim Hdec; auto].
rewrite Hdec´ in MUpdate, MOrigin; inv MOrigin; inv MUpdate.
refine_split´.
+
eapply plus_one.
eapply ieexec_step_builtin; eauto.
× rewrite Hdec´; simpl; eauto.
× rewrite Hdec´; simpl; eauto.
+
inv HMatch; constructor; intros; try auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss.
intros contra; inv contra.
× unfold total_machine_regset in ×.
rewrite Hcurid.
case_eq (zeq i current_thread).
{ intros; subst.
eexists; left; rewrite ZMap.gss; auto. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; constructor; auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss; intros contra; inv contra.
× rewrite Hcurid.
case_eq (zeq i current_thread).
{ intros; subst.
rewrite ZMap.gss; intros contra; inv contra. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; auto.
-
rename l´ into l.
assert (Hcurid: proc_id (uRData l) = current_thread).
{ inv HMatch.
case_eq (zeq (proc_id (uRData l)) current_thread); intros; subst; auto.
clear H; eapply HRsmDom1 in n.
- rewrite n in H9; inv H9.
- apply all_cid_in_full_thread_list. }
assert (Hcond: ZMap.get (proc_id (uRData l)) rsm_l = Running rs ∧
fst mp_l = fst mp_h ∧
ZMap.get (proc_id (uRData l)) dp_l = Some d).
{ inv HMatch.
rewrite Hcurid in ×.
rewrite <- HRsmRel, <- HDprocRel; auto. }
destruct Hcond as (Hcond1 & Hcond2 & Hcond3).
destruct mp_h, mp_l, mp_h´; simpl in ×.
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; [ | elim Hdec; auto].
rewrite Hdec´ in MUpdate, MOrigin; inv MOrigin; inv MUpdate.
refine_split´.
+
eapply plus_one.
eapply ieexec_step_annot; eauto.
× rewrite Hdec´; simpl; eauto.
× rewrite Hdec´; simpl; eauto.
+
inv HMatch; constructor; intros; try auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss.
intros contra; inv contra.
× unfold total_machine_regset in ×.
rewrite Hcurid.
case_eq (zeq i current_thread).
{ intros; subst.
eexists; left; rewrite ZMap.gss; auto. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; constructor; auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss; intros contra; inv contra.
× rewrite Hcurid.
case_eq (zeq i current_thread).
{ intros; subst.
rewrite ZMap.gss; intros contra; inv contra. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; auto.
-
assert (Hproc_id_same: proc_id (uRData l) = proc_id (uRData l´)).
{ destruct ef; try (subst; auto).
clear MOrigin MUpdate.
subdestruct.
- contradiction.
- contradiction.
- destruct NON_YIELD as (largs & choice & Ha & Hb & Hc); subst.
symmetry.
eapply uRData_proc_id_eq.
simpl; auto.
- subst; auto. }
assert (Hcurid: proc_id (uRData l) = current_thread ∧ proc_id (uRData l´) = current_thread).
{ inv HMatch.
case_eq (zeq (proc_id (uRData l)) current_thread); intros; subst; auto.
- split; auto.
rewrite <- Hproc_id_same.
auto.
- clear H.
eapply HRsmDom1 in n.
rewrite n in H9.
inv H9.
apply all_cid_in_full_thread_list. }
destruct Hcurid as (Hcurid & Hcurid´).
assert (Hcond: ZMap.get (proc_id (uRData l)) rsm_l = Running rs ∧
fst mp_l = fst mp_h ∧
ZMap.get (proc_id (uRData l)) dp_l = Some d).
{ inv HMatch.
rewrite Hcurid in ×.
rewrite <- HRsmRel, <- HDprocRel; auto. }
destruct Hcond as (Hcond1 & Hcond2 & Hcond3).
destruct mp_h, mp_l, mp_h´; simpl in ×.
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; [ | elim Hdec; auto].
rewrite Hdec´ in MUpdate, MOrigin; inv MOrigin; inv MUpdate.
refine_split´.
+
eapply plus_one.
eapply ieexec_step_external; eauto.
× rewrite Hdec´; simpl; eauto.
× rewrite Hdec´; simpl; eauto.
+
inv HMatch; constructor; intros; try auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss.
intros contra; inv contra.
× unfold total_machine_regset in ×.
rewrite Hcurid.
case_eq (zeq i current_thread).
{ intros; subst.
eexists; left; rewrite ZMap.gss; auto. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; constructor; auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss; intros contra; inv contra.
× rewrite Hcurid.
case_eq (zeq i current_thread).
{ intros; subst.
rewrite ZMap.gss; intros contra; inv contra. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; auto.
-
assert (Hproc_id_same: proc_id (uRData l) = proc_id (uRData l´)).
{ destruct ef; try (subst; auto).
clear MOrigin MUpdate.
subdestruct.
- contradiction.
- contradiction.
- subst.
symmetry.
eapply uRData_proc_id_eq.
simpl; auto.
- subst; auto. }
assert (Hcurid: proc_id (uRData l) = current_thread ∧ proc_id (uRData l´) = current_thread).
{ inv HMatch.
case_eq (zeq (proc_id (uRData l)) current_thread); intros; subst; auto.
- split; auto.
rewrite <- Hproc_id_same.
auto.
- clear H.
eapply HRsmDom1 in n.
rewrite n in H7.
inv H7.
apply all_cid_in_full_thread_list. }
destruct Hcurid as (Hcurid & Hcurid´).
assert (Hcond: ZMap.get (proc_id (uRData l)) rsm_l = Running rs ∧
fst mp_l = fst mp_h ∧
ZMap.get (proc_id (uRData l)) dp_l = Some d).
{ inv HMatch.
rewrite Hcurid in ×.
rewrite <- HRsmRel, <- HDprocRel; auto. }
destruct Hcond as (Hcond1 & Hcond2 & Hcond3).
destruct mp_h, mp_l, mp_h´; simpl in ×.
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; [ | elim Hdec; auto].
rewrite Hdec´ in MUpdate, MOrigin; inv MOrigin; inv MUpdate; simpl in ×.
refine_split´.
+
eapply plus_one.
eapply ieexec_step_prim_call; simpl; eauto.
× rewrite Hdec´; eauto.
× rewrite Hdec´; eauto.
+
inv HMatch; constructor; intros; try auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss.
intros contra; inv contra.
× unfold total_machine_regset in ×.
rewrite Hcurid.
case_eq (zeq i current_thread).
{ intros; subst.
eexists; left; rewrite ZMap.gss; auto. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; constructor; auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss; intros contra; inv contra.
× rewrite Hcurid.
case_eq (zeq i current_thread).
{ intros; subst.
rewrite ZMap.gss; intros contra; inv contra. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; auto.
-
rename rsm_h´ into rsm_h.
rename dp_h´ into dp_h.
rename mp_h´ into mp_h.
assert (Hcurid: proc_id (uRData l) = current_thread).
{ inv HMatch.
case_eq (zeq (proc_id (uRData l)) current_thread); intros; subst; auto.
clear H; eapply HRsmDom1 in n.
- rewrite n in H9; inv H9.
- apply all_cid_in_full_thread_list. }
assert (Hcond: ZMap.get (proc_id (uRData l)) rsm_l = Running rs ∧
fst mp_l = fst mp_h ∧
ZMap.get (proc_id (uRData l)) dp_l = Some d).
{ inv HMatch.
rewrite Hcurid in ×.
rewrite <- HRsmRel, <- HDprocRel; auto. }
destruct Hcond as (Hcond1 & Hcond2 & Hcond3).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; [ | elim Hdec; auto].
rewrite Hdec´ in MOrigin; inv MOrigin; simpl in ×.
refine_split´.
+
eapply plus_one.
eapply ieexec_step_external_yield; eauto.
× rewrite Hdec´; eauto.
× unfold state_checks in ×.
rewrite Hcond3.
rewrite H11 in H18.
auto.
+
inv HMatch; constructor; intros; try auto.
-
rename rsm_h´ into rsm_h.
rename dp_h´ into dp_h.
rename mp_h´ into mp_h.
assert (Hcurid: proc_id (uRData l) = current_thread).
{ inv HMatch.
case_eq (zeq (proc_id (uRData l)) current_thread); intros; subst; auto.
clear H; eapply HRsmDom1 in n.
- rewrite n in H9; inv H9.
- apply all_cid_in_full_thread_list. }
assert (Hcond: ZMap.get (proc_id (uRData l)) rsm_l = Running rs ∧
fst mp_l = fst mp_h ∧
ZMap.get (proc_id (uRData l)) dp_l = Some d).
{ inv HMatch.
rewrite Hcurid in ×.
rewrite <- HRsmRel, <- HDprocRel; auto. }
destruct Hcond as (Hcond1 & Hcond2 & Hcond3).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; [ | elim Hdec; auto].
rewrite Hdec´ in MOrigin; inv MOrigin; simpl in ×.
refine_split´.
+
eapply plus_one.
eapply ieexec_step_external_sleep; eauto.
× rewrite Hdec´; eauto.
× unfold state_checks in ×.
rewrite Hcond3.
rewrite H11 in H18.
auto.
+
inv HMatch; constructor; intros; try auto.
-
rename rsm_h´ into rsm_h.
rename mp_h´ into mp_h.
rename dp_h´ into dp_h.
assert (Hcurid: (proc_id (uRData l)) ≠ current_thread).
{ inv HMatch.
intros contra.
rewrite <- contra in HRsmDom2.
rewrite H6 in HRsmDom2.
elim HRsmDom2.
auto. }
exploit env_step_match; eauto.
intros.
destruct H as (rsm_l´´ & mp_l´´ & dp_l´´ & t & Hstep).
assert (t = E0) by (eapply star_step_no_trace in Hstep; auto); subst.
exploit star_log_append_split; eauto.
clear Hstep.
intros.
destruct H as (rsm_f & mp_f & dp_f & rsm_l´ & mp_l´ & dp_l´ & Hstep_f & Hstep & _).
clear rsm_l´´ mp_l´´ dp_l´´.
∃ rsm_l´, mp_l´, dp_l´.
split.
+
eapply star_plus_trans.
exact Hstep_f.
eapply plus_one.
exact Hstep.
simpl; reflexivity.
+
assert (HMatch_f: match_iestate_state ge (IEState (proc_id (uRData l)) rsm_h mp_h dp_h l)
(IEState (proc_id (uRData l)) rsm_f mp_f dp_f l)).
{ exploit star_step_preserve; eauto.
inv HMatch.
intros H.
destruct H as (Ha & Hb & Hc & Hd & He).
destruct He as (He & _).
generalize (He Hcurid); clear He; intros He.
assert (Hcurid´: current_thread ≠ (proc_id (uRData l))).
{ auto. }
generalize (Hb current_thread Hcurid´).
intros (Hba & Hbb).
rewrite <- HRsmRel in Hba.
rewrite <- HDprocRel in Hbb.
rewrite He in HMemRel.
constructor; simpl; intros; auto. }
clear HMatch.
clear Hstep_f.
remember (Single_Oracle l) as ev.
clear Heqev.
assert (lastEvType (ev::l) = Some LogYieldTy ∨ lastEvType (ev::l) ≠ Some LogYieldTy).
{ unfold lastEvType in *; simpl.
destruct ev; destruct l0; simpl; tauto. }
destruct H.
× exploit yield_log_preserve; eauto.
inv HMatch_f.
intros H1.
destruct H1 as (Ha & Hb & Hc); subst.
constructor; simpl; subst; auto.
× exploit non_yield_log_preserve; eauto.
inv HMatch_f.
intros H1.
destruct H1 as (Ha & Hb & Hc & Hd & He).
destruct He as (He & _).
generalize (He Hcurid); clear He; intros He.
assert (Hcurid´: current_thread ≠ (proc_id (uRData l))).
{ auto. }
generalize (Hb current_thread Hcurid´).
intros (Hba & Hbb).
rewrite <- HRsmRel in Hba.
rewrite <- HDprocRel in Hbb.
rewrite He in HMemRel.
constructor; simpl; subst; auto.
-
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. }
remember (LEvent (proc_id (uRData l)) LogYieldBack :: l) as l´.
remember (mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat (Mem.nextblock m) % nat)) as m´.
symmetry in Heqm´.
remember ((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) as rs´.
assert (Hcurid: proc_id (uRData l) = current_thread ∧ proc_id (uRData l´) = current_thread).
{ inv HMatch.
case_eq (zeq (proc_id (uRData l)) current_thread); intros; subst; auto.
- split; auto.
rewrite <- Hproc_id_same.
auto.
- clear H.
eapply HDprocDom1 in n.
rewrite n in H11.
inv H11.
apply all_cid_in_full_thread_list. }
destruct Hcurid as (Hcurid & Hcurid´).
assert (Hcond: fst mp_l = fst mp_h ∧
ZMap.get (proc_id (uRData l)) dp_l = Some d).
{ inv HMatch.
rewrite Hcurid in ×.
rewrite <- HDprocRel; auto. }
destruct Hcond as (Hcond1 & Hcond2).
case_eq (decide (proc_id (uRData l) = current_thread)); intros Hdec Hdec´; [ | elim Hdec; auto].
rewrite Hdec´ in MOrigin, MUpdate; inv MOrigin; simpl in ×.
refine_split´.
+
eapply plus_one.
eapply ieexec_step_external_yield_back; eauto.
× rewrite Hdec´; eauto.
× instantiate (1:= rs0); eauto.
inv HMatch.
rewrite Hdec.
rewrite Hdec in H7.
rewrite <- HRsmRel.
destruct H7; [left | right]; auto.
× rewrite Hdec´; eauto.
+
inv HMatch; constructor; intros; try auto.
× rewrite Hcurid; rewrite ZMap.gso; auto.
× rewrite Hcurid; rewrite ZMap.gss.
intros contra; inv contra.
× unfold total_machine_regset in ×.
rewrite Hcurid.
case_eq (zeq i current_thread).
{ intros; subst.
eexists; left; rewrite ZMap.gss; auto. }
{ intros; rewrite ZMap.gso; auto. }
× rewrite Hcurid; rewrite ?ZMap.gss; constructor; auto.
× simpl.
rewrite HMemRel; auto.
Qed.
End Refinement.
Section Link.
Require Import AuxFunctions.
Require Import liblayers.compat.CompatLayers.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import CompatExternalCalls.
Require Import MakeProgram.
Require Import LAsmModuleSem.
Require Import I64Layer.
Require Import Soundness.
Require Import LinkTactic.
Require Import LAsmModuleSemAux.
Require Import LAsm.
Require Import MakeProgramImpl.
Require Import LAsmAbsDataProperty.
Context `{s_config_link : SingleLinkConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Context `{LH: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined (LH ⊕ L64)}.
Context `{extcallsx: !ExternalCallsXDefined (LH ⊕ L64)}.
Context `{primcall_props: !PrimcallProperties IIEAsm.sprimitive_call}.
Context `{ie2ie_rel: !IE2IERel}.
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_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.
Theorem cl_backward_simulation:
∀ (s: StencilImpl.stencil) (CTXT: LAsm.module) (ph: AST.program fundef unit)
(Hmakep: make_program (module_ops:= LAsm.module_ops) s CTXT (LH ⊕ L64) = OK ph),
backward_simulation
(IIEAsm.iesemantics (current_thread::nil) ph)
(IIEAsm.iesemantics (full_thread_list) ph).
Proof.
intros. apply forward_to_backward_simulation; eauto.
- eapply forward_simulation_plus
with (match_states:= match_iestate_state (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 (Hproc_id_nil_full: In (proc_id (uRData nil)) full_thread_list).
{ apply all_cid_in_full_thread_list. }
constructor; auto; intros; auto.
× unfold rsm.
simpl.
rewrite ZMap.gso; auto.
rewrite ZMap.gi; auto.
× unfold rsm.
simpl.
rewrite ZMap.gss; auto.
unfold init_regset; simpl.
case_eq (decide (current_thread = main_thread)).
{ intros.
intro contra; inv contra. }
{ intros.
intro contra; inv contra. }
× exploit (init_state_total_machine_regset i rsm´ ph) ; eauto.
× unfold rsm; unfold rsm´.
simpl; rewrite ?ZMap.gss; auto.
× unfold dm.
simpl.
rewrite ZMap.gso; auto.
rewrite ZMap.gi; auto.
× unfold dm.
simpl.
rewrite ZMap.gss; auto.
intro contra; inv contra.
× generalize (init_state_total_dproc i dm´) ; eauto.
× unfold dm; unfold dm´.
simpl; rewrite ?ZMap.gss; auto.
+
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 ieasm_semantics_determinate; eauto.
Qed.
End Link.