Library mcertikos.multithread.phbthread.ObjPHBThreadSCHED
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 CalTicketLock.
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 PHBSPECSSched.
Context `{real_param_ops : RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
Context `{threads_conf_ops: ThreadsConfigurationOps}.
Section SINGLE_SCHED_SPECS.
thread sched related functions
Function single_big_sched_init_spec_share (mbi_adr : Z) (adt: sharedData) :=
if zeq (ZMap.get (CPU_ID adt) (cid adt)) main_thread then
if zle_lt 0 (CPU_ID adt) TOTAL_CPU then
match (init adt, pg adt) with
| (false, false) ⇒
Some (adt {sh_vmxinfo: real_vmxinfo} {sh_pg: true} {sh_nps: real_nps}
{sh_init: true} {sh_big_log: BigDef nil} {sh_lock: real_lock (lock adt)}
{sh_idpde: real_idpde (idpde adt)}
{sh_cid: ZMap.set (CPU_ID adt) main_thread (cid adt)})
| _ ⇒ None
end
else None
else None.
Function single_big_sched_init_spec (mbi_adr: Z) (adt: PData) : option PData :=
if zeq (ZMap.get (CPU_ID (fst adt)) (cid (fst adt))) main_thread then
match (ikern (snd adt), ihost (snd adt), ipt (snd adt), intr_flag (snd adt), in_intr (snd adt)) with
| (true, true, true, true, false) ⇒
match single_big_sched_init_spec_share mbi_adr (fst adt) with
| Some adt´ ⇒
let pv_adt := (snd adt) in
let n := pv_adt.(ioapic).(s).(IoApicMaxIntr) + 1 in
if zeq n (Zlength (pv_adt.(ioapic).(s).(IoApicIrqs))) then
if zeq n (Zlength (pv_adt.(ioapic).(s).(IoApicEnables))) then
Some (adt´, pv_adt {pv_ioapic/s: ioapic_init_aux pv_adt.(ioapic).(s) (Z.to_nat (n - 1))}
{pv_lapic: (mkLApicData
(mkLApicState 0 NoIntr (LapicMaxLvt (s (lapic pv_adt))) true
(32 + 7) true true true 0 50 false 0))
{l1: l1 (lapic pv_adt)}
{l2: l2 (lapic pv_adt)}
{l3: l3 (lapic pv_adt)}
} {pv_ioapic / s / CurrentIrq: None}
{pv_AC: (mkContainer (root_quota/TOTAL_CPU) 0 0 nil true)} {pv_PT: 0}
{pv_ptpool: real_pt (ptpool (snd adt))}
{pv_syncchpool: real_syncchpool (syncchpool (snd adt))})
else None
else None
| _ ⇒ None
end
| _ ⇒ None
end
else None.
Function single_big_proc_create_spec_share (adt : sharedData) (buc: block) (ofs_uc: int) q
(child_id : Z) : option (sharedData × Z) :=
let curid := ZMap.get (CPU_ID adt) (cid adt) in
let cpu := CPU_ID adt in
let ofs := Int.repr ((child_id + 1) × PgSize -4) in
match (init adt, pg adt) with
| (true, true) ⇒ match big_log adt with
| BigDef l ⇒
match B_GetContainerUsed child_id cpu l, (In_dec zeq) child_id full_thread_list with
| false, left _ ⇒
let to := big_oracle adt in
let l1 := (to cpu l) ++ l in
let e := TBSHARED (BTDSPAWN curid child_id q ofs buc ofs_uc) in
let l´ := (TBEVENT cpu e) :: l1 in
match B_CalTCB_log_real l´ with
| Some _ ⇒ Some (adt {sh_big_log: BigDef l´}, child_id)
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_big_proc_create_spec (d: PData) (b b´ buc: block) (ofs_uc: int) (q : Z) : option (PData × Z) :=
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
let cpu := CPU_ID (fst d) in
let c := (AC (snd d)) in
let i := curid × max_children + 1 + Z_of_nat (length (cchildren c)) in
match (ikern (snd d), ihost (snd d), ipt (snd d),
zlt_lt 0 i num_proc, zlt (Z_of_nat (length (cchildren c))) max_children,
zle_le 0 q (cquota c - cusage c),
B_inLock cpu (big_log (fst d))) with
| (true, true, true, left _, left _, left _, false) ⇒
match big_log (fst d) with
| BigDef l ⇒
if B_GetContainerUsed curid cpu l then
let parent := (mkContainer (cquota c) (cusage c + q)
(cparent c) (i :: cchildren c) (cused c)) in
match single_big_proc_create_spec_share (fst d) buc ofs_uc q i with
| Some (adt´, i´) ⇒ Some (adt´, (snd d) {pv_AC: parent}, i)
| _ ⇒ None
end
else None
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_big_proc_create_spec_test (d: PData) (buc: block) (ofs_uc: int) (q : Z) : Z :=
let curid := ZMap.get (CPU_ID (fst d)) (cid (fst d)) in
let c := (AC (snd d)) in
let i := curid × max_children + 1 + Z_of_nat (length (cchildren c)) in
i.
Function single_big_thread_wakeup_spec_share (cv: Z) (adt: sharedData) : option (sharedData × Z) :=
let me := CPU_ID adt in
match (init adt, pg adt) with
| (true, true) ⇒
let n := slp_q_id cv 0 in
let sc_id := n + lock_TCB_range in
if zle_lt 0 cv num_cv then
match big_log adt, ZMap.get (n + ID_AT_range) (lock adt),
B_inLock me (big_log adt) with
| BigDef l, LockFalse, true ⇒
let to := big_oracle adt in
let l1 := (to me l) ++ l in
let e := TBSHARED (BTDWAKE (ZMap.get (CPU_ID adt) (cid adt)) cv) in
let l´ := (TBEVENT me e) :: l1 in
match B_CalTCB_log_real l´ with
| Some (TCBWAKE_F) ⇒
Some (adt {sh_big_log: BigDef l´}, 0)
| Some (TCBWAKE_T tid) ⇒
match B_GetContainerUsed tid me l, (In_dec zeq) tid full_thread_list with
| true, left _ ⇒
Some (adt {sh_big_log: BigDef l´}, 1)
| _, _ ⇒ None
end
| Some (TCBWAKE tid cpu´) ⇒
let e´ := TBSHARED (BTDWAKE_DIFF (ZMap.get (CPU_ID adt) (cid adt)) cv tid cpu´) in
let l´´ := (TBEVENT me e´) :: l´ in
match B_CalTCB_log_real l´´,
ZMap.get (msg_q_id cpu´ + ID_AT_range) (lock adt),
B_GetContainerUsed tid me l, (In_dec zeq) tid full_thread_list with
| Some _, LockFalse, true, left _ ⇒
Some (adt {sh_big_log: BigDef l´´}, 1)
| _,_,_,_ ⇒ None
end
| _ ⇒ None
end
| _, _, _ ⇒ None
end
else None
| _ ⇒ None
end.
Function single_big_thread_wakeup_spec (cv: Z) (d: PData) : option (PData × Z) :=
match (ikern (snd d), ihost (snd d), ipt (snd d)) with
| (true, true, true) ⇒
match single_big_thread_wakeup_spec_share cv (fst d) with
| Some (adt´, res) ⇒ Some ((adt´, snd d), res)
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_proc_create_postinit_spec (elf_id: Z) (adt: PData) :=
match (init (fst adt), ikern (snd adt), ihost (snd adt)) with
| (true, true, true) ⇒
Some adt
| _ ⇒ None
end.
Function single_yield_dummy_spec (adt: PData) := Some adt.
Function single_sleep_dummy_spec (i : Z) (adt: PData) := Some adt.
End SINGLE_SCHED_SPECS.
End PHBSPECSSched.