Library mcertikos.objects.tmobj.ObjTMVMM
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import AbstractDataType.
Require Import Integers.
Require Import Values.
Require Import Constant.
Require Import RealParams.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import CalTicketLock.
Require Import DeviceStateDataType.
Require Export ObjInterruptDriver.
Require Import BigStepLogReplay.
Require Import CommonTactic.
Require Import ObjLMM0.
Require Import ObjLMM1.
Require Import ObjVMM.
Require Import ObjCPU.
Require Import ObjCV.
Require Import ObjContainer.
Require Import ObjBigThread.
Require Import ObjInterruptController.
Require Import ObjInterruptManagement.
Require Import ObjSerialDriver.
Require Import ObjConsole.
Require Import ObjVMCS.
Require Import ObjEPT.
Require Import ObjVMX.
Require Import liblayers.compat.CompatGenSem.
Require Import Z64Lemma.
Require Import SingleOracle.
Require Import BigLogThreadConfigFunction.
Section OBJ_SECOND_Thread_VMM.
Context `{real_params: RealParams}.
Context `{oracle_ops: MultiOracleOps}.
Context `{big_oracle_ops: BigOracleOps}.
Function thread_vmxinfo_get_spec (i: Z) (adt: RData) :=
vmxinfo_get_spec i adt.
Function big2_palloc_spec (n: Z) (adt: RData): option (RData × Z) :=
let abid := 0 in
let cpu := CPU_ID adt in
let c := ZMap.get n (AC adt) in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq n curid then
match (init adt, ikern adt, ihost adt, pg adt, ipt adt , B_inLock cpu (big_log adt)) with
| (true, true, true, true, true , false) ⇒
match big_log adt, ZMap.get abid (lock adt) with
| BigDef l, LockFalse ⇒
if B_GetContainerUsed curid cpu l then
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
if (cusage c) <? (cquota c) then
let cur := mkContainer (cquota c) (cusage c + 1) (cparent c)
(cchildren c) (cused c) in
match B_CalAT_log_real l1 with
| Some a ⇒
match first_free a (nps adt) with
| inleft (exist i _) ⇒
let l´ := (TBEVENT cpu (TBSHARED (BPALLOCE curid i))) :: l1 in
Some (adt {big_log: BigDef l´}
{pperm: ZMap.set i PGAlloc (pperm adt)}
{AC: ZMap.set n cur (AC adt)},i)
| _ ⇒
let l´ := (TBEVENT cpu (TBSHARED (BPALLOCE curid 0))) :: l1 in
Some (adt{big_log: BigDef l´}, 0)
end
| _ ⇒ None
end
else
let l´ := (TBEVENT cpu (TBSHARED (BPALLOCE curid 0))) :: l1 in
Some (adt{big_log: BigDef l´}, 0)
else None
| _,_ ⇒ None
end
| _ ⇒ None
end
else None.
Lemma big2_palloc_inv_prop:
∀ n d d´ v,
big2_palloc_spec n d = Some (d´, v) →
ptpool d´ = ptpool d
∧ (v ≠ 0 →
ZMap.get v (pperm d´) = PGAlloc
∧ 0 < v < nps d´)
∧ pg d´ = true.
Proof.
unfold big2_palloc_spec. intros.
subdestruct; inv H; simpl; subst.
- repeat rewrite ZMap.gss. refine_split´; trivial.
destruct a0 as (? & ? & ?). intros.
refine_split´; trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
- refine_split´; trivial.
intros HF; elim HF. trivial.
Qed.
Function thread_setPT_spec (n : Z) (adt : RData) : option RData :=
if init adt then setPT_spec n adt else None.
Function thread_ptRead_spec (n vadr : Z) (adt : RData) : option Z :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if (init adt) then if zeq curid n then ptRead_spec n vadr adt else None else None.
Section INSERT2.
Function big2_ptInsertPTE0_spec (nn vadr padr: Z) (p: PTPerm) (adt: RData): option RData :=
match (init adt, ikern adt, ihost adt, pg adt, ipt adt, pt_Arg nn vadr padr (nps adt)) with
| (true, true, true, true, true, true) ⇒
let pt := ZMap.get nn (ptpool adt) in
let pdi := PDX vadr in
let pti := PTX vadr in
match (ZMap.get pdi pt, ZMap.get padr (pperm adt)) with
| (PDEValid pi pdt, PGAlloc) ⇒
match ZMap.get pti pdt with
| PTEValid _ _ ⇒ None
| _ ⇒
let pdt´:= ZMap.set pti (PTEValid padr p) pdt in
let pt´ := ZMap.set pdi (PDEValid pi pdt´) pt in
Some adt {ptpool: ZMap.set nn pt´ (ptpool adt)}
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function big2_ptAllocPDE_spec (nn vadr: Z) (adt: RData): option (RData × Z) :=
let pdi := PDX vadr in
let c := ZMap.get nn (AC adt) in
match (init adt, ikern adt, ihost adt, pg adt, ipt adt, pt_Arg´ nn vadr) with
| (true, true, true, true, true, true) ⇒
match ZMap.get pdi (ZMap.get nn (ptpool adt)) with
| PDEUnPresent ⇒
match big2_palloc_spec nn adt with
| Some (adt´, pi) ⇒
if zeq pi 0 then
Some (adt´, pi)
else
Some (adt´ {HP: FlatMem.free_page pi (HP adt´)}
{pperm: ZMap.set pi (PGHide (PGPMap nn pdi)) (pperm adt´)}
{ptpool: (ZMap.set nn (ZMap.set pdi (PDEValid pi real_init_PTE)
(ZMap.get nn (ptpool adt´))) (ptpool adt´))}
, pi)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
primitve: set the n-th page table with virtual address vadr to (padr + perm) The pt insert at this layer, is slightly different from the one at MPTComm.
0th page map has been reserved for the kernel thread, which couldn't be modified after the initialization
Function big2_ptInsert_spec (nn vadr padr perm: Z) (adt: RData) : option (RData × Z) :=
match (init adt, ikern adt, ihost adt, ipt adt, pg adt, pt_Arg nn vadr padr (nps adt)) with
| (true, true, true, true, true, true) ⇒
match ZtoPerm perm with
| Some p ⇒
let pt := ZMap.get nn (ptpool adt) in
let pdi := PDX vadr in
let pti := PTX vadr in
match ZMap.get pdi pt with
| PDEValid pi pdt ⇒
match big2_ptInsertPTE0_spec nn vadr padr p adt with
| Some adt´ ⇒ Some (adt´, 0)
| _ ⇒ None
end
| PDEUnPresent ⇒
match big2_ptAllocPDE_spec nn vadr adt with
| Some (adt´, v) ⇒
if zeq v 0 then Some (adt´, MagicNumber)
else
match big2_ptInsertPTE0_spec nn vadr padr p adt´ with
| Some adt´´ ⇒ Some (adt´´, v)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End INSERT2.
Function big2_ptResv_spec (n vadr perm: Z) (adt: RData): option (RData × Z) :=
if zeq n (ZMap.get (CPU_ID adt) (cid adt)) then
match big2_palloc_spec n adt with
| Some (abd´, b) ⇒
if zeq b 0 then Some (abd´, MagicNumber)
else big2_ptInsert_spec n vadr b perm abd´
| _ ⇒ None
end
else None.
Function thread_container_get_nchildren_spec (i: Z) (adt: RData) : option Z :=
let c := ZMap.get i (AC adt) in
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq i curid then
match (init adt, ikern adt, ihost adt ) with
| (true, true, true ) ⇒
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
Some (Z_of_nat (length (cchildren c)))
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function thread_container_get_quota_spec (i: Z) (adt: RData) : option Z :=
let c := ZMap.get i (AC adt) in
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq i curid then
match (init adt, ikern adt, ihost adt ) with
| (true, true, true) ⇒
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then Some (cquota c)
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function thread_container_get_usage_spec (i: Z) (adt: RData): option Z :=
let c := ZMap.get i (AC adt) in
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq i curid then
match (init adt, ikern adt, ihost adt ) with
| (true, true, true ) ⇒
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then Some (cusage c)
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function thread_container_can_consume_spec (i: Z) (n: Z) (adt: RData) : option Z :=
let c := ZMap.get i (AC adt) in
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq i curid then
match (init adt, ikern adt, ihost adt ) with
| (true, true, true ) ⇒
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then Some (if zle_le 0 n (cquota c - cusage c)
then 1 else 0)
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
End OBJ_SECOND_Thread_VMM.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import GlobIdent.
Require Import AuxLemma.
Require Import INVLemmaThread.
Local Open Scope Z_scope.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Local Open Scope Z_scope.
Context `{oracle_ops: MultiOracleOps}.
Context `{big_oracle_ops: BigOracleOps}.
Section THREAD_VMXINFO_GET_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmxinfo}.
Lemma thread_vmxinfo_get_exist:
∀ s i habd labd v f,
thread_vmxinfo_get_spec i habd = Some v
→ relate_AbData s f habd labd
→ thread_vmxinfo_get_spec i labd = Some v.
Proof.
unfold thread_vmxinfo_get_spec; intros.
subdestruct.
eauto using vmxinfo_get_exist.
Qed.
Lemma thread_vmxinfo_get_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_vmxinfo_get_spec)
(id ↦ gensem thread_vmxinfo_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_vmxinfo_get_exist; eauto 1; trivial.
Qed.
End THREAD_VMXINFO_GET_SIM_PROOF.
Section BIG2_PALLOC_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_cid}.
Context {re11: relate_impl_big_oracle}.
Context {re12: relate_impl_init}.
Lemma big2_palloc_exist:
∀ s f habd habd´ labd n a,
big2_palloc_spec n habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big2_palloc_spec n labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_palloc_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_AC_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
exploit relate_impl_lock_eq; eauto.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_pperm_eq; eauto.
exploit relate_impl_big_oracle_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ.
- refine_split´. rewrite H3 in Hdestruct10. rewrite Hdestruct10.
rewrite Hdestruct11. reflexivity.
eapply relate_impl_AC_update.
eapply relate_impl_pperm_update.
rewrite H3.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. rewrite H3 in Hdestruct10. rewrite Hdestruct10.
rewrite Hdestruct11.
reflexivity.
rewrite H3.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
rewrite H3. eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_AC}.
Context {mt2: match_impl_pperm}.
Context {mt4: match_impl_big_log}.
Lemma big2_palloc_match:
∀ s d d´ m f n a,
big2_palloc_spec n d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_palloc_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_AC_update.
eapply match_impl_pperm_update.
eapply match_impl_big_log_update.
assumption.
- eapply match_impl_big_log_update.
assumption.
- eapply match_impl_big_log_update.
assumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_palloc_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_palloc_spec}.
Lemma big2_palloc_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_palloc_spec)
(id ↦ gensem big2_palloc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_palloc_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_palloc_match; eauto.
Qed.
End BIG2_PALLOC_SIM_PROOF.
Section THREAD_SETPT_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_ptpool}.
Context {re5: relate_impl_init}.
Lemma thread_setPT_exist:
∀ s habd habd´ labd i f,
thread_setPT_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_setPT_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold thread_setPT_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
rewrite <- H1.
subdestruct.
eauto using setPT_exist.
Qed.
Context {mt1: match_impl_PT}.
Lemma thread_setPT_match:
∀ s d d´ m i f,
thread_setPT_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_setPT_spec; intros.
subdestruct; trivial.
inv H.
eapply setPT_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_setPT_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_setPT_spec}.
Lemma thread_setPT_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_setPT_spec)
(id ↦ gensem thread_setPT_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_setPT_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_setPT_match; eauto.
Qed.
End THREAD_SETPT_SIM_PROOF.
Section THREAD_PT_READ_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_ptpool}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_cid}.
Lemma thread_ptRead_exist:
∀ s habd labd n vadr z f,
thread_ptRead_spec n vadr habd = Some z
→ relate_AbData s f habd labd
→ thread_ptRead_spec n vadr labd = Some z.
Proof.
unfold thread_ptRead_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
rewrite <- H1, <- H2, <- H3.
subdestruct.
eapply ptRead_exist; eauto.
Qed.
Lemma thread_ptRead_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_ptRead_spec)
(id ↦ gensem thread_ptRead_spec).
Proof.
intros. layer_sim_simpl.
compatsim_simpl´.
match_external_states_simpl.
erewrite thread_ptRead_exist; eauto.
reflexivity.
Qed.
End THREAD_PT_READ_SIM_PROOF.
Section BIG2_PT_RESV_SIM_PROOF_MOD.
Section BIG2_PTALLOCPDE_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_pperm}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_cid}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_init}.
Lemma big2_ptAllocPDE_exist:
∀ s f habd habd´ labd n v p,
big2_ptAllocPDE_spec n v habd = Some (habd´, p)
→ relate_AbData s f habd labd
→ ∃ labd´, big2_ptAllocPDE_spec n v labd = Some (labd´, p)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_ptAllocPDE_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_HP_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
- specialize (big2_palloc_exist _ _ _ _ _ _ _ Hdestruct6 H0). intros [ld1 [Hballoc Hrealloc]].
rewrite Hballoc. simpl. subst.
∃ ld1. split; eauto.
- specialize (big2_palloc_exist _ _ _ _ _ _ _ Hdestruct6 H0). intros [ld1 [Hballoc Hrealloc]].
rewrite Hballoc. rewrite Hdestruct8.
esplit. split. reflexivity.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_pperm_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
eapply relate_impl_ptpool_update.
eapply relate_impl_pperm_update.
eapply relate_impl_HP_update; eauto.
eapply FlatMem.free_page_inj´. unfold FlatMem.flatmem_inj. intros. eapply relate_impl_HP_eq; eauto.
Grab Existential Variables.
eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Lemma big2_ptAllocPDE_match:
∀ s d d´ m f n v p,
big2_ptAllocPDE_spec n v d = Some (d´, p)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_ptAllocPDE_spec; intros.
subdestruct; inv H; trivial.
- subst. eapply big2_palloc_match; eauto.
- eapply match_impl_ptpool_update.
eapply match_impl_pperm_update.
eapply match_impl_HP_update.
eapply big2_palloc_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_ptAllocPDE_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_ptAllocPDE_spec}.
Lemma big2_ptAllocPDE_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_ptAllocPDE_spec)
(id ↦ gensem big2_ptAllocPDE_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_ptAllocPDE_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_ptAllocPDE_match; eauto.
Qed.
End BIG2_PTALLOCPDE_SIM_PROOF.
Section BIG2_PT_RESV_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_pperm}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_big_oracle}.
Context {re10: relate_impl_HP}.
Context {re11: relate_impl_ptpool}.
Context {re12: relate_impl_cid}.
Context {re13: relate_impl_init}.
Lemma big2_ptInsertPTE0_exist:
∀ s habd habd´ labd n v pa pe f,
big2_ptInsertPTE0_spec n v pa pe habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big2_ptInsertPTE0_spec n v pa pe labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_ptInsertPTE0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_pperm_eq; eauto.
exploit relate_impl_init_eq; eauto.
intros. revert H.
subrewrite. subdestruct; inv HQ; refine_split´; trivial.
- apply relate_impl_ptpool_update; assumption.
- apply relate_impl_ptpool_update; assumption.
Qed.
Lemma big2_ptInsert_exist:
∀ s f habd habd´ labd n vadr perm z a,
big2_ptInsert_spec n vadr perm z habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big2_ptInsert_spec n vadr perm z labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_ptInsert_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_nps_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
revert H. subrewrite. subdestruct; inv HQ.
- exploit big2_ptInsertPTE0_exist; eauto.
intros (labd´ & → & Hr).
refine_split´; eauto.
- exploit big2_ptAllocPDE_exist; eauto.
intros (labd´ & → & Hr).
rewrite zeq_true.
refine_split´; eauto.
- exploit big2_ptAllocPDE_exist; eauto.
intros (labd´ & → & Hr).
rewrite zeq_false; auto.
exploit big2_ptInsertPTE0_exist; eauto.
intros (labd´´ & → & Hr´).
refine_split´; eauto.
Qed.
Lemma big2_ptResv_exist:
∀ s f habd habd´ labd n vadr perm a,
big2_ptResv_spec n vadr perm habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big2_ptResv_spec n vadr perm labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_ptResv_spec. intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct_one.
subdestruct_one. destruct p.
exploit big2_palloc_exist; eauto.
intros (labd´ & → & Hr).
subdestruct; inv H.
- refine_split´; eauto.
rewrite H1, H2; rewrite zeq_true; auto.
- rewrite H1, H2; rewrite zeq_true; eauto.
exploit big2_ptInsert_exist; eauto.
rewrite H1, H2; eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Lemma big2_ptInsertPTE0_match:
∀ s n v pa pe d d´ m f,
big2_ptInsertPTE0_spec n v pa pe d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_ptInsertPTE0_spec; intros.
subdestruct; inv H; trivial;
eapply match_impl_ptpool_update;
assumption.
Qed.
Lemma big2_ptInsert_match:
∀ s d d´ m f n vadr perm z a,
big2_ptInsert_spec n vadr perm z d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_ptInsert_spec; intros.
subdestruct; inv H; trivial.
- eapply big2_ptInsertPTE0_match; eauto.
- eapply big2_ptAllocPDE_match; eauto.
- eapply big2_ptInsertPTE0_match; eauto.
eapply big2_ptAllocPDE_match; eauto.
Qed.
Lemma big2_ptResv_match:
∀ s d d´ m f n vadr perm a,
big2_ptResv_spec n vadr perm d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_ptResv_spec; intros.
subdestruct; inv H; trivial.
- eapply big2_palloc_match; eauto.
- eapply big2_palloc_match in Hdestruct0; eauto.
eapply big2_ptInsert_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_ptResv_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_ptResv_spec}.
Lemma big2_ptResv_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_ptResv_spec)
(id ↦ gensem big2_ptResv_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_ptResv_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_ptResv_match; eauto.
Qed.
End BIG2_PT_RESV_SIM_PROOF.
End BIG2_PT_RESV_SIM_PROOF_MOD.
Section THREAD_CONTAINER_GET_NCHILDREN_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_AC}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_big_log}.
Lemma thread_container_get_nchildren_exist:
∀ s habd labd i p f,
thread_container_get_nchildren_spec i habd = Some p
→ relate_AbData s f habd labd
→ thread_container_get_nchildren_spec i labd = Some p.
Proof.
unfold thread_container_get_nchildren_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
intros.
revert H; subrewrite.
Qed.
Lemma thread_container_get_nchildren_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_container_get_nchildren_spec)
(id ↦ gensem thread_container_get_nchildren_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_container_get_nchildren_exist; eauto 1.
reflexivity.
Qed.
End THREAD_CONTAINER_GET_NCHILDREN_SIM_PROOF.
Section THREAD_CONTAINER_GET_QUOTA_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_AC}.
Context {re3 : relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_big_log}.
Lemma thread_container_get_quota_exist:
∀ s habd labd i p f,
thread_container_get_quota_spec i habd = Some p
→ relate_AbData s f habd labd
→ thread_container_get_quota_spec i labd = Some p.
Proof.
unfold thread_container_get_quota_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
intros.
revert H; subrewrite.
Qed.
Lemma thread_container_get_quota_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_container_get_quota_spec)
(id ↦ gensem thread_container_get_quota_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_container_get_quota_exist; eauto 1.
reflexivity.
Qed.
End THREAD_CONTAINER_GET_QUOTA_SIM_PROOF.
Section THREAD_CONTAINER_GET_USAGE_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_AC}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_big_log}.
Lemma thread_container_get_usage_exist:
∀ s habd labd i p f,
thread_container_get_usage_spec i habd = Some p
→ relate_AbData s f habd labd
→ thread_container_get_usage_spec i labd = Some p.
Proof.
unfold thread_container_get_usage_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
intros.
revert H; subrewrite.
Qed.
Lemma thread_container_get_usage_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_container_get_usage_spec)
(id ↦ gensem thread_container_get_usage_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_container_get_usage_exist; eauto 1.
reflexivity.
Qed.
End THREAD_CONTAINER_GET_USAGE_SIM_PROOF.
Section THREAD_CONTAINER_CAN_CONSUME_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_AC}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_big_log}.
Lemma thread_container_can_consume_exist:
∀ s habd labd i n b f,
thread_container_can_consume_spec i n habd = Some b
→ relate_AbData s f habd labd
→ thread_container_can_consume_spec i n labd = Some b.
Proof.
unfold thread_container_can_consume_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
intros.
revert H; subrewrite.
Qed.
Lemma thread_container_can_consume_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_container_can_consume_spec)
(id ↦ gensem thread_container_can_consume_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_container_can_consume_exist; eauto 1.
reflexivity.
Qed.
End THREAD_CONTAINER_CAN_CONSUME_SIM_PROOF.
End OBJ_SIM.
match (init adt, ikern adt, ihost adt, ipt adt, pg adt, pt_Arg nn vadr padr (nps adt)) with
| (true, true, true, true, true, true) ⇒
match ZtoPerm perm with
| Some p ⇒
let pt := ZMap.get nn (ptpool adt) in
let pdi := PDX vadr in
let pti := PTX vadr in
match ZMap.get pdi pt with
| PDEValid pi pdt ⇒
match big2_ptInsertPTE0_spec nn vadr padr p adt with
| Some adt´ ⇒ Some (adt´, 0)
| _ ⇒ None
end
| PDEUnPresent ⇒
match big2_ptAllocPDE_spec nn vadr adt with
| Some (adt´, v) ⇒
if zeq v 0 then Some (adt´, MagicNumber)
else
match big2_ptInsertPTE0_spec nn vadr padr p adt´ with
| Some adt´´ ⇒ Some (adt´´, v)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
End INSERT2.
Function big2_ptResv_spec (n vadr perm: Z) (adt: RData): option (RData × Z) :=
if zeq n (ZMap.get (CPU_ID adt) (cid adt)) then
match big2_palloc_spec n adt with
| Some (abd´, b) ⇒
if zeq b 0 then Some (abd´, MagicNumber)
else big2_ptInsert_spec n vadr b perm abd´
| _ ⇒ None
end
else None.
Function thread_container_get_nchildren_spec (i: Z) (adt: RData) : option Z :=
let c := ZMap.get i (AC adt) in
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq i curid then
match (init adt, ikern adt, ihost adt ) with
| (true, true, true ) ⇒
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
Some (Z_of_nat (length (cchildren c)))
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function thread_container_get_quota_spec (i: Z) (adt: RData) : option Z :=
let c := ZMap.get i (AC adt) in
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq i curid then
match (init adt, ikern adt, ihost adt ) with
| (true, true, true) ⇒
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then Some (cquota c)
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function thread_container_get_usage_spec (i: Z) (adt: RData): option Z :=
let c := ZMap.get i (AC adt) in
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq i curid then
match (init adt, ikern adt, ihost adt ) with
| (true, true, true ) ⇒
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then Some (cusage c)
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function thread_container_can_consume_spec (i: Z) (n: Z) (adt: RData) : option Z :=
let c := ZMap.get i (AC adt) in
let cpu := CPU_ID adt in
let curid := ZMap.get (CPU_ID adt) (cid adt) in
if zeq i curid then
match (init adt, ikern adt, ihost adt ) with
| (true, true, true ) ⇒
match big_log adt with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then Some (if zle_le 0 n (cquota c - cusage c)
then 1 else 0)
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
End OBJ_SECOND_Thread_VMM.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import PrimSemantics.
Require Import GlobIdent.
Require Import AuxLemma.
Require Import INVLemmaThread.
Local Open Scope Z_scope.
Section OBJ_SIM.
Context `{data : CompatData RData}.
Context `{data0 : CompatData RData}.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModel}.
Context `{Hmwd: UseMemWithData mem}.
Context `{real_params: RealParams}.
Notation HDATAOps := (cdata (cdata_prf := data) RData).
Notation LDATAOps := (cdata (cdata_prf := data0) RData).
Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
(stencil_ops:= stencil_ops) HDATAOps LDATAOps}.
Local Open Scope Z_scope.
Context `{oracle_ops: MultiOracleOps}.
Context `{big_oracle_ops: BigOracleOps}.
Section THREAD_VMXINFO_GET_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_vmxinfo}.
Lemma thread_vmxinfo_get_exist:
∀ s i habd labd v f,
thread_vmxinfo_get_spec i habd = Some v
→ relate_AbData s f habd labd
→ thread_vmxinfo_get_spec i labd = Some v.
Proof.
unfold thread_vmxinfo_get_spec; intros.
subdestruct.
eauto using vmxinfo_get_exist.
Qed.
Lemma thread_vmxinfo_get_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_vmxinfo_get_spec)
(id ↦ gensem thread_vmxinfo_get_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_vmxinfo_get_exist; eauto 1; trivial.
Qed.
End THREAD_VMXINFO_GET_SIM_PROOF.
Section BIG2_PALLOC_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re8: relate_impl_pperm}.
Context {re9: relate_impl_CPU_ID}.
Context {re10: relate_impl_cid}.
Context {re11: relate_impl_big_oracle}.
Context {re12: relate_impl_init}.
Lemma big2_palloc_exist:
∀ s f habd habd´ labd n a,
big2_palloc_spec n habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big2_palloc_spec n labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_palloc_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_AC_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
exploit relate_impl_lock_eq; eauto.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_pperm_eq; eauto.
exploit relate_impl_big_oracle_eq; eauto.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ.
- refine_split´. rewrite H3 in Hdestruct10. rewrite Hdestruct10.
rewrite Hdestruct11. reflexivity.
eapply relate_impl_AC_update.
eapply relate_impl_pperm_update.
rewrite H3.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. rewrite H3 in Hdestruct10. rewrite Hdestruct10.
rewrite Hdestruct11.
reflexivity.
rewrite H3.
eapply relate_impl_big_log_update.
assumption.
- refine_split´. reflexivity.
rewrite H3. eapply relate_impl_big_log_update.
assumption.
Qed.
Context {mt1: match_impl_AC}.
Context {mt2: match_impl_pperm}.
Context {mt4: match_impl_big_log}.
Lemma big2_palloc_match:
∀ s d d´ m f n a,
big2_palloc_spec n d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_palloc_spec; intros.
subdestruct; inv H; trivial.
- eapply match_impl_AC_update.
eapply match_impl_pperm_update.
eapply match_impl_big_log_update.
assumption.
- eapply match_impl_big_log_update.
assumption.
- eapply match_impl_big_log_update.
assumption.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_palloc_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_palloc_spec}.
Lemma big2_palloc_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_palloc_spec)
(id ↦ gensem big2_palloc_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_palloc_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_palloc_match; eauto.
Qed.
End BIG2_PALLOC_SIM_PROOF.
Section THREAD_SETPT_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_PT}.
Context {re3: relate_impl_ipt}.
Context {re4: relate_impl_ptpool}.
Context {re5: relate_impl_init}.
Lemma thread_setPT_exist:
∀ s habd habd´ labd i f,
thread_setPT_spec i habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, thread_setPT_spec i labd = Some labd´ ∧
relate_AbData s f habd´ labd´.
Proof.
unfold thread_setPT_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
rewrite <- H1.
subdestruct.
eauto using setPT_exist.
Qed.
Context {mt1: match_impl_PT}.
Lemma thread_setPT_match:
∀ s d d´ m i f,
thread_setPT_spec i d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold thread_setPT_spec; intros.
subdestruct; trivial.
inv H.
eapply setPT_match; eauto.
Qed.
Context {inv: PreservesInvariants (HD:= data) thread_setPT_spec}.
Context {inv0: PreservesInvariants (HD:= data0) thread_setPT_spec}.
Lemma thread_setPT_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_setPT_spec)
(id ↦ gensem thread_setPT_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit thread_setPT_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply thread_setPT_match; eauto.
Qed.
End THREAD_SETPT_SIM_PROOF.
Section THREAD_PT_READ_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_ptpool}.
Context {re4: relate_impl_init}.
Context {re5: relate_impl_CPU_ID}.
Context {re6: relate_impl_cid}.
Lemma thread_ptRead_exist:
∀ s habd labd n vadr z f,
thread_ptRead_spec n vadr habd = Some z
→ relate_AbData s f habd labd
→ thread_ptRead_spec n vadr labd = Some z.
Proof.
unfold thread_ptRead_spec; intros.
exploit relate_impl_init_eq; eauto; intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
rewrite <- H1, <- H2, <- H3.
subdestruct.
eapply ptRead_exist; eauto.
Qed.
Lemma thread_ptRead_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem thread_ptRead_spec)
(id ↦ gensem thread_ptRead_spec).
Proof.
intros. layer_sim_simpl.
compatsim_simpl´.
match_external_states_simpl.
erewrite thread_ptRead_exist; eauto.
reflexivity.
Qed.
End THREAD_PT_READ_SIM_PROOF.
Section BIG2_PT_RESV_SIM_PROOF_MOD.
Section BIG2_PTALLOCPDE_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_pperm}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_cid}.
Context {re10: relate_impl_big_oracle}.
Context {re11: relate_impl_HP}.
Context {re12: relate_impl_ptpool}.
Context {re13: relate_impl_init}.
Lemma big2_ptAllocPDE_exist:
∀ s f habd habd´ labd n v p,
big2_ptAllocPDE_spec n v habd = Some (habd´, p)
→ relate_AbData s f habd labd
→ ∃ labd´, big2_ptAllocPDE_spec n v labd = Some (labd´, p)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_ptAllocPDE_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_pperm_eq; eauto. intros.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_HP_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto. intros.
exploit relate_impl_big_oracle_eq; eauto. intros.
exploit relate_impl_big_log_eq; eauto. intros.
exploit relate_impl_cid_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
- specialize (big2_palloc_exist _ _ _ _ _ _ _ Hdestruct6 H0). intros [ld1 [Hballoc Hrealloc]].
rewrite Hballoc. simpl. subst.
∃ ld1. split; eauto.
- specialize (big2_palloc_exist _ _ _ _ _ _ _ Hdestruct6 H0). intros [ld1 [Hballoc Hrealloc]].
rewrite Hballoc. rewrite Hdestruct8.
esplit. split. reflexivity.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_pperm_eq; eauto. intros.
revert H. subrewrite; subdestruct; inv HQ; subst.
eapply relate_impl_ptpool_update.
eapply relate_impl_pperm_update.
eapply relate_impl_HP_update; eauto.
eapply FlatMem.free_page_inj´. unfold FlatMem.flatmem_inj. intros. eapply relate_impl_HP_eq; eauto.
Grab Existential Variables.
eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Lemma big2_ptAllocPDE_match:
∀ s d d´ m f n v p,
big2_ptAllocPDE_spec n v d = Some (d´, p)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_ptAllocPDE_spec; intros.
subdestruct; inv H; trivial.
- subst. eapply big2_palloc_match; eauto.
- eapply match_impl_ptpool_update.
eapply match_impl_pperm_update.
eapply match_impl_HP_update.
eapply big2_palloc_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_ptAllocPDE_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_ptAllocPDE_spec}.
Lemma big2_ptAllocPDE_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_ptAllocPDE_spec)
(id ↦ gensem big2_ptAllocPDE_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_ptAllocPDE_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_ptAllocPDE_match; eauto.
Qed.
End BIG2_PTALLOCPDE_SIM_PROOF.
Section BIG2_PT_RESV_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_ipt}.
Context {re3: relate_impl_AC}.
Context {re4: relate_impl_big_log}.
Context {re5: relate_impl_lock}.
Context {re6: relate_impl_nps}.
Context {re7: relate_impl_pperm}.
Context {re8: relate_impl_CPU_ID}.
Context {re9: relate_impl_big_oracle}.
Context {re10: relate_impl_HP}.
Context {re11: relate_impl_ptpool}.
Context {re12: relate_impl_cid}.
Context {re13: relate_impl_init}.
Lemma big2_ptInsertPTE0_exist:
∀ s habd habd´ labd n v pa pe f,
big2_ptInsertPTE0_spec n v pa pe habd = Some habd´
→ relate_AbData s f habd labd
→ ∃ labd´, big2_ptInsertPTE0_spec n v pa pe labd = Some labd´
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_ptInsertPTE0_spec; intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_nps_eq; eauto.
exploit relate_impl_ptpool_eq; eauto.
exploit relate_impl_ipt_eq; eauto.
exploit relate_impl_pperm_eq; eauto.
exploit relate_impl_init_eq; eauto.
intros. revert H.
subrewrite. subdestruct; inv HQ; refine_split´; trivial.
- apply relate_impl_ptpool_update; assumption.
- apply relate_impl_ptpool_update; assumption.
Qed.
Lemma big2_ptInsert_exist:
∀ s f habd habd´ labd n vadr perm z a,
big2_ptInsert_spec n vadr perm z habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big2_ptInsert_spec n vadr perm z labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_ptInsert_spec. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_ipt_eq; eauto. intros.
exploit relate_impl_nps_eq; eauto. intros.
exploit relate_impl_ptpool_eq; eauto. intros.
exploit relate_impl_init_eq; eauto. intros.
revert H. subrewrite. subdestruct; inv HQ.
- exploit big2_ptInsertPTE0_exist; eauto.
intros (labd´ & → & Hr).
refine_split´; eauto.
- exploit big2_ptAllocPDE_exist; eauto.
intros (labd´ & → & Hr).
rewrite zeq_true.
refine_split´; eauto.
- exploit big2_ptAllocPDE_exist; eauto.
intros (labd´ & → & Hr).
rewrite zeq_false; auto.
exploit big2_ptInsertPTE0_exist; eauto.
intros (labd´´ & → & Hr´).
refine_split´; eauto.
Qed.
Lemma big2_ptResv_exist:
∀ s f habd habd´ labd n vadr perm a,
big2_ptResv_spec n vadr perm habd = Some (habd´, a)
→ relate_AbData s f habd labd
→ ∃ labd´, big2_ptResv_spec n vadr perm labd = Some (labd´, a)
∧ relate_AbData s f habd´ labd´.
Proof.
unfold big2_ptResv_spec. intros.
exploit relate_impl_CPU_ID_eq; eauto; intros.
exploit relate_impl_cid_eq; eauto; intros.
subdestruct_one.
subdestruct_one. destruct p.
exploit big2_palloc_exist; eauto.
intros (labd´ & → & Hr).
subdestruct; inv H.
- refine_split´; eauto.
rewrite H1, H2; rewrite zeq_true; auto.
- rewrite H1, H2; rewrite zeq_true; eauto.
exploit big2_ptInsert_exist; eauto.
rewrite H1, H2; eauto.
Qed.
Context {mt1: match_impl_ptpool}.
Context {mt2: match_impl_pperm}.
Context {mt3: match_impl_HP}.
Context {mt4: match_impl_big_log}.
Context {mt5: match_impl_AC}.
Lemma big2_ptInsertPTE0_match:
∀ s n v pa pe d d´ m f,
big2_ptInsertPTE0_spec n v pa pe d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_ptInsertPTE0_spec; intros.
subdestruct; inv H; trivial;
eapply match_impl_ptpool_update;
assumption.
Qed.
Lemma big2_ptInsert_match:
∀ s d d´ m f n vadr perm z a,
big2_ptInsert_spec n vadr perm z d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_ptInsert_spec; intros.
subdestruct; inv H; trivial.
- eapply big2_ptInsertPTE0_match; eauto.
- eapply big2_ptAllocPDE_match; eauto.
- eapply big2_ptInsertPTE0_match; eauto.
eapply big2_ptAllocPDE_match; eauto.
Qed.
Lemma big2_ptResv_match:
∀ s d d´ m f n vadr perm a,
big2_ptResv_spec n vadr perm d = Some (d´, a)
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold big2_ptResv_spec; intros.
subdestruct; inv H; trivial.
- eapply big2_palloc_match; eauto.
- eapply big2_palloc_match in Hdestruct0; eauto.
eapply big2_ptInsert_match; eauto.
Qed.
Context {inv1: PreservesInvariants (HD:= data) big2_ptResv_spec}.
Context {inv2: PreservesInvariants (HD:= data0) big2_ptResv_spec}.
Lemma big2_ptResv_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem big2_ptResv_spec)
(id ↦ gensem big2_ptResv_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
exploit big2_ptResv_exist; eauto 1; intros [labd´ [HP HM]].
match_external_states_simpl.
eapply big2_ptResv_match; eauto.
Qed.
End BIG2_PT_RESV_SIM_PROOF.
End BIG2_PT_RESV_SIM_PROOF_MOD.
Section THREAD_CONTAINER_GET_NCHILDREN_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_AC}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_big_log}.
Lemma thread_container_get_nchildren_exist:
∀ s habd labd i p f,
thread_container_get_nchildren_spec i habd = Some p
→ relate_AbData s f habd labd
→ thread_container_get_nchildren_spec i labd = Some p.
Proof.
unfold thread_container_get_nchildren_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
intros.
revert H; subrewrite.
Qed.
Lemma thread_container_get_nchildren_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_container_get_nchildren_spec)
(id ↦ gensem thread_container_get_nchildren_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_container_get_nchildren_exist; eauto 1.
reflexivity.
Qed.
End THREAD_CONTAINER_GET_NCHILDREN_SIM_PROOF.
Section THREAD_CONTAINER_GET_QUOTA_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_AC}.
Context {re3 : relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_big_log}.
Lemma thread_container_get_quota_exist:
∀ s habd labd i p f,
thread_container_get_quota_spec i habd = Some p
→ relate_AbData s f habd labd
→ thread_container_get_quota_spec i labd = Some p.
Proof.
unfold thread_container_get_quota_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
intros.
revert H; subrewrite.
Qed.
Lemma thread_container_get_quota_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_container_get_quota_spec)
(id ↦ gensem thread_container_get_quota_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_container_get_quota_exist; eauto 1.
reflexivity.
Qed.
End THREAD_CONTAINER_GET_QUOTA_SIM_PROOF.
Section THREAD_CONTAINER_GET_USAGE_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_AC}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_big_log}.
Lemma thread_container_get_usage_exist:
∀ s habd labd i p f,
thread_container_get_usage_spec i habd = Some p
→ relate_AbData s f habd labd
→ thread_container_get_usage_spec i labd = Some p.
Proof.
unfold thread_container_get_usage_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
intros.
revert H; subrewrite.
Qed.
Lemma thread_container_get_usage_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_container_get_usage_spec)
(id ↦ gensem thread_container_get_usage_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_container_get_usage_exist; eauto 1.
reflexivity.
Qed.
End THREAD_CONTAINER_GET_USAGE_SIM_PROOF.
Section THREAD_CONTAINER_CAN_CONSUME_SIM_PROOF.
Context {re1: relate_impl_iflags}.
Context {re2: relate_impl_AC}.
Context {re3: relate_impl_CPU_ID}.
Context {re4: relate_impl_cid}.
Context {re5: relate_impl_init}.
Context {re6: relate_impl_big_log}.
Lemma thread_container_can_consume_exist:
∀ s habd labd i n b f,
thread_container_can_consume_spec i n habd = Some b
→ relate_AbData s f habd labd
→ thread_container_can_consume_spec i n labd = Some b.
Proof.
unfold thread_container_can_consume_spec; intros.
exploit relate_impl_init_eq; eauto. intros.
exploit relate_impl_iflags_eq; eauto. inversion 1.
exploit relate_impl_AC_eq; eauto. intros.
exploit relate_impl_CPU_ID_eq; eauto.
exploit relate_impl_cid_eq; eauto.
exploit relate_impl_big_log_eq; eauto.
intros.
revert H; subrewrite.
Qed.
Lemma thread_container_can_consume_sim:
∀ id,
sim (crel RData RData) (id ↦ gensem thread_container_can_consume_spec)
(id ↦ gensem thread_container_can_consume_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
match_external_states_simpl.
erewrite thread_container_can_consume_exist; eauto 1.
reflexivity.
Qed.
End THREAD_CONTAINER_CAN_CONSUME_SIM_PROOF.
End OBJ_SIM.