Library mcertikos.multithread.lowrefins.AsmE2L
This file provide the semantics for the Asm instructions. Since we introduce paging mechanisms, the semantics of memory load and store are different from Compcert Asm
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
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 AlgebraicMem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Require Import SingleOracle.
Require Import AbstractDataType.
Require Export ObjMultiprocessor.
Require Export PBThread.
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 MakeProgramImpl.
Require Import StencilImpl.
Require Import LAsmModuleSemAux.
Require Import SingleConfiguration.
Require Import LAsm.
Require Import EAsm.
Require Import VCGen.
Section LIBRARY.
Context {D}`{data_prf : CompatData D}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{Hstencil: Stencil (stencil := stencil)}.
Context `{L: compatlayer (cdata D)}.
Local Instance : ExternalCallsOps (mwd (cdata D)) := CompatExternalCalls.compatlayer_extcall_ops L.
Lemma exec_external_prop:
∀ (ge: genv) WB ef args t vl (m m´: mwd (cdata D)),
external_call´ WB ef ge args m t vl m´ →
∀ (BUILTIN_ENABLED : match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
snd m´ = snd m.
Proof.
intros; simpl in ×.
destruct m; destruct m´; subst; simpl.
inversion H; subst.
destruct ef; try contradiction;
try (inversion H0; subst; auto; fail).
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H7; subst; try tauto.
inversion H2; lift_unfold.
destruct H4; subst; tauto.
+ destruct decode_longs in *; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H8; subst; auto.
inversion H2; lift_unfold.
destruct H5; subst; tauto.
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H8; lift_unfold.
destruct H2; destruct H3; destruct H8; subst; tauto.
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H9; lift_unfold.
destruct H2; subst; tauto.
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H14; lift_unfold.
destruct H2; subst; tauto.
Qed.
End LIBRARY.
Section Refinement.
Context `{s_link_config : SingleLinkConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil (stencil := stencil)}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{LH: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined (LH ⊕ L64)}.
Context `{extcallsx: !ExternalCallsXDefined (LH ⊕ L64)}.
Local Instance ec_ops : ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops (LH ⊕ L64).
Local Instance lcfg_ops : LayerConfigurationOps := compatlayer_configuration_ops (LH ⊕ L64).
Lemma ef_case_extern_call:
∀ ef,
(match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id then True else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id then False else True
| _ ⇒ True
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True
else False
| _ ⇒ False
end).
Proof.
intros. destruct ef; auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
destruct (has_event name); auto.
Qed.
Lemma ef_case_prim_call:
∀ ef,
(match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True
else False
| _ ⇒ False
end).
Proof.
intros. destruct ef; auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
Qed.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
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 AlgebraicMem.
Require Import LAsmAbsDataProperty.
Require Import RegsetLessdef.
Require Import SingleOracle.
Require Import AbstractDataType.
Require Export ObjMultiprocessor.
Require Export PBThread.
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 MakeProgramImpl.
Require Import StencilImpl.
Require Import LAsmModuleSemAux.
Require Import SingleConfiguration.
Require Import LAsm.
Require Import EAsm.
Require Import VCGen.
Section LIBRARY.
Context {D}`{data_prf : CompatData D}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{Hstencil: Stencil (stencil := stencil)}.
Context `{L: compatlayer (cdata D)}.
Local Instance : ExternalCallsOps (mwd (cdata D)) := CompatExternalCalls.compatlayer_extcall_ops L.
Lemma exec_external_prop:
∀ (ge: genv) WB ef args t vl (m m´: mwd (cdata D)),
external_call´ WB ef ge args m t vl m´ →
∀ (BUILTIN_ENABLED : match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
snd m´ = snd m.
Proof.
intros; simpl in ×.
destruct m; destruct m´; subst; simpl.
inversion H; subst.
destruct ef; try contradiction;
try (inversion H0; subst; auto; fail).
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H7; subst; try tauto.
inversion H2; lift_unfold.
destruct H4; subst; tauto.
+ destruct decode_longs in *; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H8; subst; auto.
inversion H2; lift_unfold.
destruct H5; subst; tauto.
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H8; lift_unfold.
destruct H2; destruct H3; destruct H8; subst; tauto.
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H9; lift_unfold.
destruct H2; subst; tauto.
+ destruct decode_longs in H0; [inversion H0 |].
simpl in H0; inversion H0; subst.
inversion H14; lift_unfold.
destruct H2; subst; tauto.
Qed.
End LIBRARY.
Section Refinement.
Context `{s_link_config : SingleLinkConfiguration}.
Context `{Hmwd: UseMemWithData mem}.
Context `{data_prf : CompatData PData}.
Context `{Hstencil: Stencil (stencil := stencil)}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Context `{real_params : RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{LH: compatlayer (cdata PData)}.
Context `{ass_def: !AccessorsDefined (LH ⊕ L64)}.
Context `{extcallsx: !ExternalCallsXDefined (LH ⊕ L64)}.
Local Instance ec_ops : ExternalCallsOps (mwd (cdata PData)) := CompatExternalCalls.compatlayer_extcall_ops (LH ⊕ L64).
Local Instance lcfg_ops : LayerConfigurationOps := compatlayer_configuration_ops (LH ⊕ L64).
Lemma ef_case_extern_call:
∀ ef,
(match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id then True else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id then False else True
| _ ⇒ True
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True
else False
| _ ⇒ False
end).
Proof.
intros. destruct ef; auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
destruct (has_event name); auto.
Qed.
Lemma ef_case_prim_call:
∀ ef,
(match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else True
| _ ⇒ True
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end)
∨ (match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True
else False
| _ ⇒ False
end).
Proof.
intros. destruct ef; auto.
destruct (peq name thread_yield); auto.
destruct (peq name thread_sleep); auto.
Qed.
In the definition of EAsm and in some of the properties below,
the new log is specified using a NON_YIELD hypothesis with a
somewhat contorted structure. These hypotheses are somtimes
difficult to manipulate because the event added to the log is not
immidiately available. To work around this we introduce the
following definitions and lemma.
Definition oapp {A} (o: option A) (l : list A) :=
match o with
| Some a ⇒ a :: l
| None ⇒ l
end.
Definition external_function_event ef largs l choice dSnapShot:=
match ef with
| EF_external id _ ⇒
if has_event id then
Some (LEvent (proc_id (uRData l)) (LogPrim id largs choice dSnapShot))
else
None
| _ ⇒
None
end.
Lemma untangle_non_yield l l´ ef largs choice dSnapShot:
match ef with
| EF_external id _ ⇒
if peq id thread_yield then False else
if peq id thread_sleep then False else
if has_event id then
l´ = LEvent (proc_id (uRData l)) (LogPrim id largs choice dSnapShot) :: l
else
l´ = l
| _ ⇒
l´ = l
end →
l´ = oapp (external_function_event ef largs l choice dSnapShot) l.
Proof.
unfold external_function_event.
destruct ef; eauto.
destruct (peq name thread_yield); try contradiction.
destruct (peq name thread_sleep); try contradiction.
destruct (has_event name); eauto.
Qed.
For each EAsm thread, as long as it is in the Available
state, the (possibly saved) register state in the low-level LAsm
machine should match the thread registers' initial state as
computed by thread_initial_state (if any). For the main
thread, the initial state is the usual "ready to execute main()"
state. For other threads, their initial state can be computed
from the log by locating a corresponding spawn event.
Once the thread switches to the Running state, its registers
are set using that initial state, and from now on the
corresponding low-level state should match the running state in
the EAsm machine.
Definition total_machine_regset (i : Z) rsm :=
∃ rs, ZMap.get i rsm = Running rs ∨ ZMap.get i rsm = Available.
Definition match_estate_regset (ge: genv) (i: Z) rsm (l : Log) (rs: regset) :=
(ZMap.get i rsm = Available ∧ initial_thread_kctxt ge i l = Some rs) ∨
(ZMap.get i rsm = Running rs).
Definition match_estate_kctxt (rs: regset) (kctxt: regset) :=
∀ r n, PregtoZ r = Some n → rs r = kctxt r.
We need to maintain the following invariant: any running thread
has already been initialized.
Definition thread_init_invariant (ge: genv) rsm l :=
∀ i rs,
ZMap.get i rsm = Running rs →
initial_thread_kctxt ge i l ≠ None.
Lemma initial_thread_kctxt_incr (ge: genv) i es l:
initial_thread_kctxt ge i l ≠ None →
initial_thread_kctxt ge i (es ++ l) ≠ None.
Proof.
unfold initial_thread_kctxt.
intros H.
induction es; eauto.
clear H.
simpl.
destruct (initial_thread_pc ge i (es ++ l)); congruence.
Qed.
Lemma thread_init_invariant_cons (ge: genv) rsm e l:
thread_init_invariant ge rsm l →
thread_init_invariant ge rsm (e::l).
Proof.
unfold thread_init_invariant.
unfold initial_thread_kctxt.
intros H i rs Hrs.
specialize (H i rs Hrs).
simpl.
destruct (initial_thread_pc ge i l); congruence.
Qed.
Lemma thread_init_invariant_app (ge: genv) rsm es l:
thread_init_invariant ge rsm l →
thread_init_invariant ge rsm (es++l).
Proof.
induction es; eauto using thread_init_invariant_cons.
Qed.
Lemma thread_init_invariant_set ge i rs s´ rsm l:
ZMap.get i rsm = Running rs →
thread_init_invariant ge rsm l →
thread_init_invariant ge (ZMap.set i s´ rsm) l.
Proof.
unfold thread_init_invariant.
intros Hi H j rsj Hrsj.
destruct (decide (i = j)).
- subst; eauto.
- rewrite ZMap.gso in Hrsj; eauto.
Qed.
The function below modifies a KContextPool to account for any
spawns performed in the given log fragment. The KContextPool
will only be updated the first time and initialization event is
encountered.
Definition do_init (ge: genv) (e : option LogEvent) l (kctxt: KContextPool) :=
match e with
| None ⇒ kctxt
| Some e ⇒
match thread_init_pc ge e with
| Some (i, pc) ⇒
match initial_thread_kctxt ge i l with
| Some _ ⇒ kctxt
| None ⇒ ZMap.set i (initial_regset_kctxt pc) kctxt
end
| None ⇒ kctxt
end
end.
We can show that do_init preserves the relation between the
context pool and the EAsm per-thread register state as defined
above.
Lemma match_estate_regset_kctxt_do_init ge i rsm kctxt e l rs:
thread_init_invariant ge rsm l →
(match_estate_regset ge i rsm l rs →
match_estate_kctxt rs (ZMap.get i kctxt)) →
(match_estate_regset ge i rsm (oapp e l) rs →
match_estate_kctxt rs (ZMap.get i (do_init ge e l kctxt))).
Proof.
intros Hinv H.
unfold match_estate_regset, do_init in ×.
destruct e as [e|]; eauto.
specialize (Hinv i rs).
unfold initial_thread_kctxt in ×.
simpl.
destruct (thread_init_pc_of ge i e) as [rsi|] eqn:Hinit.
-
unfold thread_init_pc_of in Hinit.
destruct (thread_init_pc ge e) as [[j rsj]|]; try discriminate.
destruct (decide _); try discriminate.
inv Hinit.
destruct (initial_thread_pc ge j l).
+
eauto.
+
rewrite ZMap.gss.
intros [[Hj Hrs] | Hj].
×
inversion Hrs.
repeat intro; reflexivity.
×
elim Hinv; eauto.
-
unfold thread_init_pc_of in Hinit.
destruct (thread_init_pc ge e) as [[j rsj]|]; try discriminate.
+
destruct (decide _); try discriminate.
destruct (initial_thread_pc ge j l);
destruct (initial_thread_pc ge i l);
rewrite ?ZMap.gso; eauto.
+
destruct (initial_thread_pc ge i l);
eauto.
Qed.
Section WITH_ORACLE.
Section ABSTRACT_REL.
Class AbstractRel :=
{
match_EData_RData: EData → Log → RData → Prop;
match_init:
match_EData_RData
(initial_map None (fun i ⇒ Some (thread_init_dproc i)) full_thread_list)
nil
(init_adt multi_oracle_init7);
match_gss:
∀ l dp d a
(Hget_dp : ZMap.get (proc_id (uRData l)) dp = Some d)
(Hdata : match_EData_RData dp l a),
match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d) dp) l a;
acc_exec_load_match:
∀ (ge: genv) a rs rd rs´ TY (m m´: mem) ds´ l dp d´ d addr,
(acc_exec_load (cl_oplus (cdata PData) LH L64))
fundef unit ge TY ((m, (uRData l, d)) : mwd (cdata PData)) addr rs rd
= Next rs´ ((m´, (ds´, d´)) : mwd (cdata PData)) →
lastEvType l ≠ Some LogYieldTy →
match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d) dp) l a →
ZMap.get (proc_id (uRData l)) dp = Some d →
∃ a´,
PBThread.exec_loadex ge TY ((m, a) : mwd (cdata RData)) addr rs rd
= Next rs´ ((m´, a´) : mwd (cdata RData)) ∧
ds´ = uRData l ∧
match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d´) dp) l a´ ∧
kctxt a´ = kctxt a;
acc_exec_store_match:
∀ (ge: genv) a rs rd rs´ TY ST (m m´: mem) ds´ l dp d´ d addr,
(acc_exec_store (cl_oplus (cdata PData) LH L64))
fundef unit ge TY ((m, (uRData l, d)) : mwd (cdata PData)) addr rs rd ST =
Next rs´ ((m´, (ds´, d´)) : mwd (cdata PData)) →
lastEvType l ≠ Some LogYieldTy →
match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d) dp) l a →
ZMap.get (proc_id (uRData l)) dp = Some d →
∃ a´,
PBThread.exec_storeex ge TY ((m, a) : mwd (cdata RData)) addr rs rd ST
= Next rs´ ((m´, a´) : mwd (cdata RData))∧
ds´ = uRData l ∧
match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d´) dp) l a´ ∧
kctxt a´ = kctxt a;
log_yield_call_match:
∀ (ge: genv) (s : stencil) (b : block) (sg : signature)
(m m´ : mem) rsm rs des_rs´ rs´ l l´ l´´ d d´ dp (a: cdata RData) nb yield_ev,
(∀ i : Z,
In i full_thread_list → total_machine_regset i rsm) →
(∀ i : Z,
i ≠ proc_id (uRData l) →
∀ rs0 : regset,
match_estate_regset ge i rsm l rs0 →
match_estate_kctxt rs0 (ZMap.get i (kctxt a))) →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (External (EF_external thread_yield sg)) →
find_symbol s thread_yield = Some b →
match_EData_RData dp l a →
ZMap.get (proc_id (uRData l)) dp = Some d →
ZMap.get (proc_id (uRData l)) rsm = Running rs →
ZMap.get (proc_id (uRData l´)) rsm = Available ∧
initial_thread_kctxt ge (proc_id (uRData l´)) l´ = Some des_rs´ ∨
ZMap.get (proc_id (uRData l´)) rsm = Running des_rs´ →
ZMap.get (proc_id (uRData l´)) dp = Some d´ →
thread_init_invariant ge rsm l →
lastEvType l ≠ Some LogYieldTy →
state_checks thread_yield nil l dp →
yield_ev = LEvent (proc_id (uRData l)) (LogYield (Mem.nextblock m)) →
l´ = yield_ev :: l →
l´´ = LEvent (proc_id (uRData l´)) LogYieldBack :: l´ →
getLogEventNB yield_ev = Some nb →
rs PC = Vptr b Int.zero →
m´ = (mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat (Mem.nextblock m) % nat)) →
rs´ = (((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) des_rs´))
# EAX <- Vundef) # PC <- (des_rs´ RA)) # RA <- Vundef →
∃ (a´: cdata RData),
primcall_thread_schedule_sem (prim_ident := thread_yield) big_thread_yield_spec s rs (m, a) rs´ (m´, a´) ∧
(∀ i´ : Z,
i´ ≠ proc_id (uRData l´´) →
∀ rs´´ : regset,
match_estate_regset ge i´
(ZMap.set (proc_id (uRData l´´)) (Running rs´) rsm) l´´ rs´´ →
match_estate_kctxt rs´´ (ZMap.get i´ (kctxt a´))) ∧
thread_init_invariant ge (ZMap.set (proc_id (uRData l´´)) (Running rs´) rsm) l´´ ∧
match_EData_RData dp l´´ a´;
log_sleep_call_match:
∀ (ge: genv) (s : stencil) (b : block) (sg : signature)
(m m´ : mem) rsm rs des_rs´ rs´ l l´ l´´ d d´ dp (a: cdata RData) nb sleep_ev i0,
(∀ i : Z,
In i full_thread_list → total_machine_regset i rsm) →
(∀ i : Z,
i ≠ proc_id (uRData l) →
∀ rs0 : regset,
match_estate_regset ge i rsm l rs0 →
match_estate_kctxt rs0 (ZMap.get i (kctxt a))) →
stencil_matches s ge →
Genv.find_funct_ptr ge b = Some (External (EF_external thread_sleep sg)) →
find_symbol s thread_sleep = Some b →
extcall_arguments rs m {| sig_args := Tint :: nil;
sig_res := None;
sig_cc := cc_default |} (Vint i0 :: nil) →
match_EData_RData dp l a →
ZMap.get (proc_id (uRData l)) dp = Some d →
ZMap.get (proc_id (uRData l)) rsm = Running rs →
ZMap.get (proc_id (uRData l´)) rsm = Available ∧
initial_thread_kctxt ge (proc_id (uRData l´)) l´ = Some des_rs´ ∨
ZMap.get (proc_id (uRData l´)) rsm = Running des_rs´ →
ZMap.get (proc_id (uRData l´)) dp = Some d´ →
thread_init_invariant ge rsm l →
lastEvType l ≠ Some LogYieldTy →
state_checks thread_sleep (Lint i0 :: nil) l dp →
sleep_ev = LEvent (proc_id (uRData l)) (LogSleep (Int.unsigned i0) (Mem.nextblock m)
(sync_chpool_check thread_sleep (Lint i0 :: nil) (uRData l) d)) →
l´ = sleep_ev :: l →
l´´ = LEvent (proc_id (uRData l´)) LogYieldBack :: l´ →
getLogEventNB sleep_ev = Some nb →
rs PC = Vptr b Int.zero →
m´ = (mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat (Mem.nextblock m) % nat)) →
rs´ = (((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) des_rs´))
# EAX <- Vundef) # PC <- (des_rs´ RA)) # RA <- Vundef →
∃ (a´: cdata RData),
primcall_thread_transfer_sem big_thread_sleep_spec s rs (m, a) rs´ (m´, a´) ∧
(∀ i´ : Z,
i´ ≠ proc_id (uRData l´´) →
∀ rs´´ : regset,
match_estate_regset ge i´
(ZMap.set (proc_id (uRData l´´)) (Running rs´) rsm) l´´ rs´´ →
match_estate_kctxt rs´´ (ZMap.get i´ (kctxt a´))) ∧
thread_init_invariant ge (ZMap.set (proc_id (uRData l´´)) (Running rs´) rsm) l´´ ∧
match_EData_RData dp l´´ a´;
external_call_match_no_event:
∀ (ge: genv) WB ef (args: list val) t res (m m´ : mem) l d d´ ds´ (dp : EData) (a: RData),
external_call´ (mem := mwd (cdata PData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (LH ⊕ L64))
WB ef ge args (m, (uRData l, d)) t res (m´, (ds´, d´)) →
lastEvType l ≠ Some LogYieldTy →
match_EData_RData dp l a →
ZMap.get (proc_id (uRData l)) dp = Some d →
∀ (BUILTIN_ENABLED : match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id then False else True
| _ ⇒ True
end),
∃ (a´: RData),
external_call´ (mem := mwd (cdata RData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (pbthread ⊕ L64))
WB ef ge args (m, a) t res (m´, a´) ∧
ds´ = uRData l ∧
match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d´) dp) l a´ ∧
kctxt a´ = do_init ge None l (kctxt a);
external_call_match_has_event:
∀ (ge: genv) WB ef (args: list val) (largs : list lval) t res (m m´ : mem) l l´ d d´ ds´
(dp : EData) (a: RData) (choice : Z) ,
external_call´ (mem := mwd (cdata PData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (LH ⊕ L64))
WB ef ge args (m, (uRData l, d)) t res (m´, (ds´, d´)) →
lastEvType l ≠ Some LogYieldTy →
match_EData_RData dp l a →
ZMap.get (proc_id (uRData l)) dp = Some d →
val2Lval_list args largs →
∀ (BUILTIN_ENABLED : match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else if has_event id
then
choice_check id largs (uRData l) d = choice ∧
l´ = LEvent (proc_id (uRData l)) (LogPrim id largs choice (snap_func d)) :: l
else False
| _ ⇒ False
end),
∃ (a´: RData),
external_call´ (mem := mwd (cdata RData))
(external_calls_ops := CompatExternalCalls.compatlayer_extcall_ops (pbthread ⊕ L64))
WB ef ge args (m, a) t res (m´, a´) ∧
ds´ = uRData l´ ∧
match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d´) dp) l´ a´ ∧
kctxt a´ = do_init ge (external_function_event ef largs l choice (snap_func d)) l (kctxt a);
primitive_call_match:
∀ (ge: genv) ef t rs rs´ (m m´ : mem) l l´ d d´ ds´ dp (a: cdata RData),
primitive_call (LayerConfigurationOps := LC (LH ⊕ L64))
(mem := mwd (cdata PData)) ef ge rs (m, (uRData l, d)) t rs´ (m´, (ds´, d´)) →
lastEvType l ≠ Some LogYieldTy →
match_EData_RData dp l a →
ZMap.get (proc_id (uRData l)) dp = Some d →
∀ (BUILTIN_ENABLED : match ef with
| EF_external id _ ⇒
if peq id thread_yield then False
else if peq id thread_sleep then False
else
if has_event id
then
l´ =
LEvent (proc_id (uRData l)) (LogPrim id nil 0 (snap_func d)) :: l
else l´ = l
| _ ⇒ l´ = l
end),
∃ (a´: cdata RData),
primitive_call (LayerConfigurationOps := LC (pbthread ⊕ L64))
(mem := mwd (cdata RData)) ef ge rs (m, a) t rs´ (m´, a´) ∧
ds´ = uRData l´ ∧
match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d´) dp) l´ a´ ∧
kctxt a´ = do_init ge (external_function_event ef nil l 0 (snap_func d)) l (kctxt a)
}.
End ABSTRACT_REL.
Context `{abs_rel: AbstractRel}.
Inductive match_estate_state ge: (estate (mem := mem)) →
(state (mem:= mwd (cdata RData))) → Prop :=
| MATCH_ESTATE_STATE_NORMAL:
∀ (rs: regset) (m: mem) a ae (l : Log) rsm
(Hlst_ev_type: lastEvType l ≠ Some LogYieldTy)
(Htotal : ∀ i, In i full_thread_list → total_machine_regset i rsm)
(Hrs: match_estate_regset ge (proc_id (uRData l)) rsm l rs)
(Hrsm: ∀ i,
i ≠ (proc_id (uRData l)) →
∀ rs0,
match_estate_regset ge i rsm l rs0 →
match_estate_kctxt rs0 (ZMap.get i (kctxt a)))
(Hinit_inv: thread_init_invariant ge rsm l)
(Hdata: match_EData_RData ae l a),
match_estate_state ge (EState (proc_id (uRData l)) rsm m ae l) (State rs (m, a))
| MATCH_ESTATE_STATE_SCHED:
∀ (rs: regset) (m: mem) a ae (l : Log) rsm
(Hlst_ev_type: lastEvType l = Some LogYieldTy)
(Htotal : ∀ i, In i full_thread_list → total_machine_regset i rsm)
(Hrs: match_estate_regset ge (proc_id (uRData (remove_hd l))) rsm (remove_hd l) rs)
(Hrsm: ∀ i,
i ≠ (proc_id (uRData (remove_hd l))) →
∀ rs0,
match_estate_regset ge i rsm (remove_hd l) rs0 →
match_estate_kctxt rs0 (ZMap.get i (kctxt a)))
(Hinit_inv: thread_init_invariant ge rsm (remove_hd l))
(Hdata: match_EData_RData ae (remove_hd l) a)
(pre_step: EAsm.estep ge (EState (proc_id (uRData (remove_hd l))) rsm m ae (remove_hd l)) E0
(EState (proc_id (uRData l)) rsm m ae l)),
match_estate_state ge (EState (proc_id (uRData l)) rsm m ae l) (State rs (m, a)).
Lemma asm_exec_instr_match :
∀ ge f (i : Asm.instruction) rs rs´ (m m´: mem) l ds´ d d´ dp a
(Hexec: exec_instr (lcfg_ops := LC (LH ⊕ L64)) ge f i rs (m, (uRData l, d)) = Next rs´ (m´, (ds´, d´)))
(Hlogtype: lastEvType l ≠ Some LogYieldTy)
(Hmatch: match_EData_RData dp l a)
(Hget_dp: ZMap.get (proc_id (uRData l)) dp = Some d),
∃ a´,
exec_instr (lcfg_ops:= LC (pbthread ⊕ L64)) ge f i rs (m, a) = Next rs´ (m´, a´)
∧ ds´ = uRData l
∧ match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d´) dp) l a´
∧ kctxt a´ = kctxt a.
Proof.
intros; simpl in ×.
exploit match_gss; eauto; intros.
destruct i; try (simpl in *; inversion Hexec; subst; ∃ a; eauto; fail);
simpl in *; try (eauto using acc_exec_load_match; fail); try (eauto using acc_exec_store_match; fail).
- destruct (Val.divu (rs EAX) (rs # EDX <- Vundef r1)); [ | inversion Hexec].
destruct (Val.modu (rs EAX) (rs # EDX <- Vundef r1)); inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
- destruct (Val.divs (rs EAX) (rs # EDX <- Vundef r1)); [ | inversion Hexec].
destruct (Val.mods (rs EAX) (rs # EDX <- Vundef r1)); inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
- destruct (eval_testcond c rs).
+ destruct b; inversion Hexec; subst.
× ∃ a; split; [ simpl; auto | split; auto].
× ∃ a; split; [ simpl; auto | split; auto].
+ inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
- unfold goto_label in ×.
destruct (label_pos l0 0 (fn_code f)); try (inversion Hexec; fail).
destruct (rs PC); try (inversion Hexec; fail).
inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
- destruct (eval_testcond c rs); try (inversion Hexec; fail).
destruct b; subst.
+ unfold goto_label in ×.
destruct (label_pos l0 0 (fn_code f)); try (inversion Hexec; fail).
destruct (rs PC); try (inversion Hexec; fail).
inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
+ inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
- destruct (eval_testcond c1); try (inversion Hexec; fail).
destruct b; simpl.
+ destruct (eval_testcond c2 rs); try (inversion Hexec; fail).
destruct b.
× unfold goto_label in ×.
destruct (label_pos l0 0 (fn_code f)); try (inversion Hexec; fail).
destruct (rs PC); try (inversion Hexec; fail).
inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
× inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
+ destruct (eval_testcond c2 rs); inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
- destruct (rs r); try (inversion Hexec; fail).
destruct (list_nth_z tbl (Int.unsigned i)); try (inversion Hexec; fail).
unfold goto_label in ×.
destruct (label_pos l0 0 (fn_code f)); try (inversion Hexec; fail).
destruct (rs PC); try (inversion Hexec; fail).
inversion Hexec; subst.
∃ a; split; [ simpl; auto | split; auto].
- simpl in Hexec.
lift_unfold; simpl in ×.
destruct (Mem.alloc m 0 sz); simpl in ×.
destruct (Mem.store Mint32 m0 b (Int.unsigned (Int.add Int.zero ofs_link)) (rs ESP));
[simpl in × | inversion Hexec].
destruct (Mem.store Mint32 m1 b (Int.unsigned (Int.add Int.zero ofs_ra)) (rs RA));
[simpl in × | inversion Hexec].
inversion Hexec; subst.
∃ a; split; [ auto | split; auto].
- unfold Mem.loadv in *; simpl in ×.
destruct (Val.add (rs ESP) (Vint ofs_ra)); try (inversion Hexec; fail).
lift_unfold; simpl in ×.
destruct (Mem.load Mint32 m b (Int.unsigned i)); try (inversion Hexec; fail).
destruct (Val.add (rs ESP) (Vint ofs_link)); try (inversion Hexec; fail).
destruct (Mem.load Mint32 m b0 (Int.unsigned i0)); try (inversion Hexec; fail).
destruct (rs ESP); try (inversion Hexec; fail).
destruct (Mem.free m b1 0 sz); try (inversion Hexec; fail).
simpl in *; inversion Hexec; subst.
∃ a; split; [ auto | split; auto].
Fail idtac.
Qed.
Lemma exec_instr_match:
∀ ge f i rs rs´ (m m´: mem) l ds´ d d´ dp a
(Hexec: exec_instr (lcfg_ops := LC (LH ⊕ L64)) ge f i rs (m, (uRData l, d)) = Next rs´ (m´, (ds´, d´)))
(Hlogtype: lastEvType l ≠ Some LogYieldTy)
(Hmatch: match_EData_RData dp l a)
(Hget_dp: ZMap.get (proc_id (uRData l)) dp = Some d),
∃ a´,
exec_instr (lcfg_ops:= LC (pbthread ⊕ L64)) ge f i rs (m, a) = Next rs´ (m´, a´)
∧ ds´ = uRData l
∧ match_EData_RData (ZMap.set (proc_id (uRData l)) (Some d´) dp) l a´
∧ kctxt a´ = kctxt a.
Proof.
intros.
exploit match_gss; eauto; intros.
unfold exec_instr in Hexec; simpl.
subdestruct; try (inv Hexec; esplit; eauto; fail);
simpl in *; try (eauto using acc_exec_load_match; fail); try (eauto using acc_exec_store_match; fail).
eapply asm_exec_instr_match; eauto.
Qed.
Lemma big_thread_yield_spec_match_gss:
∀ a rs a´ r rs´ n,
big_thread_yield_spec a ((Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
#EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA))
= Some (a´, rs´) →
PregtoZ r = Some n →
rs r = (ZMap.get (ZMap.get (CPU_ID a) (cid a)) (kctxt a´)) r.
Proof.
intros until n.
intros Hfunc preg_prop.
functional inversion Hfunc.
simpl.
rewrite ZMap.gss.
eapply PregToZ_correct in preg_prop.
functional inversion preg_prop; trivial.
Qed.
Lemma big_thread_yield_spec_match_gso:
∀ a rs a´ rs´ i,
big_thread_yield_spec a ((Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
#EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA))
= Some (a´, rs´) →
i ≠ ZMap.get (CPU_ID a) (cid a) →
ZMap.get i (kctxt a´) = ZMap.get i (kctxt a).
Proof.
intros until i.
intros Hfunc Hcid_neq.
functional inversion Hfunc.
simpl.
rewrite ZMap.gso; eauto.
Qed.
Lemma big_thread_sleep_spec_match_gss:
∀ a rs a´ r rs´ n i,
big_thread_sleep_spec a (Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
#EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA) (Int.unsigned i) = Some (a´, rs´) →
PregtoZ r = Some n →
rs r = (ZMap.get (ZMap.get (CPU_ID a) (cid a)) (kctxt a´)) r.
Proof.
intros until i.
intros Hfunc preg_prop.
functional inversion Hfunc.
simpl.
rewrite ZMap.gss.
eapply PregToZ_correct in preg_prop.
functional inversion preg_prop; trivial.
Qed.
Lemma big_thread_sleep_spec_match_gso:
∀ a rs a´ rs´ i i0,
big_thread_sleep_spec a (Pregmap.init Vundef)#ESP <- (rs#ESP)#EDI <- (rs#EDI)#ESI <- (rs#ESI)
#EBX <- (rs#EBX)#EBP <- (rs#EBP)#RA <- (rs#RA) (Int.unsigned i0) = Some (a´, rs´) →
i ≠ ZMap.get (CPU_ID a) (cid a) →
ZMap.get i (kctxt a´) = ZMap.get i (kctxt a).
Proof.
intros until i0.
intros Hfunc Hcid_neq.
functional inversion Hfunc.
simpl.
rewrite ZMap.gso; eauto.
Qed.
Lemma match_estate_regset_running ge rs rs´ i rsm l:
match_estate_regset ge i rsm l rs →
ZMap.get i rsm = Running rs´ →
rs´ = rs.
Proof.
intros [[Hrsmi _] | Hrsmi] Hrsmi´; congruence.
Qed.
Lemma match_estate_regset_available ge i rsm l rs rs´:
match_estate_regset ge i rsm l rs →
initial_thread_kctxt ge i l = Some rs´ →
ZMap.get i rsm = Available →
rs´ = rs.
Proof.
destruct 1 as [[? ?] | ]; congruence.
Qed.
Lemma match_estate_regset_ss ge i rsm l rs:
match_estate_regset ge i (ZMap.set i (Running rs) rsm) l rs.
Proof.
right.
apply ZMap.gss.
Qed.
Lemma match_estate_regset_so ge i j rs rsm l rs´:
i ≠ j →
(match_estate_regset ge i (ZMap.set j (Running rs) rsm) l rs´ ↔
match_estate_regset ge i rsm l rs´).
Proof.
intros Hij.
split;
(intros [[H Hinit] | H]; [left | right]);
rewrite ZMap.gso in *; eauto.
Qed.
Lemma match_estate_regset_fw ge i rsm e l rs:
match_estate_regset ge i rsm l rs →
thread_init_pc_of ge i e = None →
match_estate_regset ge i rsm (e :: l) rs.
Proof.
intros H He.
unfold match_estate_regset in ×.
unfold initial_thread_kctxt in ×.
simpl.
rewrite He.
destruct (initial_thread_pc ge i l); eauto.
Qed.
Lemma match_estate_regset_bw ge i rsm e l rs:
match_estate_regset ge i rsm (e :: l) rs →
thread_init_pc_of ge i e = None →
match_estate_regset ge i rsm l rs.
Proof.
intros H He.
unfold match_estate_regset in ×.
unfold initial_thread_kctxt in ×.
simpl in H.
rewrite He in H.
destruct (initial_thread_pc ge i l); eauto.
Qed.
Since EAsm "start" steps don't have a corresponding LAsm step,
we need to find some measure that they decrease instead. I
choose to count the number of pending initializations in the
log, that is, initializations of threads that are currently in
the Available state.
Section MEASURE.
Local Open Scope nat.
Definition measure_estate (s: estate (mem:=mem)) :=
match s with EState _ _ _ _ l ⇒
match lastEvType l with
| Some LogYieldTy ⇒ O
| _ ⇒ S O
end
end.
End MEASURE.
For the proof below, we need this property on our global environment.
Record genv_wf (ge : genv) :=
{
genv_wf_external b f sg:
Genv.find_funct_ptr ge b = Some (External (EF_external f sg)) →
Genv.find_symbol ge f = Some b
}.
Local Existing Instance MakeProgramImpl.make_program_ops.
Lemma make_globalenv_wf (s: stencil) M (L: compatlayer (cdata PData)) ge:
make_globalenv s M L = OK ge →
genv_wf ge.
Proof.
intros Hge.
constructor.
- intros b f sg Hf.
eapply make_globalenv_find_funct_ptr in Hf; eauto.
destruct Hf as (i & Hib & [(fi & Hi & Hfi) | (fe & Hi & Hfe)]).
+ simpl in Hfi.
destruct (instrs_OK _); discriminate.
+ simpl in Hfe.
inversion Hfe; clear Hfe; subst.
assumption.
Qed.
Lemma make_program_genv_wf (s: stencil) M (L: compatlayer (cdata PData)) p:
make_program s M L = OK p →
genv_wf (Genv.globalenv p).
Proof.
intros.
eapply make_globalenv_wf.
eapply make_program_make_globalenv.
eassumption.
Qed.
With this we're ready to prove the refinement for one step.
Theorem EAsm_refine_LAsm:
∀ ge t cst cst´ rs m,
genv_wf ge →
EAsm.estep ge cst t cst´ →
match_estate_state ge cst (State rs m) →
(∃ st´,
LAsm.step (lcfg_ops := LC (pbthread ⊕ L64)) ge (State rs m) t st´
∧ match_estate_state ge cst´ st´) ∨
((measure_estate cst´ < measure_estate cst)%nat ∧
t = E0 ∧
match_estate_state ge cst´ (State rs m)).
Proof.
intros ? ? ? ? ? ? Hge; intros.
inv H; [left .. | right | right | | left].
-
inv H0; [ | elim H6; assumption].
assert (rs0 = rs) by eauto using match_estate_regset_running; subst.
exploit exec_instr_match; eauto.
intros (a´ & Hexec & ? & Hmatch & Hkctxt); subst.
esplit. split.
+ eapply exec_step_internal; eauto.
+ econstructor; eauto.
intros.
× unfold total_machine_regset in ×.
case_eq (zeq i0 (proc_id (uRData l))); intros; subst.
{ rewrite ZMap.gss.
∃ rs´; left; auto. }
{ rewrite ZMap.gso; eauto. }
× right.
rewrite ZMap.gss.
trivial.
× intros.
apply match_estate_regset_so in H0; eauto.
rewrite Hkctxt. eapply Hrsm; eauto.
× eapply thread_init_invariant_set; eauto.
-
inv H0; [ | elim H6; assumption].
assert (rs0 = rs) by eauto using match_estate_regset_running; subst.
rename H1 into Hrsm_rs.
pose proof H7 as Hext.
eapply exec_external_prop in H7; eauto.
inv H7.
esplit.
split.
+ eapply exec_step_builtin; eauto.
instantiate (1:= (m´, a)).
instantiate (1:= vl).
inversion Hext; subst.
econstructor.
instantiate (1:= v).
× subdestruct; try (inversion BUILTIN_ENABLED; fail).
{ simpl in H.
inversion H; subst; simpl in *; subdestruct; subst; repeat setoid_rewrite Hdestruct.
- inv H; eapply CompCertBuiltins.builtin_sem_i64_neg; eauto.
- inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_neg; eauto.
- inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_add; eauto.
- inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_add; eauto.
- inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_sub; eauto.
- inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_sub; eauto.
- inv H1.
inv H; eapply CompCertBuiltins.builtin_sem_i64_mul; eauto. }
{ simpl in H.
subdestruct; subst; setoid_rewrite Hdestruct0; inv H.
econstructor.
inv H10; econstructor; eauto. }
{ simpl in ×.
subdestruct; repeat setoid_rewrite Hdestruct0; try (inv H; fail);
try (subst; inv H; econstructor; eauto;
(inversion H12 || inversion H11); subst; econstructor; eauto;
simpl in *; lift_unfold;
destruct H0; split; eauto; fail). }
{ simpl in ×.
inv H;
unfold PregEq.t in H0;
rewrite <- H0; clear H0;
subdestruct;
econstructor; eauto;
inv H11; econstructor; eauto. }
{ simpl in ×.
subdestruct; simpl in *;
unfold PregEq.t in *; rewrite Hdestruct1;
inv H; econstructor; eauto;
(inv H12 || inv H7); econstructor; eauto; lift_unfold; destruct H0; split; auto. }
{ simpl in H; subdestruct; subst; setoid_rewrite Hdestruct0.
- inv H; econstructor; eauto.
- inv H.
destruct m´0.
simpl in H7, H12; lift_unfold.
destruct H7, H12.
econstructor; lift_unfold.
+ instantiate (1:= (m, a)).
split; eauto.
+ split; eauto. }
{ inv H; subst.
subdestruct; setoid_rewrite Hdestruct.
rewrite <- H0.
econstructor; eauto.
simpl in *; lift_unfold.
destruct H8; split; auto. }
{ simpl in H; subdestruct; setoid_rewrite Hdestruct0.
inv H; subst.
- inv H.
- inv H; subst.
econstructor; eauto.
simpl in ×.
lift_unfold.
destruct H19; split; auto. }
{ simpl in H; inv H; econstructor; eauto. }
{ simpl in H; subdestruct; unfold PregEq.t in *; rewrite Hdestruct1;
inversion H; subst; econstructor; eauto. }
{ inv H. }
× reflexivity.
+ econstructor; eauto.
× unfold total_machine_regset in *; intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
{ rewrite ZMap.gss.
eexists; left; auto. }
{ rewrite ZMap.gso; eauto. }
× apply match_estate_regset_ss.
× intros. apply match_estate_regset_so in H0; eauto.
× eapply thread_init_invariant_set; eauto.
× eapply match_gss; eauto.
-
inv H0; [ | elim H7; assumption].
assert (rs0 = rs) by eauto using match_estate_regset_running; subst.
rename H1 into Hrsm_rs.
pose proof H8 as Hext.
eapply exec_external_prop in H8; eauto. inv H8.
esplit.
split.
+ eapply exec_step_annot; eauto.
instantiate (1:= vargs).
× unfold annot_arguments in ×.
clearAllExceptOne H6.
induction H6; simpl; try constructor; try assumption.
inversion H; subst; try econstructor.
eassumption; simpl.
lift_unfold; auto.
× instantiate (1:= (m´, a)).
instantiate (1:= v).
inversion Hext; subst.
econstructor.
instantiate (1:= v0).
{ subdestruct; try (inversion BUILTIN_ENABLED; fail).
- simpl in H.
inversion H; subst.
+ eapply CompCertBuiltins.builtin_sem_i64_neg; eauto.
+ eapply CompCertBuiltins.builtin_sem_i64_add; eauto.
+ eapply CompCertBuiltins.builtin_sem_i64_sub; eauto.
+ eapply CompCertBuiltins.builtin_sem_i64_mul; eauto.
- simpl in H.
subdestruct; subst; inv H.
inversion H11; subst.
+ inversion H11; subst.
econstructor; econstructor; eauto.
+ inversion H11; subst.
econstructor; econstructor; eauto.
- simpl in ×.
subdestruct; subst; try (inv H; fail);
try (inv H; econstructor;
(inv H13 || inv H12); econstructor; eauto;
simpl in *; lift_unfold;
destruct H0; split; eauto; fail).
- simpl in ×.
inv H; subdestruct; econstructor; eauto; inv H12; econstructor; eauto.
- simpl in ×.
subdestruct; simpl in *; inv H; econstructor; eauto;
(inv H13 || inv H8); econstructor; eauto; lift_unfold; destruct H0; split; eauto.
- simpl in H; subdestruct; subst.
+ inv H; econstructor; eauto.
+ inv H.
destruct m´0.
simpl in H8, H13; lift_unfold.
destruct H8, H13.
econstructor; lift_unfold.
instantiate (1:= (m, a)).
× split; eauto.
× split; eauto.
- inv H; subst; subdestruct.
econstructor; eauto.
simpl in *; lift_unfold.
destruct H9; split; auto.
- simpl in H; subdestruct; inv H; subst.
econstructor; eauto.
simpl in ×.
lift_unfold.
destruct H20; split; auto.
- simpl in H; inv H; econstructor; eauto.
- simpl in H; subdestruct; inv H; econstructor; eauto.
- inv H. }
{ reflexivity. }
+ econstructor; eauto.
× unfold total_machine_regset in *; intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
{ rewrite ZMap.gss.
eexists; left; auto. }
{ rewrite ZMap.gso; eauto. }
× apply match_estate_regset_ss.
× intros. apply match_estate_regset_so in H0; eauto.
× eapply thread_init_invariant_set; eauto.
× eapply match_gss; eauto.
-
assert (EF_CASES:
(match ef with
| EF_external id _ ⇒ if peq id thread_yield
then False else if peq id thread_sleep
then False else
if has_event id then False else True
| _ ⇒ True
end) ∨ (∃ largs choice,
val2Lval_list args largs ∧
(match ef with
| EF_external id _ ⇒
if peq id thread_yield
then False else if peq id thread_sleep then False
else if has_event id
then
choice_check id largs (uRData l) d = choice ∧
l´ = LEvent (proc_id (uRData l))
(LogPrim id largs choice (snap_func d)) :: l
else False
| _ ⇒ False
end))).
{ destruct ef; try (left; auto; fail).
case_eq (peq name thread_yield); intros; subst.
rewrite peq_true in NON_YIELD; try contradiction.
case_eq (peq name thread_sleep); intros; subst.
rewrite peq_true in NON_YIELD; try contradiction.
case_eq (has_event name); intros; subst.
- rewrite peq_false in NON_YIELD; auto.
rewrite peq_false in NON_YIELD; auto.
rewrite H8 in NON_YIELD.
right; auto.
- rewrite peq_false in NON_YIELD; auto. }
destruct EF_CASES.
+
inv H0; [ | elim H6; assumption].
assert (rs0 = rs) by eauto using match_estate_regset_running; subst.
rename H1 into Hrsm_rs.
exploit external_call_match_no_event; eauto.
intro evidence.
destruct evidence as (a´ & (eval_evid & match_evid)).
destruct match_evid as (Hds & Hmatch & Hkctxt).
assert (l´eq: l´ = l).
{ destruct ef; try auto.
case_eq (peq name thread_yield); intros; subst;
[ rewrite peq_true in H; contradiction |].
rewrite peq_false in NON_YIELD, H; try assumption.
case_eq (peq name thread_sleep); intros; subst;
[ rewrite peq_true in H; contradiction |].
rewrite peq_false in NON_YIELD, H; try assumption.
destruct (has_event name); try contradiction.
subst; reflexivity. }
esplit; split.
× eapply exec_step_external; eauto.
clearAllExceptOne H5.
unfold extcall_arguments in ×.
simpl in ×.
induction H5.
constructor.
constructor; try auto.
inv H.
econstructor.
Opaque Z.add Z.mul.
remember (Stacklayout.fe_ofs_arg + 4 × ofs) as index_val.
econstructor; eauto.
Transparent Z.add Z.mul.
× subst; econstructor.
{ assumption. }
{ unfold total_machine_regset in *; intros.
case_eq (zeq i (proc_id (uRData l))); intros; subst.
{ rewrite ZMap.gss.
eexists; left; auto. }
{ rewrite ZMap.gso; eauto. } }
{ apply match_estate_regset_ss. }
{ intros.
simpl in H1.
apply match_estate_regset_so in H1; eauto.
simpl in Hkctxt.
rewrite Hkctxt.
eapply Hrsm; eauto.
}
{ eapply thread_init_invariant_set; eauto.
}
{ auto.
}
+
inv H0; [ | elim H6; assumption].
assert (rs0 = rs) by eauto using match_estate_regset_running; subst.
rename H1 into Hrsm_rs.
destruct H as (largs & choice & Ha & Hb).
exploit external_call_match_has_event; eauto.
intro evidence.
destruct evidence as (a´ & (eval_evid & match_evid)).
destruct match_evid as (Hds & Hmatch & Hkctxt).
esplit; split.
× eapply exec_step_external; eauto.
clearAllExceptOne H5.
unfold extcall_arguments in ×.
simpl in ×.
induction H5.
constructor.
constructor; try auto.
inv H.
econstructor.
Opaque Z.add Z.mul.
remember (Stacklayout.fe_ofs_arg + 4 × ofs) as index_val.
econstructor; eauto.
Transparent Z.add Z.mul.
× clear NON_YIELD.
rename Hb into NON_YIELD.
destruct ef; try (inv NON_YIELD; fail).
case_eq (peq name thread_yield); intros; subst; simpl in NON_YIELD; [rewrite peq_true in NON_YIELD; try contradiction | rewrite peq_false in NON_YIELD; auto].
case_eq (peq name thread_sleep); intros; subst; simpl in NON_YIELD; [rewrite peq_true in NON_YIELD; try contradiction | rewrite peq_false in NON_YIELD; auto].
case_eq (has_event name); intros Hhas_event; rewrite Hhas_event in NON_YIELD; try contradiction.
assert (l´ = oapp (external_function_event (EF_external name sg) largs l choice (snap_func d)) l).
{ unfold external_function_event.
rewrite Hhas_event.
unfold oapp; auto.
destruct NON_YIELD; auto. }
simpl in H1.
rewrite Hhas_event in H1.
simpl in H1.
assert (last_event_type: lastEvType l´ ≠ Some LogYieldTy).
{ subst.
unfold lastEvType; simpl; intro contra; inv contra. }
assert (proc_id_same : proc_id (uRData l´) = proc_id (uRData l)).
{ unfold uRData; subst.
eapply update_proc_id; eauto; eauto. }
rewrite <- proc_id_same.
subst; econstructor.
{ assumption. }
{ unfold total_machine_regset in *; intros.
rewrite proc_id_same; case_eq (zeq i (proc_id (uRData l))); intros; subst.
{ rewrite ZMap.gss.
eexists; left; auto. }
{ rewrite ZMap.gso; eauto. } }
{ apply match_estate_regset_ss. }
{ intros.
apply match_estate_regset_so in H2; eauto.
rewrite Hkctxt; clear Hkctxt.
eapply match_estate_regset_kctxt_do_init; eauto.
intros.
eapply Hrsm; eauto.
rewrite <- proc_id_same; auto.
simpl; rewrite Hhas_event; simpl; auto.
}
{ simpl.
eapply thread_init_invariant_cons; eauto.
eapply thread_init_invariant_set; eauto.
rewrite proc_id_same; eauto. }
{ rewrite proc_id_same; eauto. }
-
inv H0; [ | elim H5; assumption].
assert (rs0 = rs) by eauto using match_estate_regset_running; subst.
rename H1 into Hrsm_rs.
exploit primitive_call_match; eauto.
intro evidence.
destruct evidence as (a´ & (eval_evid & match_evid)).
assert (last_event_type: lastEvType l´ ≠ Some LogYieldTy).
{ destruct ef; subst; eauto.
case_eq (peq name thread_yield); intros; subst;
[ rewrite peq_true in NON_YIELD; contradiction | ].
rewrite peq_false in NON_YIELD; try assumption.
case_eq (peq name thread_sleep); intros; subst;
[ rewrite peq_true in NON_YIELD; contradiction | ].
rewrite peq_false in NON_YIELD; try assumption.
destruct (has_event name); subst; auto.
unfold lastEvType; simpl.
intro contra; inv contra. }
assert (proc_id_same : proc_id (uRData l´) = proc_id (uRData l)).
{ destruct ef; subst; eauto.
case_eq (peq name thread_yield); intros; subst;
[ rewrite peq_true in NON_YIELD; contradiction | ].
rewrite peq_false in NON_YIELD; try assumption.
case_eq (peq name thread_sleep); intros; subst;
[ rewrite peq_true in NON_YIELD; contradiction | ].
rewrite peq_false in NON_YIELD; try assumption.
destruct (has_event name); subst; auto.
unfold uRData.
eapply update_proc_id; eauto; eauto. }
esplit; split.
+ eapply exec_step_prim_call; eauto.
+ destruct match_evid as (match_evid1 & (match_evid2 & match_evid3)).
eapply untangle_non_yield in NON_YIELD.
rewrite <- proc_id_same.
subst; econstructor.
× unfold oapp, external_function_event; simpl.
destruct ef; eauto.
× unfold total_machine_regset in *; intros.
rewrite proc_id_same; case_eq (zeq i (proc_id (uRData l))); intros; subst.
{ rewrite ZMap.gss.
eexists; left; auto. }
{ rewrite ZMap.gso; eauto. }
× apply match_estate_regset_ss.
× intros.
simpl.
apply match_estate_regset_so in H0; eauto.
rewrite match_evid3.
eapply match_estate_regset_kctxt_do_init; eauto.
eapply Hrsm; eauto.
rewrite proc_id_same in H; auto.
× eapply thread_init_invariant_set; eauto.
destruct (external_function_event _ _ _); simpl; eauto.
unfold oapp in proc_id_same; rewrite proc_id_same; auto.
unfold oapp.
unfold external_function_event; destruct ef; eauto.
destruct (has_event name); eauto.
eapply thread_init_invariant_cons; eauto.
× rewrite proc_id_same.
auto.
-
split; simpl.
unfold lastEvType in H8.
destruct l; simpl in *; auto.
unfold getLogEventType in ×.
destruct l.
unfold getLogEventUnitType in ×.
destruct l in *; try (elim H8; reflexivity; fail); auto.
split; auto.
set (l´ := LEvent (proc_id (uRData l)) (LogYield (Mem.nextblock m0))::l).
assert (l´_type: lastEvType l´ = Some LogYieldTy).
{ unfold l´.
unfold lastEvType.
simpl; auto. }
inv H0; [ | elim H8; assumption].
assert (rmv_hd_val: remove_hd l´ = l).
{ unfold l´; simpl; auto. }
eapply MATCH_ESTATE_STATE_SCHED; eauto.
rewrite rmv_hd_val.
unfold l´.
eapply eexec_step_external_yield; eauto.
-
split; simpl.
unfold lastEvType in H8.
destruct l; simpl in *; auto.
unfold getLogEventType in ×.
destruct l.
unfold getLogEventUnitType in ×.
destruct l in *; try (elim H8; reflexivity; fail); auto.
split; auto.
set (l´ := LEvent (proc_id (uRData l))
(LogSleep (Int.unsigned i) (Mem.nextblock m0)
(sync_chpool_check thread_sleep (Lint i :: nil) (uRData l) d)) :: l).
assert (l´_type: lastEvType l´ = Some LogYieldTy).
{ unfold l´.
unfold lastEvType.
simpl; auto. }
inv H0; [ | elim H8; assumption].
assert (rmv_hd_val: remove_hd l´ = l).
{ unfold l´; simpl; auto. }
eapply MATCH_ESTATE_STATE_SCHED; eauto.
rewrite rmv_hd_val.
unfold l´.
eapply eexec_step_external_sleep; eauto.
-
inv H0.
+ red in Htotal.
generalize (Htotal (proc_id (uRData l))); intros.
destruct H as (rs0 & H).
eapply all_cid_in_full_thread_list.
rewrite H1 in H; destruct H; inv H.
+ red in Htotal.
generalize (Htotal (proc_id (uRData l))); intros.
destruct H as (rs0 & H).
eapply all_cid_in_full_thread_list.
rewrite H1 in H; destruct H; inv H.
-
inv H0.
+
assert (rs0 = rs).
{
destruct H1 as [[? ?] | ?];
destruct Hrs as [[? ?] | ?];
try congruence.
}
subst.
assert (lastEvType l = Some LogYieldTy).
{ destruct l.
- simpl in H4.
inv H4.
- simpl in H4.
inv H4.
unfold lastEvType.
simpl.
unfold getLogEventNB in Hnextblock.
destruct e.
unfold getLogEventUnitNB in Hnextblock.
destruct l; simpl; auto; inv Hnextblock. }
elim Hlst_ev_type; assumption.
+
assert (lastEvType l = Some LogYieldTy).
{ destruct l.
- simpl in H4.
inv H4.
- simpl in H4.
inv H4.
unfold lastEvType.
simpl.
unfold getLogEventNB in Hnextblock.
destruct e.
unfold getLogEventUnitNB in Hnextblock.
destruct l; simpl; auto; inv Hnextblock. }
assert (Hl_ev: ∃ ev l´, l = ev::l´).
{ destruct l.
- unfold lastEvType in H; simpl in H; inv H.
- ∃ l, l0; auto. }
destruct Hl_ev as (ev & l´ & Hl_ev); subst.
unfold remove_hd in ×.
generalize H; intro ev_type.
unfold lastEvType in ev_type.
simpl in ev_type.
inv ev_type.
unfold getLogEventType in H5.
destruct ev.
unfold getLogEventUnitType in H5.
destruct l; try (inv H5; fail).
×
clear H H5.
inversion pre_step; try contradiction.
{ destruct ef; try (generalize NON_YIELD; clear;
intros contra; eapply cons_lst_eq_lst_contradiction in contra; contradiction; fail).
destruct (peq name thread_yield); try contradiction.
destruct (peq name thread_sleep); try contradiction.
destruct (has_event name);
try (generalize NON_YIELD; clear;
intros contra; eapply cons_lst_eq_lst_contradiction in contra; contradiction; fail).
destruct NON_YIELD as (largs & choice & ? & ? & contra); inv contra. }
{ destruct ef; try (generalize NON_YIELD; clear;
intros contra; eapply cons_lst_eq_lst_contradiction in contra; contradiction; fail).
destruct (peq name thread_yield); try contradiction.
destruct (peq name thread_sleep); try contradiction.
destruct (has_event name);
try (generalize NON_YIELD; clear;
intros contra; eapply cons_lst_eq_lst_contradiction in contra; contradiction; fail).
inv NON_YIELD. }
{
subst.
clear H3 H19.
destruct ef; try (inv NON_YIELD; fail).
destruct (peq name thread_yield); try (inv NON_YIELD; fail).
clear NON_YIELD; subst.
clear pre_step.
inv H16.
simpl in H4; inv H4.
inv Hrs.
- destruct H.
rewrite H in H10.
inv H10.
- rewrite H10 in H; inv H.
rename m0 into m.
rename l´ into l.
rename d into d´.
rename d0 into d.
rename rs0 into des_rs´.
clear H12.
remember (LEvent (proc_id (uRData l)) (LogYield (Mem.nextblock m))) as yield_ev.
remember (yield_ev::l) as l´.
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´.
remember ((((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call)
des_rs´)) # EAX <- Vundef) # PC <- (des_rs´ RA)) # RA <- Vundef) as rs´.
assert (s_find: find_symbol s thread_yield = Some b).
{ inversion H15.
eapply genv_wf_external in H14; eauto.
rewrite <- H14.
symmetry.
eapply stencil_matches_symbols. }
generalize (log_yield_call_match ge s b sg m m´ rsm rs des_rs´ rs´ l l´ l´´ d d´ dp a nb _
Htotal Hrsm H15 H14 s_find Hdata H11 H10 H1 H2 Hinit_inv H17
H18 Heqyield_ev Heql´ Heql´´ Hnextblock H13 Heqm´ Heqrs´).
intros.
destruct H as (a´ & Hdes_step & Hdes_match_regset & Hdes_init_invariant & Hdes_match).
∃ (State rs´ (m´, a´)).
split.
+
eapply exec_step_prim_call; try eauto.
econstructor.
esplit; esplit.
split; eauto.
instantiate (1:= primcall_thread_schedule_compatsem big_thread_yield_spec (prim_ident:= thread_yield)).
split; simpl; try reflexivity.
econstructor; eauto.
+
assert (procid_preserve: proc_id (uRData l´) = proc_id (uRData l´´)).
{ generalize Heql´´.
clearAll.
remember (uRData l´) as adt1.
remember (uRData l´´) as adt2.
simpl in ×.
unfold uRData in ×.
intros.
rewrite Heql´´ in Heqadt2.
rewrite Heqadt1 in Heqadt2.
symmetry.
symmetry in Heqadt1, Heqadt2.
eapply update_proc_id with (a:= LEvent (proc_id (update init_dshare l´)) LogYieldBack); eauto. }
rewrite procid_preserve.
eapply MATCH_ESTATE_STATE_NORMAL; eauto.
×
subst; unfold lastEvType.
simpl; intro contra; inv contra.
×
intros.
case_eq (zeq i (proc_id (uRData l´´))).
{ intros.
subst.
econstructor.
rewrite ZMap.gss.
left; reflexivity. }
{ intros.
eapply Htotal in H.
inversion H.
econstructor.
rewrite ZMap.gso; eauto. }
×
right; rewrite ZMap.gss; eauto. }
{ inv H16. }
{ subst.
generalize (all_cid_in_full_thread_list l´); intros.
eapply Htotal in H.
unfold total_machine_regset in H.
rewrite H10 in H.
destruct H as (rs1 & H); destruct H; inv H. }
{ inv H16. }
×
clear H H5.
inversion pre_step; try contradiction.
{ destruct ef; try (generalize NON_YIELD; clear;
intros contra; eapply cons_lst_eq_lst_contradiction in contra; contradiction; fail).
destruct (peq name thread_yield); try contradiction.
destruct (peq name thread_sleep); try contradiction.
destruct (has_event name);
try (generalize NON_YIELD; clear;
intros contra; eapply cons_lst_eq_lst_contradiction in contra; contradiction; fail).
destruct NON_YIELD as (largs & choice & ? & ? & contra); inv contra. }
{ destruct ef; try (generalize NON_YIELD; clear;
intros contra; eapply cons_lst_eq_lst_contradiction in contra; contradiction; fail).
destruct (peq name thread_yield); try contradiction.
destruct (peq name thread_sleep); try contradiction.
destruct (has_event name);
try (generalize NON_YIELD; clear;
intros contra; eapply cons_lst_eq_lst_contradiction in contra; contradiction; fail).
inv NON_YIELD. }
{ inv H16. }
{
subst.
clear H3 H19.
destruct ef; try (inv NON_YIELD; fail).
destruct (peq name thread_sleep); try (inv NON_YIELD; fail).
clear NON_YIELD; subst.
clear pre_step.
inv H16.
simpl in H4; inv H4.
inv Hrs.
- destruct H.
rewrite H in H10.
inv H10.
- rewrite H10 in H; inv H.
rename m0 into m.
rename l´ into l.
rename d into d´.
rename d0 into d.
rename rs0 into des_rs´.
clear H12.
remember (LEvent (proc_id (uRData l)) (LogSleep (Int.unsigned i0) (Mem.nextblock m)
(sync_chpool_check thread_sleep
(Lint i0 :: nil) (uRData l) d))) as sleep_ev.
remember (sleep_ev::l) as l´.
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´.
remember ((((undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call)
des_rs´)) # EAX <- Vundef) # PC <- (des_rs´ RA)) # RA <- Vundef) as rs´.
assert (s_find: find_symbol s thread_sleep = Some b).
{ inversion H15.
eapply genv_wf_external in H14; eauto.
rewrite <- H14.
symmetry.
eapply stencil_matches_symbols. }
generalize (log_sleep_call_match ge s b sg m m´ rsm rs des_rs´ rs´ l l´ l´´ d d´ dp a nb _ i0
Htotal Hrsm H15 H14 s_find Hargs Hdata H11 H10 H1 H2 Hinit_inv H17
H18 Heqsleep_ev Heql´ Heql´´ Hnextblock H13 Heqm´ Heqrs´).
intros.
destruct H as (a´ & Hdes_step & Hdes_match_regset & Hdes_init_invariant & Hdes_match).
∃ (State rs´ (m´, a´)).
split.
+
eapply exec_step_prim_call; try eauto.
econstructor.
esplit; esplit.
split; eauto.
instantiate (1:= primcall_thread_transfer_compatsem big_thread_sleep_spec).
split; simpl; try reflexivity.
econstructor; eauto.
+
assert (procid_preserve: proc_id (uRData l´) = proc_id (uRData l´´)).
{ generalize Heql´´.
clearAll.
remember (uRData l´) as adt1.
remember (uRData l´´) as adt2.
simpl in ×.
unfold uRData in ×.
intros.
rewrite Heql´´ in Heqadt2.
rewrite Heqadt1 in Heqadt2.
symmetry.
symmetry in Heqadt1, Heqadt2.
eapply update_proc_id with (a:= LEvent (proc_id (update init_dshare l´)) LogYieldBack); eauto. }
rewrite procid_preserve.
eapply MATCH_ESTATE_STATE_NORMAL; eauto.
×
subst; unfold lastEvType.
simpl; intro contra; inv contra.
×
intros.
case_eq (zeq i (proc_id (uRData l´´))).
{ intros.
subst.
econstructor.
rewrite ZMap.gss.
left; reflexivity. }
{ intros.
eapply Htotal in H.
inversion H.
econstructor.
rewrite ZMap.gso; eauto. }
×
right; rewrite ZMap.gss; eauto. }
{ subst.
generalize (all_cid_in_full_thread_list l´); intros.
eapply Htotal in H.
unfold total_machine_regset in H.
rewrite H10 in H.
destruct H as (rs1 & H); destruct H; inv H. }
{ inv H16. }
Fail idtac.
Qed.
Theorem cl_backward_simulation:
∀ (s: 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
(EAsm.esemantics full_thread_list ph)
(LAsm.semantics (lcfg_ops := LC (pbthread ⊕ L64)) ph).
Proof.
intros. apply forward_to_backward_simulation; eauto.
- eapply forward_simulation_star with
(match_states := match_estate_state (Genv.globalenv ph))
(measure := measure_estate);
simpl; intros; trivial.
+
inv H. esplit; split.
× econstructor; simpl; eauto.
instantiate (1:= (m0, init_adt (multi_oracle_init7))).
rewrite InitMem.init_mem_with_data.
rewrite H0. simpl; trivial.
× assert (lastEvType nil ≠ Some LogYieldTy).
{ unfold lastEvType; simpl; eauto.
intros contra; inv contra. }
assert (proc_id (uRData nil) = main_thread).
{ eapply null_log_proc_id. }
rewrite <- H1.
eapply MATCH_ESTATE_STATE_NORMAL with (ge := Genv.globalenv ph); eauto.
{
subst rsm.
assert (Hmain: prog_main ph = 1%positive).
{
unfold make_program in Hmakep.
inv_monad Hmakep; subst.
reflexivity.
}
revert Hmain.
clear.
induction full_thread_list.
- intros. inv H.
- intros.
simpl in H.
simpl.
case_eq (zeq i a); intros; subst.
+ unfold total_machine_regset.
rewrite ZMap.gss.
unfold init_regset; simpl.
destruct (decide _).
× ∃ (((Pregmap.init Vundef)
# PC <- (symbol_offset
(Genv.globalenv ph)
1%positive Int.zero)) # ESP <- Vzero); auto.
× ∃ (Pregmap.init Vundef); right; auto.
+ destruct H.
× elim n; subst; reflexivity.
× apply IHl in H; auto.
unfold total_machine_regset in ×.
rewrite ZMap.gso; auto.
}
{
right.
assert (Hmain: prog_main ph = 1%positive).
{
unfold make_program in Hmakep.
inv_monad Hmakep; subst.
reflexivity.
}
subst rsm.
generalize main_valid.
revert Hmain.
clear.
assert (proc_id (uRData nil) = main_thread).
{ eapply null_log_proc_id. }
intros Hmain.
induction full_thread_list.
- inversion 1.
- intros [Ha | Hl].
+ simpl.
subst.
rewrite H.
rewrite ZMap.gss.
unfold init_regset.
destruct (decide _); congruence.
+ simpl.
destruct (decide (a = main_thread)); subst.
× rewrite H.
rewrite ZMap.gss.
unfold init_regset.
destruct (decide _); congruence.
× rewrite H.
rewrite ZMap.gso by eauto.
rewrite H in IHl.
rewrite IHl by eauto.
reflexivity.
}
{
intros.
simpl.
rewrite ZMap.gi.
subst rsm.
destruct H3 as [[Hi Hrs] | Hi].
- unfold initial_thread_kctxt in Hrs; simpl in Hrs.
destruct (decide _); congruence.
- exfalso.
induction full_thread_list; simpl in Hi.
+ rewrite ZMap.gi in Hi.
discriminate.
+ destruct (decide (i = a)); subst.
× rewrite ZMap.gss in Hi.
unfold init_regset in Hi.
destruct (decide (a = main_thread)); congruence.
× rewrite ZMap.gso in Hi; eauto.
}
{
clear.
subst rsm.
intros i rs Hi.
revert Hi.
induction full_thread_list.
- simpl.
rewrite ZMap.gi.
discriminate.
- simpl.
destruct (decide (i = a)).
+ subst.
rewrite ZMap.gss.
unfold init_regset.
unfold initial_thread_kctxt.
simpl.
destruct (decide _); try discriminate.
+ rewrite ZMap.gso by eauto.
exact IHl.
}
{
unfold dm.
eapply match_init.
}
+ destruct s2.
exploit EAsm_refine_LAsm; eauto.
{
eapply make_program_genv_wf.
eassumption.
}
intros [(s2´ & Hstep & Hmatch) | (Hs & Ht & Hmatch)];
eauto using plus_one.
- apply easm_semantics_receptive; eauto.
- apply lasm_semantics_determinate.
decision. decision.
Qed.
End WITH_ORACLE.
End Refinement.