Library mcertikos.multithread.phbthread.ObjPHBThreadVMM
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import FlatMemory.
Require Import Integers.
Require Import Values.
Require Import ASTExtra.
Require Import Constant.
Require Import Constant.
Require Import GlobIdent.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.compat.CompatLayers.
Require Import CommonTactic.
Require Import RefinementTactic.
Require Import RealParams.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import CalRealIDPDE.
Require Import CalRealInitPTE.
Require Import CalRealSMSPool.
Require Import CalRealProcModule.
Require Import ObjInterruptDriver.
Require Import ObjConsole.
Require Import OracleInstances.
Require Import ObjSerialDriver.
Require Import ObjVMMDef.
Require Import DeviceStateDataType.
Require Import AbstractDataType.
Require Import AuxSingleAbstractDataType.
Require Import ObjPHBFlatMem.
Require Import AlgebraicMem.
Require Import GlobalOracleProp.
Require Import SingleConfiguration.
Require Import BigLogThreadConfigFunction.
Section PHBSPECSVmm.
Context `{real_param_ops : RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{threads_conf_ops: ThreadsConfigurationOps}.
Section SINGLE_SPECS_NORMAL.
Function single_vmxinfo_get_spec (i: Z) (d: PData) : option Z :=
match (ikern (snd d), ihost (snd d)) with
| (true, true) ⇒ Some (ZMap.get i (vmxinfo (fst d)))
| _ ⇒ None
end.
Function single_big_palloc_spec_share (n: Z) (choice: Z) (adt: sharedData): option (sharedData × Z) :=
let abid := 0 in
let cpu := CPU_ID adt in
match (init adt, pg adt) with
| (true, true) ⇒
match big_log adt, ZMap.get abid (lock adt) with
| BigDef l, LockFalse ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
if zeq choice 1 then
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 (ZMap.get (CPU_ID adt) (cid adt)) i))) :: l1 in
Some (adt {sh_big_log: BigDef l´}, i)
| _ ⇒
let l´ := (TBEVENT cpu (TBSHARED (BPALLOCE (ZMap.get (CPU_ID adt) (cid adt)) 0))) :: l1 in
Some (adt{sh_big_log: BigDef l´}, 0)
end
| _ ⇒ None
end
else
let l´ := (TBEVENT cpu (TBSHARED (BPALLOCE (ZMap.get (CPU_ID adt) (cid adt)) 0))) :: l1 in
Some (adt{sh_big_log: BigDef l´}, 0)
| _,_ ⇒ None
end
| _ ⇒ None
end.
Function single_big_palloc_spec (n: Z) (d: PData) : option (PData × Z) :=
let pd := snd d in
let c := (AC pd) in
let cpu := CPU_ID (fst d) in
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
if zeq n curid then
match (ikern pd, ihost pd, ipt pd , B_inLock cpu (big_log (fst d))) with
| (true, true, true , false) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
if (cusage c) <? (cquota c) then
let cur := mkContainer (cquota c) (cusage c + 1) (cparent c)
(cchildren c) (cused c) in
match single_big_palloc_spec_share n 1 (fst d) with
| Some (adt´, i) ⇒ if zeq i 0 then Some ((adt´, pd), i)
else let new_pd := pd {pv_pperm : ZMap.set i PGAlloc (pperm pd)}
{pv_AC : cur} in
Some ((adt´, new_pd), i)
| _ ⇒ None
end
else match single_big_palloc_spec_share n 0 (fst d) with
| Some (adt´, i) ⇒ Some ((adt´, pd), i)
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Section SINGLE_PALLOC_DISJOINT.
Lemma single_big_palloc_inv_disjoint_prop:
∀ n d d´ d´´ v v´,
single_big_palloc_spec n d = Some (d´, v) →
single_big_palloc_spec n d´ = Some (d´´, v´) →
v ≠ 0 → v´ ≠ 0 → v´ ≠ v.
Proof.
intros.
unfold single_big_palloc_spec in H.
unfold single_big_palloc_spec_share in H.
subdestruct; inv H; try (elim H1; auto; fail).
unfold single_big_palloc_spec in H0.
unfold single_big_palloc_spec_share in H0.
subdestruct; inv H0; try (elim H2; auto; fail).
simpl in ×.
assert (ZMap.get v a1 = ATValid true ATNorm).
{ assert (first_alloc: ∃ atable, B_CalAT_log_real
(TBEVENT (CPU_ID (fst d)) (TBSHARED (BPALLOCE (ZMap.get (CPU_ID (fst d)) (cid (fst d))) v))
:: big_oracle (fst d) (CPU_ID (fst d)) l ++ l) = Some atable).
{ unfold B_CalAT_log_real in Hdestruct16; unfold B_CalAT_log_real.
eauto using B_CalAT_log_sub_log_exist. }
destruct first_alloc.
assert (∀ i, ZMap.get i x = (ATValid true ATNorm) →
ZMap.get i a1 = (ATValid true ATNorm)).
{ unfold B_CalAT_log_real in Hdestruct16, H.
eapply B_CalAT_log_keeps_allocated_pages; eauto. }
unfold B_CalAT_log_real in H.
simpl in H.
subdestruct; inv H.
eapply H0.
rewrite ZMap.gss; auto. }
case_eq (zeq v v´); intros; subst; auto.
destruct a2.
destruct a3.
rewrite e1 in H.
inv H.
assert (ZMap.get v a1 = ATValid true ATNorm).
{ assert (first_alloc: ∃ atable, B_CalAT_log_real
(TBEVENT (CPU_ID (fst d)) (TBSHARED (BPALLOCE (ZMap.get (CPU_ID (fst d)) (cid (fst d))) v))
:: big_oracle (fst d) (CPU_ID (fst d)) l ++ l) = Some atable).
{ unfold B_CalAT_log_real in Hdestruct16; unfold B_CalAT_log_real.
eauto using B_CalAT_log_sub_log_exist. }
destruct first_alloc.
assert (∀ i, ZMap.get i x = (ATValid true ATNorm) →
ZMap.get i a1 = (ATValid true ATNorm)).
{ unfold B_CalAT_log_real in Hdestruct16, H.
eapply B_CalAT_log_keeps_allocated_pages; eauto. }
unfold B_CalAT_log_real in H.
simpl in H.
subdestruct; inv H.
eapply H0.
rewrite ZMap.gss; auto. }
case_eq (zeq v v´); intros; subst; auto.
Qed.
End SINGLE_PALLOC_DISJOINT.
Function single_big_palloc_spec_test (n: Z) (d: PData) : Z :=
let pd := snd d in
let c := (AC pd) in
let cpu := CPU_ID (fst d) in
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
match (ikern pd, ihost pd, ipt pd ) with
| (true, true, true ) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
if (cusage c) <? (cquota c) then 1 else 0
else 42
| _ ⇒ 42
end
| _ ⇒ 42
end.
Function single_setPT_spec (n: Z) (d: PData) : option PData :=
match (init (fst d), ikern (snd d), ihost (snd d), ipt (snd d)) with
| (true, true, true, false) ⇒
if zle_lt 0 n num_proc then Some (fst d, (snd d) {pv_PT: n}) else None
| _ ⇒ None
end.
Function single_getPDE_spec (n i: Z) (d: PData) : option Z :=
match (init (fst d), ikern (snd d), ihost (snd d), init (fst d), ipt (snd d), PDE_Arg n i) with
| (true, true, true, true, true, true) ⇒
let pt:= ZMap.get n (ptpool (snd d)) in
match ZMap.get i pt with
| PDEValid pi pdt ⇒ Some pi
| PDEUnPresent ⇒ Some 0
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_getPTE_spec (n i vadr: Z) (d: PData) : option Z :=
match (init (fst d), ikern (snd d), ihost (snd d), init (fst d), ipt (snd d), PTE_Arg n i vadr) with
| (true, true, true, true, true, true) ⇒
let pt:= ZMap.get n (ptpool (snd d)) in
match ZMap.get i pt with
| PDEValid _ pdt ⇒
match ZMap.get vadr pdt with
| PTEValid padr p ⇒
Some (padr × PgSize + PermtoZ p)
| PTEUnPresent ⇒ Some 0
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_ptRead_spec (n vadr :Z) (d: PData) : option Z :=
let pdi := PDX vadr in
let pti := PTX vadr in
let curid := (ZMap.get (CPU_ID (fst d)) (cid (fst d))) in
if zeq curid n then
match single_getPDE_spec n pdi d with
| Some pde ⇒
if zeq pde 0 then Some 0
else if zlt_lt 0 pde maxpage then
single_getPTE_spec n pdi pti d
else None
| _ ⇒ None
end
else None.
Function single_ptInsertPTE0_spec (nn vadr padr: Z) (p: PTPerm) (d: PData) : option PData :=
match (init (fst d), ikern (snd d), ihost (snd d), pg (fst d), ipt (snd d), pt_Arg nn vadr padr (nps (fst d))) with
| (true, true, true, true, true, true) ⇒
let pt := ZMap.get nn (ptpool (snd d)) in
let pdi := PDX vadr in
let pti := PTX vadr in
match (ZMap.get pdi pt, ZMap.get padr (pperm (snd d))) 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 (fst d, (snd d)
{pv_ptpool: ZMap.set nn pt´ (ptpool (snd d))})
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_big_ptAllocPDE_spec (nn vadr: Z) (d: PData) : option (PData × Z) :=
let adt := fst d in
let pd := snd d in
let pdi := PDX vadr in
let c := (AC pd) in
match (init adt, ikern pd, ihost pd, pg adt, ipt pd, pt_Arg´ nn vadr) with
| (true, true, true, true, true, true) ⇒
match ZMap.get pdi (ZMap.get nn (ptpool pd)) with
| PDEUnPresent ⇒
match single_big_palloc_spec nn d with
| Some (d´, pi) ⇒
if zeq pi 0 then
Some (d´, pi)
else
Some (fst d´, (snd d´)
{pv_HP: FlatMem.free_page pi (HP (snd d´))}
{pv_pperm: ZMap.set pi (PGHide (PGPMap nn pdi)) (pperm (snd d´))}
{pv_ptpool: (ZMap.set nn (ZMap.set pdi (PDEValid pi real_init_PTE)
(ZMap.get nn (ptpool (snd d´)))) (ptpool (snd d´)))}
, pi)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_big_ptInsert_spec (nn vadr padr perm: Z) (d: PData) : option (PData × Z) :=
let adt := fst d in
let pd := snd d in
match (init adt, ikern pd, ihost pd, ipt pd, 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 pd) in
let pdi := PDX vadr in
let pti := PTX vadr in
match ZMap.get pdi pt with
| PDEValid pi pdt ⇒
match single_ptInsertPTE0_spec nn vadr padr p d with
| Some d´ ⇒ Some (d´, 0)
| _ ⇒ None
end
| PDEUnPresent ⇒
match single_big_ptAllocPDE_spec nn vadr d with
| Some (d´, v) ⇒
if zeq v 0 then Some (d´, MagicNumber)
else
match single_ptInsertPTE0_spec nn vadr padr p d´ with
| Some d´´ ⇒ Some (d´´, v)
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_big_ptResv_spec (n vadr perm: Z) (d: PData) : option (PData × Z) :=
if zeq n (ZMap.get (CPU_ID (fst d)) (cid (fst d))) then
match single_big_palloc_spec n d with
| Some (d´, b) ⇒
if zeq b 0 then Some (d´, MagicNumber)
else single_big_ptInsert_spec n vadr b perm d´
| _ ⇒ None
end
else None.
Function single_big_ptInsert_spec_test (nn vadr padr perm: Z) (d: PData) : Z :=
let adt := fst d in
let pd := snd d in
match (init adt, ikern pd, ihost pd, ipt pd, 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 pd) in
let pdi := PDX vadr in
let pti := PTX vadr in
match ZMap.get pdi pt with
| PDEValid pi pdt ⇒ 2
| PDEUnPresent ⇒ single_big_palloc_spec_test nn d
| _ ⇒ 42
end
| _ ⇒ 42
end
| _ ⇒ 42
end.
Function single_big_ptResv_spec_test (n vadr perm: Z) (d: PData) : Z :=
match single_big_palloc_spec_test n d with
| 0 ⇒ 0
| 1 ⇒ match single_big_palloc_spec n d with
| Some (d´, b) ⇒
if zeq b 0 then 1
else match single_big_ptInsert_spec_test n vadr b perm d´ with
| 0 ⇒ 3
| 1 ⇒ 4
| 2 ⇒ 2
| _ ⇒ 42
end
| _ ⇒ 42
end
| _ ⇒ 42
end.
Function single_ptin_spec (d: PData): option PData :=
match (init (fst d), ipt (snd d), ikern (snd d), ihost (snd d)) with
| (true, false, true, true) ⇒
if zeq (PT (snd d)) 0 then
Some (fst d, (snd d) {pv_ipt: true})
else None
| _ ⇒ None
end.
Function single_ptout_spec (d: PData): option PData :=
match (init (fst d), pg (fst d), ikern (snd d), ihost (snd d), ipt (snd d)) with
| (true, true, true, true, true) ⇒ Some (fst d, (snd d) {pv_ipt: false})
| _ ⇒ None
end.
Function single_container_get_nchildren_spec (i: Z) (d: PData) : option Z :=
let c := (AC (snd d)) in
let cpu := CPU_ID (fst d) in
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
if zeq i (proc_id (fst d)) then
match (init (fst d), ikern (snd d), ihost (snd d) ) with
| (true, true, true ) ⇒
match big_log (fst d) 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 single_container_get_quota_spec (i: Z) (d: PData) : option Z :=
let c := (AC (snd d)) in
let cpu := CPU_ID (fst d) in
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
if zeq i (proc_id (fst d)) then
match (init (fst d), ikern (snd d), ihost (snd d) ) with
| (true, true, true) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then Some (cquota c)
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function single_container_get_usage_spec (i: Z) (d: PData): option Z :=
let c := (AC (snd d)) in
let cpu := CPU_ID (fst d) in
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
if zeq i (proc_id (fst d)) then
match (init (fst d), ikern (snd d), ihost (snd d) ) with
| (true, true, true ) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then Some (cusage c)
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function single_container_can_consume_spec (i: Z) (n: Z) (d: PData) : option Z :=
let c := (AC (snd d)) in
let cpu := CPU_ID (fst d) in
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
if zeq i (proc_id (fst d)) then
match (init (fst d), ikern (snd d), ihost (snd d) ) with
| (true, true, true ) ⇒
match big_log (fst d) 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.
Function single_get_CPU_ID_spec (d : PData) : option Z :=
match (init (fst d), ikern (snd d), ihost (snd d)) with
| (true, true, true) ⇒ Some (CPU_ID (fst d))
| _ ⇒ None
end.
Function single_get_curid_spec (d : PData) : option Z :=
match (init (fst d), ikern (snd d), ihost (snd d)) with
| (true, true, true) ⇒ Some (ZMap.get (CPU_ID (fst d)) (cid (fst d)))
| _ ⇒ None
end.
End SINGLE_SPECS_NORMAL.
End PHBSPECSVmm.