Library mcertikos.conlib.conmtlib.IIEAsm
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 MemoryX.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Asm.
Require Import Conventions.
Require Import Machregs.
Require Import AuxLemma.
Require Import CommonTactic.
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 LAsm.
Require Import GlobIdent.
Require Export EAsmCommon.
Require Import SingleConfiguration.
Section ESemantics.
Context `{conf : SingleConfiguration}.
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.
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 CommonTactic.
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 LAsm.
Require Import GlobIdent.
Require Export EAsmCommon.
Require Import SingleConfiguration.
Section ESemantics.
Context `{conf : SingleConfiguration}.
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.
EAsm threads can be in one of three states: environment,
available, or running. Environment threads can only take oracle
steps and will never change states. Available threads have not
been run yet, but may be "yielded back" to, at which time they
become running threads. Running threads have a current register
state and take normal steps.
Inductive iestate: Type :=
| IEState: Z → ZMap.t ThreadState → (mem × mem) → EData → Log → iestate.
Inductive iestep (ge: genv) : iestate → trace → iestate → Prop :=
| ieexec_step_internal:
∀ b ofs f i (rs: regset) mset mset´ m m´ dp d d´ ds´ rs´ curid rsm l
(MOrigin: if (decide (curid = current_thread)) then m = fst mset else m = snd mset),
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some i →
lastEvType l ≠ Some LogYieldTy →
exec_instr ge f i rs (m, (uRData l,d)) = Next rs´ (m´, (ds´,d´)) →
∀ (MUpdate: if (decide (curid = current_thread)) then mset´ = (m´, snd mset)
else mset´ = (fst mset, m´))
(Hget_dp: ZMap.get curid dp = Some d),
iestep ge (IEState curid rsm mset dp l) E0
(IEState curid (ZMap.set curid (Running rs´) rsm) mset´
(ZMap.set curid (Some d´) dp) l)
| ieexec_step_builtin:
∀ b ofs f ef args res (rs: regset) mset mset´ m m´ dp d d´ ds´ t vl rs´ curid rsm l
(MOrigin: if (decide (curid = current_thread)) then m = fst mset else m = snd mset),
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some (asm_instruction (Pbuiltin ef args res)) →
lastEvType l ≠ Some LogYieldTy →
external_call´ (mem:= mwd (cdata PData)) (fun _ ⇒ True) ef ge (map rs args) (m, (uRData l,d)) t vl (m´, (ds´, d´)) →
rs´ = nextinstr_nf
(set_regs res vl
(undef_regs (map preg_of (destroyed_by_builtin ef)) rs)) →
∀ BUILTIN_ENABLED:
match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end,
∀ BUILTIN_WT:
subtype_list (proj_sig_res´ (ef_sig ef)) (map typ_of_preg res) = true,
∀ (Hget_dp: ZMap.get curid dp = Some d),
∀ (MUpdate: if (decide (curid = current_thread)) then mset´ = (m´, snd mset)
else mset´ = (fst mset, m´)),
iestep ge (IEState curid rsm mset dp l) t
(IEState curid (ZMap.set curid (Running rs´) rsm) mset´
(ZMap.set curid (Some d´) dp) l)
| ieexec_step_annot:
∀ b ofs f ef args (rs: regset) mset mset´ m m´ dp d d´ ds´ vargs t v curid rsm l
(MOrigin: if (decide (curid = current_thread)) then m = fst mset else m = snd mset),
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b ofs →
Genv.find_funct_ptr ge b = Some (Internal f) →
find_instr (Int.unsigned ofs) f.(fn_code) = Some (asm_instruction (Pannot ef args)) →
annot_arguments rs m args vargs →
lastEvType l ≠ Some LogYieldTy →
external_call´ (mem:= mwd (cdata PData)) (fun _ ⇒ True) ef ge vargs (m, (uRData l, d)) t v (m´, (ds´, d´)) →
∀ BUILTIN_ENABLED:
match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end,
∀ (Hget_dp: ZMap.get curid dp = Some d),
∀ (MUpdate: if (decide (curid = current_thread)) then mset´ = (m´, snd mset)
else mset´ = (fst mset, m´)),
iestep ge (IEState curid rsm mset dp l) t
(IEState curid (ZMap.set curid (Running (nextinstr rs)) rsm) mset´
(ZMap.set curid (Some d´) dp) l)
| ieexec_step_external:
∀ b ef args res (rs: regset) mset mset´ m m´ dp d d´ ds´ t rs´ curid rsm l l´
(MOrigin: if (decide (curid = current_thread)) then m = fst mset else m = snd mset),
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
extcall_arguments rs m (ef_sig ef) args →
lastEvType l ≠ Some LogYieldTy →
external_call´ (mem:= mwd (cdata PData)) (fun _ ⇒ True) ef ge args (m, (uRData l, d)) t res (m´, (ds´,d´)) →
rs´ = (set_regs (loc_external_result (ef_sig ef)) res
(undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs)))
#PC <- (rs RA) #RA <- Vundef →
∀ NON_YIELD:
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
∃ largs choice,
val2Lval_list args largs ∧
choice_check id largs (uRData l) d = choice ∧
l´ = (LEvent curid (LogPrim id largs choice (snap_func d)) :: l)
else
l´ = l
| _ ⇒ l´ = l
end,
∀ STACK:
∀ b o, rs ESP = Vptr b o →
(Ple (Genv.genv_next ge) b ∧ Plt b (Mem.nextblock m)),
∀ SP_NOT_VUNDEF: rs ESP ≠ Vundef,
∀ RA_NOT_VUNDEF: rs RA ≠ Vundef,
∀ (Hget_dp: ZMap.get curid dp = Some d),
∀ (MUpdate: if (decide (curid = current_thread)) then mset´ = (m´, snd mset)
else mset´ = (fst mset, m´)),
iestep ge (IEState curid rsm mset dp l) t
(IEState curid (ZMap.set curid (Running rs´) rsm)
mset´ (ZMap.set curid (Some d´) dp) l´)
| ieexec_step_prim_call:
∀ b ef (rs: regset) mset mset´ m m´ dp d d´ ds´ t rs´ curid rsm l l´
(MOrigin: if (decide (curid = current_thread)) then m = fst mset else m = snd mset),
ZMap.get curid rsm = Running rs →
proc_id (uRData l) = curid →
rs PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
lastEvType l ≠ Some LogYieldTy →
primitive_call (mem:= mwd (cdata PData)) ef ge rs (m, (uRData l, d)) t rs´ (m´, (ds´, d´)) →
∀ NON_YIELD:
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 curid (LogPrim id nil 0 (snap_func d)) :: l)
else
l´ = l
| _ ⇒ l´ = l
end,
∀ (Hget_dp: ZMap.get curid dp = Some d),
∀ (MUpdate: if (decide (curid = current_thread)) then mset´ = (m´, snd mset)
else mset´ = (fst mset, m´)),
iestep ge (IEState curid rsm mset dp l) t
(IEState curid (ZMap.set curid (Running rs´) rsm) mset´
(ZMap.set curid (Some d´) dp) l´)
| ieexec_step_external_yield:
∀ b ef (rs: regset) (mset : (mem × mem)) (m: mem) curid curid´ rsm s l l´ dp d
(MOrigin: if (decide (curid = current_thread)) then m = fst mset else m = snd mset),
ZMap.get curid rsm = Running rs →
ZMap.get curid dp = Some d →
proc_id (uRData l) = curid →
rs PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
stencil_matches s ge →
l´ = (LEvent curid (LogYield (Mem.nextblock m))::l) →
lastEvType l ≠ Some LogYieldTy →
state_checks thread_yield nil l dp →
curid´ = proc_id (uRData l´) →
∀ (NON_YIELD: match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end),
iestep ge (IEState curid rsm mset dp l) E0
(IEState curid´ rsm mset dp l´)
| ieexec_step_external_sleep:
∀ b ef (rs: regset) (mset : (mem × mem)) (m: mem) curid curid´ rsm s l l´ dp d i
(MOrigin: if (decide (curid = current_thread)) then m = fst mset else m = snd mset),
ZMap.get curid rsm = Running rs →
ZMap.get curid dp = Some d →
proc_id (uRData l) = curid →
rs PC = Vptr b Int.zero →
Genv.find_funct_ptr ge b = Some (External ef) →
stencil_matches s ge →
l´ = (LEvent curid (LogSleep (Int.unsigned i) (Mem.nextblock m)
(sync_chpool_check thread_sleep ((Lint i)::nil) (uRData l) d))::l) →
lastEvType l ≠ Some LogYieldTy →
state_checks thread_sleep (Lint i::nil) l dp →
curid´ = proc_id (uRData l´) →
∀
(Hargs: extcall_arguments rs m (mksignature (Tint:: nil) None cc_default) (Vint i:: nil))
(NON_YIELD: match ef with
| EF_external id _ ⇒
if peq id thread_sleep then True
else False
| _ ⇒ False
end),
iestep ge (IEState curid rsm mset dp l) E0
(IEState curid´ rsm mset dp l´)
Environment step
| ieexec_step_external_empty:
∀ (mset: (mem × mem)) curid curid´ rsm dp l l´,
ZMap.get curid rsm = Environment →
ZMap.get curid dp = None →
proc_id (uRData l) = curid →
l´ = (Single_Oracle l::l) →
curid´ = proc_id (uRData l´) →
iestep ge (IEState curid rsm mset dp l) E0
(IEState curid´ rsm mset dp l´)
| ieexec_step_external_yield_back:
∀ (rs´ rs0: regset) (mset mset´ : (mem × mem)) (m m´: mem) curid rsm l l´ nb dp d e
(MOrigin: if (decide (curid = current_thread)) then m = fst mset else m = snd mset),
(ZMap.get curid rsm = Available ∧ initial_thread_kctxt ge curid l = Some rs0) ∨
ZMap.get curid rsm = Running rs0 →
ZMap.get curid dp = Some d →
proc_id (uRData l) = curid →
last_op l = Some e →
l´ = (LEvent curid LogYieldBack::l) →
rs´ = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs0))
# EAX <- Vundef #PC <- (rs0 RA) #RA <- Vundef →
∀
(Hnextblock: getLogEventNB (e) = Some nb)
(LIFT_NEXTBLOCK: mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat (Mem.nextblock m) % nat) = m´)
(MUpdate: if (decide (curid = current_thread)) then mset´ = (m´, snd mset)
else mset´ = (fst mset, m´)),
iestep ge (IEState curid rsm mset dp l) E0
(IEState curid (ZMap.set curid (Running rs´) rsm) mset´ dp l´).
Context (active_threads : list Z).
∀ (mset: (mem × mem)) curid curid´ rsm dp l l´,
ZMap.get curid rsm = Environment →
ZMap.get curid dp = None →
proc_id (uRData l) = curid →
l´ = (Single_Oracle l::l) →
curid´ = proc_id (uRData l´) →
iestep ge (IEState curid rsm mset dp l) E0
(IEState curid´ rsm mset dp l´)
| ieexec_step_external_yield_back:
∀ (rs´ rs0: regset) (mset mset´ : (mem × mem)) (m m´: mem) curid rsm l l´ nb dp d e
(MOrigin: if (decide (curid = current_thread)) then m = fst mset else m = snd mset),
(ZMap.get curid rsm = Available ∧ initial_thread_kctxt ge curid l = Some rs0) ∨
ZMap.get curid rsm = Running rs0 →
ZMap.get curid dp = Some d →
proc_id (uRData l) = curid →
last_op l = Some e →
l´ = (LEvent curid LogYieldBack::l) →
rs´ = (undef_regs (CR ZF :: CR CF :: CR PF :: CR SF :: CR OF :: nil)
(undef_regs (map preg_of destroyed_at_call) rs0))
# EAX <- Vundef #PC <- (rs0 RA) #RA <- Vundef →
∀
(Hnextblock: getLogEventNB (e) = Some nb)
(LIFT_NEXTBLOCK: mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat (Mem.nextblock m) % nat) = m´)
(MUpdate: if (decide (curid = current_thread)) then mset´ = (m´, snd mset)
else mset´ = (fst mset, m´)),
iestep ge (IEState curid rsm mset dp l) E0
(IEState curid (ZMap.set curid (Running rs´) rsm) mset´ dp l´).
Context (active_threads : list Z).
An active main thread is initialized as usual, other active
threads start out in the Available state, and non-active threads
are assigned to be Environment threads.
Inductive ieinitial_state {F V} (p: AST.program F V): iestate → Prop :=
| ieinitial_state_intro:
∀ m0,
Genv.init_mem p = Some m0 →
let rsm := initial_map Environment (init_regset (Genv.globalenv p)) active_threads in
let dm := initial_map None (fun i ⇒ Some (thread_init_dproc i)) active_threads in
let dmem := (m0, m0) in
ieinitial_state p (IEState main_thread rsm dmem dm nil).
Definition iefinal_state: iestate → int → Prop :=
fun _ _ ⇒ False.
Definition iesemantics (p: program) :=
Smallstep.Semantics iestep (ieinitial_state p) iefinal_state (Genv.globalenv p).
Section Properties.
Context `{extcallsx: !ExternalCallsXDefined L}.
Context `{norepet: CompCertBuiltins.BuiltinIdentsNorepet}.
Instance iexternalcall_prf:
ExternalCalls (mwd (cdata PData)) (external_calls_ops:= ec_ops).
Proof.
eapply compatlayer_extcall_strong; assumption.
Defined.
Lemma ieasm_semantics_single_events:
∀ p, single_events (iesemantics p).
Proof.
intros p s t s´ Hstep; inv Hstep; auto.
- inv H5; eapply external_call_trace_length; eauto.
- inv H6; eapply external_call_trace_length; eauto.
- inv H5; eapply external_call_trace_length; eauto.
- destruct H4 as [? [? [? [? [? Hsem]]]]]; inv Hsem; auto.
Qed.
Lemma ieasm_semantics_receptive:
∀ p, receptive (iesemantics p).
Proof.
intros; constructor.
- inversion 1; subst; try solve [inversion 1; subst; eauto].
+ destruct mset, mset´.
case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
intros. inv H6.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. econstructor; eauto.
rewrite Hdec; reflexivity.
econstructor; eauto.
rewrite Hdec; reflexivity.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
intros. inv H6.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. econstructor; eauto.
rewrite Hdec; reflexivity.
econstructor; eauto.
rewrite Hdec; reflexivity.
+ destruct mset, mset´.
case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
intros. inv H7.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply ieexec_step_annot; eauto.
rewrite Hdec; reflexivity.
econstructor; eauto.
rewrite Hdec; reflexivity.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
intros. inv H7.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply ieexec_step_annot; eauto.
rewrite Hdec; reflexivity.
econstructor; eauto.
rewrite Hdec; reflexivity.
+ destruct mset, mset´.
case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
intros. inv H6.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply ieexec_step_external; eauto.
rewrite Hdec; reflexivity.
econstructor; eauto.
rewrite Hdec; reflexivity.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
intros. inv H6.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply ieexec_step_external; eauto.
rewrite Hdec; reflexivity.
econstructor; eauto.
rewrite Hdec; reflexivity.
+ destruct mset, mset´.
case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
intros. inv H5.
destruct H6 as [?[?[?[? Hsem]]]]; subst.
inv Hsem. inv H1. eauto.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
intros. inv H5.
destruct H6 as [?[?[?[? Hsem]]]]; subst.
inv Hsem. inv H1. eauto.
- apply ieasm_semantics_single_events.
Qed.
Inductive sprimitive_call : stencil → regset → mwd (cdata PData) →
regset → mwd (cdata PData) → Prop :=
| sprim_intro:
∀ s rs m rs´ m´ ef ge t,
stencil_matches s ge →
primitive_call ef ge rs m t rs´ m´ →
sprimitive_call s rs m rs´ m´.
Context `{primcall_props: !PrimcallProperties sprimitive_call}.
Lemma prim_call_determ:
∀ ef ge rs m t1 t2 rs1´ rs2´ m1´ m2´,
primitive_call ef ge rs m t1 rs1´ m1´ →
primitive_call ef ge rs m t2 rs2´ m2´ →
t1 = E0 ∧ t2 = E0 ∧ rs1´ = rs2´ ∧ m1´ = m2´.
Proof.
intros until m2´; intros Hp1 Hp2.
assert (Hp1´:=Hp1).
destruct Hp1´ as [? [? [? [? [? Hp1´]]]]]; destruct Hp1´.
edestruct primitive_call_determ.
{ econstructor; [eauto | eapply Hp1]. }
{ econstructor; [eauto | eapply Hp2]. }
destruct Hp1 as [? [? [? [? [? Hp1]]]]]; inv Hp1.
destruct Hp2 as [? [? [? [? [? Hp2]]]]]; inv Hp2; auto.
Qed.
Lemma val2Lval_determ:
∀ v v1 v2,
val2Lval v v1 → val2Lval v v2 → v1 = v2.
Proof.
destruct v; inversion 1; inversion 1; auto.
Qed.
Lemma val2Lval_list_determ:
∀ l l1 l2,
val2Lval_list l l1 → val2Lval_list l l2 → l1 = l2.
Proof.
induction l; simpl; inversion 1; inversion 1; subst; auto.
assert (v´ = v´0) by (eapply val2Lval_determ; eauto).
assert (l´ = l´0) by (eapply IHl; eauto); subst; auto.
Qed.
Lemma external_call´_primitive_call:
∀ WB ef ge m rs1 rs2 t1 t2 rs1´ rs2´ m1´ m2´,
external_call´ WB ef ge rs1 m t1 rs1´ m1´ →
primitive_call ef ge rs2 m t2 rs2´ m2´ → False.
Proof.
intros until m2´; intros Hx Hp.
destruct Hp as [? [? [? [? [? Hp]]]]]; subst.
destruct Hx as [? Hx].
destruct Hx as [? [? Hx]]; rewrite_inv.
destruct Hx as [? [? [? [? [? ?]]]]]; subst; inv Hp.
Qed.
Import Events.
Lemma ieasm_semantics_determinate:
∀ p, determinate (iesemantics p).
Proof.
intros; constructor.
- intros s t1 s1 t2 s2 Hstep1 Hstep2.
inv Hstep1.
+
destruct mset, mset´.
case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
split; auto; try constructor.
intros.
simpl in ×.
rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
rewrite H5 in H18.
inv H18.
auto.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
split; auto; try constructor.
intros.
simpl in ×.
rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
rewrite H5 in H18.
inv H18.
auto.
+
destruct mset, mset´.
case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
destruct H5 as [? Hx1]; destruct H18 as [? Hx2].
rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
destruct H5 as [? Hx1]; destruct H18 as [? Hx2].
rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence.
+
destruct mset, mset´.
case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
destruct H6 as [? Hx1]; destruct H20 as [? Hx2].
assert (vargs = vargs0) by (eapply annot_arguments_determ; eauto); subst.
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
destruct H6 as [? Hx1]; destruct H20 as [? Hx2].
assert (vargs = vargs0) by (eapply annot_arguments_determ; eauto); subst.
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence.
+
destruct mset, mset´.
case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
{ destruct H5 as [? Hx1]; destruct H18 as [? Hx2].
assert (args = args0) by (eapply extcall_arguments_determ; eauto); subst.
subdestruct; try (destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2)
as [? Heq]; split; auto;
assert (l´ = l´0) by (subdestruct; try contradiction; subst; auto); subst;
intro Ht; destruct (Heq Ht); subst; congruence; fail).
destruct NON_YIELD as (largs & choice & H1 & H2 & H5).
destruct NON_YIELD0 as (largs0 & choice0 & H1´ & H2´ & H5´).
assert (largs = largs0) by (eapply val2Lval_list_determ; eauto); subst.
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence. }
{ rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
assert False by (eapply external_call´_primitive_call; eauto); contradiction. }
{ subdestruct; contradiction. }
{ subdestruct; contradiction. }
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
{ destruct H5 as [? Hx1]; destruct H18 as [? Hx2].
assert (args = args0) by (eapply extcall_arguments_determ; eauto); subst.
subdestruct; try (destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2)
as [? Heq]; split; auto;
assert (l´ = l´0) by (subdestruct; try contradiction; subst; auto); subst;
intro Ht; destruct (Heq Ht); subst; congruence; fail).
destruct NON_YIELD as (largs & choice & H1 & H2 & H5).
destruct NON_YIELD0 as (largs0 & choice0 & H1´ & H2´ & H5´).
assert (largs = largs0) by (eapply val2Lval_list_determ; eauto); subst.
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence. }
{ rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
assert False by (eapply external_call´_primitive_call; eauto); contradiction. }
{ subdestruct; contradiction. }
{ subdestruct; contradiction. }
+
destruct mset, mset´.
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
{ rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
rewrite Hdec in MOrigin0, MUpdate0; simpl in MOrigin0, MUpdate0; inv MOrigin0.
assert False by (eapply external_call´_primitive_call; eauto); contradiction. }
{ rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
rewrite Hdec in MOrigin0, MUpdate0; simpl in MOrigin0, MUpdate0; inv MOrigin0.
assert False by (eapply external_call´_primitive_call; eauto); contradiction. }
× case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
{ rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
rewrite Hdec in MOrigin0, MUpdate0; simpl in MOrigin0, MUpdate0; inv MOrigin0.
destruct (prim_call_determ _ _ _ _ _ _ _ _ _ _ H4 H16) as [? [? [? Heq]]]; inv Heq.
assert (l´ = l´0) by (subdestruct; try contradiction; subst; auto); subst.
split; auto; constructor. }
{ rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin; inv MUpdate.
rewrite Hdec in MOrigin0, MUpdate0; simpl in MOrigin0, MUpdate0; inv MOrigin0.
destruct (prim_call_determ _ _ _ _ _ _ _ _ _ _ H4 H16) as [? [? [? Heq]]]; inv Heq.
assert (l´ = l´0) by (subdestruct; try contradiction; subst; auto); subst.
split; auto; constructor. }
× subdestruct; contradiction.
× subdestruct; contradiction.
+
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× subdestruct; contradiction.
× subdestruct; contradiction.
× case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
{ rewrite Hdec in MOrigin; simpl in MOrigin; inv MOrigin.
rewrite Hdec in MOrigin0; simpl in MOrigin0; inv MOrigin0.
split; auto.
{ constructor. } }
{ rewrite Hdec in MOrigin; simpl in MOrigin; inv MOrigin.
rewrite Hdec in MOrigin0; simpl in MOrigin0; inv MOrigin0.
split; auto.
{ constructor. } }
× subdestruct; try contradiction.
{ subst; discriminate. }
{ subst; discriminate. }
+
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× subdestruct; contradiction.
× subdestruct; contradiction.
× subdestruct; try contradiction.
{ subst; discriminate. }
{ subst; discriminate. }
× case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
{ rewrite Hdec in MOrigin; simpl in MOrigin; inv MOrigin.
rewrite Hdec in MOrigin0; simpl in MOrigin0; inv MOrigin0.
assert (i = i0).
{
exploit extcall_arguments_determ; [eapply Hargs | eapply Hargs0 |..].
inversion 1; auto.
}
subst; split; auto; constructor. }
{ rewrite Hdec in MOrigin; simpl in MOrigin; inv MOrigin.
rewrite Hdec in MOrigin0; simpl in MOrigin0; inv MOrigin0.
assert (i = i0).
{
exploit extcall_arguments_determ; [eapply Hargs | eapply Hargs0 |..].
inversion 1; auto.
}
subst; split; auto; constructor. }
+
inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
× split; auto; constructor.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [nb_last_op_solve|exec_contr].
case_eq (decide (proc_id (uRData l) = current_thread)); intros ? Hdec.
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
rewrite Hdec in MOrigin0, MUpdate0; simpl in MOrigin0, MUpdate0; inv MOrigin0.
destruct H as [[? ?] | ?]; try congruence.
{ split; [constructor | intros _].
destruct H7 as [[? ?] | ?]; try congruence. }
{ split; [constructor | intros _].
destruct H7 as [[? ?] | ?]; try congruence. }
× rewrite Hdec in MOrigin, MUpdate; simpl in MOrigin, MUpdate; inv MOrigin.
rewrite Hdec in MOrigin0, MUpdate0; simpl in MOrigin0, MUpdate0; inv MOrigin0.
destruct H as [[? ?] | ?]; try congruence.
{ split; [constructor | intros _].
destruct H7 as [[? ?] | ?]; try congruence. }
{ split; [constructor | intros _].
destruct H7 as [[? ?] | ?]; try congruence. }
- apply ieasm_semantics_single_events.
- simpl; intros s1 s2 Hs1 Hs2.
inv Hs1; inv Hs2.
subst rsm rsm0.
subst dm dm0.
subst dmem dmem0.
rewrite H0 in H; inv H.
congruence.
- simpl; intros s r Hf t s´ Hstep; inv Hf.
- simpl; intros s r1 r2 Hr1 Hr2; inv Hr1; inv Hr2.
Qed.
End Properties.
End ESemantics.