Library mcertikos.mcslock.MCSCurIDGen
This file provide the contextual refinement proof between PThreadInit layer and PQueueIntro layer
Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import MCSMCurID.
Require Import MCSMBoot.
Require Import MCSCurIDGenSpec.
Require Import LAsmModuleSemAux.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Asm.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import FlatMemory.
Require Import AuxStateDataType.
Require Import Constant.
Require Import GlobIdent.
Require Import RealParams.
Require Import LoadStoreSem1.
Require Import AsmImplLemma.
Require Import GenSem.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import compcert.cfrontend.Ctypes.
Require Import LayerCalculusLemma.
Require Import AbstractDataType.
Require Import DeviceStateDataType.
Require Import MCSMCurID.
Require Import MCSMBoot.
Require Import MCSCurIDGenSpec.
Require Import LAsmModuleSemAux.
Section Refinement.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mcurid_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{faireness: WaitTime}.
Local Open Scope string_scope.
Local Open Scope error_monad_scope.
Local Open Scope Z_scope.
Context `{real_params: RealParams}.
Context `{mcs_oracle_prop: MCSOracleProp}.
Notation HDATA := RData.
Notation LDATA := RData.
Notation HDATAOps := (cdata (cdata_ops := mcurid_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := mboot_data_ops) LDATA).
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Context `{faireness: WaitTime}.
Section REFINEMENT_REL.
Inductive match_CurID: stencil → (ZMap.t Z) → mem → meminj → Prop :=
| MATCH_CURID:
∀ m b f cid s,
(∀ i, 0 ≤ i < TOTAL_CPU →
∃ v,
Mem.load Mint32 m b (i × 4) = Some (Vint v)
∧ Mem.valid_access m Mint32 b (i × 4) Writable
∧ ZMap.get i cid = (Int.unsigned v))
→ find_symbol s CURID_LOC = Some b
→ match_CurID s cid m f.
Inductive match_CurID: stencil → (ZMap.t Z) → mem → meminj → Prop :=
| MATCH_CURID:
∀ m b f cid s,
(∀ i, 0 ≤ i < TOTAL_CPU →
∃ v,
Mem.load Mint32 m b (i × 4) = Some (Vint v)
∧ Mem.valid_access m Mint32 b (i × 4) Writable
∧ ZMap.get i cid = (Int.unsigned v))
→ find_symbol s CURID_LOC = Some b
→ match_CurID s cid m f.
Relation between the new raw data at the higher layer with the mememory at lower layer
Inductive match_RData: stencil → HDATA → mem → meminj → Prop :=
| MATCH_RDATA:
∀ hadt m f s,
match_CurID s (cid hadt) m f
→ match_RData s hadt m f.
| MATCH_RDATA:
∀ hadt m f s,
match_CurID s (cid hadt) m f
→ match_RData s hadt m f.
Relation between raw data at two layers
Record relate_RData (f: meminj) (hadt: HDATA) (ladt: LDATA) :=
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
MM_re: MM hadt = MM ladt;
MMSize_re: MMSize hadt = MMSize ladt;
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
init_re: init hadt = init ladt;
buffer_re: buffer hadt = buffer ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
multi_oracle_re: multi_oracle hadt = multi_oracle ladt;
multi_log_re: multi_log hadt = multi_log ladt;
com1_re: com1 ladt = com1 hadt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
saved_intr_flags_re: saved_intr_flags ladt = saved_intr_flags hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr hadt = in_intr ladt;
tf_re: tfs_inj f (tf hadt) (tf ladt)
}.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := CURID_LOC :: nil
}.
End REFINEMENT_REL.
mkrelate_RData {
flatmem_re: FlatMem.flatmem_inj (HP hadt) (HP ladt);
MM_re: MM hadt = MM ladt;
MMSize_re: MMSize hadt = MMSize ladt;
vmxinfo_re: vmxinfo hadt = vmxinfo ladt;
CR3_re: CR3 hadt = CR3 ladt;
ikern_re: ikern hadt = ikern ladt;
pg_re: pg hadt = pg ladt;
ihost_re: ihost hadt = ihost ladt;
ti_fst_re: (fst (ti hadt)) = (fst (ti ladt));
ti_snd_re: val_inject f (snd (ti hadt)) (snd (ti ladt));
init_re: init hadt = init ladt;
buffer_re: buffer hadt = buffer ladt;
CPU_ID_re: CPU_ID hadt = CPU_ID ladt;
multi_oracle_re: multi_oracle hadt = multi_oracle ladt;
multi_log_re: multi_log hadt = multi_log ladt;
com1_re: com1 ladt = com1 hadt;
ioapic_re: ioapic ladt = ioapic hadt;
lapic_re: lapic ladt = lapic hadt;
intr_flag_re: intr_flag ladt = intr_flag hadt;
saved_intr_flags_re: saved_intr_flags ladt = saved_intr_flags hadt;
curr_intr_num_re: curr_intr_num ladt = curr_intr_num hadt;
in_intr_re: in_intr hadt = in_intr ladt;
tf_re: tfs_inj f (tf hadt) (tf ladt)
}.
Global Instance rel_ops: CompatRelOps HDATAOps LDATAOps :=
{
relate_AbData s f d1 d2 := relate_RData f d1 d2;
match_AbData s d1 m f := match_RData s d1 m f;
new_glbl := CURID_LOC :: nil
}.
End REFINEMENT_REL.
Section Rel_Property.
Lemma inject_match_correct:
∀ s d1 m2 f m2´ j,
match_RData s d1 m2 f →
Mem.inject j m2 m2´ →
inject_incr (Mem.flat_inj (genv_next s)) j →
match_RData s d1 m2´ (compose_meminj f j).
Proof.
inversion 1; subst; intros.
inv H0.
assert (HFB0: j b = Some (b, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
econstructor; eauto; intros.
econstructor; eauto; intros.
specialize (H3 _ H0).
destruct H3 as (v & HLD & HV & HM).
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H1 HLD HFB0).
repeat rewrite Z.add_0_r.
intros [v1´[HLD1´ HV1´]].
inv HV1´.
refine_split´; eauto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB0 H1 HV).
rewrite Z.add_0_r; trivial.
Qed.
Lemma store_match_correct:
∀ s abd m0 m0´ f b2 v v´ chunk,
match_RData s abd m0 f →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.store chunk m0 b2 v v´ = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros. inv H. inv H2.
econstructor; eauto.
econstructor; eauto.
eapply H0 in H3; simpl; eauto.
intros. specialize (H _ H2).
destruct H as (v0 & HLD & HV & HM).
repeat rewrite (Mem.load_store_other _ _ _ _ _ _ H1); auto.
refine_split´; eauto.
eapply Mem.store_valid_access_1; eauto.
Qed.
Lemma storebytes_match_correct:
∀ s abd m0 m0´ f b2 v v´,
match_RData s abd m0 f →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.storebytes m0 b2 v v´ = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros. inv H. inv H2.
econstructor; eauto.
econstructor; eauto.
eapply H0 in H3; simpl; eauto.
intros. specialize (H _ H2).
destruct H as (v0 & HLD & HV & HM).
repeat rewrite (Mem.load_storebytes_other _ _ _ _ _ H1); eauto.
refine_split´; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
Qed.
Lemma free_match_correct:
∀ s abd m0 m0´ f ofs sz b2,
match_RData s abd m0 f→
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.free m0 b2 ofs sz = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros; inv H; inv H2.
econstructor; eauto.
econstructor; eauto.
eapply H0 in H3; simpl; eauto.
intros. specialize (H _ H2).
destruct H as (v0 & HLD & HV & HM).
repeat rewrite (Mem.load_free _ _ _ _ _ H1); auto.
refine_split´; eauto.
eapply Mem.valid_access_free_1; eauto.
Qed.
Lemma alloc_match_correct:
∀ s abd m´0 m´1 f f´ ofs sz b0 b´1,
match_RData s abd m´0 f→
Mem.alloc m´0 ofs sz = (m´1, b´1) →
f´ b0 = Some (b´1, 0%Z) →
(∀ b : block, b ≠ b0 → f´ b = f b) →
inject_incr f f´ →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b0) →
match_RData s abd m´1 f´.
Proof.
intros. rename H1 into HF1, H2 into HB. inv H; inv H1.
econstructor; eauto.
econstructor; eauto.
intros. specialize (H _ H1).
destruct H as (v0 & HLD & HV & HM).
refine_split´; eauto.
- apply (Mem.load_alloc_other _ _ _ _ _ H0); trivial.
- eapply Mem.valid_access_alloc_other; eauto.
Qed.
Lemma inject_match_correct:
∀ s d1 m2 f m2´ j,
match_RData s d1 m2 f →
Mem.inject j m2 m2´ →
inject_incr (Mem.flat_inj (genv_next s)) j →
match_RData s d1 m2´ (compose_meminj f j).
Proof.
inversion 1; subst; intros.
inv H0.
assert (HFB0: j b = Some (b, 0)).
{
eapply stencil_find_symbol_inject´; eauto.
}
econstructor; eauto; intros.
econstructor; eauto; intros.
specialize (H3 _ H0).
destruct H3 as (v & HLD & HV & HM).
specialize (Mem.load_inject _ _ _ _ _ _ _ _ _ H1 HLD HFB0).
repeat rewrite Z.add_0_r.
intros [v1´[HLD1´ HV1´]].
inv HV1´.
refine_split´; eauto.
specialize(Mem.valid_access_inject _ _ _ _ _ _ _ _ _ HFB0 H1 HV).
rewrite Z.add_0_r; trivial.
Qed.
Lemma store_match_correct:
∀ s abd m0 m0´ f b2 v v´ chunk,
match_RData s abd m0 f →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.store chunk m0 b2 v v´ = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros. inv H. inv H2.
econstructor; eauto.
econstructor; eauto.
eapply H0 in H3; simpl; eauto.
intros. specialize (H _ H2).
destruct H as (v0 & HLD & HV & HM).
repeat rewrite (Mem.load_store_other _ _ _ _ _ _ H1); auto.
refine_split´; eauto.
eapply Mem.store_valid_access_1; eauto.
Qed.
Lemma storebytes_match_correct:
∀ s abd m0 m0´ f b2 v v´,
match_RData s abd m0 f →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.storebytes m0 b2 v v´ = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros. inv H. inv H2.
econstructor; eauto.
econstructor; eauto.
eapply H0 in H3; simpl; eauto.
intros. specialize (H _ H2).
destruct H as (v0 & HLD & HV & HM).
repeat rewrite (Mem.load_storebytes_other _ _ _ _ _ H1); eauto.
refine_split´; eauto.
eapply Mem.storebytes_valid_access_1; eauto.
Qed.
Lemma free_match_correct:
∀ s abd m0 m0´ f ofs sz b2,
match_RData s abd m0 f→
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b2) →
Mem.free m0 b2 ofs sz = Some m0´ →
match_RData s abd m0´ f.
Proof.
intros; inv H; inv H2.
econstructor; eauto.
econstructor; eauto.
eapply H0 in H3; simpl; eauto.
intros. specialize (H _ H2).
destruct H as (v0 & HLD & HV & HM).
repeat rewrite (Mem.load_free _ _ _ _ _ H1); auto.
refine_split´; eauto.
eapply Mem.valid_access_free_1; eauto.
Qed.
Lemma alloc_match_correct:
∀ s abd m´0 m´1 f f´ ofs sz b0 b´1,
match_RData s abd m´0 f→
Mem.alloc m´0 ofs sz = (m´1, b´1) →
f´ b0 = Some (b´1, 0%Z) →
(∀ b : block, b ≠ b0 → f´ b = f b) →
inject_incr f f´ →
(∀ i b,
In i new_glbl →
find_symbol s i = Some b → b ≠ b0) →
match_RData s abd m´1 f´.
Proof.
intros. rename H1 into HF1, H2 into HB. inv H; inv H1.
econstructor; eauto.
econstructor; eauto.
intros. specialize (H _ H1).
destruct H as (v0 & HLD & HV & HM).
refine_split´; eauto.
- apply (Mem.load_alloc_other _ _ _ _ _ H0); trivial.
- eapply Mem.valid_access_alloc_other; eauto.
Qed.
Prove that after taking one step, the refinement relation still holds
Lemma relate_incr:
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
eapply tfs_inj_incr; eauto.
Qed.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor.
- apply inject_match_correct.
- apply store_match_correct.
- apply alloc_match_correct.
- apply free_match_correct.
- apply storebytes_match_correct.
- intros. eapply relate_incr; eauto.
Qed.
End Rel_Property.
∀ abd abd´ f f´,
relate_RData f abd abd´
→ inject_incr f f´
→ relate_RData f´ abd abd´.
Proof.
inversion 1; subst; intros; inv H; constructor; eauto.
eapply tfs_inj_incr; eauto.
Qed.
Global Instance rel_prf: CompatRel HDATAOps LDATAOps.
Proof.
constructor.
- apply inject_match_correct.
- apply store_match_correct.
- apply alloc_match_correct.
- apply free_match_correct.
- apply storebytes_match_correct.
- intros. eapply relate_incr; eauto.
Qed.
End Rel_Property.
Section OneStep_Forward_Relation.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section FRESH_PRIM.
Lemma get_curid_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_curid_spec) get_curid_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
exploit CPU_ID_range; eauto.
intros Hrange.
specialize (H0 _ Hrange).
destruct H0 as (v & HLD & _ & HM).
assert (HP: v = z).
{
functional inversion H2; subst.
erewrite <- CPU_ID_re in HM; eauto.
rewrite HM in H.
apply Int_unsigned_eq in H. trivial.
}
refine_split; eauto; econstructor; eauto.
lift_unfold. trivial.
Qed.
Lemma set_curid_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_curid_spec) set_curid_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ CPU_ID d2 = CPU_ID d1).
{
inv match_related. functional inversion H1; subst.
repeat split; try congruence; eauto.
}
destruct Hkern as (Hkern & HCPU_ID).
inv H. pose proof H0 as HLV.
exploit CPU_ID_range; eauto.
intros Hrange.
specialize (H0 _ Hrange).
destruct H0 as (_ & _ & HV & _).
exploit CPU_ID_re; eauto.
intros Heq.
specialize (Mem.valid_access_store _ _ _ _ (Vint i) HV); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i0 (CPU_ID d1)); subst.
{
rewrite HCPU_ID in ×.
refine_split´; eauto.
- eapply Mem.load_store_same in HST; eauto.
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gss. trivial.
}
{
specialize (HLV _ H).
destruct HLV as (v & HLD & HV´ & HM).
refine_split´; trivial.
- erewrite Mem.load_store_other; eauto.
right.
simpl; destruct (zlt i0 (CPU_ID d1));
[left; omega|right; omega].
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gso; auto.
}
- apply inject_incr_refl.
Qed.
Lemma set_curid_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_curid_init_spec) set_curid_init_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related. functional inversion H1; subst.
repeat split; try congruence; eauto.
}
assert (index_range: 0 ≤ (Int.unsigned i) < 8).
{ functional inversion H1; simpl; auto. }
inv H. pose proof H0 as HLV.
generalize index_range.
intros Hrange.
specialize (H0 _ Hrange).
destruct H0 as (_ & _ & HV & _).
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr (Int.unsigned i + 1))) HV); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial.
subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i0 (Int.unsigned i)); subst.
{
refine_split´; eauto.
- eapply Mem.load_store_same in HST; eauto.
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gss.
rewrite Int.unsigned_repr.
reflexivity.
generalize max_unsigned_val; intro.
omega.
}
{
specialize (HLV _ H).
destruct HLV as (v & HLD & HV´ & HM).
refine_split´; trivial.
- erewrite Mem.load_store_other; eauto.
right.
simpl; destruct (zlt i0 (Int.unsigned i));
[left; omega|right; omega].
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gso; auto.
}
- apply inject_incr_refl.
Qed.
End FRESH_PRIM.
Section PASSTHROUGH_PRIM.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Section FRESH_PRIM.
Lemma get_curid_spec_ref:
compatsim (crel HDATA LDATA) (gensem get_curid_spec) get_curid_spec_low.
Proof.
compatsim_simpl (@match_AbData). inv H.
assert(HOS: kernel_mode d2).
{
simpl; inv match_related.
functional inversion H2; repeat split; trivial; congruence.
}
exploit CPU_ID_range; eauto.
intros Hrange.
specialize (H0 _ Hrange).
destruct H0 as (v & HLD & _ & HM).
assert (HP: v = z).
{
functional inversion H2; subst.
erewrite <- CPU_ID_re in HM; eauto.
rewrite HM in H.
apply Int_unsigned_eq in H. trivial.
}
refine_split; eauto; econstructor; eauto.
lift_unfold. trivial.
Qed.
Lemma set_curid_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_curid_spec) set_curid_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2 ∧ CPU_ID d2 = CPU_ID d1).
{
inv match_related. functional inversion H1; subst.
repeat split; try congruence; eauto.
}
destruct Hkern as (Hkern & HCPU_ID).
inv H. pose proof H0 as HLV.
exploit CPU_ID_range; eauto.
intros Hrange.
specialize (H0 _ Hrange).
destruct H0 as (_ & _ & HV & _).
exploit CPU_ID_re; eauto.
intros Heq.
specialize (Mem.valid_access_store _ _ _ _ (Vint i) HV); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial. subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i0 (CPU_ID d1)); subst.
{
rewrite HCPU_ID in ×.
refine_split´; eauto.
- eapply Mem.load_store_same in HST; eauto.
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gss. trivial.
}
{
specialize (HLV _ H).
destruct HLV as (v & HLD & HV´ & HM).
refine_split´; trivial.
- erewrite Mem.load_store_other; eauto.
right.
simpl; destruct (zlt i0 (CPU_ID d1));
[left; omega|right; omega].
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gso; auto.
}
- apply inject_incr_refl.
Qed.
Lemma set_curid_init_spec_ref:
compatsim (crel HDATA LDATA) (gensem set_curid_init_spec) set_curid_init_spec_low.
Proof.
compatsim_simpl (@match_AbData).
assert (Hkern: kernel_mode d2).
{
inv match_related. functional inversion H1; subst.
repeat split; try congruence; eauto.
}
assert (index_range: 0 ≤ (Int.unsigned i) < 8).
{ functional inversion H1; simpl; auto. }
inv H. pose proof H0 as HLV.
generalize index_range.
intros Hrange.
specialize (H0 _ Hrange).
destruct H0 as (_ & _ & HV & _).
specialize (Mem.valid_access_store _ _ _ _ (Vint (Int.repr (Int.unsigned i + 1))) HV); intros [m´ HST].
refine_split.
- econstructor; eauto.
instantiate (2:= m´).
instantiate (1:= d2).
simpl; lift_trivial.
subrewrite´.
- constructor.
- pose proof H1 as Hspec.
functional inversion Hspec; subst.
split; eauto; pattern2_refinement_simpl.
econstructor; simpl; eauto.
econstructor; eauto; intros.
destruct (zeq i0 (Int.unsigned i)); subst.
{
refine_split´; eauto.
- eapply Mem.load_store_same in HST; eauto.
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gss.
rewrite Int.unsigned_repr.
reflexivity.
generalize max_unsigned_val; intro.
omega.
}
{
specialize (HLV _ H).
destruct HLV as (v & HLD & HV´ & HM).
refine_split´; trivial.
- erewrite Mem.load_store_other; eauto.
right.
simpl; destruct (zlt i0 (Int.unsigned i));
[left; omega|right; omega].
- eapply Mem.store_valid_access_1; eauto.
- rewrite ZMap.gso; auto.
}
- apply inject_incr_refl.
Qed.
End FRESH_PRIM.
Section PASSTHROUGH_PRIM.
Section Exists.
Lemma atomic_mcs_log_exist:
∀ habd habd´ labd la bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7 ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7 abid cpuid f,
atomic_mcs_log_spec abid cpuid habd = Some (habd´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7))
→ relate_RData f habd labd
→ ∃ labd´, atomic_mcs_log_spec abid cpuid labd = Some (labd´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7))
∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold atomic_mcs_log_spec; intros until f; exist_simpl.
Qed.
Lemma atomic_mcs_log_match:
∀ s abid cpuid d d´ m f la bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7 ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7,
atomic_mcs_log_spec abid cpuid d = Some (d´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7))
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold atomic_mcs_log_spec; intros.
subdestruct.
inv H.
inv H0.
econstructor; eauto.
Qed.
Ltac store_mapped_inject_resolve m Hst Hinj Hstore :=
exploit Mem.store_mapped_inject; eauto;
rewrite Z.add_0_r;
intros (m & Hst & Hinj);
revert Hstore;
intros.
Ltac nextblock_store_rewrite Hstore :=
eapply Mem.nextblock_store in Hstore; eauto; rewrite Hstore.
Lemma atomic_mcs_log_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_atomic_mcs_log_compatsem atomic_mcs_log_spec)
(id ↦ primcall_atomic_mcs_log_compatsem atomic_mcs_log_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit atomic_mcs_log_exist; eauto 1; intros (labd´ & HP & HM & Hcid).
assert (Hf: ι b = Some (b, 0)).
{ eapply stencil_find_symbol_inject´; eauto. }
store_mapped_inject_resolve m2´ Hst2 Hinj2 Hstore_busy0; store_mapped_inject_resolve m3´ Hst3 Hinj3 Hstore_next0.
store_mapped_inject_resolve m4´ Hst4 Hinj4 Hstore_busy1; store_mapped_inject_resolve m5´ Hst5 Hinj5 Hstore_next1.
store_mapped_inject_resolve m6´ Hst6 Hinj6 Hstore_busy2; store_mapped_inject_resolve m7´ Hst7 Hinj7 Hstore_next2.
store_mapped_inject_resolve m8´ Hst8 Hinj8 Hstore_busy3; store_mapped_inject_resolve m9´ Hst9 Hinj9 Hstore_next3.
store_mapped_inject_resolve m10´ Hst10 Hinj10 Hstore_busy4; store_mapped_inject_resolve m11´ Hst11 Hinj11 Hstore_next4.
store_mapped_inject_resolve m12´ Hst12 Hinj12 Hstore_busy5; store_mapped_inject_resolve m13´ Hst13 Hinj13 Hstore_next5.
store_mapped_inject_resolve m14´ Hst14 Hinj14 Hstore_busy6; store_mapped_inject_resolve m15´ Hst15 Hinj15 Hstore_next6.
store_mapped_inject_resolve m16´ Hst16 Hinj16 Hstore_busy7; store_mapped_inject_resolve m17´ Hst17 Hinj17 Hstore_next7.
exploit Mem.store_mapped_inject; eauto.
rewrite Z.add_0_r.
intros (m18´ & Hst18 & Hinj18).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in Harg.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
econstructor; eauto ; try congruence.
-
assert (Hid: ∀ i0 b0, In i0 new_glbl → find_symbol s i0 = Some b0 → b0 ≠ b).
{ intros.
destruct (peq i0 MCS_LOCK_LOC).
+ subst. inv H; inv H1.
+ red; intros; subst.
elim n.
eapply (genv_vars_inj s i0 MCS_LOCK_LOC); eauto. }
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply atomic_mcs_log_match; eauto.
-
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto.
eapply Mem.nextblock_store in Hst2; eauto; eapply Mem.nextblock_store in Hst3; eauto.
eapply Mem.nextblock_store in Hst4; eauto; eapply Mem.nextblock_store in Hst5; eauto.
eapply Mem.nextblock_store in Hst6; eauto; eapply Mem.nextblock_store in Hst7; eauto.
eapply Mem.nextblock_store in Hst8; eauto; eapply Mem.nextblock_store in Hst9; eauto.
eapply Mem.nextblock_store in Hst10; eauto; eapply Mem.nextblock_store in Hst11; eauto.
eapply Mem.nextblock_store in Hst12; eauto; eapply Mem.nextblock_store in Hst13; eauto.
eapply Mem.nextblock_store in Hst14; eauto; eapply Mem.nextblock_store in Hst15; eauto.
eapply Mem.nextblock_store in Hst16; eauto; eapply Mem.nextblock_store in Hst17; eauto.
eapply Mem.nextblock_store in Hst18; eauto.
rewrite Hst18, Hst17, Hst16, Hst15, Hst14, Hst13, Hst12, Hst11, Hst10, Hst9, Hst8, Hst7, Hst6, Hst5, Hst4, Hst3, Hst2.
assumption.
-
intros; red; intros; eapply match_newglob_noperm; eauto; repeat (eapply Mem.perm_store_2; eauto).
-
nextblock_store_rewrite Hstore_next7; nextblock_store_rewrite Hstore_busy7.
nextblock_store_rewrite Hstore_next6; nextblock_store_rewrite Hstore_busy6.
nextblock_store_rewrite Hstore_next5; nextblock_store_rewrite Hstore_busy5.
nextblock_store_rewrite Hstore_next4; nextblock_store_rewrite Hstore_busy4.
nextblock_store_rewrite Hstore_next3; nextblock_store_rewrite Hstore_busy3.
nextblock_store_rewrite Hstore_next2; nextblock_store_rewrite Hstore_busy2.
nextblock_store_rewrite Hstore_next1; nextblock_store_rewrite Hstore_busy1.
nextblock_store_rewrite Hstore_next0; nextblock_store_rewrite Hstore_busy0.
erewrite Mem.nextblock_store; eauto.
Qed.
Lemma atomic_mcs_SWAP_exist:
∀ habd habd´ labd prev_tail bound abid cpuid f,
atomic_mcs_SWAP_spec bound abid cpuid habd = Some (habd´, prev_tail)
→ relate_RData f habd labd
→ ∃ labd´, atomic_mcs_SWAP_spec bound abid cpuid labd = Some (labd´, prev_tail) ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold atomic_mcs_SWAP_spec; intros until f; exist_simpl.
Qed.
Lemma atomic_mcs_SWAP_match:
∀ s bound abid cpuid d d´ m f prev_tail,
atomic_mcs_SWAP_spec bound abid cpuid d = Some (d´, prev_tail)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold atomic_mcs_SWAP_spec; intros; subdestruct; (inv H; inv H0; econstructor; eauto).
Qed.
Lemma atomic_mcs_SWAP_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_atomic_mcs_SWAP_compatsem atomic_mcs_SWAP_spec)
(id ↦ primcall_atomic_mcs_SWAP_compatsem atomic_mcs_SWAP_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit atomic_mcs_SWAP_exist; eauto 1; intros (labd´ & HP & HM & Hcid).
assert (Hf: ι b = Some (b, 0)).
{ eapply stencil_find_symbol_inject´; eauto. }
store_mapped_inject_resolve m2´ Hst Hinj Hstore_next.
store_mapped_inject_resolve m3´ Hst´ Hinj´ Hstore_busy.
exploit Mem.store_mapped_inject; eauto.
rewrite Z.add_0_r.
intros (m4´ & Hst´´ & Hinj´´).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in Harg.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
econstructor; eauto ; try congruence.
-
assert (Hid: ∀ i0 b0, In i0 new_glbl → find_symbol s i0 = Some b0 → b0 ≠ b).
{ intros.
destruct (peq i0 MCS_LOCK_LOC).
+ subst. inv H; inv H1.
+ red; intros; subst.
elim n.
eapply (genv_vars_inj s i0 MCS_LOCK_LOC); eauto. }
eapply store_match_correct; eauto; eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply atomic_mcs_SWAP_match; eauto.
-
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
eapply Mem.nextblock_store in Hst; eauto; eapply Mem.nextblock_store in Hst´; eauto; eapply Mem.nextblock_store in Hst´´; eauto.
rewrite Hst´´, Hst´, Hst.
assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto; repeat (eapply Mem.perm_store_2; eauto).
-
nextblock_store_rewrite Hstore_busy; nextblock_store_rewrite Hstore_next.
erewrite Mem.nextblock_store; eauto.
Qed.
Lemma atomic_mcs_CAS_exist:
∀ habd habd´ labd succeed abid cpuid f,
atomic_mcs_CAS_spec abid cpuid habd = Some (habd´, succeed)
→ relate_RData f habd labd
→ ∃ labd´, atomic_mcs_CAS_spec abid cpuid labd = Some (labd´, succeed) ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold atomic_mcs_CAS_spec; intros until f; exist_simpl.
Qed.
Lemma atomic_mcs_CAS_match:
∀ s abid cpuid d d´ m f succeed,
atomic_mcs_CAS_spec abid cpuid d = Some (d´, succeed)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold atomic_mcs_CAS_spec; intros; subdestruct; inv H; inv H0; econstructor; eauto.
Qed.
Lemma atomic_mcs_CAS_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_atomic_mcs_CAS_compatsem atomic_mcs_CAS_spec)
(id ↦ primcall_atomic_mcs_CAS_compatsem atomic_mcs_CAS_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit atomic_mcs_CAS_exist; eauto 1; intros (labd´ & HP & HM & Hcid).
assert (Hf: ι b = Some (b, 0)).
{ eapply stencil_find_symbol_inject´; eauto. }
exploit Mem.store_mapped_inject; eauto.
rewrite Z.add_0_r.
intros (m2´ & Hst & Hinj).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in Harg.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
econstructor; eauto ; try congruence.
-
assert (Hid: ∀ i0 b0, In i0 new_glbl → find_symbol s i0 = Some b0 → b0 ≠ b).
{ intros.
destruct (peq i0 MCS_LOCK_LOC).
+ subst. inv H; inv H1.
+ red; intros; subst.
elim n.
eapply (genv_vars_inj s i0 MCS_LOCK_LOC); eauto. }
eapply store_match_correct; eauto.
eapply atomic_mcs_CAS_match; eauto.
-
erewrite Mem.nextblock_store; eauto.
eapply Mem.nextblock_store in Hst; eauto.
rewrite Hst.
assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto.
eapply Mem.perm_store_2; eauto.
-
erewrite Mem.nextblock_store; eauto.
Qed.
Lemma mcs_init_node_log_exist:
∀ habd habd´ labd abid f,
mcs_init_node_log_spec abid habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_init_node_log_spec abid labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_init_node_log_spec; intros until f; exist_simpl.
Qed.
Lemma mcs_GET_NEXT_log_exist:
∀ habd habd´ labd abid cpuid f,
mcs_GET_NEXT_log_spec abid cpuid habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_GET_NEXT_log_spec abid cpuid labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_GET_NEXT_log_spec; intros until f; exist_simpl.
Qed.
Lemma mcs_SET_NEXT_log_exist:
∀ habd habd´ labd abid cpuid prev_id f,
mcs_SET_NEXT_log_spec abid cpuid prev_id habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_SET_NEXT_log_spec abid cpuid prev_id labd = Some labd´
∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_SET_NEXT_log_spec; intros until f; exist_simpl.
Qed.
Lemma mcs_GET_BUSY_log_exist:
∀ habd habd´ labd abid cpuid f,
mcs_GET_BUSY_log_spec abid cpuid habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_GET_BUSY_log_spec abid cpuid labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_GET_BUSY_log_spec; intros until f; exist_simpl.
Qed.
Lemma mcs_SET_BUSY_log_exist:
∀ habd habd´ labd abid cpuid f,
mcs_SET_BUSY_log_spec abid cpuid habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_SET_BUSY_log_spec abid cpuid labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_SET_BUSY_log_spec; intros until f; exist_simpl.
Qed.
End Exists.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
Proof.
accessor_prop_tac.
- eapply flatmem_store´_exists; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) mcurid_passthrough mboot.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy´´´_sim.
- apply page_copy_back´_sim.
- apply vmxinfo_get_sim.
- apply setPG_sim.
- apply setCR3_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
- apply bootloader0_sim.
- apply release_shared0_sim.
- apply (acquire_shared0_mcs_sim (valid_id_args:= Shared2ID_valid0)).
intros. inv H. trivial. inv H0.
- apply atomic_mcs_log_sim.
- apply atomic_mcs_SWAP_sim.
- apply atomic_mcs_CAS_sim.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_init_node_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_GET_NEXT_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_SET_NEXT_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_GET_BUSY_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_SET_BUSY_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- apply get_CPU_ID_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply serial_irq_check_sim.
- apply iret_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_irq_current_sim.
- apply ic_intr_sim.
- apply save_context_sim.
- apply restore_context_sim.
- apply local_irq_save_sim.
- apply local_irq_restore_sim.
- apply serial_in_sim.
- apply serial_out_sim.
- apply serial_hw_intr_sim.
- apply ioapic_read_sim.
- apply ioapic_write_sim.
- apply lapic_read_sim.
- apply lapic_write_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End PASSTHROUGH_PRIM.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.
Lemma atomic_mcs_log_exist:
∀ habd habd´ labd la bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7 ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7 abid cpuid f,
atomic_mcs_log_spec abid cpuid habd = Some (habd´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7))
→ relate_RData f habd labd
→ ∃ labd´, atomic_mcs_log_spec abid cpuid labd = Some (labd´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7))
∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold atomic_mcs_log_spec; intros until f; exist_simpl.
Qed.
Lemma atomic_mcs_log_match:
∀ s abid cpuid d d´ m f la bs0 bs1 bs2 bs3 bs4 bs5 bs6 bs7 ne0 ne1 ne2 ne3 ne4 ne5 ne6 ne7,
atomic_mcs_log_spec abid cpuid d = Some (d´, la, (bs0, bs1, bs2, bs3, bs4, bs5, bs6, bs7),
(ne0, ne1, ne2, ne3, ne4, ne5, ne6, ne7))
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold atomic_mcs_log_spec; intros.
subdestruct.
inv H.
inv H0.
econstructor; eauto.
Qed.
Ltac store_mapped_inject_resolve m Hst Hinj Hstore :=
exploit Mem.store_mapped_inject; eauto;
rewrite Z.add_0_r;
intros (m & Hst & Hinj);
revert Hstore;
intros.
Ltac nextblock_store_rewrite Hstore :=
eapply Mem.nextblock_store in Hstore; eauto; rewrite Hstore.
Lemma atomic_mcs_log_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_atomic_mcs_log_compatsem atomic_mcs_log_spec)
(id ↦ primcall_atomic_mcs_log_compatsem atomic_mcs_log_spec).
Proof.
intros.
layer_sim_simpl.
compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit atomic_mcs_log_exist; eauto 1; intros (labd´ & HP & HM & Hcid).
assert (Hf: ι b = Some (b, 0)).
{ eapply stencil_find_symbol_inject´; eauto. }
store_mapped_inject_resolve m2´ Hst2 Hinj2 Hstore_busy0; store_mapped_inject_resolve m3´ Hst3 Hinj3 Hstore_next0.
store_mapped_inject_resolve m4´ Hst4 Hinj4 Hstore_busy1; store_mapped_inject_resolve m5´ Hst5 Hinj5 Hstore_next1.
store_mapped_inject_resolve m6´ Hst6 Hinj6 Hstore_busy2; store_mapped_inject_resolve m7´ Hst7 Hinj7 Hstore_next2.
store_mapped_inject_resolve m8´ Hst8 Hinj8 Hstore_busy3; store_mapped_inject_resolve m9´ Hst9 Hinj9 Hstore_next3.
store_mapped_inject_resolve m10´ Hst10 Hinj10 Hstore_busy4; store_mapped_inject_resolve m11´ Hst11 Hinj11 Hstore_next4.
store_mapped_inject_resolve m12´ Hst12 Hinj12 Hstore_busy5; store_mapped_inject_resolve m13´ Hst13 Hinj13 Hstore_next5.
store_mapped_inject_resolve m14´ Hst14 Hinj14 Hstore_busy6; store_mapped_inject_resolve m15´ Hst15 Hinj15 Hstore_next6.
store_mapped_inject_resolve m16´ Hst16 Hinj16 Hstore_busy7; store_mapped_inject_resolve m17´ Hst17 Hinj17 Hstore_next7.
exploit Mem.store_mapped_inject; eauto.
rewrite Z.add_0_r.
intros (m18´ & Hst18 & Hinj18).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in Harg.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
econstructor; eauto ; try congruence.
-
assert (Hid: ∀ i0 b0, In i0 new_glbl → find_symbol s i0 = Some b0 → b0 ≠ b).
{ intros.
destruct (peq i0 MCS_LOCK_LOC).
+ subst. inv H; inv H1.
+ red; intros; subst.
elim n.
eapply (genv_vars_inj s i0 MCS_LOCK_LOC); eauto. }
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply store_match_correct; eauto; eapply atomic_mcs_log_match; eauto.
-
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
erewrite Mem.nextblock_store; eauto.
eapply Mem.nextblock_store in Hst2; eauto; eapply Mem.nextblock_store in Hst3; eauto.
eapply Mem.nextblock_store in Hst4; eauto; eapply Mem.nextblock_store in Hst5; eauto.
eapply Mem.nextblock_store in Hst6; eauto; eapply Mem.nextblock_store in Hst7; eauto.
eapply Mem.nextblock_store in Hst8; eauto; eapply Mem.nextblock_store in Hst9; eauto.
eapply Mem.nextblock_store in Hst10; eauto; eapply Mem.nextblock_store in Hst11; eauto.
eapply Mem.nextblock_store in Hst12; eauto; eapply Mem.nextblock_store in Hst13; eauto.
eapply Mem.nextblock_store in Hst14; eauto; eapply Mem.nextblock_store in Hst15; eauto.
eapply Mem.nextblock_store in Hst16; eauto; eapply Mem.nextblock_store in Hst17; eauto.
eapply Mem.nextblock_store in Hst18; eauto.
rewrite Hst18, Hst17, Hst16, Hst15, Hst14, Hst13, Hst12, Hst11, Hst10, Hst9, Hst8, Hst7, Hst6, Hst5, Hst4, Hst3, Hst2.
assumption.
-
intros; red; intros; eapply match_newglob_noperm; eauto; repeat (eapply Mem.perm_store_2; eauto).
-
nextblock_store_rewrite Hstore_next7; nextblock_store_rewrite Hstore_busy7.
nextblock_store_rewrite Hstore_next6; nextblock_store_rewrite Hstore_busy6.
nextblock_store_rewrite Hstore_next5; nextblock_store_rewrite Hstore_busy5.
nextblock_store_rewrite Hstore_next4; nextblock_store_rewrite Hstore_busy4.
nextblock_store_rewrite Hstore_next3; nextblock_store_rewrite Hstore_busy3.
nextblock_store_rewrite Hstore_next2; nextblock_store_rewrite Hstore_busy2.
nextblock_store_rewrite Hstore_next1; nextblock_store_rewrite Hstore_busy1.
nextblock_store_rewrite Hstore_next0; nextblock_store_rewrite Hstore_busy0.
erewrite Mem.nextblock_store; eauto.
Qed.
Lemma atomic_mcs_SWAP_exist:
∀ habd habd´ labd prev_tail bound abid cpuid f,
atomic_mcs_SWAP_spec bound abid cpuid habd = Some (habd´, prev_tail)
→ relate_RData f habd labd
→ ∃ labd´, atomic_mcs_SWAP_spec bound abid cpuid labd = Some (labd´, prev_tail) ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold atomic_mcs_SWAP_spec; intros until f; exist_simpl.
Qed.
Lemma atomic_mcs_SWAP_match:
∀ s bound abid cpuid d d´ m f prev_tail,
atomic_mcs_SWAP_spec bound abid cpuid d = Some (d´, prev_tail)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold atomic_mcs_SWAP_spec; intros; subdestruct; (inv H; inv H0; econstructor; eauto).
Qed.
Lemma atomic_mcs_SWAP_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_atomic_mcs_SWAP_compatsem atomic_mcs_SWAP_spec)
(id ↦ primcall_atomic_mcs_SWAP_compatsem atomic_mcs_SWAP_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit atomic_mcs_SWAP_exist; eauto 1; intros (labd´ & HP & HM & Hcid).
assert (Hf: ι b = Some (b, 0)).
{ eapply stencil_find_symbol_inject´; eauto. }
store_mapped_inject_resolve m2´ Hst Hinj Hstore_next.
store_mapped_inject_resolve m3´ Hst´ Hinj´ Hstore_busy.
exploit Mem.store_mapped_inject; eauto.
rewrite Z.add_0_r.
intros (m4´ & Hst´´ & Hinj´´).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in Harg.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
econstructor; eauto ; try congruence.
-
assert (Hid: ∀ i0 b0, In i0 new_glbl → find_symbol s i0 = Some b0 → b0 ≠ b).
{ intros.
destruct (peq i0 MCS_LOCK_LOC).
+ subst. inv H; inv H1.
+ red; intros; subst.
elim n.
eapply (genv_vars_inj s i0 MCS_LOCK_LOC); eauto. }
eapply store_match_correct; eauto; eapply store_match_correct; eauto; eapply store_match_correct; eauto.
eapply atomic_mcs_SWAP_match; eauto.
-
erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto; erewrite Mem.nextblock_store; eauto.
eapply Mem.nextblock_store in Hst; eauto; eapply Mem.nextblock_store in Hst´; eauto; eapply Mem.nextblock_store in Hst´´; eauto.
rewrite Hst´´, Hst´, Hst.
assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto; repeat (eapply Mem.perm_store_2; eauto).
-
nextblock_store_rewrite Hstore_busy; nextblock_store_rewrite Hstore_next.
erewrite Mem.nextblock_store; eauto.
Qed.
Lemma atomic_mcs_CAS_exist:
∀ habd habd´ labd succeed abid cpuid f,
atomic_mcs_CAS_spec abid cpuid habd = Some (habd´, succeed)
→ relate_RData f habd labd
→ ∃ labd´, atomic_mcs_CAS_spec abid cpuid labd = Some (labd´, succeed) ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold atomic_mcs_CAS_spec; intros until f; exist_simpl.
Qed.
Lemma atomic_mcs_CAS_match:
∀ s abid cpuid d d´ m f succeed,
atomic_mcs_CAS_spec abid cpuid d = Some (d´, succeed)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold atomic_mcs_CAS_spec; intros; subdestruct; inv H; inv H0; econstructor; eauto.
Qed.
Lemma atomic_mcs_CAS_sim:
∀ id,
sim (crel RData RData)
(id ↦ primcall_atomic_mcs_CAS_compatsem atomic_mcs_CAS_spec)
(id ↦ primcall_atomic_mcs_CAS_compatsem atomic_mcs_CAS_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit atomic_mcs_CAS_exist; eauto 1; intros (labd´ & HP & HM & Hcid).
assert (Hf: ι b = Some (b, 0)).
{ eapply stencil_find_symbol_inject´; eauto. }
exploit Mem.store_mapped_inject; eauto.
rewrite Z.add_0_r.
intros (m2´ & Hst & Hinj).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in Harg.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
econstructor; eauto ; try congruence.
-
assert (Hid: ∀ i0 b0, In i0 new_glbl → find_symbol s i0 = Some b0 → b0 ≠ b).
{ intros.
destruct (peq i0 MCS_LOCK_LOC).
+ subst. inv H; inv H1.
+ red; intros; subst.
elim n.
eapply (genv_vars_inj s i0 MCS_LOCK_LOC); eauto. }
eapply store_match_correct; eauto.
eapply atomic_mcs_CAS_match; eauto.
-
erewrite Mem.nextblock_store; eauto.
eapply Mem.nextblock_store in Hst; eauto.
rewrite Hst.
assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto.
eapply Mem.perm_store_2; eauto.
-
erewrite Mem.nextblock_store; eauto.
Qed.
Lemma mcs_init_node_log_exist:
∀ habd habd´ labd abid f,
mcs_init_node_log_spec abid habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_init_node_log_spec abid labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_init_node_log_spec; intros until f; exist_simpl.
Qed.
Lemma mcs_GET_NEXT_log_exist:
∀ habd habd´ labd abid cpuid f,
mcs_GET_NEXT_log_spec abid cpuid habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_GET_NEXT_log_spec abid cpuid labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_GET_NEXT_log_spec; intros until f; exist_simpl.
Qed.
Lemma mcs_SET_NEXT_log_exist:
∀ habd habd´ labd abid cpuid prev_id f,
mcs_SET_NEXT_log_spec abid cpuid prev_id habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_SET_NEXT_log_spec abid cpuid prev_id labd = Some labd´
∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_SET_NEXT_log_spec; intros until f; exist_simpl.
Qed.
Lemma mcs_GET_BUSY_log_exist:
∀ habd habd´ labd abid cpuid f,
mcs_GET_BUSY_log_spec abid cpuid habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_GET_BUSY_log_spec abid cpuid labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_GET_BUSY_log_spec; intros until f; exist_simpl.
Qed.
Lemma mcs_SET_BUSY_log_exist:
∀ habd habd´ labd abid cpuid f,
mcs_SET_BUSY_log_spec abid cpuid habd = Some habd´
→ relate_RData f habd labd
→ ∃ labd´, mcs_SET_BUSY_log_spec abid cpuid labd = Some labd´ ∧ relate_RData f habd´ labd´
∧ cid habd´ = cid habd.
Proof.
unfold mcs_SET_BUSY_log_spec; intros until f; exist_simpl.
Qed.
End Exists.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
Proof.
accessor_prop_tac.
- eapply flatmem_store´_exists; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) mcurid_passthrough mboot.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy´´´_sim.
- apply page_copy_back´_sim.
- apply vmxinfo_get_sim.
- apply setPG_sim.
- apply setCR3_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
- apply bootloader0_sim.
- apply release_shared0_sim.
- apply (acquire_shared0_mcs_sim (valid_id_args:= Shared2ID_valid0)).
intros. inv H. trivial. inv H0.
- apply atomic_mcs_log_sim.
- apply atomic_mcs_SWAP_sim.
- apply atomic_mcs_CAS_sim.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_init_node_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_GET_NEXT_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_SET_NEXT_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_GET_BUSY_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit mcs_SET_BUSY_log_exist; eauto 1; intros (labd´ & HP & HM & CID).
match_external_states_simpl.
- apply get_CPU_ID_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply serial_irq_check_sim.
- apply iret_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_irq_current_sim.
- apply ic_intr_sim.
- apply save_context_sim.
- apply restore_context_sim.
- apply local_irq_save_sim.
- apply local_irq_restore_sim.
- apply serial_in_sim.
- apply serial_out_sim.
- apply serial_hw_intr_sim.
- apply ioapic_read_sim.
- apply ioapic_write_sim.
- apply lapic_read_sim.
- apply lapic_write_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End PASSTHROUGH_PRIM.
End OneStep_Forward_Relation.
End WITHMEM.
End Refinement.