Library mcertikos.conlib.conmtlib.TAsm
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 Import SingleConfiguration.
Section WithOracle.
Context `{s_oracle : SingleConfiguration}.
Fixpoint get_env_log (n: nat) (curid: Z) (l: Log) :=
match n with
| O ⇒ None
| S n ⇒
if zeq (proc_id (uRData l)) curid then
Some l
else
get_env_log n curid (Single_Oracle l:: l)
end.
End WithOracle.
Section TSemantics.
Context `{s_config : 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.
Inductive tstate: Type :=
| TState: Z → regset → mem → dproc → Log → tstate.
Inductive tstep (ge: genv) : tstate → trace → tstate → Prop :=
| texec_step_internal:
∀ b ofs f i (rs: regset) m m´ d d´ ds´ rs´ curid l,
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´)) →
tstep ge (TState curid rs m d l) E0
(TState curid rs´ m´ d´ l)
| texec_step_builtin:
∀ b ofs f ef args res (rs: regset) m m´ d d´ ds´ t vl rs´ curid l,
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,
tstep ge (TState curid rs m d l) t
(TState curid rs´ m´ d´ l)
| texec_step_annot:
∀ b ofs f ef args (rs: regset) m m´ d d´ ds´ vargs t v curid l,
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,
tstep ge (TState curid rs m d l) t
(TState curid (nextinstr rs) m´ d´ l)
| texec_step_external:
∀ b ef args res (rs: regset) m m´ d d´ ds´ t rs´ curid l l´,
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,
tstep ge (TState curid rs m d l) t
(TState curid rs´ m´ d´ l´)
| texec_step_prim_call:
∀ b ef (rs: regset) m m´ d d´ ds´ t rs´ curid l l´,
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,
tstep ge (TState curid rs m d l) t
(TState curid rs´ m´ d´ l´)
| texec_step_external_yield:
∀ b ef (rs0 rs´: regset) (m m´: mem) curid s l l´ l´´ l´´´ nb d e,
proc_id (uRData l) = curid →
rs0 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 →
get_env_log limit curid l´ = Some l´´ →
last_op l´´ = Some e →
state_check thread_yield nil l d →
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)
(NON_YIELD: match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end)
(LIFT_NEXTBLOCK: mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat(Mem.nextblock m) % nat) = m´),
tstep ge (TState curid rs0 m d l) E0
(TState curid rs´ m´ d l´´´)
| texec_step_external_sleep:
∀ b ef (rs0 rs´: regset) (m m´: mem) curid s l l´ l´´ l´´´ nb d e i,
proc_id (uRData l) = curid →
rs0 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 →
get_env_log limit curid l´ = Some l´´ →
last_op l´´ = Some e →
state_check thread_sleep (Lint i::nil) l d →
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)
(Hargs: extcall_arguments rs0 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)
(LIFT_NEXTBLOCK: mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat (Mem.nextblock m) % nat) = m´),
tstep ge (TState curid rs0 m d l) E0
(TState curid rs´ m´ d l´´´).
Definition tfinal_state : tstate → int → Prop :=
fun _ _ ⇒ False.
Definition init_dproc :=
if zeq main_thread current_thread then main_init_dproc else nomain_init_dproc.
Inductive tinitial_state {F V} (p: AST.program F V): tstate → Prop :=
| tinitial_state_intro:
∀ m0 m1 rs0,
Genv.init_mem p = Some m0 →
init_mem_lift_nextblock m0 = m1 →
initial_thread_state (Genv.globalenv p) current_thread init_log = Some rs0 →
tinitial_state p (TState current_thread rs0 m1 (thread_init_dproc current_thread) init_log).
Definition tsemantics (p: program) :=
Smallstep.Semantics tstep (tinitial_state p) tfinal_state (Genv.globalenv p).
Section Properties.
Context `{extcallsx: !ExternalCallsXDefined L}.
Context `{norepet: CompCertBuiltins.BuiltinIdentsNorepet}.
Instance externalcall_prf:
ExternalCalls (mwd (cdata PData)) (external_calls_ops:= ec_ops).
Proof.
eapply compatlayer_extcall_strong; assumption.
Defined.
Lemma tasm_semantics_single_events:
∀ p, single_events (tsemantics p).
Proof.
intros p s t s´ Hstep; inv Hstep; auto.
- inv H4; eapply external_call_trace_length; eauto.
- inv H5; eapply external_call_trace_length; eauto.
- inv H4; eapply external_call_trace_length; eauto.
- destruct H3 as [? [? [? [? [? Hsem]]]]]; inv Hsem; auto.
Qed.
Lemma tasm_semantics_receptive:
∀ p, receptive (tsemantics p).
Proof.
intros; constructor.
- inversion 1; subst; try solve [inversion 1; subst; eauto].
+ intros. inv H5.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. econstructor; eauto. econstructor; eauto.
+ intros. inv H6.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply texec_step_annot; eauto. econstructor; eauto.
+ intros. inv H5.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply texec_step_external; eauto. econstructor; eauto.
+ intros. inv H4.
destruct H5 as [?[?[?[? Hsem]]]]; subst.
inv Hsem. inv H0. eauto.
- apply tasm_semantics_single_events.
Qed.
Ltac rewrite_inv :=
repeat match goal with
| [ H : ?a = _, H´ : ?a = _ |- _ ] ⇒
rewrite H´ in H; inv H
end.
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.
Ltac exec_contr :=
match goal with
| [ H: exec_instr _ _ _ _ _ = _ |- _ ] ⇒ inv H
end.
Import Events.
Lemma tasm_semantics_determinate:
∀ p, determinate (tsemantics p).
Proof.
intros; constructor.
- intros s t1 s1 t2 s2 Hstep1 Hstep2.
inv Hstep1.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
split; auto; constructor.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
destruct H4 as [? Hx1]; destruct H16 as [? Hx2].
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
destruct H5 as [? Hx1]; destruct H18 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.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
× destruct H4 as [? Hx1]; destruct H16 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 & Ha & Hb & Hc).
destruct NON_YIELD0 as (largs0 & choice0 & Ha´ & Hb´ & Hc´).
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.
× assert False by (eapply external_call´_primitive_call; eauto); contradiction.
× subdestruct; contradiction.
× subdestruct; contradiction.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
× assert False by (eapply external_call´_primitive_call; eauto); contradiction.
× destruct (prim_call_determ _ _ _ _ _ _ _ _ _ _ H3 H14) 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 [exec_contr].
× subdestruct; contradiction.
× subdestruct; contradiction.
× split; auto.
constructor.
× subdestruct; try contradiction.
subst; discriminate.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
× subdestruct; contradiction.
× subdestruct; contradiction.
× subdestruct; try contradiction.
subst; discriminate.
× assert (i = i0).
{
exploit extcall_arguments_determ; [eapply Hargs | eapply Hargs0 |..].
inversion 1; auto.
}
subst; rewrite_inv; split; auto; constructor.
- apply tasm_semantics_single_events.
- simpl; intros s1 s2 Hs1 Hs2.
inv Hs1; inv Hs2.
congruence.
- contradiction.
- simpl; intros s r1 r2 Hr1 Hr2; inv Hr1; inv Hr2; congruence.
Qed.
End Properties.
End TSemantics.
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 Import SingleConfiguration.
Section WithOracle.
Context `{s_oracle : SingleConfiguration}.
Fixpoint get_env_log (n: nat) (curid: Z) (l: Log) :=
match n with
| O ⇒ None
| S n ⇒
if zeq (proc_id (uRData l)) curid then
Some l
else
get_env_log n curid (Single_Oracle l:: l)
end.
End WithOracle.
Section TSemantics.
Context `{s_config : 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.
Inductive tstate: Type :=
| TState: Z → regset → mem → dproc → Log → tstate.
Inductive tstep (ge: genv) : tstate → trace → tstate → Prop :=
| texec_step_internal:
∀ b ofs f i (rs: regset) m m´ d d´ ds´ rs´ curid l,
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´)) →
tstep ge (TState curid rs m d l) E0
(TState curid rs´ m´ d´ l)
| texec_step_builtin:
∀ b ofs f ef args res (rs: regset) m m´ d d´ ds´ t vl rs´ curid l,
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,
tstep ge (TState curid rs m d l) t
(TState curid rs´ m´ d´ l)
| texec_step_annot:
∀ b ofs f ef args (rs: regset) m m´ d d´ ds´ vargs t v curid l,
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,
tstep ge (TState curid rs m d l) t
(TState curid (nextinstr rs) m´ d´ l)
| texec_step_external:
∀ b ef args res (rs: regset) m m´ d d´ ds´ t rs´ curid l l´,
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,
tstep ge (TState curid rs m d l) t
(TState curid rs´ m´ d´ l´)
| texec_step_prim_call:
∀ b ef (rs: regset) m m´ d d´ ds´ t rs´ curid l l´,
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,
tstep ge (TState curid rs m d l) t
(TState curid rs´ m´ d´ l´)
| texec_step_external_yield:
∀ b ef (rs0 rs´: regset) (m m´: mem) curid s l l´ l´´ l´´´ nb d e,
proc_id (uRData l) = curid →
rs0 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 →
get_env_log limit curid l´ = Some l´´ →
last_op l´´ = Some e →
state_check thread_yield nil l d →
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)
(NON_YIELD: match ef with
| EF_external id _ ⇒
if peq id thread_yield then True
else False
| _ ⇒ False
end)
(LIFT_NEXTBLOCK: mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat(Mem.nextblock m) % nat) = m´),
tstep ge (TState curid rs0 m d l) E0
(TState curid rs´ m´ d l´´´)
| texec_step_external_sleep:
∀ b ef (rs0 rs´: regset) (m m´: mem) curid s l l´ l´´ l´´´ nb d e i,
proc_id (uRData l) = curid →
rs0 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 →
get_env_log limit curid l´ = Some l´´ →
last_op l´´ = Some e →
state_check thread_sleep (Lint i::nil) l d →
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)
(Hargs: extcall_arguments rs0 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)
(LIFT_NEXTBLOCK: mem_lift_nextblock m (Pos.to_nat (nb) - Pos.to_nat (Mem.nextblock m) % nat) = m´),
tstep ge (TState curid rs0 m d l) E0
(TState curid rs´ m´ d l´´´).
Definition tfinal_state : tstate → int → Prop :=
fun _ _ ⇒ False.
Definition init_dproc :=
if zeq main_thread current_thread then main_init_dproc else nomain_init_dproc.
Inductive tinitial_state {F V} (p: AST.program F V): tstate → Prop :=
| tinitial_state_intro:
∀ m0 m1 rs0,
Genv.init_mem p = Some m0 →
init_mem_lift_nextblock m0 = m1 →
initial_thread_state (Genv.globalenv p) current_thread init_log = Some rs0 →
tinitial_state p (TState current_thread rs0 m1 (thread_init_dproc current_thread) init_log).
Definition tsemantics (p: program) :=
Smallstep.Semantics tstep (tinitial_state p) tfinal_state (Genv.globalenv p).
Section Properties.
Context `{extcallsx: !ExternalCallsXDefined L}.
Context `{norepet: CompCertBuiltins.BuiltinIdentsNorepet}.
Instance externalcall_prf:
ExternalCalls (mwd (cdata PData)) (external_calls_ops:= ec_ops).
Proof.
eapply compatlayer_extcall_strong; assumption.
Defined.
Lemma tasm_semantics_single_events:
∀ p, single_events (tsemantics p).
Proof.
intros p s t s´ Hstep; inv Hstep; auto.
- inv H4; eapply external_call_trace_length; eauto.
- inv H5; eapply external_call_trace_length; eauto.
- inv H4; eapply external_call_trace_length; eauto.
- destruct H3 as [? [? [? [? [? Hsem]]]]]; inv Hsem; auto.
Qed.
Lemma tasm_semantics_receptive:
∀ p, receptive (tsemantics p).
Proof.
intros; constructor.
- inversion 1; subst; try solve [inversion 1; subst; eauto].
+ intros. inv H5.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. econstructor; eauto. econstructor; eauto.
+ intros. inv H6.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply texec_step_annot; eauto. econstructor; eauto.
+ intros. inv H5.
exploit external_call_receptive; eauto.
intros [? [[? [? ?]] ?]]. esplit. eapply texec_step_external; eauto. econstructor; eauto.
+ intros. inv H4.
destruct H5 as [?[?[?[? Hsem]]]]; subst.
inv Hsem. inv H0. eauto.
- apply tasm_semantics_single_events.
Qed.
Ltac rewrite_inv :=
repeat match goal with
| [ H : ?a = _, H´ : ?a = _ |- _ ] ⇒
rewrite H´ in H; inv H
end.
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.
Ltac exec_contr :=
match goal with
| [ H: exec_instr _ _ _ _ _ = _ |- _ ] ⇒ inv H
end.
Import Events.
Lemma tasm_semantics_determinate:
∀ p, determinate (tsemantics p).
Proof.
intros; constructor.
- intros s t1 s1 t2 s2 Hstep1 Hstep2.
inv Hstep1.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
split; auto; constructor.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
destruct H4 as [? Hx1]; destruct H16 as [? Hx2].
destruct (external_call_determ _ _ _ _ _ _ _ _ _ _ _ Hx1 Hx2) as [? Heq]; split; auto.
intro Ht; destruct (Heq Ht); congruence.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
destruct H5 as [? Hx1]; destruct H18 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.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
× destruct H4 as [? Hx1]; destruct H16 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 & Ha & Hb & Hc).
destruct NON_YIELD0 as (largs0 & choice0 & Ha´ & Hb´ & Hc´).
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.
× assert False by (eapply external_call´_primitive_call; eauto); contradiction.
× subdestruct; contradiction.
× subdestruct; contradiction.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
× assert False by (eapply external_call´_primitive_call; eauto); contradiction.
× destruct (prim_call_determ _ _ _ _ _ _ _ _ _ _ H3 H14) 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 [exec_contr].
× subdestruct; contradiction.
× subdestruct; contradiction.
× split; auto.
constructor.
× subdestruct; try contradiction.
subst; discriminate.
+ inv Hstep2; rewrite_inv; try contradiction; try solve [exec_contr].
× subdestruct; contradiction.
× subdestruct; contradiction.
× subdestruct; try contradiction.
subst; discriminate.
× assert (i = i0).
{
exploit extcall_arguments_determ; [eapply Hargs | eapply Hargs0 |..].
inversion 1; auto.
}
subst; rewrite_inv; split; auto; constructor.
- apply tasm_semantics_single_events.
- simpl; intros s1 s2 Hs1 Hs2.
inv Hs1; inv Hs2.
congruence.
- contradiction.
- simpl; intros s r1 r2 Hr1 Hr2; inv Hr1; inv Hr2; congruence.
Qed.
End Properties.
End TSemantics.