Library mcertikos.proc.QueueIntroGenPassthrough
This file provide the contextual refinement proof between PThreadInit layer and PQueueIntro layer
Require Import QueueIntroGenDef.
Require Import LAsmModuleSemAux.
Require Import QueueIntroGenLemma.
Require Import LAsmModuleSemAux.
Require Import QueueIntroGenLemma.
Section Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section Exists.
Lemma relate_TCB_Log_Pool_gss:
∀ s hl ll l0,
relate_TCB_Log_Pool s hl ll →
relate_TCB_Log_Pool s
(ZMap.set 0 l0 hl) (ZMap.set 0 l0 ll).
Proof.
intros. inv H. constructor; eauto.
- intros. destruct (zeq r 0); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- intros.
assert (Hneq: i + ID_AT_range ≠ 0).
{
unfold ID_AT_range. omega.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_relate_TCB_Log_Pool:
∀ s habd labd,
relate_TCB_Log_Pool s (multi_log habd) (multi_log labd) →
relate_TCB_Log_Pool s (CalTicketLock.real_multi_log (multi_log habd)) (CalTicketLock.real_multi_log (multi_log labd)).
Proof.
assert (Hcases: ∀ a b, 0 ≤ a < b ∨ (a < 0 ∨ b ≤ a)) by (intros; omega).
assert (HZ2Nat: ∀ a b, 0 ≤ a < b → (0 ≤ Z.to_nat a < Z.to_nat b)%nat).
{
split.
rewrite <- Z2Nat.inj_0; rewrite <- Z2Nat.inj_le; omega.
rewrite <- Z2Nat.inj_lt; omega.
}
unfold CalTicketLock.real_multi_log; intros s d1 d2 Hrel; inv Hrel; constructor.
- intros i ofs r Hneq Hind.
destruct (Hcases r lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id r); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
- intros i Hi.
destruct (Hcases (i + ID_AT_range) lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id (i + ID_AT_range)); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto; constructor; constructor.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
Qed.
Lemma sharedmem_init_exists :
∀ s mbi_adr adt adt´ ladt f,
sharedmem_init_spec (Int.unsigned mbi_adr) adt = Some adt´
→ relate_AbData s f adt ladt
→ ∃ ladt´,
sharedmem_init_spec (Int.unsigned mbi_adr) ladt = Some ladt´
∧ relate_AbData s f adt´ ladt´.
Proof.
unfold sharedmem_init_spec.
intros until f. exist_simpl.
- apply real_relate_TCB_Log_Pool; eauto.
Qed.
Lemma sharedmem_init_match:
∀ s d d´ m i f,
sharedmem_init_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold sharedmem_init_spec; intros. subdestruct. inv H.
inv H0. econstructor; eauto.
Qed.
Lemma palloc_exist:
∀ s habd habd´ labd n i f,
palloc_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc_spec n labd = Some (labd´, i) ∧ relate_AbData s f habd´ labd´.
Proof.
unfold palloc_spec; intros.
revert H. pose proof H0 as HR. inv H0.
assert (Hlog: ZMap.get 0 (multi_log habd) = ZMap.get 0 (multi_log labd)).
{
inv multi_log_re. eapply (H 0 0); auto. omega.
}
assert (Horacle: ZMap.get 0 (multi_oracle habd) = ZMap.get 0 (multi_oracle labd)).
{
inv multi_oracle_re. eapply (H 0 0); auto. omega.
}
rewrite Horacle.
subrewrite. subdestruct; inv HQ.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_TCB_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_TCB_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_TCB_Log_Pool_gss. eauto.
Qed.
Lemma palloc_match:
∀ s d d´ m n i f,
palloc_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold palloc_spec; intros. inv H0.
subdestruct; inv H; subst; trivial.
- econstructor; eauto.
- econstructor; eauto.
- econstructor; eauto.
Qed.
Lemma ptAllocPDE0_exist:
∀ s habd habd´ labd i n v f,
ptAllocPDE0_spec n v habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptAllocPDE0_spec n v labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptAllocPDE0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; destruct p; inv HQ.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
rewrite H. rewrite Hdestruct8.
refine_split´; trivial.
inv H0.
constructor; simpl; try eassumption.
+ apply FlatMem.free_page_inj´. trivial.
+ subrewrite´.
+ subrewrite´.
Qed.
Lemma ptAllocPDE0_match:
∀ s n v i d d´ m f,
ptAllocPDE0_spec n v d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptAllocPDE0_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- exploit palloc_match; eauto.
intros Hm. inv Hm.
econstructor; eauto.
Qed.
Lemma ptInsert0_exist:
∀ s habd habd´ labd i n v pa pe f,
ptInsert0_spec n v pa pe habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptInsert0_spec n v pa pe labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptInsert0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- exploit (ptInsertPTE0_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
exploit (ptInsertPTE0_exist s); eauto.
intros (labd´0 & HptInsert0´´ & Hre´).
subrewrite´.
refine_split´; trivial.
Qed.
Lemma ptInsert0_match:
∀ s n v pa pe d d´ m i f,
ptInsert0_spec n v pa pe d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptInsert0_spec; intros. subdestruct; inv H; trivial.
- exploit ptInsertPTE0_match; eauto.
- eapply ptAllocPDE0_match; eauto.
- exploit ptInsertPTE0_match; eauto.
eapply ptAllocPDE0_match; eauto.
Qed.
Lemma ptResv_exist:
∀ s habd habd´ labd i n v p f,
ptResv_spec n v p habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv_spec n v p labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv_spec; intros.
subdestruct. destruct p0.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
Qed.
Lemma ptResv_match:
∀ s d d´ m i n v p f,
ptResv_spec n v p d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptResv_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
Qed.
Lemma ptResv2_exist:
∀ s habd habd´ labd i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv2_spec n v p n´ v´ p´ labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv2_spec; intros.
subdestruct; destruct p0; inv H.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?). revert H2.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?). intros.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
Qed.
Lemma ptResv2_match:
∀ s d d´ m i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptResv2_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
Qed.
Lemma offer_shared_mem_exists:
∀ s habd habd´ labd i1 i2 v z f,
offer_shared_mem_spec i1 i2 v habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, offer_shared_mem_spec i1 i2 v labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold offer_shared_mem_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- refine_split´; trivial.
constructor; eauto.
Qed.
Lemma offer_shared_mem_match:
∀ s d d´ m i1 i2 v z f,
offer_shared_mem_spec i1 i2 v d = Some (d´, z)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold offer_shared_mem_spec; intros. subdestruct; inv H; trivial.
- exploit ptResv2_match; eauto.
intros Hm. inv Hm.
econstructor; eauto.
- exploit ptResv2_match; eauto.
intros Hm. inv Hm.
econstructor; eauto.
- inv H0. econstructor; eauto.
Qed.
Lemma Shared2ID1_imply:
∀ i id,
Shared2ID2 i = Some id → Shared2ID1 i = Some id.
Proof.
intros. functional inversion H; subst.
auto.
Qed.
Lemma Shared2ID2_neq:
∀ i p,
Shared2ID2 i = Some p →
i ≠ ID_TCB.
Proof.
intros. functional inversion H; subst. omega.
Qed.
Lemma release_lock_exist:
∀ s i ofs e habd habd´ labd f,
release_lock_spec2 i ofs e habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_spec1 i ofs e labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct. inv HQ.
erewrite Shared2ID1_imply; eauto.
inv multi_log_re.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
subrewrite´.
refine_split´; eauto.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq; eauto.
eapply Shared2ID2_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma release_lock_match2:
∀ s i ofs e d d´ m f,
release_lock_spec2 i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_spec; intros.
subdestruct; inv H.
inv H0. econstructor; eauto.
Qed.
Lemma release_lock_sim2 :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id release_lock_spec2)
(id ↦ primcall_release_lock_compatsem id release_lock_spec1).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_lock_exist; eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- eapply release_lock_match2 in H4; eauto.
repeat (econstructor; eauto).
subst rs´. val_inject_simpl.
Qed.
Lemma acquire_lock_exist:
∀ s bound i ofs habd habd´ labd f p l,
acquire_lock_spec2 bound i ofs habd = Some (habd´, p, l)
→ relate_AbData s f habd labd
→ (∃ labd´, acquire_lock_spec1 bound i ofs labd = Some (labd´, p, l) ∧
relate_AbData s f habd´ labd´)
∧ Shared2ID2 i = Some p.
Proof.
unfold acquire_lock_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct. inv HQ.
erewrite Shared2ID1_imply; eauto.
inv multi_log_re.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
pose proof multi_oracle_re as Horacle.
inv multi_oracle_re.
exploit H1; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
subrewrite´.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq; eauto.
eapply Shared2ID2_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma acquire_lock_match:
∀ s bound i ofs d d´ m f p l,
acquire_lock_spec2 bound i ofs d = Some (d´, p, l)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_spec; intros.
subdestruct; inv H.
inv H0. econstructor; eauto.
Qed.
Lemma acquire_lock_sim2:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec2)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec1).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_lock_exist; eauto 1; intros ((labd´ & HP & HM) & HS).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
destruct l; subst.
{
exploit Mem.storebytes_mapped_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
{ eapply list_forall2_bytelist_inject; eauto. }
intros (m2´ & Hst & Hinj).
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
assert (Hmatch: match_AbData s d1´ m2´ ι).
{
eapply acquire_lock_match in H4; eauto.
eapply storebytes_match_correct; eauto.
intros.
destruct (peq i id0).
+ subst. inv H.
functional inversion HS. inv H1.
+ red; intros; subst. elim n.
eapply (genv_vars_inj s i id0); eauto.
}
match_external_states_simpl.
- simpl; trivial.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto.
eapply Mem.perm_storebytes_2; eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
-
subst rs´.
val_inject_simpl.
}
{
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
eapply acquire_lock_match in H4; eauto.
match_external_states_simpl.
subst rs´. val_inject_simpl.
}
Qed.
Section PAGE_COPY_SIM.
Lemma page_copy_exist:
∀ s habd habd´ labd index i from f,
page_copy_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_spec; intros.
inv H0.
revert H. subrewrite.
subdestruct. inv HQ.
inv multi_log_re.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
reflexivity.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
rewrite Hdestruct7.
exploit page_copy_aux_exists; eauto.
intros Hcopy´; rewrite Hcopy´.
rewrite Hdestruct11.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq; eauto.
eapply Shared2ID2_neq; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy_match:
∀ s d d´ m index i from f,
page_copy_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_spec; intros. subdestruct.
inv H. inv H0. econstructor; eauto.
Qed.
Lemma page_copy_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_spec)
(id ↦ gensem page_copy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_exist; eauto 1.
exploit page_copy_match; eauto 1.
intro Hmatch.
intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End PAGE_COPY_SIM.
Section PAGE_COPY_BACK_SIM.
Lemma page_copy_back_exist:
∀ s habd habd´ labd index i to f,
page_copy_back_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back_spec; intros.
inv H0.
revert H. subrewrite.
subdestruct. inv HQ.
inv multi_log_re.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
reflexivity.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
rewrite Hdestruct7.
rewrite Hdestruct10.
exploit page_copy_back_aux_exists; eauto.
intros [lh´ [Hcopy´ HPRel]]; rewrite Hcopy´.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq; eauto.
eapply Shared2ID2_neq; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy_back_match:
∀ s d d´ m index i to f,
page_copy_back_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back_spec; intros. subdestruct.
inv H. inv H0. econstructor; eauto.
Qed.
Lemma page_copy_back_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back_spec)
(id ↦ gensem page_copy_back_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_back_exist; eauto 1.
exploit page_copy_back_match; eauto 1.
intro Hmatch.
intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End PAGE_COPY_BACK_SIM.
End Exists.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
Proof.
accessor_prop_tac.
- eapply flatmem_store_exists; eauto.
- eapply flatmem_store_match; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) pqueueintro_passthrough psleeper.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply page_copy_sim.
- apply page_copy_back_sim.
- apply vmxinfo_get_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit palloc_exist; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply palloc_match; eauto).
match_external_states_simpl.
- apply setPT_sim.
- apply ptRead_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit ptResv_exist; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply ptResv_match; eauto).
match_external_states_simpl.
- apply kctxt_new_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit sharedmem_init_exists; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply sharedmem_init_match; eauto).
match_external_states_simpl.
- apply shared_mem_status_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit offer_shared_mem_exists; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply offer_shared_mem_match; eauto).
match_external_states_simpl.
- apply ptin_sim.
- apply ptout_sim.
- apply container_get_nchildren_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply sleeper_inc_sim.
- apply sleeper_dec_sim.
- apply sleeper_zzz_sim.
- apply release_lock_sim2.
- apply acquire_lock_sim2.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_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 kctxt_switch_sim.
- layer_sim_simpl.
+ eapply load_correct2.
+ eapply store_correct2.
Qed.
End WITHMEM.
End Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section Exists.
Lemma relate_TCB_Log_Pool_gss:
∀ s hl ll l0,
relate_TCB_Log_Pool s hl ll →
relate_TCB_Log_Pool s
(ZMap.set 0 l0 hl) (ZMap.set 0 l0 ll).
Proof.
intros. inv H. constructor; eauto.
- intros. destruct (zeq r 0); subst.
+ repeat rewrite ZMap.gss. trivial.
+ repeat rewrite ZMap.gso; eauto.
- intros.
assert (Hneq: i + ID_AT_range ≠ 0).
{
unfold ID_AT_range. omega.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma real_relate_TCB_Log_Pool:
∀ s habd labd,
relate_TCB_Log_Pool s (multi_log habd) (multi_log labd) →
relate_TCB_Log_Pool s (CalTicketLock.real_multi_log (multi_log habd)) (CalTicketLock.real_multi_log (multi_log labd)).
Proof.
assert (Hcases: ∀ a b, 0 ≤ a < b ∨ (a < 0 ∨ b ≤ a)) by (intros; omega).
assert (HZ2Nat: ∀ a b, 0 ≤ a < b → (0 ≤ Z.to_nat a < Z.to_nat b)%nat).
{
split.
rewrite <- Z2Nat.inj_0; rewrite <- Z2Nat.inj_le; omega.
rewrite <- Z2Nat.inj_lt; omega.
}
unfold CalTicketLock.real_multi_log; intros s d1 d2 Hrel; inv Hrel; constructor.
- intros i ofs r Hneq Hind.
destruct (Hcases r lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id r); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
- intros i Hi.
destruct (Hcases (i + ID_AT_range) lock_range) as [Hcase|Hcase].
+ rewrite <- (Z2Nat.id (i + ID_AT_range)); try omega.
rewrite 2 CalTicketLock.real_multi_log_pb_in; auto; constructor; constructor.
+ rewrite <- (Z2Nat.id lock_range) in Hcase.
rewrite 2 CalTicketLock.real_multi_log_pb_notin; eauto.
compute; intuition.
Qed.
Lemma sharedmem_init_exists :
∀ s mbi_adr adt adt´ ladt f,
sharedmem_init_spec (Int.unsigned mbi_adr) adt = Some adt´
→ relate_AbData s f adt ladt
→ ∃ ladt´,
sharedmem_init_spec (Int.unsigned mbi_adr) ladt = Some ladt´
∧ relate_AbData s f adt´ ladt´.
Proof.
unfold sharedmem_init_spec.
intros until f. exist_simpl.
- apply real_relate_TCB_Log_Pool; eauto.
Qed.
Lemma sharedmem_init_match:
∀ s d d´ m i f,
sharedmem_init_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold sharedmem_init_spec; intros. subdestruct. inv H.
inv H0. econstructor; eauto.
Qed.
Lemma palloc_exist:
∀ s habd habd´ labd n i f,
palloc_spec n habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, palloc_spec n labd = Some (labd´, i) ∧ relate_AbData s f habd´ labd´.
Proof.
unfold palloc_spec; intros.
revert H. pose proof H0 as HR. inv H0.
assert (Hlog: ZMap.get 0 (multi_log habd) = ZMap.get 0 (multi_log labd)).
{
inv multi_log_re. eapply (H 0 0); auto. omega.
}
assert (Horacle: ZMap.get 0 (multi_oracle habd) = ZMap.get 0 (multi_oracle labd)).
{
inv multi_oracle_re. eapply (H 0 0); auto. omega.
}
rewrite Horacle.
subrewrite. subdestruct; inv HQ.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_TCB_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_TCB_Log_Pool_gss. eauto.
- refine_split´; eauto.
constructor; eauto; simpl.
eapply relate_TCB_Log_Pool_gss. eauto.
Qed.
Lemma palloc_match:
∀ s d d´ m n i f,
palloc_spec n d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold palloc_spec; intros. inv H0.
subdestruct; inv H; subst; trivial.
- econstructor; eauto.
- econstructor; eauto.
- econstructor; eauto.
Qed.
Lemma ptAllocPDE0_exist:
∀ s habd habd´ labd i n v f,
ptAllocPDE0_spec n v habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptAllocPDE0_spec n v labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptAllocPDE0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; destruct p; inv HQ.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
rewrite H. rewrite Hdestruct8.
refine_split´; trivial.
inv H0.
constructor; simpl; try eassumption.
+ apply FlatMem.free_page_inj´. trivial.
+ subrewrite´.
+ subrewrite´.
Qed.
Lemma ptAllocPDE0_match:
∀ s n v i d d´ m f,
ptAllocPDE0_spec n v d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptAllocPDE0_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- exploit palloc_match; eauto.
intros Hm. inv Hm.
econstructor; eauto.
Qed.
Lemma ptInsert0_exist:
∀ s habd habd´ labd i n v pa pe f,
ptInsert0_spec n v pa pe habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptInsert0_spec n v pa pe labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptInsert0_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- exploit (ptInsertPTE0_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
refine_split´; trivial.
- exploit ptAllocPDE0_exist; eauto.
intros (labd´ & HptInsert0´ & Hre).
subrewrite´.
exploit (ptInsertPTE0_exist s); eauto.
intros (labd´0 & HptInsert0´´ & Hre´).
subrewrite´.
refine_split´; trivial.
Qed.
Lemma ptInsert0_match:
∀ s n v pa pe d d´ m i f,
ptInsert0_spec n v pa pe d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptInsert0_spec; intros. subdestruct; inv H; trivial.
- exploit ptInsertPTE0_match; eauto.
- eapply ptAllocPDE0_match; eauto.
- exploit ptInsertPTE0_match; eauto.
eapply ptAllocPDE0_match; eauto.
Qed.
Lemma ptResv_exist:
∀ s habd habd´ labd i n v p f,
ptResv_spec n v p habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv_spec n v p labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv_spec; intros.
subdestruct. destruct p0.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
Qed.
Lemma ptResv_match:
∀ s d d´ m i n v p f,
ptResv_spec n v p d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptResv_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
Qed.
Lemma ptResv2_exist:
∀ s habd habd´ labd i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ habd = Some (habd´, i)
→ relate_AbData s f habd labd
→ ∃ labd´, ptResv2_spec n v p n´ v´ p´ labd = Some (labd´, i)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold ptResv2_spec; intros.
subdestruct; destruct p0; inv H.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?).
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. inv H. refine_split´; trivial.
- exploit palloc_exist; eauto.
intros (? & ? & ?). revert H2.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?). intros.
exploit (ptInsert0_exist s); eauto.
intros (? & ? & ?).
subrewrite´. refine_split´; trivial.
Qed.
Lemma ptResv2_match:
∀ s d d´ m i n v p n´ v´ p´ f,
ptResv2_spec n v p n´ v´ p´ d = Some (d´, i)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold ptResv2_spec; intros. subdestruct; inv H; trivial.
- eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
- eapply ptInsert0_match; eauto.
eapply ptInsert0_match; eauto.
eapply palloc_match; eauto.
Qed.
Lemma offer_shared_mem_exists:
∀ s habd habd´ labd i1 i2 v z f,
offer_shared_mem_spec i1 i2 v habd = Some (habd´, z)
→ relate_AbData s f habd labd
→ ∃ labd´, offer_shared_mem_spec i1 i2 v labd = Some (labd´, z)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold offer_shared_mem_spec; intros.
pose proof H0 as HR. inv H0.
revert H. subrewrite.
subdestruct; inv HQ.
- refine_split´; trivial.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- exploit (ptResv2_exist s); eauto.
intros (labd´ & HptInsert0´ & Hre).
inv Hre.
subrewrite´.
refine_split´; trivial.
constructor; eauto.
- refine_split´; trivial.
constructor; eauto.
Qed.
Lemma offer_shared_mem_match:
∀ s d d´ m i1 i2 v z f,
offer_shared_mem_spec i1 i2 v d = Some (d´, z)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold offer_shared_mem_spec; intros. subdestruct; inv H; trivial.
- exploit ptResv2_match; eauto.
intros Hm. inv Hm.
econstructor; eauto.
- exploit ptResv2_match; eauto.
intros Hm. inv Hm.
econstructor; eauto.
- inv H0. econstructor; eauto.
Qed.
Lemma Shared2ID1_imply:
∀ i id,
Shared2ID2 i = Some id → Shared2ID1 i = Some id.
Proof.
intros. functional inversion H; subst.
auto.
Qed.
Lemma Shared2ID2_neq:
∀ i p,
Shared2ID2 i = Some p →
i ≠ ID_TCB.
Proof.
intros. functional inversion H; subst. omega.
Qed.
Lemma release_lock_exist:
∀ s i ofs e habd habd´ labd f,
release_lock_spec2 i ofs e habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, release_lock_spec1 i ofs e labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold release_lock_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct. inv HQ.
erewrite Shared2ID1_imply; eauto.
inv multi_log_re.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
subrewrite´.
refine_split´; eauto.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq; eauto.
eapply Shared2ID2_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma release_lock_match2:
∀ s i ofs e d d´ m f,
release_lock_spec2 i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_lock_spec; intros.
subdestruct; inv H.
inv H0. econstructor; eauto.
Qed.
Lemma release_lock_sim2 :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id release_lock_spec2)
(id ↦ primcall_release_lock_compatsem id release_lock_spec1).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit release_lock_exist; eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- eapply release_lock_match2 in H4; eauto.
repeat (econstructor; eauto).
subst rs´. val_inject_simpl.
Qed.
Lemma acquire_lock_exist:
∀ s bound i ofs habd habd´ labd f p l,
acquire_lock_spec2 bound i ofs habd = Some (habd´, p, l)
→ relate_AbData s f habd labd
→ (∃ labd´, acquire_lock_spec1 bound i ofs labd = Some (labd´, p, l) ∧
relate_AbData s f habd´ labd´)
∧ Shared2ID2 i = Some p.
Proof.
unfold acquire_lock_spec; intros.
pose proof H0 as HR. inv H0.
revert H.
subrewrite.
subdestruct. inv HQ.
erewrite Shared2ID1_imply; eauto.
inv multi_log_re.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
pose proof multi_oracle_re as Horacle.
inv multi_oracle_re.
exploit H1; eauto.
{
eapply Shared2ID2_neq; eauto.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
subrewrite´.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq; eauto.
eapply Shared2ID2_neq; eauto.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma acquire_lock_match:
∀ s bound i ofs d d´ m f p l,
acquire_lock_spec2 bound i ofs d = Some (d´, p, l)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold acquire_lock_spec; intros.
subdestruct; inv H.
inv H0. econstructor; eauto.
Qed.
Lemma acquire_lock_sim2:
∀ id,
sim (crel RData RData)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec2)
(id ↦ primcall_acquire_lock_compatsem acquire_lock_spec1).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit acquire_lock_exist; eauto 1; intros ((labd´ & HP & HM) & HS).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H10.
destruct l; subst.
{
exploit Mem.storebytes_mapped_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
{ eapply list_forall2_bytelist_inject; eauto. }
intros (m2´ & Hst & Hinj).
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
assert (Hmatch: match_AbData s d1´ m2´ ι).
{
eapply acquire_lock_match in H4; eauto.
eapply storebytes_match_correct; eauto.
intros.
destruct (peq i id0).
+ subst. inv H.
functional inversion HS. inv H1.
+ red; intros; subst. elim n.
eapply (genv_vars_inj s i id0); eauto.
}
match_external_states_simpl.
- simpl; trivial.
-
erewrite Mem.nextblock_storebytes; eauto.
eapply Mem.nextblock_storebytes in Hst; eauto.
rewrite Hst. assumption.
-
intros. red; intros.
eapply match_newglob_noperm; eauto.
eapply Mem.perm_storebytes_2; eauto.
-
erewrite Mem.nextblock_storebytes; eauto.
-
subst rs´.
val_inject_simpl.
}
{
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
eapply acquire_lock_match in H4; eauto.
match_external_states_simpl.
subst rs´. val_inject_simpl.
}
Qed.
Section PAGE_COPY_SIM.
Lemma page_copy_exist:
∀ s habd habd´ labd index i from f,
page_copy_spec index i from habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_spec index i from labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_spec; intros.
inv H0.
revert H. subrewrite.
subdestruct. inv HQ.
inv multi_log_re.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
reflexivity.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
rewrite Hdestruct7.
exploit page_copy_aux_exists; eauto.
intros Hcopy´; rewrite Hcopy´.
rewrite Hdestruct11.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq; eauto.
eapply Shared2ID2_neq; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy_match:
∀ s d d´ m index i from f,
page_copy_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_spec; intros. subdestruct.
inv H. inv H0. econstructor; eauto.
Qed.
Lemma page_copy_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_spec)
(id ↦ gensem page_copy_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_exist; eauto 1.
exploit page_copy_match; eauto 1.
intro Hmatch.
intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End PAGE_COPY_SIM.
Section PAGE_COPY_BACK_SIM.
Lemma page_copy_back_exist:
∀ s habd habd´ labd index i to f,
page_copy_back_spec index i to habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, page_copy_back_spec index i to labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold page_copy_back_spec; intros.
inv H0.
revert H. subrewrite.
subdestruct. inv HQ.
inv multi_log_re.
exploit H; eauto.
{
eapply Shared2ID2_neq; eauto.
reflexivity.
}
intros Htcb. rewrite <- Htcb. clear Htcb.
rewrite Hdestruct7.
rewrite Hdestruct10.
exploit page_copy_back_aux_exists; eauto.
intros [lh´ [Hcopy´ HPRel]]; rewrite Hcopy´.
refine_split´; trivial.
constructor; eauto; simpl.
constructor; simpl.
+ intros.
destruct (zeq r z); subst.
× repeat rewrite ZMap.gss; eauto.
× repeat rewrite ZMap.gso; eauto.
+ intros.
assert (Hneq: z ≠ (i0 + ID_AT_range)).
{
eapply index2Z_neq; eauto.
eapply Shared2ID2_neq; eauto.
reflexivity.
}
repeat rewrite ZMap.gso; eauto.
Qed.
Lemma page_copy_back_match:
∀ s d d´ m index i to f,
page_copy_back_spec index i to d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy_back_spec; intros. subdestruct.
inv H. inv H0. econstructor; eauto.
Qed.
Lemma page_copy_back_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy_back_spec)
(id ↦ gensem page_copy_back_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy_back_exist; eauto 1.
exploit page_copy_back_match; eauto 1.
intro Hmatch.
intros [labd´ [HP HM]].
match_external_states_simpl.
Qed.
End PAGE_COPY_BACK_SIM.
End Exists.
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store) (lflatmem_store:= flatmem_store)).
Proof.
accessor_prop_tac.
- eapply flatmem_store_exists; eauto.
- eapply flatmem_store_match; eauto.
Qed.
Lemma passthrough_correct:
sim (crel HDATA LDATA) pqueueintro_passthrough psleeper.
Proof.
sim_oplus.
- apply fload_sim.
- apply fstore_sim.
- apply page_copy_sim.
- apply page_copy_back_sim.
- apply vmxinfo_get_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit palloc_exist; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply palloc_match; eauto).
match_external_states_simpl.
- apply setPT_sim.
- apply ptRead_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit ptResv_exist; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply ptResv_match; eauto).
match_external_states_simpl.
- apply kctxt_new_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit sharedmem_init_exists; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply sharedmem_init_match; eauto).
match_external_states_simpl.
- apply shared_mem_status_sim.
-
layer_sim_simpl; compatsim_simpl (@match_AbData); intros.
exploit offer_shared_mem_exists; eauto 1; intros (labd´ & HP & HM).
assert (Hm: match_AbData s d1´ m2 ι) by (eapply offer_shared_mem_match; eauto).
match_external_states_simpl.
- apply ptin_sim.
- apply ptout_sim.
- apply container_get_nchildren_sim.
- apply container_get_quota_sim.
- apply container_get_usage_sim.
- apply container_can_consume_sim.
- apply get_CPU_ID_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply sleeper_inc_sim.
- apply sleeper_dec_sim.
- apply sleeper_zzz_sim.
- apply release_lock_sim2.
- apply acquire_lock_sim2.
- apply cli_sim.
- apply sti_sim.
- apply serial_intr_disable_sim.
- apply serial_intr_enable_sim.
- apply serial_putc_sim.
- apply cons_buf_read_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 kctxt_switch_sim.
- layer_sim_simpl.
+ eapply load_correct2.
+ eapply store_correct2.
Qed.
End WITHMEM.
End Refinement.