Library mcertikos.multithread.phbthread.ObjPHBThreadIPC
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 ObjPHBThreadVMM.
Require Import AlgebraicMem.
Require Import GlobalOracleProp.
Require Import SingleConfiguration.
Require Import BigLogThreadConfigFunction.
Section PHBSPECSIpc.
Context `{real_param_ops : RealParamsOps}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section SINGLE_SPECS_IPC_NORMAL.
Definition single_big_acquire_lock_SC_spec_share (index: Z) (adt: sharedData) : option (sharedData × (option SyncChanPool)) :=
let abid := (index + lock_TCB_range) in
let cpu := CPU_ID adt in
if zle_lt 0 index num_chan then
match (init adt, B_inLock cpu (big_log adt)) with
| (true, false) ⇒
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
let l´ := (TBEVENT cpu (TBLOCK abid (BWAIT_LOCK (ZMap.get (CPU_ID adt) (cid adt)) local_lock_bound))) :: l1 in
match B_CalLock abid l´ with
| Some _ ⇒
match B_GetSharedSC abid l´ with
| Some e ⇒
Some (adt {sh_big_log: BigDef l´}
{sh_lock: ZMap.set abid (LockOwn true) (lock adt)},
Some e)
| _ ⇒
Some (adt {sh_big_log: BigDef l´}
{sh_lock: ZMap.set abid (LockOwn true) (lock adt)},
Some (B_GetlastPush cpu (big_log adt)))
end
| _ ⇒ None
end
| _,_ ⇒ None
end
| _ ⇒ None
end
else None.
Definition single_big_acquire_lock_SC_spec (index: Z) (d: PData) : option PData :=
match (ikern (snd d), ihost (snd d)) with
| (true, true) ⇒ match single_big_acquire_lock_SC_spec_share index (fst d) with
| Some (adt´, Some e) ⇒
Some (adt´, (snd d) {pv_syncchpool : e})
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_big_release_lock_SC_spec_share (index:Z) (syncch_val : SyncChanPool) (adt: sharedData)
: option sharedData :=
let abid := (index + lock_TCB_range) in
let cpu := CPU_ID adt in
match (init adt, pg adt,
B_inLock cpu (big_log adt)) with
| (true, true, true) ⇒
if zle_lt 0 index num_chan then
match big_log adt, ZMap.get abid (lock adt) with
| BigDef l, LockOwn true ⇒
let e := TBLOCK abid (BREL_LOCK (ZMap.get (CPU_ID adt) (cid adt)) syncch_val) in
let l´ := (TBEVENT cpu e) :: l in
match B_CalLock abid l´ with
| Some _ ⇒
Some (adt {sh_big_log: BigDef l´}
{sh_lock: ZMap.set abid LockFalse (lock adt)})
| _ ⇒ None
end
| _,_ ⇒ None
end
else None
| _ ⇒ None
end.
Function single_big_release_lock_SC_spec (index:Z) (d: PData) : option PData :=
match (ikern (snd d), ihost (snd d)) with
| (true, true) ⇒ match single_big_release_lock_SC_spec_share index (syncchpool (snd d)) (fst d) with
| Some adt´ ⇒ Some (adt´, snd d)
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_big_release_lock_SC_chan_pool (index:Z) (d: PData) : option SyncChanPool :=
match (ikern (snd d), ihost (snd d)) with
| (true, true) ⇒ Some (syncchpool (snd d))
| _ ⇒ None
end.
Function single_get_sync_chan_busy_spec (i: Z) (d : PData) : option Z :=
match (init (fst d ), ikern (snd d), pg (fst d), ihost (snd d), ipt (snd d),
B_inLock (CPU_ID (fst d)) (big_log (fst d))) with
| (true, true, true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool (snd d)) with
| SyncChanValid _ _ _ busy ⇒ Some (Int.unsigned busy)
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function single_set_sync_chan_busy_spec (i busy: Z) (d: PData) : option PData :=
match (init (fst d), ikern (snd d), pg (fst d), ihost (snd d), ipt (snd d),
B_inLock (CPU_ID (fst d)) (big_log (fst d))) with
| (true, true, true, true, true, true) ⇒
if zle_lt 0 i num_chan then
match ZMap.get i (syncchpool (snd d)) with
| SyncChanValid t v c _
⇒ Some (fst d, (snd d) {pv_syncchpool: ZMap.set i (SyncChanValid t v c (Int.repr busy))
(syncchpool (snd d))})
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function single_get_kernel_pa_spec (pid vaddr : Z) (d : PData) : option Z :=
match pg (fst d) with
| true ⇒
match single_ptRead_spec pid vaddr d with
| Some paddr ⇒
if zeq paddr 0 then None else Some (paddr / PgSize × PgSize + (vaddr mod PgSize))
| _ ⇒ None
end
| _ ⇒ None
end.
Function single_big_page_copy_back_spec (cv: Z) (count: Z) (to: Z) (adt: PData) :=
let sh_adt := fst adt in
let pv_adt := snd adt in
let index := slp_q_id cv 0 in
match (ikern pv_adt, ihost pv_adt, ipt pv_adt, index2Z ID_SC index) with
| (true, true, true, Some abid) ⇒
if zle_lt 0 to adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize to HPS then
match ZMap.get (PageI to) (pperm pv_adt) with
| PGAlloc ⇒
match big_log sh_adt, ZMap.get abid (lock sh_adt) with
| BigDef l, LockOwn true ⇒
match B_GetSharedBuffer abid l, B_CalLock abid l with
| Some b, Some (_, LHOLD, Some cpu_id) ⇒
if zeq cpu_id (CPU_ID sh_adt) then
match ObjFlatMem.page_copy_back_aux (Z.to_nat count) to b (HP pv_adt) with
| Some h ⇒ Some (sh_adt, pv_adt {pv_HP: h})
| _ ⇒ None
end
else None
| _, _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function single_big_ipc_receive_body_spec (chid vaddr rcount : Z) (adt : PData) : option (PData × Z) :=
let sh_adt := fst adt in
let pv_adt := snd adt in
let curid := ZMap.get (CPU_ID sh_adt) (cid sh_adt) in
match (init sh_adt, pg sh_adt, ikern pv_adt, ihost pv_adt, ipt pv_adt,
B_inLock (CPU_ID sh_adt) (big_log sh_adt)) with
| (true, true, true, true, true, true) ⇒
if zle_lt 0 chid num_chan then
match ZMap.get chid (syncchpool pv_adt) with
| SyncChanValid sender spaddr scount busy ⇒
let arecvcount := Z.min (Int.unsigned scount) rcount in
match single_big_page_copy_back_spec chid arecvcount vaddr adt with
| Some adt1 ⇒
Some ((fst adt1), (snd adt1)
{pv_syncchpool:
ZMap.set chid
(SyncChanValid sender spaddr Int.zero busy)
(syncchpool (snd adt1))}, arecvcount)
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
Function single_big_page_copy_spec (cv: Z) (count: Z) (from: Z) (adt: PData) :=
let sh_adt := fst adt in
let pv_adt := snd adt in
let cpu := CPU_ID sh_adt in
let index := slp_q_id cv 0 in
match (ikern pv_adt, ihost pv_adt, ipt pv_adt, index2Z ID_SC index) with
| (true, true, true, Some abid) ⇒
if zle_lt 0 from adr_low then
if zle_le 0 count one_k then
if Zdivide_dec PgSize from HPS then
match ZMap.get (PageI from) (pperm pv_adt) with
| PGAlloc ⇒
match big_log sh_adt, ZMap.get abid (lock sh_adt) with
| BigDef l, LockOwn true ⇒
match ObjFlatMem.page_copy_aux (Z.to_nat count) from (HP pv_adt) with
| Some b ⇒
let l´ := TBEVENT cpu (TBSHARED (BBUFFERE (ZMap.get cpu (cid sh_adt)) cv b)) :: l in
match B_CalLock abid l´ with
| Some _ ⇒ Some (sh_adt {sh_big_log: BigDef l´}, pv_adt)
| _ ⇒ None
end
| _ ⇒ None
end
| _, _ ⇒ None
end
| _ ⇒ None
end
else None
else None
else None
| _ ⇒ None
end.
Function single_big_ipc_send_body_spec (chid vaddr scount : Z) (adt : PData) : option (PData × Z) :=
let sh_adt := fst adt in
let pv_adt := snd adt in
let curid := ZMap.get (CPU_ID sh_adt) (cid sh_adt) in
match (init sh_adt, pg sh_adt, ikern pv_adt, ihost pv_adt, ipt pv_adt,
B_inLock (CPU_ID sh_adt) (big_log sh_adt)) with
| (true, true, true, true, true, true) ⇒
if zle_lt 0 chid num_chan then
match ZMap.get chid (syncchpool pv_adt) with
| SyncChanValid sender spaddr _ busy ⇒
let asendval := Z.min (scount) (1024) in
match single_big_page_copy_spec chid asendval vaddr adt with
| Some adt´ ⇒
Some (fst adt´, (snd adt´) {pv_syncchpool :
ZMap.set chid
(SyncChanValid sender spaddr (Int.repr asendval) busy)
(syncchpool (snd adt´))}, asendval)
| _ ⇒ None
end
| _ ⇒ None
end
else None
| _ ⇒ None
end.
End SINGLE_SPECS_IPC_NORMAL.
End PHBSPECSIpc.