Library mcertikos.multicore.refins.AsmLAsmtoSepSem
Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Events.
Require Import Globalenvs.
Require Import Conventions.
Require Import AuxLemma.
Require Import GlobIdent.
Require Import Smallstep.
Require Import CommonTactic.
Require Import Coq.Logic.FunctionalExtensionality.
Require Import AuxFunctions.
Require Import LAsm.
Require Import GlobalOracle.
Require Import liblayers.compat.CompatLayers.
Require Import MBoot.
Require Import RealParams.
Require Import AbstractDataType.
Require Import FlatMemory.
Require Import Decision.
Require Import LAsmModuleSem.
Require Import Soundness.
Require Import CompatExternalCalls.
Require Import LinkTactic.
Require Import I64Layer.
Require Import StencilImpl.
Require Import MakeProgram.
Require Import MakeProgramImpl.
Require Import LAsmModuleSemAux.
Require Import liblayers.compat.CompatGenSem.
Require Import TacticsForTesting.
Require Import Concurrent_Linking_Lib.
Require Import Concurrent_Linking_Def.
Require Import Concurrent_Linking_Prop.
Require Import HWSemImpl.
Require Import ConcurrentOracle.
Require Import SeparateSemImpl.
Section LinkwithLAsm.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).
Local Open Scope Z_scope.
Context `{pmap: PartialMap}.
Context `{zset_op: ZSet_operation}.
Existing Instance hdseting.
Existing Instance op_sep.
Context `{mc_oracle_cond: MCLinkOracleCond (mem := mem) (memory_model_ops := memory_model_ops) (Hmwd := Hmwd)
(Hmem := Hmem) (real_params_ops := real_params_ops)
(oracle_ops0 := oracle_ops0) (oracle_ops := oracle_ops) (big_ops := big_ops)
(builtin_idents_norepet_prf := builtin_idents_norepet_prf)
(zset_op := zset_op) (pmap := pmap)}.
Section WITH_GE.
Variables (ge: genv) (sten: stencil) (M: module).
Context {Hmakege: make_globalenv (module_ops:= LAsm.module_ops) (mkp_ops:= make_program_ops)
sten M (mboot ⊕ L64) = ret ge}.
Lemma oget_exists:
∀ cid c l ml l0 id
(Hrel_log : relate_log_pool l ml)
(Hid: ZMap.get id ml = MultiDef l0)
(Hfake: ¬ fake_atomic_primitive_without_switch_points c),
∃ l´, oget (OracleProp:= op_sep) (s_set cid) (id, ZMap.get id l, c) sep_oracle = Some l´
∧ relate_log (ZMap.get id multi_oracle_init0 cid l0 ++ l0) (l´ ++ ZMap.get id l).
Proof.
intros. inv Hrel_log. pose proof (Hrel id) as Hrel´.
rewrite Hid in Hrel´. inv Hrel´.
exploit (fake_oracle_assumption id cid c); eauto.
intros (l1 & Hget & _).
specialize (relate_oracle_correct).
exploit relate_oracle_correct; eauto.
Qed.
Lemma oget_exists´:
∀ cid c l ml l0 id
(Hrel_log : relate_log_pool l ml)
(Hid: ZMap.get id ml = MultiDef l0)
(Hfake: fake_atomic_primitive_without_switch_points c),
oget (OracleProp:= op_sep) (s_set cid) (id, ZMap.get id l, c) sep_oracle = Some nil
∧ relate_log l0 (ZMap.get id l).
Proof.
intros. inv Hrel_log. pose proof (Hrel id) as Hrel´.
rewrite Hid in Hrel´. inv Hrel´.
exploit (fake_oracle_assumption id cid c); eauto.
intros (l1 & Hget & Hasum). exploit Hasum; eauto.
intros; subst. eauto.
Qed.
Lemma oget_exists´´:
∀ cid c l ml id
(Hrel_log : relate_log_pool l ml),
∃ l´, oget (OracleProp:= op_sep) (s_set cid) (id, ZMap.get id l, c) sep_oracle = Some l´.
Proof.
intros. inv Hrel_log. pose proof (Hrel id) as Hrel´.
exploit (fake_oracle_assumption id cid c); eauto.
intros (l1 & Hget & _). eauto.
Qed.
Lemma relate_log_pool_gss:
∀ gl ml id l l0
(Hrel: relate_log_pool gl ml)
(Hrel_l: relate_log l0 l),
relate_log_pool (ZMap.set id l gl) (ZMap.set id (MultiDef l0) ml).
Proof.
intros. inv Hrel.
econstructor. intros.
destruct (zeq id id0); subst.
- repeat rewrite ZMap.gss.
constructor. trivial.
- repeat rewrite ZMap.gso; eauto.
Qed.
Lemma relate_log_pool_acq:
∀ l ml z c l0
(Hrel_log : relate_log_pool l ml)
(Hget: ZMap.get z ml = MultiDef l0),
relate_log_pool
(ZMap.set z (SEACQ c :: nil ++ ZMap.get z l) l)
(ZMap.set z (MultiDef (TEVENT c (TSHARED OPULL) :: l0)) ml).
Proof.
intros. inv Hrel_log.
constructor. intros. pose proof (Hrel id) as Hrel´.
inv Hrel´.
- destruct (zeq id z); subst.
+ congruence.
+ repeat rewrite ZMap.gso; eauto.
- simpl. destruct (zeq id z); subst.
+ repeat rewrite ZMap.gss. econstructor; eauto.
constructor; eauto. rewrite <- H0 in Hget. inv Hget. trivial.
+ repeat rewrite ZMap.gso; eauto.
Qed.
Ltac subdestruct_if´ term :=
match term with
| context [if ?con then _ else _] ⇒
progress subdestruct_if´ con
| context [match ?con with
| _ ⇒ _
end] ⇒ progress subdestruct_if´ con
| _ ⇒ let H := fresh "Hdestruct" in
destruct term eqn:H
end.
Ltac subdestruct´ :=
repeat progress
(match goal with
| HT:context [if ?con then _ else _] |- _ ⇒
subdestruct_if´ con; simpl in HT; try solve [discriminate HT]
| HT:context [match ?con with | _ ⇒ _ end] |- _ ⇒
subdestruct_if´ con; simpl in HT; try solve [discriminate HT]
end; simpl).
Ltac subdestruct_one´ :=
match goal with
| HT:context [if ?con then _ else _]
|- _ ⇒ subdestruct_if´ con; simpl in HT; try solve [discriminate HT]
| HT:context [match ?con with
| _ ⇒ _
end] |- _ ⇒ subdestruct_if´ con; simpl in HT; try solve [discriminate HT]
end; simpl.
Lemma CalValidBit_relate:
∀ l l´ t z
(Hrel: relate_log l l´)
(Hvalid: CalValidBit l = Some t),
match t with
| FreeToPull ⇒ ∃ d, CalOwner (separate_log_type_2_log l´ z) z = OFREE d
| PullBy i ⇒ CalOwner (separate_log_type_2_log l´ z) z = (OWN i)
end.
Proof.
induction l; simpl; intros.
- inv Hvalid. inv Hrel. simpl. eauto.
- destruct a. destruct (CalValidBit l) eqn: Hind; try (inv Hvalid; fail).
destruct s; eauto.
+ inv Hrel. inv Hrel_e.
specialize (IHl _ _ z Hrel_l refl_equal). simpl in IHl.
destruct IHl as (d & Hcal).
destruct e; inv H0; inv Hvalid.
× destruct e; inv H1; eauto.
× destruct e; inv H1; inv H0; eauto.
simpl. rewrite zeq_true. rewrite Hcal. eauto.
+ inv Hrel.
specialize (IHl _ _ z Hrel_l refl_equal).
simpl in IHl.
inv Hrel_e.
destruct e; inv Hvalid.
× destruct e; inv H0; simpl; eauto.
× destruct e; inv H0; inv H1.
destruct (zeq i0 i); subst; eauto.
{
inv H0. simpl; eauto.
rewrite IHl; repeat rewrite zeq_true; repeat rewrite zeq_false; eauto.
}
{ inv H0. }
{ simpl. trivial. }
Qed.
Lemma CalOwner_free_relate´:
∀ l l´ z d
(Hbit: CalValidBit l = Some FreeToPull)
(Hcal: ∃ d, CalOwner (separate_log_type_2_log l´ z) z = OFREE d)
(Hrel: relate_log l l´)
(Hshare: GetSharedMemEvent l = d),
CalOwner (separate_log_type_2_log l´ z) z = OFREE (d).
Proof.
induction l; simpl; intros.
- inv Hrel. simpl. trivial.
- simpl in ×. destruct a. destruct (CalValidBit l) eqn: Hbit´; try (inv Hbit; fail).
destruct Hcal as (d´ & Hcal).
inv Hrel. inv Hrel_e.
destruct e; inv H0.
+ destruct s; inv Hbit.
destruct e; inv H1; simpl in *; eauto.
+ destruct e; inv H1.
× destruct s; inv Hbit.
destruct (zeq i0 i); subst; inv H0.
simpl in ×. repeat rewrite zeq_true in ×.
destruct (CalOwner (separate_log_type_2_log l1 z) z) eqn: Hcal´; inv Hcal.
{
eapply (CalValidBit_relate _ l1 _ z) in Hbit´; eauto.
simpl in Hbit´. congruence.
}
{
destruct (zeq i0 i); subst; inv H0.
trivial.
}
× destruct s; inv Hbit.
simpl in Hcal. exploit IHl; eauto.
× destruct s; inv Hbit.
Qed.
Lemma CalOwner_free_relate:
∀ l l´ z d
(Hbit: CalValidBit l = Some FreeToPull)
(Hrel: relate_log l l´)
(Hshare: GetSharedMemEvent l = d),
CalOwner (separate_log_type_2_log l´ z) z = OFREE (d).
Proof.
intros.
pose proof Hbit as Hcal.
eapply (CalValidBit_relate _ l´ _ z) in Hcal; eauto. simpl in Hcal.
eapply CalOwner_free_relate´; eauto.
Qed.
The only way exec_instr can change the abstract data is to
access it with exec_load or exec_store, hence we prove that
any property on the data that is preserved by them is also
preserved by exec_instr as a whole.
Lemma exec_instr_data f i rs rs´ m m´ a a´ P:
(∀ chunk am r,
exec_loadex ge chunk (m, a) am rs r = Next rs´ (m´, a´) → P a´) →
(∀ chunk am r rr,
exec_storeex ge chunk (m, a) am rs r rr = Next rs´ (m´, a´) → P a´) →
P a →
exec_instr ge f i rs (m, a) = Next rs´ (m´, a´) →
P a´.
Proof.
clear.
intros HPload HPstore Ha Hinstr.
Because inversion is very slow at QED time, we try to use
this lemma instead whenever possible.
assert (∀ rs´´ m´´, Next rs´´ (m´´, a) = Next rs´ (m´, a´) → P a´)
as Hinv
by congruence.
assert (Stuck = Next rs´ (m´, a´) → P a´)
as Hdiscr
by discriminate.
destruct i; [destruct i | ..];
simpl in Hinstr;
repeat
lazymatch type of Hinstr with
| context [@goto_label] ⇒
unfold goto_label in Hinstr
| context [match ?x with _ ⇒ _ end] ⇒
let Hx := fresh in destruct x eqn:Hx
end;
eauto; try congruence.
- lift_unfold.
unfold π_data in ×.
destruct H, H0, H1.
inversion Hinstr.
subst.
simpl in ×.
congruence.
- lift_unfold.
unfold π_data in ×.
destruct H2.
inversion Hinstr.
subst.
simpl in ×.
congruence.
Fail idtac.
Qed.
as Hinv
by congruence.
assert (Stuck = Next rs´ (m´, a´) → P a´)
as Hdiscr
by discriminate.
destruct i; [destruct i | ..];
simpl in Hinstr;
repeat
lazymatch type of Hinstr with
| context [@goto_label] ⇒
unfold goto_label in Hinstr
| context [match ?x with _ ⇒ _ end] ⇒
let Hx := fresh in destruct x eqn:Hx
end;
eauto; try congruence.
- lift_unfold.
unfold π_data in ×.
destruct H, H0, H1.
inversion Hinstr.
subst.
simpl in ×.
congruence.
- lift_unfold.
unfold π_data in ×.
destruct H2.
inversion Hinstr.
subst.
simpl in ×.
congruence.
Fail idtac.
Qed.
Now we can use the above lemma to prove some of the properties
we need about exec_instr.
Ltac reduce_access H :=
repeat
match type of H with
| _ ⇒
progress unfold
exec_loadex,
exec_storeex,
LoadStoreSem1.exec_loadex1,
LoadStoreSem1.exec_storeex1,
HostAccess1.exec_host_load1,
HostAccess1.exec_host_store1,
FlatLoadStoreSem.exec_flatmem_load,
FlatLoadStoreSem.exec_flatmem_store,
PageFault.exec_pagefault,
GuestAccessIntel1.exec_guest_intel_load1,
GuestAccessIntel1.exec_guest_intel_store1,
GuestAccessIntel1.load_accessor1,
GuestAccessIntel1.store_accessor1,
GuestAccessIntelDef0.exec_guest_intel_accessor1,
Asm.exec_load,
Asm.exec_store,
flatmem_store´,
trapinfo_set,
goto_label
in ×
| context [match ?x with _ ⇒ _ end] ⇒
let Hx := fresh in destruct x eqn:Hx
| context [Pregmap.set _ (FlatMem.load ?chunk ?b ?ofs) _] ⇒
destruct (FlatMem.load chunk b ofs)
end.
Lemma exec_instr_unchanged:
∀ f i rs rs´ m m´ a a´
(Hinstr: exec_instr ge f i rs (m, a) = Next rs´ (m´, a´)),
multi_log a´ = multi_log a
∧ CPU_ID a´ = CPU_ID a
∧ multi_oracle a´ = multi_oracle a.
Proof.
intros.
Again, because inversion is very slow at QED time, we try to
use these lemmas instead.
assert (∀ P,
Stuck = Next (mem := mwd LDATAOps) rs´ (m´, a´) →
P)
as Hdiscr
by discriminate.
assert (∀ rs´´ m´´ T (f: _ → T),
Next rs´´ (m´´, a) = Next (mem := mwd LDATAOps) rs´ (m´, a´) →
f a´ = f a)
as Hinv
by congruence.
pattern a´.
eapply exec_instr_data; eauto.
- clear Hinstr. intros chunk am r Hload.
reduce_access Hload;
first
[ eapply Hdiscr; eassumption
| eauto ];
(inv Hload; eauto; fail).
- clear.
intros chunk am r rr Hstore.
reduce_access Hstore;
try solve
[ eapply Hdiscr; eassumption
| eauto
| inv Hstore; simpl; eauto ].
+ destruct m0 as [m0 a0].
lift_unfold.
destruct H2.
assert (a´ = a) by congruence.
subst.
eauto.
Fail idtac.
Qed.
Lemma exec_external_builtin_data_unchanged:
∀ ef WB args vl t m m´
(BUILTIN_ENABLED: match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end)
(Hm´: external_call´ (mem := mwd LDATAOps) WB ef ge args m t vl m´),
snd m´ = snd m.
Proof.
intros.
destruct Hm´.
revert H.
destruct ef; try contradiction; destruct 1; eauto.
- destruct H; eauto.
lift_unfold.
destruct H1.
unfold π_data in *; simpl in ×.
congruence.
- destruct H1; eauto.
lift_unfold.
destruct H2.
unfold π_data in *; simpl in ×.
congruence.
- lift_unfold.
destruct H, H1.
unfold π_data in *; simpl in ×.
congruence.
- lift_unfold.
destruct H2.
unfold π_data in *; simpl in ×.
congruence.
- lift_unfold.
destruct H7.
unfold π_data in *; simpl in ×.
congruence.
Qed.
Lemma exec_external_buildin_unchanged:
∀ ef WB args vl t m m´ a a´
(Hinstr: external_call´ (mem:= mwd LDATAOps) WB ef ge args (m, a) t vl (m´, a´))
(BUILTIN_ENABLED: match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
multi_log a´ = multi_log a
∧ CPU_ID a´ = CPU_ID a
∧ multi_oracle a´ = multi_oracle a.
Proof.
intros.
change a with (snd (m, a)).
change a´ with (snd (m´, a´)).
erewrite exec_external_builtin_data_unchanged; eauto.
Qed.
Stuck = Next (mem := mwd LDATAOps) rs´ (m´, a´) →
P)
as Hdiscr
by discriminate.
assert (∀ rs´´ m´´ T (f: _ → T),
Next rs´´ (m´´, a) = Next (mem := mwd LDATAOps) rs´ (m´, a´) →
f a´ = f a)
as Hinv
by congruence.
pattern a´.
eapply exec_instr_data; eauto.
- clear Hinstr. intros chunk am r Hload.
reduce_access Hload;
first
[ eapply Hdiscr; eassumption
| eauto ];
(inv Hload; eauto; fail).
- clear.
intros chunk am r rr Hstore.
reduce_access Hstore;
try solve
[ eapply Hdiscr; eassumption
| eauto
| inv Hstore; simpl; eauto ].
+ destruct m0 as [m0 a0].
lift_unfold.
destruct H2.
assert (a´ = a) by congruence.
subst.
eauto.
Fail idtac.
Qed.
Lemma exec_external_builtin_data_unchanged:
∀ ef WB args vl t m m´
(BUILTIN_ENABLED: match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end)
(Hm´: external_call´ (mem := mwd LDATAOps) WB ef ge args m t vl m´),
snd m´ = snd m.
Proof.
intros.
destruct Hm´.
revert H.
destruct ef; try contradiction; destruct 1; eauto.
- destruct H; eauto.
lift_unfold.
destruct H1.
unfold π_data in *; simpl in ×.
congruence.
- destruct H1; eauto.
lift_unfold.
destruct H2.
unfold π_data in *; simpl in ×.
congruence.
- lift_unfold.
destruct H, H1.
unfold π_data in *; simpl in ×.
congruence.
- lift_unfold.
destruct H2.
unfold π_data in *; simpl in ×.
congruence.
- lift_unfold.
destruct H7.
unfold π_data in *; simpl in ×.
congruence.
Qed.
Lemma exec_external_buildin_unchanged:
∀ ef WB args vl t m m´ a a´
(Hinstr: external_call´ (mem:= mwd LDATAOps) WB ef ge args (m, a) t vl (m´, a´))
(BUILTIN_ENABLED: match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
multi_log a´ = multi_log a
∧ CPU_ID a´ = CPU_ID a
∧ multi_oracle a´ = multi_oracle a.
Proof.
intros.
change a with (snd (m, a)).
change a´ with (snd (m´, a´)).
erewrite exec_external_builtin_data_unchanged; eauto.
Qed.
Next we want to prove that any calls to builtins are
insensitive to the log. As for exec_external_buildin_unchanged,
it is in fact the case that they are insensitive to the whole
abstract state. Since they also leave it unchanged, we can boil
this down to the following lemma.
Lemma exec_external_builtin_data:
∀ ef WB args vl t m1 m1´ a2
(Hm´: external_call´ (mem:= mwd LDATAOps) WB ef ge args m1 t vl m1´)
(BUILTIN_ENABLED: match ef with
| EF_external _ _ ⇒ False
| _ ⇒ True
end),
external_call´ WB ef ge args (fst m1, a2) t vl (fst m1´, a2).
Proof.
intros.
destruct Hm´.
eapply external_call´_intro with (v0 := v); eauto.
revert H.
destruct ef; try contradiction; simpl;
destruct 1; try solve [ econstructor; eauto ].
- eapply CompCertBuiltins.builtin_sem_i64_sub; eauto.
- eapply CompCertBuiltins.builtin_sem_i64_mul; eauto.
- constructor.
destruct H; constructor; eauto.
- constructor.
destruct H; constructor; eauto.
lift_unfold.
destruct H1.
eauto.
- econstructor; eauto.
destruct H1; constructor; eauto.
- econstructor; eauto.
destruct H1; constructor; eauto.
lift_unfold.
destruct H2.
eauto.
- ∃ (fst m´, a2).
+ lift_unfold.
destruct H.
eauto.
+ lift_unfold.
destruct H1.
eauto.
- econstructor; eauto.
lift_unfold.
destruct H2.
eauto.
- econstructor; eauto.
lift_unfold.
destruct H7.
eauto.
Qed.
Complement the get_layer_eqn_inversion tactic to deal with
memory accessors and unfolding named layers.
Lemma get_layer_primitive_eqn_accessors D i acc:
∀ r,
get_layer_primitive (D:=D) i (accessors ↦ acc) = OK (Some r) →
False.
Proof.
intro r.
change (get_layer_primitive (D:=D) i (∅ ⊕ ∅) = OK (Some r) → False).
get_layer_normalize.
discriminate.
Qed.
Ltac get_layer_eqn_inversion´ H :=
let continue tac H :=
lazymatch type of H with
| get_layer_primitive _ (accessors ↦ _) = _ ⇒
apply get_layer_primitive_eqn_accessors in H; solve [destruct H]
| get_layer_primitive _ ?layer = _ ⇒
let layer´ := eval red in layer in
change layer with layer´ in H;
tac H
| ?T ⇒
fail "Can't handle:" T
end in
get_layer_eqn_inversion_tac continue H.
Unfold f in H : f x1 x2 ... xn = y
Ltac unfold_eq_left_head H :=
let rec uh t := lazymatch t with ?a ?b ⇒ uh a | ?c ⇒ unfold c in H end in
lazymatch type of H with ?x = ?y ⇒ uh x end.
Ltac destruct_eq_left_matched H :=
lazymatch type of H with
| match ?x with _ ⇒ _ end = ?y ⇒
let Heqn := fresh in
destruct x eqn:Heqn;
destruct_eq_left_matched H
| _ ⇒
idtac
end.
Lemma compatsem_private_unchanged:
∀ name σe s WB vargs m vres m´,
private_id name →
get_layer_primitive name (mboot ⊕ L64) = OK (Some (inl σe)) →
sextcall_primsem_step _ σe s WB vargs m vres m´ →
multi_log (snd m´) = multi_log (snd m) ∧
CPU_ID (snd m´) = CPU_ID (snd m) ∧
multi_oracle (snd m´) = multi_oracle (snd m).
Proof.
intros name σe s WB vargs m vres m´ Hname Hσe Hstep.
red in Hname.
repeat
match type of Hname with
| if ?c then _ else _ ⇒
destruct c; try contradiction
end.
clear Hname.
get_layer_eqn_inversion´ Hσe;
destruct Hσe as [Hname Hσe];
inversion Hσe; clear Hσe;
try contradiction;
subst;
simpl in Hstep;
CompatGenSem.inv_generic_sem Hstep;
eauto;
unfold_eq_left_head H0;
destruct_eq_left_matched H0;
inversion H0; simpl; eauto.
- unfold_eq_left_head H.
destruct_eq_left_matched H;
inversion H; simpl; eauto.
- unfold_eq_left_head H.
destruct_eq_left_matched H;
inversion H; subst; simpl in *; eauto.
destruct d; subst; simpl in *; eauto.
- unfold_eq_left_head H.
destruct_eq_left_matched H;
inversion H; subst; simpl in *; eauto.
- unfold_eq_left_head H1.
destruct_eq_left_matched H1;
inversion H1; subst; simpl in *; eauto.
- unfold_eq_left_head H1.
destruct_eq_left_matched H1;
inversion H1; subst; simpl in *; eauto.
Fail idtac.
Qed.
Lemma exec_external_private_unchanged:
∀ ef WB args vl t m m´ a a´
(Hinstr: external_call´ (mem:= mwd LDATAOps) WB ef ge args (m, a) t vl (m´, a´))
(BUILTIN_ENABLED: match ef with
| EF_external eid _ ⇒
private_id eid
| _ ⇒ False
end),
multi_log a´ = multi_log a
∧ CPU_ID a´ = CPU_ID a
∧ multi_oracle a´ = multi_oracle a.
Proof.
intros.
destruct Hinstr as [? Hec].
destruct ef; try contradiction.
repeat red in Hec.
destruct Hec as (σ & Hσ & Hσsem).
destruct Hσsem as (s & σe & Hs & Hstep & Hσe & Hsg & Ht); subst.
eapply compatsem_private_unchanged in Hstep; eauto.
Qed.
Lemma private_imply_atomic:
∀ name x
(Hneq: ¬ private_id name)
(Hget: get_layer_primitive name (mboot ⊕ L64) = OK (Some x)),
atomic_id name ∨ name = atomic_FAI ∨ name = acquire_shared ∨ name = release_shared.
Proof.
unfold private_id, atomic_id; intros.
Opaque sep_oracle.
destruct (peq name acquire_shared); [subst; auto |].
destruct (peq name release_shared); [subst; auto |].
destruct (peq name atomic_FAI); [subst; auto |].
destruct (peq name log_get); [subst; auto |].
destruct (peq name log_incr); [subst; auto |].
destruct (peq name log_hold); [subst; auto |].
destruct (peq name log_init); [subst; auto |].
destruct (peq name page_copy); [subst; auto |].
elim Hneq; auto.
Qed.
Lemma sprimcall_ext_false:
∀ x sg WB F V ge args m t v m´,
¬ compatsem_extcall (D:= LDATAOps) (inr x) sg WB F V ge args m t v m´.
Proof.
red; intros. inv H.
destruct H0 as (? & _ & _ & HF´ & _). inv HF´.
Qed.
Lemma extcall_no_primcall D (σ: compatsem D) σe rs m t rs´ m´:
σ = inl σe →
¬ compatsem_primcall_sem σ ge rs m t rs´ m´.
Proof.
intros Hσ Hstep.
subst.
inversion Hstep.
Qed.
Lemma primcall_private_unchanged:
∀ (ge: genv) name m m´ a a´ σ rs rs´ t
(Hsem: get_layer_primitive (D:= LDATAOps) name (mboot ⊕ L64)
= OK (Some σ))
(Hprivate: private_id name)
(Hexe: compatsem_primcall_sem σ ge rs (m, a) t rs´ (m´, a´)),
multi_log a´ = multi_log a
∧ CPU_ID a´ = CPU_ID a
∧ multi_oracle a´ = multi_oracle a.
Proof.
intros.
red in Hprivate.
repeat
match type of Hprivate with
| if ?c then _ else _ ⇒
destruct c; try contradiction
end.
clear Hprivate.
get_layer_eqn_inversion´ Hsem;
destruct Hsem as [Hname Hσe];
try contradiction;
try solve [ eapply extcall_no_primcall in Hexe; [destruct Hexe | eauto] ];
At this point we have 8 primitives left.
subst;
inversion Hexe; clear Hexe; subst;
lazymatch goal with
| H: sprimcall_step _ _ _ _ _ _ |- _ ⇒
simpl in H;
inversion H; clear H; subst
end;
eauto;
lazymatch goal with
| H: _ = Some a´ |- _ ⇒
unfold_eq_left_head H;
destruct_eq_left_matched H;
try discriminate H;
inversion H; clear H; subst
| _ ⇒ idtac
end;
eauto.
inversion Hexe; clear Hexe; subst;
lazymatch goal with
| H: sprimcall_step _ _ _ _ _ _ |- _ ⇒
simpl in H;
inversion H; clear H; subst
end;
eauto;
lazymatch goal with
| H: _ = Some a´ |- _ ⇒
unfold_eq_left_head H;
destruct_eq_left_matched H;
try discriminate H;
inversion H; clear H; subst
| _ ⇒ idtac
end;
eauto.
restore_context_spec has a special format
unfold_eq_left_head H5.
destruct_eq_left_matched H5;
inversion H5;
eauto.
Fail idtac.
Qed.
Inductive match_state_link : mstate → sp_state → Prop :=
| match_state_link_intro:
∀ rs m a l
(Hrel_log: relate_log_pool l (multi_log a))
(Hrel_CPU_ID: CPU_ID a = current_CPU_ID)
(Hrel_multi_oracle: multi_oracle a = multi_oracle_init0)
,
match_state_link (Asm.State rs (m, a))
(SPState (Asm.State (mem:= mwd LDATAOps) rs (m, a)) l).
destruct_eq_left_matched H5;
inversion H5;
eauto.
Fail idtac.
Qed.
Inductive match_state_link : mstate → sp_state → Prop :=
| match_state_link_intro:
∀ rs m a l
(Hrel_log: relate_log_pool l (multi_log a))
(Hrel_CPU_ID: CPU_ID a = current_CPU_ID)
(Hrel_multi_oracle: multi_oracle a = multi_oracle_init0)
,
match_state_link (Asm.State rs (m, a))
(SPState (Asm.State (mem:= mwd LDATAOps) rs (m, a)) l).
We want to show that running builtin external function will
leave the log and CPU_ID unchanged. In the case of builtins we
can actually prove the stronger property that it will leave the
data unchanged.
Definition single_separate_step_aux´ :=
@single_separate_step_aux mem memory_model_ops Hmem Hmwd
real_params_ops oracle_ops0 oracle_ops big_ops
builtin_idents_norepet_prf zset_op mc_oracle
ge sten M Hmakege.
Hint Unfold single_separate_step_aux´.
Lemma step_relation_link:
∀ s1 s1´ s2 t
(Hstep: step ge s1 t s1´)
(Hmatch: match_state_link s1 s2),
∃ s2´,
single_separate_step_aux´ s2 t s2´ ∧
match_state_link s1´ s2´.
Proof.
unfold single_separate_step_aux.
intros. inv Hmatch.
destruct s1´.
inv Hstep; subst; intros.
-
destruct m0 as (m´, a1´).
refine_split´; eauto.
+ eapply single_exec_step_progress_separate_local; eauto.
econstructor.
× eapply command_internal; eauto.
× eapply private_step_internal; eauto.
+ eapply exec_instr_unchanged in H7; eauto.
destruct H7 as (Hel & Hec & Ho).
econstructor; eauto; congruence.
-
destruct (ef_OK ef) as [[]|] eqn:Hcase.
+ destruct m0 as (m´, a1´).
exploit exec_external_E0; eauto. intros; subst.
refine_split´; eauto.
× eapply single_exec_step_progress_separate_local; eauto.
econstructor.
eapply command_internal; eauto.
eapply private_step_builtin; eauto.
× eapply exec_external_buildin_unchanged in H7; eauto.
destruct H7 as (Hel & Hec & Ho).
econstructor; eauto; congruence.
+ assert (Hcon: instr_OK (Pbuiltin ef args res) = OK tt) by
(eapply (make_globalenv_instr_OK (make_program_prf:= make_program_prf)); eassumption).
simpl in Hcon; rewrite Hcase in Hcon; discriminate.
-
destruct (ef_OK ef) as [[]|] eqn:Hcase.
+ destruct m0 as (m´, a1´).
exploit exec_external_E0; eauto. intros; subst.
refine_split´; eauto.
× eapply single_exec_step_progress_separate_local; eauto.
econstructor.
eapply command_internal; eauto.
eapply private_step_annot; eauto.
× eapply exec_external_buildin_unchanged in H8; eauto.
destruct H8 as (Hel & Hec & Ho).
econstructor; eauto; congruence.
+ assert (Hcon: instr_OK (Pannot ef args) = OK tt) by
(eapply (make_globalenv_instr_OK (make_program_prf:= make_program_prf)); eassumption).
simpl in Hcon; rewrite Hcase in Hcon; discriminate.
-
destruct (ef_or ef) as [HF | HF].
+
eapply make_globalenv_find_funct_ptr in H4; eauto.
destruct H4 as [i [Hfs [Hcase|Hcase]]].
× destruct Hcase as [? [_ ?]].
simpl in *; destruct (instrs_OK (fn_code x)); discriminate.
× destruct Hcase as [? [_ Hme]].
inv Hme; inv HF.
+
destruct ef eqn: Hef; subst; try solve [inv HF].
destruct m0 as (m´, a1´).
exploit exec_external_E0; eauto. clear HF; intros; subst.
destruct (private_id_dec name).
×
refine_split´; eauto.
{
eapply single_exec_step_progress_separate_local; eauto.
econstructor.
{
eapply command_prim_private; eauto.
}
{
eapply private_step_external; eauto.
}
}
{
eapply exec_external_private_unchanged in H7; eauto.
destruct H7 as (Hel & Hec & Ho).
econstructor; eauto.
{ rewrite Hel. trivial. }
{ rewrite Hec; trivial. }
{ rewrite Ho; trivial. }
}
×
inv H7. inv H.
destruct H0 as (Hget & Hsem).
exploit private_imply_atomic; eauto.
intros Hname.
destruct Hname as [Hatom | [HFAI | [HACQ | HREL]]]; subst.
{
unfold atomic_id in ×.
subdestruct´; subst.
- assert (HF: get_layer_primitive log_get (mboot ⊕ L64) =
OK (Some (primcall_atomic_GET_compatsem log_get_spec))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hget. inv Hget.
eapply sprimcall_ext_false in Hsem. inv Hsem.
-
assert (HF: get_layer_primitive log_incr (mboot ⊕ L64) =
OK (Some (gensem log_incr_spec))).
{
reflexivity.
}
pose proof Hsem as Hsem´.
unfold ident in ×.
rewrite HF in Hget. inv Hget.
destruct Hsem as (s & σ & Hstencil & Hsem & Heq & Hsg & _); subst.
clear HF.
inv Heq; simpl in ×.
inv Hsem. inv_generic_sem H5.
destruct args; [discriminate|].
destruct args; [discriminate|].
inv Hargs.
pose proof H0 as Hspec.
unfold log_incr_spec in H0.
subdestruct´; inv H0.
exploit (oget_exists´ current_CPU_ID log_incr); eauto.
intros (Hget & Hrel).
refine_split´; trivial.
+ eapply single_exec_step_progress_separate_log; eauto.
{
instantiate (2:= SEATOMIC current_CPU_ID OINC_NOW).
eapply Hget.
}
eapply separate_local_exec_step_atomic; eauto.
{
eapply command_prim_atomic; eauto.
simpl. intro HF. inv HF.
}
{
eapply atomic_step_external; eauto.
- econstructor; eauto.
econstructor; eauto.
split; eauto. trivial.
- simpl. rewrite ZMap.gss. simpl. trivial.
}
+ econstructor; eauto.
× eapply relate_log_pool_gss; eauto. rewrite Hrel_CPU_ID.
simpl. econstructor; eauto.
-
assert (HF: get_layer_primitive log_hold (mboot ⊕ L64) =
OK (Some (gensem log_hold_spec))).
{
reflexivity.
}
pose proof Hsem as Hsem´.
unfold ident in ×.
rewrite HF in Hget. inv Hget.
destruct Hsem as (s & σ & Hstencil & Hsem & Heq & Hsg & _); subst.
clear HF.
inv Heq; simpl in ×.
inv Hsem. inv_generic_sem H5.
destruct args; [discriminate|].
destruct args; [discriminate|].
inv Hargs.
pose proof H0 as Hspec.
unfold log_hold_spec in H0.
subdestruct´; inv H0.
exploit (oget_exists´ current_CPU_ID log_hold); eauto.
intros (Hget & Hrel).
refine_split´; trivial.
+ eapply single_exec_step_progress_separate_log; eauto.
{
instantiate (2:= SEATOMIC current_CPU_ID OHOLD_LOCK).
eapply Hget.
}
eapply separate_local_exec_step_atomic; eauto.
{
eapply command_prim_atomic; eauto.
simpl. intro HF. inv HF.
}
{
eapply atomic_step_external; eauto.
- econstructor; eauto.
econstructor; eauto.
split; eauto. trivial.
- simpl. rewrite ZMap.gss. simpl. trivial.
}
+ econstructor; eauto.
× eapply relate_log_pool_gss; eauto. rewrite Hrel_CPU_ID.
simpl. econstructor; eauto.
-
assert (HF: get_layer_primitive log_init (mboot ⊕ L64) =
OK (Some (gensem log_init_spec))).
{
reflexivity.
}
pose proof Hsem as Hsem´.
unfold ident in ×.
rewrite HF in Hget. inv Hget.
destruct Hsem as (s & σ & Hstencil & Hsem & Heq & Hsg & _); subst.
clear HF.
inv Heq; simpl in ×.
inv Hsem. inv_generic_sem H5.
destruct args; [discriminate|].
destruct args; [discriminate|].
inv Hargs.
pose proof H0 as Hspec.
unfold log_init_spec in H0.
subdestruct´; inv H0.
exploit (oget_exists´´ current_CPU_ID log_init); eauto.
intros (l´ & Hget).
refine_split´; trivial.
+ eapply single_exec_step_progress_separate_log; eauto.
{
instantiate (2:= SEATOMIC current_CPU_ID OINIT).
eapply Hget.
}
eapply separate_local_exec_step_atomic; eauto.
{
eapply command_prim_atomic; eauto.
simpl. intro HF. inv HF.
}
{
eapply atomic_step_external; eauto.
- econstructor; eauto.
econstructor; eauto.
split; eauto. trivial.
- simpl. rewrite ZMap.gss. simpl. trivial.
}
+ econstructor; eauto.
× eapply relate_log_pool_gss; eauto.
simpl in Hget.
unfold ZIndexed.t, ident in Hget.
destruct (sep_oracle (z, ZMap.get z l, log_init)) eqn: Ho; try congruence.
destruct p.
eapply sep_oget_init in Ho. destruct Ho as (-> & ->).
destruct (s_set current_CPU_ID z0); inv Hget.
simpl. econstructor; eauto.
-
assert (HF: get_layer_primitive page_copy (mboot ⊕ L64) =
OK (Some (gensem page_copy´´´_spec))).
{
reflexivity.
}
pose proof Hsem as Hsem´.
unfold ident in ×.
rewrite HF in Hget. inv Hget.
destruct Hsem as (s & σ & Hstencil & Hsem & Heq & Hsg & _); subst.
clear HF.
inv Heq; simpl in ×.
inv Hsem. inv_generic_sem H5.
destruct args; [discriminate|].
destruct args; [discriminate|].
destruct args; [discriminate|].
inv Hargs.
pose proof H0 as Hspec.
unfold page_copy´´´_spec in H0.
subdestruct´; inv H0.
exploit (oget_exists´ current_CPU_ID page_copy); eauto.
intros (Hget & Hrel).
refine_split´; trivial.
+ eapply single_exec_step_progress_separate_log; eauto.
{
instantiate (2:= SEATOMIC current_CPU_ID (OPAGE_COPY l1)).
eapply Hget.
}
eapply separate_local_exec_step_atomic; eauto.
{
eapply command_prim_page_copy; eauto.
}
{
eapply atomic_step_external; eauto.
- econstructor; eauto.
econstructor; eauto.
split; eauto. trivial.
- simpl. rewrite ZMap.gss. simpl. trivial.
}
+ econstructor; eauto.
× eapply relate_log_pool_gss; eauto. rewrite Hrel_CPU_ID.
simpl. econstructor; eauto.
- inv Hatom.
}
{
assert (HF: get_layer_primitive atomic_FAI (mboot ⊕ L64) =
OK (Some (primcall_atomic_FAI_compatsem atomic_FAI_spec))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hget. inv Hget.
eapply sprimcall_ext_false in Hsem. inv Hsem.
}
{
assert (HF: get_layer_primitive acquire_shared (mboot ⊕ L64) =
OK (Some (primcall_acquire_shared_compatsem acquire_shared0_spec0))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hget. inv Hget.
eapply sprimcall_ext_false in Hsem. inv Hsem.
}
{
assert (HF: get_layer_primitive release_shared (mboot ⊕ L64) =
OK (Some (primcall_release_lock_compatsem release_shared release_shared0_spec0))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hget. inv Hget.
eapply sprimcall_ext_false in Hsem. inv Hsem.
}
-
destruct H6 as (name & sg & σ & ? & Hlayer & Hsem); subst.
destruct m0 as (m´, a1´).
pose proof Hsem as Hsem´.
inv Hsem.
destruct (private_id_dec name).
× refine_split´; eauto.
{
eapply single_exec_step_progress_separate_local; eauto.
econstructor.
{
eapply command_prim_private; eauto.
}
{
eapply private_step_prim_call; eauto.
econstructor; eauto.
}
}
{
eapply primcall_private_unchanged in Hsem´; eauto.
destruct Hsem´ as (Hel & Hec & Ho).
econstructor; eauto.
{ rewrite Hel. trivial. }
{ rewrite Hec; trivial. }
{ rewrite Ho; trivial. }
}
×
exploit private_imply_atomic; eauto.
intros Hname.
destruct Hname as [Hatom | [HFAI | [HACQ | HREL]]]; subst.
{
unfold atomic_id in ×.
subdestruct´; subst.
-
assert (HF: get_layer_primitive log_get (mboot ⊕ L64) =
OK (Some (primcall_atomic_GET_compatsem log_get_spec))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hlayer. inv Hlayer.
clear HF. simpl in ×.
inv Hsem´. inv H3.
pose proof Hspec as Hspec´.
unfold log_get_spec in Hspec´.
subdestruct´; inv Hspec´. inv Hpos.
exploit (oget_exists current_CPU_ID log_get); eauto.
intros (l´ & Hget & Hrel).
refine_split´; trivial.
+ eapply single_exec_step_progress_separate_log; eauto.
{
instantiate (2:= SEATOMIC current_CPU_ID OGET_NOW).
eapply Hget.
}
pose proof Harg as Harg´.
eapply (extcall_args_with_data (D:= LDATAOps) a) in Harg.
eapply separate_local_exec_step_atomic; eauto.
{
eapply command_prim_atomic; eauto.
simpl. intro HF. inv HF.
}
{
eapply atomic_step_prim_call; eauto.
- econstructor; eauto.
refine_split´; eauto.
+ instantiate (1:= (primcall_atomic_GET_compatsem log_get_spec)).
trivial.
+ econstructor; eauto.
econstructor; eauto.
- simpl. rewrite ZMap.gss. simpl. trivial.
}
+ econstructor; eauto.
eapply relate_log_pool_gss; eauto. subrewrite´.
simpl. econstructor; eauto.
-
assert (HF: get_layer_primitive log_incr (mboot ⊕ L64) =
OK (Some (gensem log_incr_spec))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hlayer. inv Hlayer.
-
assert (HF: get_layer_primitive log_hold (mboot ⊕ L64) =
OK (Some (gensem log_hold_spec))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hlayer. inv Hlayer.
-
assert (HF: get_layer_primitive log_init (mboot ⊕ L64) =
OK (Some (gensem log_init_spec))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hlayer. inv Hlayer.
-
assert (HF: get_layer_primitive page_copy (mboot ⊕ L64) =
OK (Some (gensem page_copy´´´_spec))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hlayer. inv Hlayer.
- inv Hatom.
}
{
assert (HF: get_layer_primitive atomic_FAI (mboot ⊕ L64) =
OK (Some (primcall_atomic_FAI_compatsem atomic_FAI_spec))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hlayer. inv Hlayer.
clear HF. simpl in ×.
inv Hsem´. inv H3.
pose proof Hspec as Hspec´.
unfold atomic_FAI_spec in Hspec´.
subdestruct´; inv Hspec´. inv Hpos.
exploit (oget_exists current_CPU_ID atomic_FAI); eauto.
intros (l´ & Hget & Hrel).
pose proof Harg as Harg´.
eapply (extcall_args_with_data (D:= LDATAOps) a) in Harg.
refine_split´; trivial.
+ eapply single_exec_step_progress_separate_log; eauto.
{
instantiate (2:= SEATOMIC current_CPU_ID (OINC_TICKET (Z.to_nat (Int.unsigned bound)))).
eapply Hget.
}
eapply separate_local_exec_step_atomic; eauto.
{
eapply command_prim_FAI; eauto.
simpl. rewrite peq_true; trivial.
}
{
eapply atomic_step_prim_call; eauto.
- econstructor; eauto.
refine_split´; eauto.
+ instantiate (1:= (primcall_atomic_FAI_compatsem atomic_FAI_spec)).
trivial.
+ econstructor; eauto.
econstructor; eauto.
- simpl. rewrite ZMap.gss. simpl. trivial.
}
+ econstructor; eauto.
eapply relate_log_pool_gss; eauto. subrewrite´.
simpl. econstructor; eauto.
}
{
assert (HF: get_layer_primitive acquire_shared (mboot ⊕ L64) =
OK (Some (primcall_acquire_shared_compatsem acquire_shared0_spec0))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hlayer. inv Hlayer.
clear HF. simpl in ×.
inv Hsem´. inv H3. inv H0.
rename H8 into Hspec.
pose proof Hspec as Hspec´.
unfold acquire_shared0_spec in Hspec´.
d5 subdestruct_one´.
exploit (oget_exists´ current_CPU_ID acquire_shared); eauto.
{
reflexivity.
}
intros (Hget & Hrel).
rename H17 into Harg.
pose proof Harg as Harg´.
eapply (extcall_args_with_data (D:= LDATAOps) a) in Harg.
specialize (extcall_arguments_determ _ _ _ _ _ H15 Harg´).
intros Hl. inv Hl.
repeat Equalities.
subdestruct´; try solve [discriminate Hspec´].
- inv Hspec´.
refine_split´; trivial.
+ eapply single_exec_step_progress_separate_log; eauto.
{
instantiate (2:= SEACQ current_CPU_ID).
eapply Hget.
}
eapply separate_local_exec_step_acq; eauto.
{
eapply acq_prim_call; eauto.
reflexivity.
}
{ instantiate (1:= Some l3).
eapply CalOwner_free_relate; eauto.
}
{
destruct (id2size (Int.unsigned index0)) as [[size id´]|] eqn:Hsi.
- econstructor.
+ inv H.
erewrite stencil_matches_symbols; eauto.
+ instantiate (1 := size).
instantiate (1 := index0).
revert Hdestruct2 Hsi.
clear.
destruct (Int.unsigned _); try discriminate; simpl.
× inversion 1.
inversion 1.
reflexivity.
× destruct p; try discriminate.
destruct p; try discriminate.
solve [ inversion 1; inversion 1; reflexivity ].
solve [ inversion 1; inversion 1; reflexivity ].
+ instantiate (1:= m´).
lift_simpl. eauto.
+ eauto.
+ eapply Harg´.
+ eauto.
+ eauto.
- exfalso.
revert Hdestruct2 Hsi.
clear.
destruct (Int.unsigned _); try discriminate.
destruct p; try discriminate.
destruct p; try discriminate.
}
+ econstructor; eauto. rewrite Hrel_CPU_ID.
eapply relate_log_pool_acq; eauto.
- inv Hspec´; subst.
refine_split´; trivial.
+ eapply single_exec_step_progress_separate_log; eauto.
{
instantiate (2:= SEACQ current_CPU_ID).
eapply Hget.
}
eapply separate_local_exec_step_acq; eauto.
{
eapply acq_prim_call; eauto.
reflexivity.
}
{
instantiate (1:= None).
eapply CalOwner_free_relate; eauto.
}
{
destruct (id2size (Int.unsigned index0)) as [[size id´]|] eqn:Hsi.
- econstructor.
+ inv H.
erewrite stencil_matches_symbols; eauto.
+ instantiate (1 := size).
instantiate (1 := index0).
revert Hdestruct2 Hsi.
clear.
destruct (Int.unsigned _); try discriminate; simpl.
× inversion 1.
inversion 1.
reflexivity.
× destruct p; try discriminate.
destruct p; try discriminate.
solve [ inversion 1; inversion 1; reflexivity ].
solve [ inversion 1; inversion 1; reflexivity ].
+ reflexivity.
+ eauto.
+ eauto.
+ eauto.
+ eauto.
- exfalso.
revert Hdestruct2 Hsi.
clear.
destruct (Int.unsigned _); try discriminate.
destruct p; try discriminate.
destruct p; try discriminate.
}
+ econstructor; eauto. rewrite Hrel_CPU_ID.
eapply relate_log_pool_acq; eauto.
}
{
assert (HF: get_layer_primitive release_shared (mboot ⊕ L64) =
OK (Some (primcall_release_lock_compatsem release_shared release_shared0_spec0))).
{
reflexivity.
}
unfold ident in ×.
rewrite HF in Hlayer. inv Hlayer.
clear HF. simpl in ×.
inv Hsem´. inv H3. inv H0.
rename H7 into Hspec.
pose proof Hspec as Hspec´.
unfold release_shared0_spec in Hspec´.
subdestruct´. inv Hspec´.
exploit (oget_exists´ current_CPU_ID release_shared); eauto.
{
reflexivity.
}
intros (Hget & Hrel).
rename H18 into Harg.
pose proof Harg as Harg´.
eapply (extcall_args_with_data (D:= LDATAOps) a) in Harg.
refine_split´; trivial.
+ eapply single_exec_step_progress_separate_log; eauto.
{
instantiate (2:= SEREL current_CPU_ID l1).
eapply Hget.
}
eapply separate_local_exec_step_rel; eauto.
{
eapply rel_prim_call; eauto.
- rewrite H4 in HPC0. inv HPC0. eauto.
- reflexivity.
}
{
eapply (CalValidBit_relate _ (ZMap.get z l) _ z) in Hdestruct4; eauto.
simpl in Hdestruct4. simpl. rewrite Hdestruct4. rewrite Hrel_CPU_ID.
trivial.
}
{
specialize (extcall_arguments_determ _ _ _ _ _ H16 Harg´).
intros Hl. inv Hl.
repeat Equalities.
econstructor; eauto.
- inv H.
erewrite stencil_matches_symbols; eauto.
}
+ econstructor; eauto.
eapply relate_log_pool_gss; eauto. subrewrite´.
simpl. econstructor; eauto.
}
Fail idtac.
Qed.
Lemma genv_alloc_correct:
∀ gl (ge: genv) m m´ a a´
(Hgenv: Genv.alloc_globals (mem:= mwd LDATAOps) ge (m, a) gl = Some (m´, a´)),
a´ = a.
Proof.
intros.
setoid_rewrite InitMem.alloc_globals_with_data in Hgenv.
destruct (Genv.alloc_globals _ _ _); inversion Hgenv; eauto.
Qed.
End WITH_GE.
End LinkwithLAsm.
Section LinkWithLAsmSim.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet}.
Notation LDATA := RData.
Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).
Local Open Scope Z_scope.
Context `{pmap: PartialMap}.
Context `{zset_op: ZSet_operation}.
Context `{mc_oracle_cond: MCLinkOracleCond (mem := mem) (memory_model_ops := memory_model_ops) (Hmwd := Hmwd)
(Hmem := Hmem) (real_params_ops := real_params_ops)
(oracle_ops0 := oracle_ops0) (oracle_ops := oracle_ops) (big_ops := big_ops)
(builtin_idents_norepet_prf := builtin_idents_norepet_prf)
(zset_op := zset_op) (pmap := pmap)}.
Lemma single_separate_step_aux_eq :
∀ (ge:genv) sten M
(Hmakege: make_globalenv sten M (mboot ⊕ L64) = ret ge)
s t s´,
single_separate_step_aux_ge ge sten M (Hmakege:=Hmakege) ge s t s´ ↔
single_separate_step_aux ge sten M (Hmakege:=Hmakege) s t s´.
Proof.
intros; split; intros.
inversion H; auto.
constructor; auto.
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 (mboot ⊕ L64) = OK ph),
backward_simulation
(LAsm.semantics (lcfg_ops := LC (mboot ⊕ L64)) ph)
(single_separate_semantics
(Hmakege := make_program_globalenv (make_program_ops := make_program_ops) _ _ _ _ Hmakep)
(Genv.globalenv ph) s CTXT ph).
Proof.
intros. apply forward_to_backward_simulation; eauto.
- eapply forward_simulation_step with (match_states:= match_state_link); simpl; intros; trivial.
+
inv H. esplit; split.
× econstructor; eauto.
× destruct m0 as (m0, a).
unfold Genv.init_mem in H0. simpl in H0.
eapply genv_alloc_correct in H0. subst.
subst rs0.
econstructor; simpl; eauto.
econstructor; eauto.
intros.
repeat rewrite ZMap.gi; eauto. econstructor.
+ edestruct step_relation_link; eauto.
eexists; rewrite single_separate_step_aux_eq; eauto.
-
eapply lasm_semantics_receptive.
decision.
-
eapply single_separate_semantics_determinate; eauto.
Qed.
End LinkWithLAsmSim.