updated translated haskell spec
This commit is contained in:
Joel Beeren
Gerwin Klein
parent
002cf370bb
commit
7b6ddc5212
|
|
@ -161,7 +161,7 @@ begin
|
|||
|
||||
definition
|
||||
makeObject_asidpool: "(makeObject :: asidpool) \<equiv> ASIDPool $
|
||||
funArray (const Nothing)"
|
||||
funPartialArray (const Nothing) (0,1023)"
|
||||
|
||||
definition
|
||||
loadObject_asidpool[simp]:
|
||||
|
|
|
|||
|
|
@ -27,46 +27,61 @@ consts
|
|||
idleThreadCode :: "machine_word list"
|
||||
|
||||
consts
|
||||
initKernelVM :: "unit kernel"
|
||||
mapKernelWindow :: "unit kernel"
|
||||
|
||||
consts
|
||||
initVSpace :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
createGlobalPD :: "unit kernel"
|
||||
|
||||
consts
|
||||
activateGlobalPD :: "unit kernel"
|
||||
|
||||
consts
|
||||
mapKernelRegion :: "(paddr * paddr) \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
mapKernelFrame :: "paddr \<Rightarrow> vptr \<Rightarrow> vmrights \<Rightarrow> vmattributes \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
allocKernelPT :: "(machine_word) kernel"
|
||||
createSectionPDE :: "vptr \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
mapKernelDevice :: "(paddr * machine_word) \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
createGlobalsFrame :: "unit kernel"
|
||||
activateGlobalPD :: "unit kernel"
|
||||
|
||||
consts
|
||||
createITPDPTs :: "capability \<Rightarrow> vptr \<Rightarrow> vptr \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts
|
||||
writeITPDPTs :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
createITASIDPool :: "capability \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts
|
||||
writeITASIDPool :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
mapITPTCap :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
mapITFrameCap :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
createIPCBufferFrame :: "capability \<Rightarrow> vptr \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts
|
||||
createBIFrame :: "capability \<Rightarrow> vptr \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts
|
||||
createITFrameCap :: "machine_word \<Rightarrow> vptr \<Rightarrow> asid option \<Rightarrow> bool \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts
|
||||
createFramesOfRegion :: "capability \<Rightarrow> region \<Rightarrow> bool \<Rightarrow> vptr \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
mapGlobalsFrame :: "unit kernel"
|
||||
|
||||
consts
|
||||
createInitialRoot :: "machine_word \<Rightarrow> capability kernel_init"
|
||||
writeIdleCode :: "unit kernel"
|
||||
|
||||
consts
|
||||
populateInitialRoot :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel_init"
|
||||
mapKernelFrame :: "paddr \<Rightarrow> vptr \<Rightarrow> vmrights \<Rightarrow> vmattributes \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
allocUserPT :: "asid \<Rightarrow> vptr \<Rightarrow> (machine_word) kernel_init"
|
||||
getARMGlobalPT :: "(machine_word) kernel"
|
||||
|
||||
consts
|
||||
mapUserFrame :: "machine_word \<Rightarrow> asid \<Rightarrow> paddr \<Rightarrow> vptr \<Rightarrow> unit kernel_init"
|
||||
createDeviceFrames :: "capability \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
copyGlobalMappings :: "machine_word \<Rightarrow> unit kernel"
|
||||
|
|
@ -146,12 +161,6 @@ isValidVTableRoot :: "capability \<Rightarrow> bool"
|
|||
consts
|
||||
checkValidIPCBuffer :: "vptr \<Rightarrow> capability \<Rightarrow> ( syscall_error , unit ) kernel_f"
|
||||
|
||||
consts
|
||||
createInitPage :: "paddr \<Rightarrow> capability kernel"
|
||||
|
||||
consts
|
||||
createDeviceCap :: "(paddr * paddr) \<Rightarrow> capability kernel"
|
||||
|
||||
consts
|
||||
maskVMRights :: "vmrights \<Rightarrow> cap_rights \<Rightarrow> vmrights"
|
||||
|
||||
|
|
|
|||
|
|
@ -23,7 +23,7 @@ defs kernelBase_def:
|
|||
"kernelBase \<equiv> VPtr 0xf0000000"
|
||||
|
||||
defs globalsBase_def:
|
||||
"globalsBase \<equiv> VPtr 0xff000000"
|
||||
"globalsBase \<equiv> VPtr 0xffffc000"
|
||||
|
||||
defs idleThreadStart_def:
|
||||
"idleThreadStart \<equiv> globalsBase + VPtr 0x100"
|
||||
|
|
@ -36,62 +36,22 @@ defs idleThreadCode_def:
|
|||
, 0xeafffffc
|
||||
]"
|
||||
|
||||
defs initKernelVM_def:
|
||||
"initKernelVM\<equiv> (do
|
||||
createGlobalPD;
|
||||
allMemory \<leftarrow> doMachineOp getMemoryRegions;
|
||||
mapM_x mapKernelRegion allMemory;
|
||||
kernelDevices \<leftarrow> doMachineOp getKernelDevices;
|
||||
mapM_x mapKernelDevice kernelDevices;
|
||||
createGlobalsFrame;
|
||||
mapGlobalsFrame;
|
||||
activateGlobalPD
|
||||
od)"
|
||||
|
||||
defs initVSpace_def:
|
||||
"initVSpace cRootSlot vRootSlot\<equiv> (do
|
||||
provideRegion $ BootRegion
|
||||
(CPtr $ fromVPtr kernelBase) maxBound BRCapsOnly 0;
|
||||
vRoot \<leftarrow> createInitialRoot vRootSlot;
|
||||
cRoot \<leftarrow> doKernelOp $ getSlotCap cRootSlot;
|
||||
populateInitialRoot vRoot cRoot;
|
||||
doKernelOp $ doMachineOp cleanCaches_PoU
|
||||
od)"
|
||||
|
||||
defs createGlobalPD_def:
|
||||
"createGlobalPD\<equiv> (do
|
||||
globalPD \<leftarrow> gets $ armKSGlobalPD \<circ> ksArchState;
|
||||
deleteObjects (PPtr $ fromPPtr globalPD) pdBits;
|
||||
placeNewObject (PPtr $ fromPPtr globalPD) (makeObject ::pde)
|
||||
(pdBits `~shiftR~` (objBits (makeObject ::pde)));
|
||||
globalPTs \<leftarrow> gets $ armKSGlobalPTs \<circ> ksArchState;
|
||||
deleteObjects (PPtr $ fromPPtr $ head globalPTs) pageBits;
|
||||
placeNewObject (PPtr $ fromPPtr $ head globalPTs) (makeObject ::pte)
|
||||
(pageBits `~shiftR~` (objBits (makeObject ::pte)));
|
||||
return ()
|
||||
od)"
|
||||
|
||||
defs activateGlobalPD_def:
|
||||
"activateGlobalPD\<equiv> (do
|
||||
doMachineOp cleanCaches_PoU;
|
||||
globalPD \<leftarrow> gets $ armKSGlobalPD \<circ> ksArchState;
|
||||
doMachineOp $ (do
|
||||
setCurrentPD $ addrFromPPtr globalPD;
|
||||
invalidateTLB
|
||||
od)
|
||||
od)"
|
||||
|
||||
defs mapKernelRegion_def:
|
||||
"mapKernelRegion x0\<equiv> (case x0 of
|
||||
(phys, physEnd) \<Rightarrow> (do
|
||||
magnitude \<leftarrow> return ( physEnd - phys);
|
||||
defs mapKernelWindow_def:
|
||||
"mapKernelWindow\<equiv> (do
|
||||
vbase \<leftarrow> return ( kernelBase `~shiftR~` pageBitsForSize (ARMSection));
|
||||
pdeBits \<leftarrow> return ( objBits (undefined ::pde));
|
||||
haskell_assert (magnitude \<ge> bit (pageBitsForSize ARMSection))
|
||||
[];
|
||||
pteBits \<leftarrow> return ( objBits (undefined ::pte));
|
||||
ptSize \<leftarrow> return ( ptBits - pteBits);
|
||||
pdSize \<leftarrow> return ( pdBits - pdeBits);
|
||||
globalPD \<leftarrow> gets $ armKSGlobalPD \<circ> ksArchState;
|
||||
if (magnitude < bit (pageBitsForSize ARMSuperSection))
|
||||
then forM_x [phys, phys + bit (pageBitsForSize ARMSection) .e. phys + magnitude - 1] (\<lambda> phys. (do
|
||||
virt \<leftarrow> return ( VPtr $ fromPPtr $ ptrFromPAddr phys);
|
||||
globalPTs \<leftarrow> gets $ armKSGlobalPTs \<circ> ksArchState;
|
||||
deleteObjects (PPtr $ fromPPtr globalPD) pdBits;
|
||||
placeNewObject (PPtr $ fromPPtr globalPD) (makeObject ::pde) pdSize;
|
||||
forM_x [vbase, vbase+16 .e. (bit pdSize) - 16 - 1] $ createSectionPDE;
|
||||
forM_x [(bit pdSize) - 16, (bit pdSize) - 2] (\<lambda> v. (do
|
||||
offset \<leftarrow> return ( fromVPtr v);
|
||||
virt \<leftarrow> return ( v `~shiftL~` pageBitsForSize (ARMSection));
|
||||
phys \<leftarrow> return ( addrFromPPtr $ PPtr $ fromVPtr virt);
|
||||
pde \<leftarrow> return ( SectionPDE_ \<lparr>
|
||||
pdeFrame= phys,
|
||||
pdeParity= True,
|
||||
|
|
@ -100,226 +60,334 @@ defs mapKernelRegion_def:
|
|||
pdeGlobal= True,
|
||||
pdeExecuteNever= False,
|
||||
pdeRights= VMKernelOnly \<rparr>);
|
||||
offset \<leftarrow> return ( fromVPtr virt `~shiftR~` pageBitsForSize ARMSection);
|
||||
slot \<leftarrow> return ( globalPD + PPtr (offset `~shiftL~` pdeBits));
|
||||
storePDE slot pde
|
||||
od))
|
||||
else forM_x [phys, phys + bit (pageBitsForSize ARMSuperSection) .e. phys + magnitude - 1] (\<lambda> phys. (do
|
||||
virt \<leftarrow> return ( VPtr $ fromPPtr $ ptrFromPAddr phys);
|
||||
pde \<leftarrow> return ( SuperSectionPDE_ \<lparr>
|
||||
pdeFrame= phys,
|
||||
pdeParity= True,
|
||||
pdeCacheable= True,
|
||||
pdeGlobal= True,
|
||||
pdeExecuteNever= False,
|
||||
pdeRights= VMKernelOnly \<rparr>);
|
||||
offset \<leftarrow> return ( fromVPtr virt `~shiftR~` pageBitsForSize ARMSection);
|
||||
slots \<leftarrow> return ( map (\<lambda> n. globalPD + PPtr (n `~shiftL~` pdeBits))
|
||||
[offset .e. offset + 15]);
|
||||
mapM_x (flip storePDE pde) slots
|
||||
od))
|
||||
od)
|
||||
)"
|
||||
|
||||
defs mapKernelFrame_def:
|
||||
"mapKernelFrame paddr vptr rights attributes\<equiv> (do
|
||||
haskell_assert (vptr \<ge> kernelBase) [];
|
||||
pd \<leftarrow> gets $ armKSGlobalPD \<circ> ksArchState;
|
||||
pdSlot \<leftarrow> return ( lookupPDSlot pd vptr);
|
||||
pde \<leftarrow> getObject pdSlot;
|
||||
pteBits \<leftarrow> return ( objBits (undefined ::pte));
|
||||
ptIndex \<leftarrow> return ( fromVPtr $ vptr `~shiftR~` 12 && 0xff);
|
||||
ptSlot \<leftarrow> (case pde of
|
||||
PageTablePDE _ _ _ \<Rightarrow> (do
|
||||
pt \<leftarrow> return ( ptrFromPAddr $ pdeTable pde);
|
||||
return $ pt + (PPtr $ ptIndex `~shiftL~` pteBits)
|
||||
od)
|
||||
| InvalidPDE \<Rightarrow> (do
|
||||
ptFrame \<leftarrow> allocKernelPT;
|
||||
pde \<leftarrow> return ( PageTablePDE_ \<lparr>
|
||||
pdeTable= addrFromPPtr ptFrame,
|
||||
pdeParity= True,
|
||||
pdeDomain= 0 \<rparr>);
|
||||
storePDE pdSlot pde;
|
||||
return $ PPtr $ fromPPtr ptFrame + (ptIndex `~shiftL~` pteBits)
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
);
|
||||
pte \<leftarrow> getObject ptSlot;
|
||||
(case pte of
|
||||
InvalidPTE \<Rightarrow> (do
|
||||
pte' \<leftarrow> return ( SmallPagePTE_ \<lparr>
|
||||
pteFrame= paddr,
|
||||
pteCacheable= armPageCacheable attributes,
|
||||
pteGlobal= True,
|
||||
pteExecuteNever= False,
|
||||
pteRights= rights \<rparr>);
|
||||
storePTE ptSlot pte'
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
)
|
||||
od));
|
||||
paddr \<leftarrow> return ( addrFromPPtr $ PPtr $ fromPPtr $ head globalPTs);
|
||||
pde \<leftarrow> return ( PageTablePDE_ \<lparr>pdeTable= paddr ,pdeParity= True, pdeDomain= 0\<rparr>);
|
||||
slot \<leftarrow> return ( globalPD + PPtr (((bit pdSize) - 1) `~shiftL~` pdeBits));
|
||||
deleteObjects (PPtr $ fromPPtr $ head globalPTs) ptBits;
|
||||
placeNewObject (PPtr $ fromPPtr $ head globalPTs) (makeObject ::pte) ptSize;
|
||||
storePDE slot pde;
|
||||
mapGlobalsFrame;
|
||||
kernelDevices \<leftarrow> doMachineOp getKernelDevices;
|
||||
mapM_x mapKernelDevice kernelDevices
|
||||
od)"
|
||||
|
||||
defs allocKernelPT_def:
|
||||
"allocKernelPT\<equiv> (do
|
||||
pts \<leftarrow> gets $ armKSGlobalPTs \<circ> ksArchState;
|
||||
(case pts of
|
||||
[] \<Rightarrow> haskell_fail []
|
||||
| (pt#pts') \<Rightarrow> (do
|
||||
modify (\<lambda> ks. ks \<lparr>
|
||||
ksArchState := (ksArchState ks) \<lparr> armKSGlobalPTs := pts' \<rparr> \<rparr>);
|
||||
return pt
|
||||
od)
|
||||
)
|
||||
defs createSectionPDE_def:
|
||||
"createSectionPDE v\<equiv> (do
|
||||
vbase \<leftarrow> return ( kernelBase `~shiftR~` pageBitsForSize (ARMSection));
|
||||
pdeBits \<leftarrow> return ( objBits (undefined ::pde));
|
||||
pteBits \<leftarrow> return ( objBits (undefined ::pte));
|
||||
globalPD \<leftarrow> gets $ armKSGlobalPD \<circ> ksArchState;
|
||||
offset \<leftarrow> return ( fromVPtr v);
|
||||
virt \<leftarrow> return ( (v - vbase) `~shiftL~` (pageBitsForSize (ARMSuperSection) - 4));
|
||||
phys \<leftarrow> return ( addrFromPPtr $ PPtr $ fromVPtr virt);
|
||||
pde \<leftarrow> return ( SuperSectionPDE_ \<lparr>
|
||||
pdeFrame= phys,
|
||||
pdeParity= True,
|
||||
pdeCacheable= True,
|
||||
pdeGlobal= True,
|
||||
pdeExecuteNever= False,
|
||||
pdeRights= VMKernelOnly \<rparr>);
|
||||
slots \<leftarrow> return ( map (\<lambda> n. globalPD + PPtr (n `~shiftL~` pdeBits))
|
||||
[offset .e. offset + 15]);
|
||||
(flip $ mapM_x ) slots (\<lambda> slot. storePDE slot pde)
|
||||
od)"
|
||||
|
||||
defs mapKernelDevice_def:
|
||||
"mapKernelDevice x0\<equiv> (case x0 of
|
||||
(addr, ptr) \<Rightarrow> (do
|
||||
vptr \<leftarrow> return ( VPtr $ fromPPtr ptr);
|
||||
mapKernelFrame addr vptr VMKernelOnly $ VMAttributes False False False
|
||||
mapKernelFrame addr vptr VMKernelOnly $ VMAttributes False False True
|
||||
od)
|
||||
)"
|
||||
|
||||
defs createGlobalsFrame_def:
|
||||
"createGlobalsFrame\<equiv> (do
|
||||
globals \<leftarrow> gets $ armKSGlobalsFrame \<circ> ksArchState;
|
||||
deleteObjects (PPtr $ fromPPtr globals) pageBits;
|
||||
reserveFrame (PPtr $ fromPPtr globals) True;
|
||||
offset \<leftarrow> return ( fromVPtr $ idleThreadStart - globalsBase);
|
||||
doMachineOp $ mapM_x
|
||||
(split storeWord
|
||||
)
|
||||
(zipE2 (globals + PPtr offset) ( globals + PPtr offset + 4) (idleThreadCode))
|
||||
defs activateGlobalPD_def:
|
||||
"activateGlobalPD\<equiv> (do
|
||||
globalPD \<leftarrow> gets $ armKSGlobalPD \<circ> ksArchState;
|
||||
doMachineOp $ (do
|
||||
setCurrentPD $ addrFromPPtr globalPD;
|
||||
invalidateTLB
|
||||
od)
|
||||
od)"
|
||||
|
||||
defs createITPDPTs_def:
|
||||
"createITPDPTs rootCNCap vptrStart biFrameVPtr\<equiv> (do
|
||||
pdSize \<leftarrow> return ( pdBits - objBits (makeObject ::pde));
|
||||
ptSize \<leftarrow> return ( ptBits - objBits (makeObject ::pte));
|
||||
pdPPtr \<leftarrow> allocRegion pdBits;
|
||||
doKernelOp $ placeNewObject (ptrFromPAddr pdPPtr) (makeObject::pde) pdSize;
|
||||
pdCap \<leftarrow> return $ ArchObjectCap $ PageDirectoryCap (ptrFromPAddr pdPPtr) (Just itASID);
|
||||
slot \<leftarrow> doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapITPD;
|
||||
doKernelOp $ insertInitCap slot $ pdCap;
|
||||
slotBefore \<leftarrow> noInitFailure $ gets $ initSlotPosCur;
|
||||
btmVPtr \<leftarrow> return ( vptrStart `~shiftR~` (pdSize + pageBits) `~shiftL~` (pdSize + pageBits));
|
||||
step \<leftarrow> return ( 1 `~shiftL~` (ptSize + pageBits));
|
||||
topVPtr \<leftarrow> return ( biFrameVPtr + (bit biFrameSizeBits) - 1);
|
||||
forM_x [btmVPtr,btmVPtr + step .e. topVPtr] (\<lambda> vptr. (do
|
||||
ptPPtr \<leftarrow> allocRegion ptBits;
|
||||
doKernelOp $ placeNewObject (ptrFromPAddr ptPPtr) (makeObject::pte) ptSize;
|
||||
provideCap rootCNCap $ ArchObjectCap $ PageTableCap (ptrFromPAddr ptPPtr) (Just (itASID, vptr))
|
||||
od));
|
||||
slotAfter \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
bootInfo \<leftarrow> noInitFailure $ gets initBootInfo;
|
||||
bootInfo' \<leftarrow> return ( bootInfo \<lparr> bifUIPTCaps := [slotBefore .e. slotAfter - 1] \<rparr>);
|
||||
noInitFailure $ modify (\<lambda> s. s \<lparr> initBootInfo := bootInfo' \<rparr>);
|
||||
return pdCap
|
||||
od)"
|
||||
|
||||
defs writeITPDPTs_def:
|
||||
"writeITPDPTs rootCNCap pdCap \<equiv>
|
||||
(case pdCap of
|
||||
ArchObjectCap cap \<Rightarrow> (do
|
||||
doKernelOp $ copyGlobalMappings $ capPDBasePtr cap;
|
||||
ptSlots \<leftarrow> noInitFailure $ gets $ bifUIPTCaps \<circ> initBootInfo;
|
||||
doKernelOp $ (
|
||||
(flip mapM) ptSlots (\<lambda> pos. (do
|
||||
slot \<leftarrow> locateSlot (capCNodePtr rootCNCap) pos;
|
||||
cte \<leftarrow> getCTE slot;
|
||||
mapITPTCap pdCap (cteCap cte)
|
||||
od)
|
||||
)
|
||||
);
|
||||
frameSlots \<leftarrow> noInitFailure $ gets $ bifUIFrameCaps \<circ> initBootInfo;
|
||||
doKernelOp $ (do
|
||||
(flip mapM) frameSlots (\<lambda> pos. (do
|
||||
slot \<leftarrow> locateSlot (capCNodePtr rootCNCap) pos;
|
||||
cte \<leftarrow> getCTE slot;
|
||||
mapITFrameCap pdCap (cteCap cte)
|
||||
od)
|
||||
);
|
||||
slot \<leftarrow> locateSlot (capCNodePtr rootCNCap) biCapITIPCBuf;
|
||||
cte \<leftarrow> getCTE slot;
|
||||
mapITFrameCap pdCap (cteCap cte);
|
||||
slot \<leftarrow> locateSlot (capCNodePtr rootCNCap) biCapBIFrame;
|
||||
cte \<leftarrow> getCTE slot;
|
||||
mapITFrameCap pdCap (cteCap cte)
|
||||
od)
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail $ (show pdCap) @ []
|
||||
)"
|
||||
|
||||
defs createITASIDPool_def:
|
||||
"createITASIDPool rootCNCap\<equiv> (do
|
||||
apPPtr \<leftarrow> allocRegion $ objBits (undefined ::asidpool);
|
||||
doKernelOp $ placeNewObject (ptrFromPAddr apPPtr) (makeObject::asidpool) 0;
|
||||
slot \<leftarrow> doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapITASIDPool;
|
||||
asidPoolCap \<leftarrow> return $ ArchObjectCap $ ASIDPoolCap (ptrFromPAddr apPPtr) 0;
|
||||
doKernelOp $ insertInitCap slot asidPoolCap;
|
||||
slot \<leftarrow> doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapASIDControl;
|
||||
asidControlCap \<leftarrow> return $ ArchObjectCap $ ASIDControlCap;
|
||||
doKernelOp $ insertInitCap slot asidControlCap;
|
||||
return asidPoolCap
|
||||
od)"
|
||||
|
||||
defs writeITASIDPool_def:
|
||||
"writeITASIDPool apCap pdCap\<equiv> (do
|
||||
apPtr \<leftarrow> (case apCap of
|
||||
ArchObjectCap (ASIDPoolCap ptr _) \<Rightarrow> return ptr
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
);
|
||||
pdPtr \<leftarrow> (case pdCap of
|
||||
ArchObjectCap (PageDirectoryCap ptr _) \<Rightarrow> return ptr
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
);
|
||||
ap \<leftarrow> liftM (inv ASIDPool) $ getObject apPtr;
|
||||
ap' \<leftarrow> return ( ap aLU [(itASID, Just pdPtr)]);
|
||||
setObject apPtr (ASIDPool ap');
|
||||
asidTable \<leftarrow> gets (armKSASIDTable \<circ> ksArchState);
|
||||
asidTable' \<leftarrow> return ( asidTable aLU [(asidHighBitsOf itASID, Just apPtr)]);
|
||||
modify (\<lambda> s. s \<lparr>
|
||||
ksArchState := (ksArchState s) \<lparr> armKSASIDTable := asidTable' \<rparr>\<rparr>)
|
||||
od)"
|
||||
|
||||
defs mapITPTCap_def:
|
||||
"mapITPTCap pdCap ptCap\<equiv> (do
|
||||
pd \<leftarrow> (case pdCap of
|
||||
ArchObjectCap (PageDirectoryCap ptr _) \<Rightarrow> return ptr
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
);
|
||||
ptCap' \<leftarrow> (case ptCap of
|
||||
ArchObjectCap c \<Rightarrow> return c
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
);
|
||||
(pt,vptr) \<leftarrow> (case ptCap' of
|
||||
PageTableCap pt' (Some (_, vptr')) \<Rightarrow> return (pt', vptr')
|
||||
| _ \<Rightarrow> haskell_fail $ [] @ (show ptCap)
|
||||
);
|
||||
offset \<leftarrow> return ( fromVPtr $ vptr `~shiftR~` pageBitsForSize ARMSection);
|
||||
targetSlot \<leftarrow> return ( pd + (PPtr $ offset `~shiftL~` 2));
|
||||
pde \<leftarrow> return ( PageTablePDE_ \<lparr>
|
||||
pdeTable= addrFromPPtr pt,
|
||||
pdeParity= True,
|
||||
pdeDomain= 0 \<rparr>);
|
||||
storePDE targetSlot pde
|
||||
od)"
|
||||
|
||||
defs mapITFrameCap_def:
|
||||
"mapITFrameCap pdCap frameCap\<equiv> (do
|
||||
pd' \<leftarrow> (case pdCap of
|
||||
ArchObjectCap (PageDirectoryCap ptr _) \<Rightarrow> return ptr
|
||||
| _ \<Rightarrow> haskell_fail $ [] @ (show pdCap)
|
||||
);
|
||||
frameCap' \<leftarrow> (case frameCap of
|
||||
ArchObjectCap c \<Rightarrow> return c
|
||||
| _ \<Rightarrow> haskell_fail $ [] @ (show frameCap)
|
||||
);
|
||||
(frame,vptr) \<leftarrow> (case frameCap' of
|
||||
PageCap frame' _ _ (Some (_, vptr')) \<Rightarrow> return (frame', vptr')
|
||||
| _ \<Rightarrow> haskell_fail $ [] @ (show frameCap)
|
||||
);
|
||||
offset \<leftarrow> return ( fromVPtr $ vptr `~shiftR~` pageBitsForSize ARMSection);
|
||||
pd \<leftarrow> return ( pd' + (PPtr $ offset `~shiftL~` 2));
|
||||
pde \<leftarrow> getObject pd;
|
||||
pt \<leftarrow> (case pde of
|
||||
PageTablePDE ref _ _ \<Rightarrow> return $ ptrFromPAddr ref
|
||||
| _ \<Rightarrow> haskell_fail $ [] @ (show pd) @ [] @ (show pde)
|
||||
);
|
||||
offset \<leftarrow> return ( fromVPtr $ ((vptr &&(mask $ pageBitsForSize ARMSection))
|
||||
`~shiftR~` pageBitsForSize ARMSmallPage));
|
||||
targetSlot \<leftarrow> return ( pt + (PPtr $ offset `~shiftL~` 2));
|
||||
pte \<leftarrow> return ( SmallPagePTE_ \<lparr>
|
||||
pteFrame= addrFromPPtr frame,
|
||||
pteCacheable= True,
|
||||
pteGlobal= False,
|
||||
pteExecuteNever= False,
|
||||
pteRights= VMReadWrite \<rparr>);
|
||||
storePTE targetSlot pte
|
||||
od)"
|
||||
|
||||
defs createIPCBufferFrame_def:
|
||||
"createIPCBufferFrame rootCNCap vptr\<equiv> (do
|
||||
pptr \<leftarrow> allocFrame;
|
||||
doKernelOp $ doMachineOp $ clearMemory (ptrFromPAddr pptr) (1 `~shiftL~` pageBits);
|
||||
cap \<leftarrow> createITFrameCap (ptrFromPAddr pptr) vptr (Just itASID) False;
|
||||
slot \<leftarrow> doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapITIPCBuf;
|
||||
doKernelOp $ insertInitCap slot cap;
|
||||
bootInfo \<leftarrow> noInitFailure $ gets (initBootInfo);
|
||||
bootInfo' \<leftarrow> return ( bootInfo \<lparr> bifIPCBufVPtr := vptr\<rparr>);
|
||||
noInitFailure $ modify (\<lambda> s. s \<lparr>initBootInfo := bootInfo' \<rparr>);
|
||||
return cap
|
||||
od)"
|
||||
|
||||
defs createBIFrame_def:
|
||||
"createBIFrame rootCNCap vptr nodeId numNodes\<equiv> (do
|
||||
pptr \<leftarrow> allocFrame;
|
||||
bootInfo \<leftarrow> noInitFailure $ gets initBootInfo;
|
||||
bootInfo' \<leftarrow> return ( bootInfo \<lparr> bifNodeID := nodeId,
|
||||
bifNumNodes := numNodes \<rparr>);
|
||||
noInitFailure $ modify (\<lambda> s. s \<lparr>
|
||||
initBootInfo := bootInfo',
|
||||
initBootInfoFrame := pptr,
|
||||
initSlotPosCur := biCapDynStart
|
||||
\<rparr>);
|
||||
doKernelOp $ doMachineOp $ clearMemory (ptrFromPAddr pptr) (1 `~shiftL~` pageBits);
|
||||
cap \<leftarrow> createITFrameCap (ptrFromPAddr pptr) vptr (Just itASID) False;
|
||||
slot \<leftarrow> doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapBIFrame;
|
||||
doKernelOp $ insertInitCap slot cap;
|
||||
return cap
|
||||
od)"
|
||||
|
||||
defs createITFrameCap_def:
|
||||
"createITFrameCap pptr vptr asid large\<equiv> (do
|
||||
sz \<leftarrow> return ( if large then ARMLargePage else ARMSmallPage);
|
||||
addr \<leftarrow> return ( (case asid of
|
||||
Some asid' \<Rightarrow> Just (asid', vptr)
|
||||
| None \<Rightarrow> Nothing
|
||||
));
|
||||
frame \<leftarrow> return ( PageCap_ \<lparr>
|
||||
capVPBasePtr= pptr,
|
||||
capVPRights= VMReadWrite,
|
||||
capVPSize= sz,
|
||||
capVPMappedAddress= addr \<rparr>);
|
||||
return $ ArchObjectCap $ frame
|
||||
od)"
|
||||
|
||||
defs createFramesOfRegion_def:
|
||||
"createFramesOfRegion rootCNCap region doMap pvOffset\<equiv> (do
|
||||
curSlotPos \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
(startPPtr, endPPtr) \<leftarrow> return $ fromRegion region;
|
||||
forM_x [startPPtr,startPPtr + (bit pageBits) .e. endPPtr] (\<lambda> ptr. (do
|
||||
paddr \<leftarrow> return ( fromPAddr $ addrFromPPtr ptr);
|
||||
frameCap \<leftarrow> if doMap then
|
||||
createITFrameCap ptr ((VPtr paddr) + pvOffset ) (Just itASID) False
|
||||
else createITFrameCap ptr 0 Nothing False;
|
||||
provideCap rootCNCap frameCap
|
||||
od));
|
||||
slotPosAfter \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
bootInfo \<leftarrow> noInitFailure $ gets initBootInfo;
|
||||
bootInfo' \<leftarrow> return ( bootInfo \<lparr> bifUIFrameCaps := [curSlotPos .e. slotPosAfter - 1] \<rparr>);
|
||||
noInitFailure $ modify (\<lambda> s. s \<lparr> initBootInfo := bootInfo' \<rparr>)
|
||||
od)"
|
||||
|
||||
defs mapGlobalsFrame_def:
|
||||
"mapGlobalsFrame\<equiv> (do
|
||||
globalsFrame \<leftarrow> gets $ armKSGlobalsFrame \<circ> ksArchState;
|
||||
mapKernelFrame (addrFromPPtr globalsFrame) globalsBase VMReadOnly $
|
||||
VMAttributes True True False
|
||||
VMAttributes True True True;
|
||||
writeIdleCode
|
||||
od)"
|
||||
|
||||
defs createInitialRoot_def:
|
||||
"createInitialRoot slot\<equiv> (do
|
||||
asid \<leftarrow> return ( 1);
|
||||
initPDFrame \<leftarrow> allocRegion pdBits;
|
||||
initPD \<leftarrow> return ( ptrFromPAddr initPDFrame);
|
||||
rootCap \<leftarrow> return ( ArchObjectCap $ PageDirectoryCap_ \<lparr>
|
||||
capPDBasePtr= initPD,
|
||||
capPDMappedASID= Just asid \<rparr>);
|
||||
doKernelOp $ (do
|
||||
placeNewObject (ptrFromPAddr initPDFrame) (makeObject ::pde)
|
||||
(pdBits `~shiftR~` (objBits (makeObject ::pde)));
|
||||
copyGlobalMappings initPD;
|
||||
insertInitCap slot rootCap
|
||||
od);
|
||||
initASIDPoolFrame \<leftarrow> allocRegion $ objBits (undefined ::asidpool);
|
||||
initASIDPoolPtr \<leftarrow> return ( ptrFromPAddr initASIDPoolFrame);
|
||||
emptyASIDPool \<leftarrow> liftM (inv ASIDPool) $ return ( (makeObject ::asidpool));
|
||||
initASIDPool \<leftarrow> return ( ASIDPool $ emptyASIDPool aLU [(asid && mask asidLowBits, Just initPD)]);
|
||||
doKernelOp $ (do
|
||||
placeNewObject (ptrFromPAddr initASIDPoolFrame) initASIDPool 0;
|
||||
asidTable \<leftarrow> gets (armKSASIDTable \<circ> ksArchState);
|
||||
asidTable' \<leftarrow> return (
|
||||
asidTable aLU [(asidHighBitsOf asid, Just initASIDPoolPtr)]);
|
||||
modify (\<lambda> s. s \<lparr>
|
||||
ksArchState := (ksArchState s) \<lparr> armKSASIDTable := asidTable' \<rparr>\<rparr>)
|
||||
od);
|
||||
provideCap $ ArchObjectCap $ ASIDControlCap;
|
||||
provideCap $ ArchObjectCap $ ASIDPoolCap_ \<lparr>
|
||||
capASIDPool= initASIDPoolPtr,
|
||||
capASIDBase= 0 \<rparr>;
|
||||
return rootCap
|
||||
defs writeIdleCode_def:
|
||||
"writeIdleCode\<equiv> (do
|
||||
globalsFrame \<leftarrow> gets $ armKSGlobalsFrame \<circ> ksArchState;
|
||||
offset \<leftarrow> return ( fromVPtr $ idleThreadStart - globalsBase);
|
||||
doMachineOp $ mapM_x
|
||||
(split storeWord
|
||||
)
|
||||
(zipE2 (globalsFrame + PPtr offset) ( globalsFrame + PPtr offset + 4) (idleThreadCode))
|
||||
od)"
|
||||
|
||||
defs populateInitialRoot_def:
|
||||
"populateInitialRoot vRoot cRoot\<equiv> (do
|
||||
asid \<leftarrow> return ( fromJust $ capPDMappedASID $ capCap vRoot);
|
||||
pdCap \<leftarrow> liftM capCap $ return ( vRoot);
|
||||
pd \<leftarrow> return ( capPDBasePtr pdCap);
|
||||
(case cRoot of
|
||||
CNodeCap _ _ _ _ \<Rightarrow> return ()
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
);
|
||||
haskell_assert (capCNodeGuard cRoot = 0) $
|
||||
[];
|
||||
haskell_assert (capCNodeBits cRoot + capCNodeGuardSize cRoot + pageBits =
|
||||
finiteBitSize (undefined::machine_word)) $
|
||||
[];
|
||||
forM_x [0 .e. 1 `~shiftL~` capCNodeBits cRoot - 1] (\<lambda> index. (do
|
||||
cSlot \<leftarrow> doKernelOp $ locateSlot (capCNodePtr cRoot) index;
|
||||
cte \<leftarrow> doKernelOp $ getObject cSlot;
|
||||
(let v2 = cteCap cte in
|
||||
if isArchObjectCap v2 \<and> isPageCap (capCap v2)
|
||||
then
|
||||
let pageCap = capCap v2
|
||||
in (do
|
||||
haskell_assert (capVPSize pageCap = ARMSmallPage) $
|
||||
[];
|
||||
vaddr \<leftarrow> return ( VPtr $ index `~shiftL~` pageBits);
|
||||
pageCap' \<leftarrow> return ( pageCap \<lparr>
|
||||
capVPMappedAddress := Just (asid, vaddr) \<rparr>);
|
||||
cte' \<leftarrow> return ( cte \<lparr> cteCap := ArchObjectCap pageCap' \<rparr>);
|
||||
doKernelOp $ setObject cSlot cte';
|
||||
mapUserFrame pd asid
|
||||
(addrFromPPtr $ capVPBasePtr pageCap) vaddr
|
||||
od)
|
||||
else return ()
|
||||
)
|
||||
od))
|
||||
defs mapKernelFrame_def:
|
||||
"mapKernelFrame paddr vaddr vmrights attributes\<equiv> (do
|
||||
idx \<leftarrow> return ( fromVPtr $ ( (vaddr && (mask $ pageBitsForSize ARMSection))
|
||||
`~shiftR~` pageBitsForSize ARMSmallPage));
|
||||
globalPT \<leftarrow> getARMGlobalPT;
|
||||
pte \<leftarrow> return ( SmallPagePTE_ \<lparr>
|
||||
pteFrame= paddr,
|
||||
pteCacheable= armPageCacheable attributes,
|
||||
pteGlobal= True,
|
||||
pteExecuteNever= False,
|
||||
pteRights= vmrights \<rparr>);
|
||||
storePTE (PPtr ((fromPPtr globalPT) + (idx `~shiftL~` 2))) pte
|
||||
od)"
|
||||
|
||||
defs allocUserPT_def:
|
||||
"allocUserPT asid vaddr\<equiv> (do
|
||||
initPTFrame \<leftarrow> allocRegion ptBits;
|
||||
doKernelOp $ placeNewObject (ptrFromPAddr initPTFrame)
|
||||
(makeObject ::pte) (ptBits `~shiftR~` (objBits (makeObject ::pte)));
|
||||
initPT \<leftarrow> return ( ptrFromPAddr initPTFrame);
|
||||
provideCap $ ArchObjectCap $ PageTableCap_ \<lparr>
|
||||
capPTBasePtr= initPT,
|
||||
capPTMappedAddress= Just (asid, vaddr) \<rparr>;
|
||||
return initPT
|
||||
defs getARMGlobalPT_def:
|
||||
"getARMGlobalPT\<equiv> (do
|
||||
pt \<leftarrow> gets (head \<circ> armKSGlobalPTs \<circ> ksArchState);
|
||||
return pt
|
||||
od)"
|
||||
|
||||
defs mapUserFrame_def:
|
||||
"mapUserFrame pd asid paddr vptr\<equiv> (do
|
||||
haskell_assert (vptr < kernelBase) [];
|
||||
pdSlot \<leftarrow> return ( lookupPDSlot pd vptr);
|
||||
pde \<leftarrow> doKernelOp $ getObject pdSlot;
|
||||
pteBits \<leftarrow> return ( objBits (undefined ::pte));
|
||||
ptIndex \<leftarrow> return ( fromVPtr $ vptr `~shiftR~` 12 && 0xff);
|
||||
ptSlot \<leftarrow> (case pde of
|
||||
PageTablePDE _ _ _ \<Rightarrow> (do
|
||||
pt \<leftarrow> return ( ptrFromPAddr $ pdeTable pde);
|
||||
return $ pt + (PPtr $ ptIndex `~shiftL~` pteBits)
|
||||
od)
|
||||
| InvalidPDE \<Rightarrow> (do
|
||||
ptFrame \<leftarrow> allocUserPT asid vptr;
|
||||
pde \<leftarrow> return ( PageTablePDE_ \<lparr>
|
||||
pdeTable= addrFromPPtr ptFrame,
|
||||
pdeParity= True,
|
||||
pdeDomain= 0 \<rparr>);
|
||||
doKernelOp $ storePDE pdSlot pde;
|
||||
return $ PPtr $ fromPPtr ptFrame + (ptIndex `~shiftL~` pteBits)
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
);
|
||||
doKernelOp $ (do
|
||||
pte \<leftarrow> getObject ptSlot;
|
||||
(case pte of
|
||||
InvalidPTE \<Rightarrow> (do
|
||||
pte' \<leftarrow> return ( SmallPagePTE_ \<lparr>
|
||||
pteFrame= paddr,
|
||||
pteCacheable= True,
|
||||
pteGlobal= False,
|
||||
pteExecuteNever= False,
|
||||
pteRights= VMReadWrite \<rparr>);
|
||||
storePTE ptSlot pte'
|
||||
defs createDeviceFrames_def:
|
||||
"createDeviceFrames rootCNodeCap\<equiv> (do
|
||||
deviceRegions \<leftarrow> doKernelOp $ doMachineOp getDeviceRegions;
|
||||
(flip mapM_x) deviceRegions (\<lambda> (start,end). (do
|
||||
frameSize \<leftarrow> return $ if (isAligned start (pageBitsForSize ARMSection))
|
||||
\<and> isAligned end (pageBitsForSize ARMSection)
|
||||
then ARMSection else ARMSmallPage;
|
||||
slotBefore \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
(flip mapM_x) [start, (start + (bit (pageBitsForSize frameSize))) .e. (end - 1)]
|
||||
(\<lambda> f. (do
|
||||
frameCap \<leftarrow> createITFrameCap (ptrFromPAddr f) 0 Nothing (frameSize = ARMSection);
|
||||
provideCap rootCNodeCap frameCap
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
)
|
||||
);
|
||||
slotAfter \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
biDeviceRegion \<leftarrow> return ( BIDeviceRegion_ \<lparr>
|
||||
bidrBasePAddr= start,
|
||||
bidrFrameSizeBits= fromIntegral $ pageBitsForSize frameSize,
|
||||
bidrFrameCaps= SlotRegion (slotBefore, slotAfter) \<rparr>);
|
||||
devRegions \<leftarrow> noInitFailure $ gets (bifDeviceRegions \<circ> initBootInfo);
|
||||
devRegions' \<leftarrow> return ( devRegions @ [biDeviceRegion]);
|
||||
bootInfo \<leftarrow> noInitFailure $ gets (initBootInfo);
|
||||
bootInfo' \<leftarrow> return ( bootInfo \<lparr> bifDeviceRegions := devRegions' \<rparr>);
|
||||
noInitFailure $ modify (\<lambda> st. st \<lparr> initBootInfo := bootInfo' \<rparr>)
|
||||
od)
|
||||
);
|
||||
bInfo \<leftarrow> noInitFailure $ gets (initBootInfo);
|
||||
bInfo' \<leftarrow> return ( bInfo \<lparr> bifNumDeviceRegions := (fromIntegral \<circ> length \<circ> bifDeviceRegions) bInfo \<rparr>);
|
||||
noInitFailure $ modify (\<lambda> st. st \<lparr> initBootInfo := bInfo' \<rparr>)
|
||||
od)"
|
||||
|
||||
defs copyGlobalMappings_def:
|
||||
|
|
@ -426,9 +494,9 @@ defs lookupIPCBuffer_def:
|
|||
bufferPtr \<leftarrow> threadGet tcbIPCBuffer thread;
|
||||
bufferFrameSlot \<leftarrow> getThreadBufferSlot thread;
|
||||
bufferCap \<leftarrow> getSlotCap bufferFrameSlot;
|
||||
(let v4 = bufferCap in
|
||||
if isArchObjectCap v4 \<and> isPageCap (capCap v4)
|
||||
then let frame = capCap v4
|
||||
(let v3 = bufferCap in
|
||||
if isArchObjectCap v3 \<and> isPageCap (capCap v3)
|
||||
then let frame = capCap v3
|
||||
in (do
|
||||
rights \<leftarrow> return ( capVPRights frame);
|
||||
pBits \<leftarrow> return ( pageBitsForSize $ capVPSize frame);
|
||||
|
|
@ -699,9 +767,9 @@ defs setVMRoot_def:
|
|||
| _ \<Rightarrow> return ()
|
||||
);
|
||||
globalPD \<leftarrow> gets (armKSGlobalPD \<circ> ksArchState);
|
||||
doMachineOp $ setCurrentPD $ addrFromPPtr globalPD
|
||||
doMachineOp $ setCurrentPD $ addrFromPPtr globalPD
|
||||
od)
|
||||
)
|
||||
)
|
||||
od)"
|
||||
|
||||
defs setVMRootForFlush_def:
|
||||
|
|
@ -709,8 +777,8 @@ defs setVMRootForFlush_def:
|
|||
tcb \<leftarrow> getCurThread;
|
||||
threadRootSlot \<leftarrow> getThreadVSpaceRoot tcb;
|
||||
threadRoot \<leftarrow> getSlotCap threadRootSlot;
|
||||
(let v8 = threadRoot in
|
||||
if isArchObjectCap v8 \<and> isPageDirectoryCap (capCap v8) \<and> capPDMappedASID (capCap v8) \<noteq> None \<and> capPDBasePtr (capCap v8) = pd
|
||||
(let v7 = threadRoot in
|
||||
if isArchObjectCap v7 \<and> isPageDirectoryCap (capCap v7) \<and> capPDMappedASID (capCap v7) \<noteq> None \<and> capPDBasePtr (capCap v7) = pd
|
||||
then let cur_pd = pd in return False
|
||||
else (do
|
||||
armv_contextSwitch pd asid;
|
||||
|
|
@ -734,28 +802,6 @@ defs checkValidIPCBuffer_def:
|
|||
| _ \<Rightarrow> throw IllegalOperation
|
||||
)"
|
||||
|
||||
defs createInitPage_def:
|
||||
"createInitPage addr\<equiv> (do
|
||||
ptr \<leftarrow> return ( ptrFromPAddr addr);
|
||||
reserveFrame ptr False;
|
||||
return $ ArchObjectCap $ PageCap ptr VMReadWrite ARMSmallPage Nothing
|
||||
od)"
|
||||
|
||||
defs createDeviceCap_def:
|
||||
"createDeviceCap x0\<equiv> (case x0 of
|
||||
(addr, end) \<Rightarrow> (do
|
||||
wptr \<leftarrow> return ( ptrFromPAddr addr);
|
||||
rawmagnitude \<leftarrow> return ( end - addr);
|
||||
sz \<leftarrow> return ( find (\<lambda> sz. rawmagnitude = bit (pageBitsForSize sz))
|
||||
[minBound .e. maxBound]);
|
||||
magnitude \<leftarrow> (case sz of
|
||||
Some magnitude \<Rightarrow> return magnitude
|
||||
| None \<Rightarrow> haskell_fail []
|
||||
);
|
||||
return $ ArchObjectCap $ PageCap wptr VMReadWrite magnitude Nothing
|
||||
od)
|
||||
)"
|
||||
|
||||
defs maskVMRights_def:
|
||||
"maskVMRights r m\<equiv> (case (r, capAllowRead m, capAllowWrite m) of
|
||||
(VMNoAccess, _, _) \<Rightarrow> VMNoAccess
|
||||
|
|
@ -957,15 +1003,15 @@ defs resolveVAddr_def:
|
|||
pdSlot \<leftarrow> return ( lookupPDSlot pd vaddr);
|
||||
pde \<leftarrow> getObject pdSlot;
|
||||
(case pde of
|
||||
SectionPDE frame v18 v19 v20 v21 v22 v23 \<Rightarrow> return $ Just (ARMSection, frame)
|
||||
| SuperSectionPDE frame v24 v25 v26 v27 v28 \<Rightarrow> return $ Just (ARMSuperSection, frame)
|
||||
| PageTablePDE table v29 v30 \<Rightarrow> (do
|
||||
SectionPDE frame v17 v18 v19 v20 v21 v22 \<Rightarrow> return $ Just (ARMSection, frame)
|
||||
| SuperSectionPDE frame v23 v24 v25 v26 v27 \<Rightarrow> return $ Just (ARMSuperSection, frame)
|
||||
| PageTablePDE table v28 v29 \<Rightarrow> (do
|
||||
pt \<leftarrow> return ( ptrFromPAddr table);
|
||||
pteSlot \<leftarrow> return ( lookupPTSlot_nofail pt vaddr);
|
||||
pte \<leftarrow> getObject pteSlot;
|
||||
(case pte of
|
||||
LargePagePTE frame v10 v11 v12 v13 \<Rightarrow> return $ Just (ARMLargePage, frame)
|
||||
| SmallPagePTE frame v14 v15 v16 v17 \<Rightarrow> return $ Just (ARMSmallPage, frame)
|
||||
LargePagePTE frame v9 v10 v11 v12 \<Rightarrow> return $ Just (ARMLargePage, frame)
|
||||
| SmallPagePTE frame v13 v14 v15 v16 \<Rightarrow> return $ Just (ARMSmallPage, frame)
|
||||
| _ \<Rightarrow> return Nothing
|
||||
)
|
||||
od)
|
||||
|
|
@ -1126,8 +1172,8 @@ defs decodeARMMMUInvocation_def:
|
|||
whenE (null free) $ throw DeleteFirst;
|
||||
base \<leftarrow> returnOk ( (fst $ head free) `~shiftL~` asidLowBits);
|
||||
pool \<leftarrow> returnOk ( makeObject ::asidpool);
|
||||
frame \<leftarrow> (let v31 = untyped in
|
||||
if isUntypedCap v31 \<and> capBlockSize v31 = objBits pool
|
||||
frame \<leftarrow> (let v30 = untyped in
|
||||
if isUntypedCap v30 \<and> capBlockSize v30 = objBits pool
|
||||
then (doE
|
||||
ensureNoChildren parentSlot;
|
||||
returnOk $ capPtr untyped
|
||||
|
|
|
|||
|
|
@ -25,7 +25,7 @@ where
|
|||
definition
|
||||
rootCNodeSize :: "nat"
|
||||
where
|
||||
"rootCNodeSize \<equiv> 8"
|
||||
"rootCNodeSize \<equiv> 12"
|
||||
|
||||
definition
|
||||
timeSlice :: "nat"
|
||||
|
|
|
|||
|
|
@ -261,6 +261,9 @@ where
|
|||
UnknownSyscallException v0 \<Rightarrow> True
|
||||
| _ \<Rightarrow> False"
|
||||
|
||||
datatype init_failure =
|
||||
InitFailure
|
||||
|
||||
datatype syscall_error =
|
||||
IllegalOperation
|
||||
| InvalidArgument nat
|
||||
|
|
|
|||
|
|
@ -36,7 +36,7 @@ consts
|
|||
deletingIRQHandler :: "irq \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
initInterruptController :: "capability kernel_init"
|
||||
initInterruptController :: "capability \<Rightarrow> machine_word \<Rightarrow> capability kernel_init"
|
||||
|
||||
consts
|
||||
handleInterrupt :: "irq \<Rightarrow> unit kernel"
|
||||
|
|
@ -133,19 +133,21 @@ defs deletedIRQHandler_def:
|
|||
setIRQState IRQInactive irq"
|
||||
|
||||
defs initInterruptController_def:
|
||||
"initInterruptController\<equiv> (do
|
||||
"initInterruptController rootCNCap biCapIRQC\<equiv> (do
|
||||
frame \<leftarrow> allocFrame;
|
||||
doKernelOp $ (do
|
||||
haskell_assert (length [minBound .e. (maxBound::irq)]
|
||||
`~shiftL~` (objBits (makeObject ::cte)) \<le> bit pageBits)
|
||||
[];
|
||||
placeNewObject (ptrFromPAddr frame) (makeObject ::cte)
|
||||
(bit pageBits `~shiftR~` objBits (makeObject ::cte));
|
||||
(pageBits - objBits (makeObject ::cte));
|
||||
doMachineOp $ mapM_x (maskInterrupt True) [minBound .e. maxBound];
|
||||
irqTable \<leftarrow> return ( funArray $ const IRQInactive);
|
||||
setInterruptState $ InterruptState (ptrFromPAddr frame) irqTable;
|
||||
timerIRQ \<leftarrow> doMachineOp configureTimer;
|
||||
setIRQState IRQTimer timerIRQ
|
||||
setIRQState IRQTimer timerIRQ;
|
||||
slot \<leftarrow> locateSlot (capCNodePtr rootCNCap) biCapIRQC;
|
||||
insertInitCap slot IRQControlCap
|
||||
od);
|
||||
return IRQControlCap
|
||||
od)"
|
||||
|
|
|
|||
|
|
@ -16,86 +16,56 @@ imports
|
|||
KernelInitMonad_H
|
||||
begin
|
||||
|
||||
consts
|
||||
noInitFailure :: "'a kernel_init_state \<Rightarrow> 'a kernel_init"
|
||||
|
||||
consts
|
||||
minNum4kUntypedObj :: "nat"
|
||||
|
||||
consts
|
||||
maxNumFreememRegions :: "nat"
|
||||
|
||||
consts
|
||||
getAPRegion :: "paddr \<Rightarrow> region list kernel_init"
|
||||
|
||||
consts
|
||||
initFreemem :: "paddr \<Rightarrow> region \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
allocRegion :: "nat \<Rightarrow> paddr kernel_init"
|
||||
|
||||
consts
|
||||
allocFrame :: "paddr kernel_init"
|
||||
|
||||
consts
|
||||
allocPage :: "(vptr * machine_word * machine_word) kernel_init"
|
||||
|
||||
consts
|
||||
mapForInitTask :: "paddr \<Rightarrow> vptr \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
makeRootCNode :: "capability kernel_init"
|
||||
|
||||
consts
|
||||
allocRootSlot :: "(cptr * machine_word) kernel_init"
|
||||
|
||||
consts
|
||||
allocRootSlotWithColour :: "machine_word \<Rightarrow> (cptr * machine_word) kernel_init"
|
||||
|
||||
consts
|
||||
requestRootSlot :: "cptr \<Rightarrow> (machine_word) kernel_init"
|
||||
|
||||
consts
|
||||
makeSlots :: "unit kernel_init"
|
||||
|
||||
consts
|
||||
provideCap :: "capability \<Rightarrow> (cptr * machine_word) kernel_init"
|
||||
|
||||
consts
|
||||
provideRegion :: "boot_region \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
mergeBRs :: "boot_region \<Rightarrow> boot_region \<Rightarrow> nat \<Rightarrow> boot_region option"
|
||||
|
||||
consts
|
||||
addRegionWithMerge :: "boot_region \<Rightarrow> nat \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
initKernel :: "vptr \<Rightarrow> paddr list \<Rightarrow> vptr \<Rightarrow> paddr list \<Rightarrow> paddr list \<Rightarrow> unit kernel"
|
||||
|
||||
consts
|
||||
finaliseBIFrame :: "unit kernel_init"
|
||||
|
||||
consts
|
||||
createInitialThread :: "capability \<Rightarrow> capability \<Rightarrow> capability \<Rightarrow> vptr \<Rightarrow> vptr \<Rightarrow> vptr \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
createIdleThread :: "unit kernel_init"
|
||||
|
||||
consts
|
||||
createUntypedObject :: "capability \<Rightarrow> region \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
mapTaskRegions :: "(paddr * vptr) list \<Rightarrow> ((vptr * machine_word) * (vptr * machine_word)) kernel_init"
|
||||
|
||||
consts
|
||||
createInitCaps :: "capability \<Rightarrow> (vptr * machine_word) \<Rightarrow> capability kernel_init"
|
||||
allocFrame :: "paddr kernel_init"
|
||||
|
||||
consts
|
||||
createUntypedCaps :: "unit kernel_init"
|
||||
makeRootCNode :: "capability kernel_init"
|
||||
|
||||
consts
|
||||
storeLargeBlock :: "(paddr * nat) \<Rightarrow> unit kernel_init"
|
||||
provideCap :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
makeBlockList :: "paddr \<Rightarrow> paddr \<Rightarrow> (paddr * nat) list"
|
||||
provideUntypedCap :: "capability \<Rightarrow> paddr \<Rightarrow> word8 \<Rightarrow> machine_word \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
countUntypedCaps :: "nat kernel_init"
|
||||
|
||||
consts
|
||||
getUntypedRegions :: "(paddr * paddr) list kernel_init"
|
||||
|
||||
consts
|
||||
createDeviceCaps :: "unit kernel_init"
|
||||
|
||||
consts
|
||||
createSmallBlockCaps :: "unit kernel_init"
|
||||
|
||||
consts
|
||||
storeSmallBlockCaps :: "capability list \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
storeSmallBlockCap :: "capability \<Rightarrow> unit kernel_init"
|
||||
|
||||
consts
|
||||
createFreeSlotRegions :: "unit kernel_init"
|
||||
|
||||
consts
|
||||
createEmptyRegions :: "unit kernel_init"
|
||||
coverOf :: "region list \<Rightarrow> region"
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -18,466 +18,273 @@ imports
|
|||
Config_H
|
||||
begin
|
||||
|
||||
defs noInitFailure_def:
|
||||
"noInitFailure \<equiv> lift"
|
||||
|
||||
defs minNum4kUntypedObj_def:
|
||||
"minNum4kUntypedObj \<equiv> 12"
|
||||
|
||||
defs maxNumFreememRegions_def:
|
||||
"maxNumFreememRegions \<equiv> 2"
|
||||
|
||||
defs getAPRegion_def:
|
||||
"getAPRegion kernelFrameEnd\<equiv> (do
|
||||
memRegions \<leftarrow> doKernelOp $ doMachineOp getMemoryRegions;
|
||||
subRegions \<leftarrow> return $ (flip map) memRegions (\<lambda> x.
|
||||
let (s,e) = x in
|
||||
if s < kernelFrameEnd then (kernelFrameEnd,e) else (s,e)
|
||||
);
|
||||
return $ map ptrFromPAddrRegion subRegions
|
||||
od)"
|
||||
|
||||
defs initFreemem_def:
|
||||
"initFreemem kernelFrameEnd uiRegion\<equiv> (do
|
||||
memRegions \<leftarrow> getAPRegion kernelFrameEnd;
|
||||
region \<leftarrow> return ( fromRegion uiRegion);
|
||||
fst' \<leftarrow> return ( fst \<circ> fromRegion);
|
||||
snd' \<leftarrow> return ( snd \<circ> fromRegion);
|
||||
subUI \<leftarrow> return ( \<lambda> r.
|
||||
if fst region \<ge> fst' r \<and> snd region \<le> snd' r
|
||||
then [(fst' r, fst region), (snd region, snd' r)]
|
||||
else [(fst' r, snd' r)]);
|
||||
freeRegions \<leftarrow> return ( concat $ map subUI memRegions);
|
||||
freeRegions' \<leftarrow> return ( take maxNumFreememRegions $ freeRegions @
|
||||
(if (length freeRegions < maxNumFreememRegions)
|
||||
then replicate (maxNumFreememRegions - length freeRegions) (PPtr 0, PPtr 0)
|
||||
else []));
|
||||
noInitFailure $ modify (\<lambda> st. st \<lparr> initFreeMemory := map Region freeRegions' \<rparr>)
|
||||
od)"
|
||||
|
||||
defs allocRegion_def:
|
||||
"allocRegion bits \<equiv>
|
||||
let
|
||||
s = 1 `~shiftL~` bits;
|
||||
align = (\<lambda> b. (((b - 1) `~shiftR~` bits) + 1) `~shiftL~` bits);
|
||||
isUsable = (\<lambda> (b, t). let r = align b in r \<ge> b \<and> r + s - 1 \<le> t)
|
||||
isUsable = (\<lambda> reg. let r = (align \<circ> fst \<circ> fromRegion) reg in
|
||||
r \<ge> (fst $ fromRegion reg) \<and> r + s - 1 \<le> (snd $ fromRegion reg));
|
||||
isAlignedUsable = (\<lambda> reg.
|
||||
let
|
||||
b = fst $ fromRegion reg;
|
||||
t = snd $ fromRegion reg;
|
||||
(r, q) = (align b, align t)
|
||||
in (r = b \<or> q = t) \<and> t - b \<ge> s)
|
||||
in
|
||||
(do
|
||||
freeMem \<leftarrow> gets initFreeMemory;
|
||||
(case isUsable `~break~` freeMem of
|
||||
(small, (b, t)#rest) \<Rightarrow> (do
|
||||
result \<leftarrow> return ( align b);
|
||||
below \<leftarrow> return ( if result = b then [] else [(b, result - 1)]);
|
||||
above \<leftarrow> return ( if result + s - 1 = t then [] else [(result + s, t)]);
|
||||
modify (\<lambda> st. st \<lparr> initFreeMemory := small@below@above@rest \<rparr>);
|
||||
return result
|
||||
freeMem \<leftarrow> noInitFailure $ gets initFreeMemory;
|
||||
(case isAlignedUsable `~break~` freeMem of
|
||||
(small, r#rest) \<Rightarrow> (do
|
||||
(b, t) \<leftarrow> return ( fromRegion r);
|
||||
(result, region) \<leftarrow> return ( if align b = b then (b, Region (b + s, t)) else (t - s, Region (b, t - s)));
|
||||
noInitFailure $ modify (\<lambda> st. st \<lparr> initFreeMemory := small@ [region] @rest \<rparr>);
|
||||
return $ addrFromPPtr result
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
| (_, []) \<Rightarrow>
|
||||
(case isUsable `~break~` freeMem of
|
||||
(small, r'#rest) \<Rightarrow> (do
|
||||
(b, t) \<leftarrow> return ( fromRegion r');
|
||||
result \<leftarrow> return ( align b);
|
||||
below \<leftarrow> return ( if result = b then [] else [Region (b, result)]);
|
||||
above \<leftarrow> return ( if result + s = t then [] else [Region (result + s, t)]);
|
||||
noInitFailure $ modify (\<lambda> st. st \<lparr> initFreeMemory := small@below@above@rest \<rparr>);
|
||||
return $ addrFromPPtr result
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
)
|
||||
)
|
||||
od)"
|
||||
|
||||
defs initKernel_def:
|
||||
"initKernel entry initFrames initOffset kernelFrames bootFrames\<equiv> (do
|
||||
wordSize \<leftarrow> return ( finiteBitSize entry);
|
||||
uiRegion \<leftarrow> return ( coverOf $ map (\<lambda> x. Region (ptrFromPAddr x, (ptrFromPAddr x) + bit (pageBits))) initFrames);
|
||||
kernelRegion \<leftarrow> return ( coverOf $ map (\<lambda> x. Region (ptrFromPAddr x, (ptrFromPAddr x) + bit (pageBits))) kernelFrames);
|
||||
kePPtr \<leftarrow> return ( fst $ fromRegion $ uiRegion);
|
||||
kfEndPAddr \<leftarrow> return ( addrFromPPtr kePPtr);
|
||||
(startPPtr,endPPtr) \<leftarrow> return $ fromRegion uiRegion;
|
||||
vptrStart \<leftarrow> return ( (VPtr (fromPAddr $ addrFromPPtr $ startPPtr )) + initOffset);
|
||||
vptrEnd \<leftarrow> return ( (VPtr (fromPAddr $ addrFromPPtr $ endPPtr )) + initOffset);
|
||||
allMemory \<leftarrow> doMachineOp getMemoryRegions;
|
||||
initPSpace $ map (\<lambda> (s, e). (ptrFromPAddr s, ptrFromPAddr e))
|
||||
allMemory;
|
||||
mapM (\<lambda> p. reserveFrame (ptrFromPAddr p) True) $ kernelFrames @ bootFrames;
|
||||
initKernelVM;
|
||||
initCPU;
|
||||
initPlatform;
|
||||
runInit $ (do
|
||||
initFreemem kfEndPAddr uiRegion;
|
||||
rootCNCap \<leftarrow> makeRootCNode;
|
||||
initInterruptController rootCNCap biCapIRQControl;
|
||||
ipcBufferVPtr \<leftarrow> return ( vptrEnd);
|
||||
ipcBufferCap \<leftarrow> createIPCBufferFrame rootCNCap ipcBufferVPtr;
|
||||
biFrameVPtr \<leftarrow> return ( vptrEnd + (1 `~shiftL~` pageBits));
|
||||
createBIFrame rootCNCap biFrameVPtr 0 1;
|
||||
createFramesOfRegion rootCNCap uiRegion True initOffset;
|
||||
itPDCap \<leftarrow> createITPDPTs rootCNCap vptrStart biFrameVPtr;
|
||||
writeITPDPTs rootCNCap itPDCap;
|
||||
itAPCap \<leftarrow> createITASIDPool rootCNCap;
|
||||
doKernelOp $ writeITASIDPool itAPCap itPDCap;
|
||||
createIdleThread;
|
||||
createInitialThread rootCNCap itPDCap ipcBufferCap entry ipcBufferVPtr biFrameVPtr;
|
||||
createUntypedObject rootCNCap (Region (0,0));
|
||||
createDeviceFrames rootCNCap;
|
||||
finaliseBIFrame;
|
||||
syncBIFrame
|
||||
od)
|
||||
od)"
|
||||
|
||||
defs finaliseBIFrame_def:
|
||||
"finaliseBIFrame\<equiv> (do
|
||||
cur \<leftarrow> noInitFailure $ gets $ initSlotPosCur;
|
||||
max \<leftarrow> noInitFailure $ gets $ initSlotPosMax;
|
||||
noInitFailure $ modify (\<lambda> s. s \<lparr> initBootInfo := (initBootInfo s) \<lparr>bifNullCaps := [cur .e. max - 1]\<rparr>\<rparr>)
|
||||
od)"
|
||||
|
||||
defs createInitialThread_def:
|
||||
"createInitialThread rootCNCap itPDCap ipcBufferCap entry ipcBufferVPtr biFrameVPtr\<equiv> (do
|
||||
tcbBits \<leftarrow> return ( objBits (makeObject::tcb));
|
||||
tcb' \<leftarrow> allocRegion tcbBits;
|
||||
tcbPPtr \<leftarrow> return ( ptrFromPAddr tcb');
|
||||
doKernelOp $ (do
|
||||
placeNewObject tcbPPtr (makeObject::tcb) 0;
|
||||
srcSlot \<leftarrow> locateSlot (capCNodePtr rootCNCap) biCapITCNode;
|
||||
destSlot \<leftarrow> getThreadCSpaceRoot tcbPPtr;
|
||||
cteInsert rootCNCap srcSlot destSlot;
|
||||
srcSlot \<leftarrow> locateSlot (capCNodePtr rootCNCap) biCapITPD;
|
||||
destSlot \<leftarrow> getThreadVSpaceRoot tcbPPtr;
|
||||
cteInsert itPDCap srcSlot destSlot;
|
||||
srcSlot \<leftarrow> locateSlot (capCNodePtr rootCNCap) biCapITIPCBuf;
|
||||
destSlot \<leftarrow> getThreadBufferSlot tcbPPtr;
|
||||
cteInsert ipcBufferCap srcSlot destSlot;
|
||||
threadSet (\<lambda> t. t\<lparr>tcbIPCBuffer := ipcBufferVPtr\<rparr>) tcbPPtr;
|
||||
activateInitialThread tcbPPtr entry biFrameVPtr;
|
||||
cap \<leftarrow> return $ ThreadCap tcbPPtr;
|
||||
slot \<leftarrow> locateSlot (capCNodePtr rootCNCap) biCapITTCB;
|
||||
insertInitCap slot cap
|
||||
od);
|
||||
return ()
|
||||
od)"
|
||||
|
||||
defs createIdleThread_def:
|
||||
"createIdleThread\<equiv> (do
|
||||
paddr \<leftarrow> allocRegion $ objBits (makeObject ::tcb);
|
||||
tcbPPtr \<leftarrow> return ( ptrFromPAddr paddr);
|
||||
doKernelOp $ (do
|
||||
placeNewObject tcbPPtr (makeObject::tcb) 0;
|
||||
modify (\<lambda> s. s \<lparr>ksIdleThread := tcbPPtr\<rparr>);
|
||||
setCurThread tcbPPtr;
|
||||
setSchedulerAction ResumeCurrentThread
|
||||
od);
|
||||
configureIdleThread tcbPPtr
|
||||
od)"
|
||||
|
||||
defs createUntypedObject_def:
|
||||
"createUntypedObject rootCNodeCap bootMemReuseReg\<equiv> (do
|
||||
regStart \<leftarrow> return ( (fst \<circ> fromRegion));
|
||||
regStartPAddr \<leftarrow> return ( (addrFromPPtr \<circ> regStart));
|
||||
regEnd \<leftarrow> return ( (snd \<circ> fromRegion));
|
||||
regEndPAddr \<leftarrow> return ( (addrFromPPtr \<circ> regEnd));
|
||||
slotBefore \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
mapM_x (\<lambda> i. provideUntypedCap rootCNodeCap i (fromIntegral pageBits) slotBefore)
|
||||
[regStartPAddr bootMemReuseReg, (regStartPAddr bootMemReuseReg + bit pageBits) .e. (regEndPAddr bootMemReuseReg - 1)];
|
||||
currSlot \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
mapM_x (\<lambda> _. (do
|
||||
paddr \<leftarrow> allocRegion pageBits;
|
||||
provideUntypedCap rootCNodeCap paddr (fromIntegral pageBits) slotBefore
|
||||
od)
|
||||
)
|
||||
[(currSlot - slotBefore) .e. (fromIntegral minNum4kUntypedObj - 1)];
|
||||
freemem \<leftarrow> noInitFailure $ gets initFreeMemory;
|
||||
(flip mapM) (take maxNumFreememRegions freemem)
|
||||
(\<lambda> reg. (
|
||||
(\<lambda> f. mapM (f reg) [4 .e. (finiteBitSize (undefined::machine_word)) - 2])
|
||||
(\<lambda> reg bits. (do
|
||||
reg' \<leftarrow> (if Not (isAligned (regStartPAddr reg) (bits + 1))
|
||||
\<and> (regEndPAddr reg) - (regStartPAddr reg) \<ge> bit bits
|
||||
then (do
|
||||
provideUntypedCap rootCNodeCap (regStartPAddr reg) (fromIntegral bits) slotBefore;
|
||||
return $ Region (regStart reg + bit bits, regEnd reg)
|
||||
od)
|
||||
else return reg);
|
||||
if Not (isAligned (regEndPAddr reg') (bits + 1)) \<and> (regEndPAddr reg') - (regStartPAddr reg') \<ge> bit bits
|
||||
then (do
|
||||
provideUntypedCap rootCNodeCap (regEndPAddr reg' - bit bits) (fromIntegral bits) slotBefore;
|
||||
return $ Region (regStart reg', regEnd reg' - bit bits)
|
||||
od)
|
||||
else return reg'
|
||||
od)
|
||||
)
|
||||
)
|
||||
);
|
||||
emptyReg \<leftarrow> return ( Region (PPtr 0, PPtr 0));
|
||||
freemem' \<leftarrow> return ( replicate maxNumFreememRegions emptyReg);
|
||||
slotAfter \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
noInitFailure $ modify (\<lambda> s. s \<lparr> initFreeMemory := freemem',
|
||||
initBootInfo := (initBootInfo s) \<lparr>
|
||||
bifUntypedObjCaps := [slotBefore .e. slotAfter - 1] \<rparr>\<rparr>)
|
||||
od)"
|
||||
|
||||
defs mapTaskRegions_def:
|
||||
"mapTaskRegions taskMappings\<equiv> (
|
||||
haskell_fail $ [] @ show taskMappings
|
||||
)"
|
||||
|
||||
defs allocFrame_def:
|
||||
"allocFrame \<equiv> allocRegion pageBits"
|
||||
|
||||
defs allocPage_def:
|
||||
"allocPage\<equiv> (do
|
||||
frame \<leftarrow> allocFrame;
|
||||
clr \<leftarrow> return ( (fromPPtr (ptrFromPAddr frame) `~shiftR~` pageBits)
|
||||
&& mask pageColourBits);
|
||||
(cptr, slot) \<leftarrow> allocRootSlotWithColour clr;
|
||||
doKernelOp $ (do
|
||||
cap \<leftarrow> createInitPage frame;
|
||||
byteLength \<leftarrow> return ( 1 `~shiftL~` pageBits);
|
||||
doMachineOp $ clearMemory (ptrFromPAddr frame) byteLength;
|
||||
insertInitCap slot cap
|
||||
od);
|
||||
return $ (VPtr $ fromCPtr cptr, ptrFromPAddr frame, slot)
|
||||
od)"
|
||||
|
||||
defs mapForInitTask_def:
|
||||
"mapForInitTask frame page\<equiv> (do
|
||||
slot \<leftarrow> requestRootSlot $ CPtr $ fromVPtr page;
|
||||
doKernelOp $ (do
|
||||
cap \<leftarrow> createInitPage frame;
|
||||
insertInitCap slot cap
|
||||
od)
|
||||
od)"
|
||||
|
||||
defs makeRootCNode_def:
|
||||
"makeRootCNode\<equiv> (do
|
||||
slotBits \<leftarrow> return ( objBits (undefined::cte));
|
||||
levelBits \<leftarrow> return ( rootCNodeSize);
|
||||
levelSize \<leftarrow> return ( 1 `~shiftL~` levelBits);
|
||||
frame \<leftarrow> liftM ptrFromPAddr $ allocRegion (levelBits + slotBits);
|
||||
rootCNCap \<leftarrow> doKernelOp $
|
||||
createObject (fromAPIType CapTableObject) frame levelBits;
|
||||
rootCNCap' \<leftarrow> return ( rootCNCap \<lparr>
|
||||
capCNodeGuardSize := finiteBitSize frame - pageBits - levelBits \<rparr>);
|
||||
rootSlots \<leftarrow> mapM (\<lambda> n. doKernelOp $ (do
|
||||
slot \<leftarrow> locateSlot (capCNodePtr rootCNCap') n;
|
||||
cptr \<leftarrow> return ( CPtr $ n `~shiftL~` pageBits);
|
||||
return (cptr, slot)
|
||||
od)
|
||||
) [0 .e. levelSize - 1];
|
||||
modify (\<lambda> st. st \<lparr> initFreeSlotsL1 := rootSlots \<rparr>);
|
||||
provideRegion $ BootRegion
|
||||
(CPtr 0) (CPtr $ (1 `~shiftL~` (pageBits+levelBits)) - 1)
|
||||
BRNodeL1 $ fromIntegral levelBits;
|
||||
return rootCNCap'
|
||||
od)"
|
||||
|
||||
defs allocRootSlot_def:
|
||||
"allocRootSlot\<equiv> (do
|
||||
freeSlots \<leftarrow> gets initFreeSlotsL1;
|
||||
(case freeSlots of
|
||||
result#rest \<Rightarrow> (do
|
||||
modify (\<lambda> st. st \<lparr> initFreeSlotsL1 := rest \<rparr>);
|
||||
return result
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
)
|
||||
od)"
|
||||
|
||||
defs allocRootSlotWithColour_def:
|
||||
"allocRootSlotWithColour c\<equiv> (do
|
||||
freeSlots \<leftarrow> gets initFreeSlotsL1;
|
||||
matchingSlots \<leftarrow> return ( filter (\<lambda> slot.
|
||||
fromCPtr (fst slot) `~shiftR~` pageBits
|
||||
&& mask pageColourBits = c) freeSlots);
|
||||
(case matchingSlots of
|
||||
result#_ \<Rightarrow> (do
|
||||
modify (\<lambda> st. st \<lparr> initFreeSlotsL1 := delete result freeSlots \<rparr>);
|
||||
return result
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail $ [] @ show c @ []
|
||||
)
|
||||
od)"
|
||||
|
||||
defs requestRootSlot_def:
|
||||
"requestRootSlot addr\<equiv> (do
|
||||
freeSlots \<leftarrow> gets initFreeSlotsL1;
|
||||
(requested,others) \<leftarrow> return ( partition (\<lambda> x. fst x = addr) freeSlots);
|
||||
(case requested of
|
||||
[(_,result)] \<Rightarrow> (do
|
||||
modify (\<lambda> st. st \<lparr> initFreeSlotsL1 := others \<rparr>);
|
||||
return result
|
||||
od)
|
||||
| [] \<Rightarrow> haskell_fail $ [] @ show addr
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
)
|
||||
od)"
|
||||
|
||||
defs makeSlots_def:
|
||||
"makeSlots\<equiv> (do
|
||||
slotBits \<leftarrow> return ( objBits (undefined::cte));
|
||||
slotSize \<leftarrow> return ( 1 `~shiftL~` slotBits);
|
||||
levelBits \<leftarrow> return ( pageBits - slotBits);
|
||||
levelSize \<leftarrow> return ( 1 `~shiftL~` levelBits);
|
||||
frame \<leftarrow> liftM ptrFromPAddr allocFrame;
|
||||
(cptr,slot) \<leftarrow> allocRootSlot;
|
||||
node \<leftarrow> doKernelOp $ (do
|
||||
cap \<leftarrow> createObject (fromAPIType CapTableObject)
|
||||
frame levelBits;
|
||||
cap' \<leftarrow> return ( cap \<lparr> capCNodeGuardSize := pageBits - levelBits \<rparr>);
|
||||
insertInitCap slot cap';
|
||||
return $ capCNodePtr cap'
|
||||
od);
|
||||
newSlots \<leftarrow> return ( map
|
||||
(\<lambda> n. (cptr + CPtr n, node + (slotSize * PPtr n)))
|
||||
[0 .e. levelSize - 1]);
|
||||
oldSlots \<leftarrow> gets initFreeSlotsL2;
|
||||
modify (\<lambda> st. st \<lparr> initFreeSlotsL2 := oldSlots @ newSlots \<rparr>);
|
||||
provideRegion $ BootRegion
|
||||
cptr (cptr - 1 + (CPtr $ 1 `~shiftL~` levelBits))
|
||||
BRNodeL2 $ fromIntegral levelBits
|
||||
slotBits \<leftarrow> return ( objBits (undefined::cte));
|
||||
levelBits \<leftarrow> return ( rootCNodeSize);
|
||||
frame \<leftarrow> liftM ptrFromPAddr $ allocRegion (levelBits + slotBits);
|
||||
rootCNCap \<leftarrow> doKernelOp $ createObject (fromAPIType CapTableObject) frame levelBits;
|
||||
rootCNCap \<leftarrow> return $ rootCNCap \<lparr>capCNodeGuardSize := 32 - levelBits\<rparr>;
|
||||
slot \<leftarrow> doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapITCNode;
|
||||
doKernelOp $ insertInitCap slot rootCNCap;
|
||||
return rootCNCap
|
||||
od)"
|
||||
|
||||
defs provideCap_def:
|
||||
"provideCap cap\<equiv> (do
|
||||
freeSlots \<leftarrow> gets initFreeSlotsL2;
|
||||
when (freeSlots = []) makeSlots;
|
||||
freeSlots \<leftarrow> gets initFreeSlotsL2;
|
||||
(case freeSlots of
|
||||
(cptr,slot)#rest \<Rightarrow> (do
|
||||
modify (\<lambda> st. st \<lparr> initFreeSlotsL2 := rest \<rparr>);
|
||||
unless (isNullCap cap) $ doKernelOp $ insertInitCap slot cap;
|
||||
return (cptr, slot)
|
||||
od)
|
||||
| _ \<Rightarrow> haskell_fail []
|
||||
)
|
||||
"provideCap rootCNodeCap cap\<equiv> (do
|
||||
currSlot \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
maxSlot \<leftarrow> noInitFailure $ gets initSlotPosMax;
|
||||
when (currSlot \<ge> maxSlot) $ throwError InitFailure;
|
||||
slot \<leftarrow> doKernelOp $ locateSlot (capCNodePtr rootCNodeCap) currSlot;
|
||||
doKernelOp $ insertInitCap slot cap;
|
||||
noInitFailure $ modify (\<lambda> st. st \<lparr> initSlotPosCur := currSlot + 1 \<rparr>)
|
||||
od)"
|
||||
|
||||
defs provideRegion_def:
|
||||
"provideRegion r \<equiv> addRegionWithMerge r 0"
|
||||
defs provideUntypedCap_def:
|
||||
"provideUntypedCap rootCNodeCap pptr magnitudeBits slotPosBefore\<equiv> (do
|
||||
currSlot \<leftarrow> noInitFailure $ gets initSlotPosCur;
|
||||
i \<leftarrow> return ( currSlot - slotPosBefore);
|
||||
untypedObjs \<leftarrow> noInitFailure $ gets (bifUntypedObjPAddrs \<circ> initBootInfo);
|
||||
haskell_assert (length untypedObjs = fromIntegral i) [];
|
||||
untypedObjs' \<leftarrow> noInitFailure $ gets (bifUntypedObjSizeBits \<circ> initBootInfo);
|
||||
haskell_assert (length untypedObjs' = fromIntegral i) [];
|
||||
bootInfo \<leftarrow> noInitFailure $ gets initBootInfo;
|
||||
bootInfo' \<leftarrow> return ( bootInfo \<lparr> bifUntypedObjPAddrs := untypedObjs @ [pptr],
|
||||
bifUntypedObjSizeBits := untypedObjs' @ [magnitudeBits] \<rparr>);
|
||||
noInitFailure $ modify (\<lambda> st. st \<lparr> initBootInfo := bootInfo' \<rparr>);
|
||||
provideCap rootCNodeCap $ UntypedCap_ \<lparr>
|
||||
capPtr= ptrFromPAddr pptr,
|
||||
capBlockSize= fromIntegral magnitudeBits,
|
||||
capFreeIndex= 0 \<rparr>
|
||||
od)"
|
||||
|
||||
defs mergeBRs_def:
|
||||
"mergeBRs x0 x1 n\<equiv> (case (x0, x1) of
|
||||
((BootRegion a b BRLargeBlocks s), (BootRegion c d BRLargeBlocks t)) \<Rightarrow>
|
||||
if
|
||||
(b = c - 1) \<and> (s && mask n = s) \<and> (t && mask n = 0) then Just (BootRegion a d BRLargeBlocks (s || t))
|
||||
else if
|
||||
True then Nothing
|
||||
else undefined
|
||||
| ((BootRegion a b BRSmallBlocks s), (BootRegion c d BRSmallBlocks t)) \<Rightarrow>
|
||||
if
|
||||
(b = c - 1) \<and> (s = t) then Just (BootRegion a d BRSmallBlocks s)
|
||||
else if
|
||||
True then Nothing
|
||||
else undefined
|
||||
| ((BootRegion a b BRRootTask s), (BootRegion c d BRRootTask t)) \<Rightarrow>
|
||||
if
|
||||
(b = c - 1) \<and> (s = t) then Just (BootRegion a d BRRootTask s)
|
||||
else if
|
||||
True then Nothing
|
||||
else undefined
|
||||
| ((BootRegion b1 t1 BRDeviceCaps d1), (BootRegion b2 t2 BRDeviceCaps d2)) \<Rightarrow>
|
||||
defs coverOf_def:
|
||||
"coverOf x0\<equiv> (case x0 of
|
||||
[] \<Rightarrow> Region (0,0)
|
||||
| [x] \<Rightarrow> x
|
||||
| (x#xs) \<Rightarrow>
|
||||
let
|
||||
n1 = fromCPtr $ t1 - b1 + 1;
|
||||
s1 = fromIntegral $ d1 && mask 8;
|
||||
s2 = fromIntegral $ d2 && mask 8
|
||||
(l,h) = fromRegion x;;
|
||||
(ll,hh) = fromRegion $ coverOf xs;;
|
||||
ln = if l \<le> ll then l else ll;;
|
||||
hn = if h \<le> hh then hh else h
|
||||
in
|
||||
if
|
||||
(t1 = b2 - 1) \<and> (s1 = s2) \<and> (d1 `~shiftR~` s1 = (d2 `~shiftR~` s1) - n1) then Just (BootRegion b1 t2 BRDeviceCaps d1)
|
||||
else if
|
||||
True then Nothing
|
||||
else undefined
|
||||
| (_, _) \<Rightarrow> Nothing
|
||||
Region (ln, hn)
|
||||
)"
|
||||
|
||||
defs addRegionWithMerge_def:
|
||||
"addRegionWithMerge r n \<equiv>
|
||||
let
|
||||
tryMergeList = (\<lambda> xs. (case xs of
|
||||
[] \<Rightarrow> [r]
|
||||
| _ \<Rightarrow> (case mergeBRs (last xs) r n of
|
||||
None \<Rightarrow> xs @ [r]
|
||||
| Some r' \<Rightarrow> init xs @ [r']
|
||||
)
|
||||
))
|
||||
in
|
||||
(do
|
||||
regions \<leftarrow> gets initRegions;
|
||||
modify (\<lambda> st. st \<lparr> initRegions := tryMergeList regions \<rparr>)
|
||||
od)"
|
||||
|
||||
defs initKernel_def:
|
||||
"initKernel entry initFrames initOffset kernelFrames bootFrames\<equiv> (do
|
||||
pageSize \<leftarrow> return ( bit pageBits);
|
||||
wordSize \<leftarrow> return ( finiteBitSize entry);
|
||||
allMemory \<leftarrow> doMachineOp getMemoryRegions;
|
||||
allFrames \<leftarrow> return ( concat $
|
||||
map (\<lambda> (s, e). [s, s+pageSize .e. s+(e-s) - 1])
|
||||
allMemory);
|
||||
initPSpace $ map (\<lambda> (s, e). (ptrFromPAddr s, ptrFromPAddr e))
|
||||
allMemory;
|
||||
mapM (\<lambda> p. reserveFrame (ptrFromPAddr p) True) kernelFrames;
|
||||
initKernelVM;
|
||||
when (null initFrames)
|
||||
$ haskell_fail [];
|
||||
when (null kernelFrames)
|
||||
$ haskell_fail [];
|
||||
unless (distinct initFrames)
|
||||
$ haskell_fail [];
|
||||
unless (distinct kernelFrames)
|
||||
$ haskell_fail [];
|
||||
when (0 `~elem~` initFrames)
|
||||
$ haskell_fail [];
|
||||
when (0 `~elem~` kernelFrames)
|
||||
$ haskell_fail [];
|
||||
unless (andList $ map (flip elem allFrames) initFrames)
|
||||
$ haskell_fail [];
|
||||
unless (andList $ map (flip elem allFrames) kernelFrames)
|
||||
$ haskell_fail [];
|
||||
when (orList $ map (flip elem initFrames) kernelFrames)
|
||||
$ haskell_fail [];
|
||||
unless (andList $ map (flip elem kernelFrames) bootFrames)
|
||||
$ haskell_fail [];
|
||||
unless (distinct allFrames)
|
||||
$ haskell_fail [];
|
||||
unless (isAligned (fromVPtr initOffset) pageBits)
|
||||
$ haskell_fail [];
|
||||
unless (andList $ map (\<lambda> b. isAligned b pageBits) initFrames)
|
||||
$ haskell_fail [];
|
||||
unless (andList $ map (\<lambda> b. isAligned b pageBits) kernelFrames)
|
||||
$ haskell_fail [];
|
||||
unless (distinct bootFrames)
|
||||
$ haskell_fail [];
|
||||
unless (andList $ map (\<lambda> (s, e). (e-s) < bit wordSize
|
||||
\<and> bit pageBits \<le> (e-s))
|
||||
allMemory) $ haskell_fail [];
|
||||
emptyFrames \<leftarrow> return (
|
||||
filter (flip notElem ([0] @ initFrames @ kernelFrames)) allFrames);
|
||||
freeGroups \<leftarrow> return ( rangesBy (\<lambda> a b. a + pageSize = b)
|
||||
(sort emptyFrames));
|
||||
freeMemory \<leftarrow> return (
|
||||
map (\<lambda> fs. (head fs, last fs + pageSize - 1)) freeGroups);
|
||||
bootGroups \<leftarrow> return ( rangesBy (\<lambda> a b. a + pageSize = b) bootFrames);
|
||||
bootMemory \<leftarrow> return (
|
||||
map (\<lambda> fs. (head fs, last fs + pageSize - 1)) bootGroups);
|
||||
(bootInfo, infoVPtr, infoPPtr, tcbCap) \<leftarrow>
|
||||
runInit freeMemory bootMemory $ (do
|
||||
rootCNCap \<leftarrow> makeRootCNode;
|
||||
makeSlots;
|
||||
initMappings \<leftarrow> return ( map
|
||||
(\<lambda> f. (f, (VPtr$fromIntegral f) - initOffset)) initFrames);
|
||||
(buffer, infoPtrs) \<leftarrow> mapTaskRegions initMappings;
|
||||
tcbCap \<leftarrow> createInitCaps rootCNCap buffer;
|
||||
createSmallBlockCaps;
|
||||
createDeviceCaps;
|
||||
untypedCount \<leftarrow> countUntypedCaps;
|
||||
freeSlotCount \<leftarrow> liftM length $ gets initFreeSlotsL2;
|
||||
when (freeSlotCount < untypedCount + minFreeSlots) $ (do
|
||||
makeSlots;
|
||||
untypedCount' \<leftarrow> countUntypedCaps;
|
||||
freeSlotCount' \<leftarrow> liftM length $ gets initFreeSlotsL2;
|
||||
haskell_assert (freeSlotCount' \<ge> untypedCount' + minFreeSlots) $
|
||||
[]
|
||||
od);
|
||||
createUntypedCaps;
|
||||
createFreeSlotRegions;
|
||||
createEmptyRegions;
|
||||
return (fst buffer, infoPtrs, tcbCap)
|
||||
od);
|
||||
bootInfoWords \<leftarrow> return ( wordsFromBootInfo bootInfo);
|
||||
intSize \<leftarrow> return ( finiteBitSize (undefined::machine_word) div 8);
|
||||
haskell_assert (length bootInfoWords * intSize < 1 `~shiftL~` pageBits) $
|
||||
[] @ show bootInfo;
|
||||
mapM_x
|
||||
(split storeWordUser
|
||||
)
|
||||
(zipE2 (infoPPtr) ( infoPPtr+(PPtr $ fromIntegral intSize)) (bootInfoWords));
|
||||
activateInitialThread (capTCBPtr tcbCap) entry infoVPtr
|
||||
od)"
|
||||
|
||||
defs mapTaskRegions_def:
|
||||
"mapTaskRegions taskMappings\<equiv> (do
|
||||
mapM (uncurry mapForInitTask) taskMappings;
|
||||
(bufferPtr,_,bufferSlot) \<leftarrow> allocPage;
|
||||
(infoVPtr,infoPPtr,_) \<leftarrow> allocPage;
|
||||
pages \<leftarrow> return ( sort $ map snd taskMappings);
|
||||
pageSize \<leftarrow> return ( 1 `~shiftL~` pageBits);
|
||||
pageGroups \<leftarrow> return ( [bufferPtr]#[infoVPtr]#
|
||||
rangesBy (\<lambda> a b. a + pageSize = b) pages);
|
||||
rootTaskRegions \<leftarrow> return (
|
||||
map (\<lambda> ps. BootRegion
|
||||
(CPtr $ fromVPtr $ head ps)
|
||||
(CPtr $ fromVPtr $ last ps + pageSize - 1)
|
||||
BRRootTask (fromIntegral pageBits))
|
||||
$ pageGroups);
|
||||
mapM_x provideRegion rootTaskRegions;
|
||||
return ((bufferPtr, bufferSlot), (infoVPtr, infoPPtr))
|
||||
od)"
|
||||
|
||||
defs createInitCaps_def:
|
||||
"createInitCaps rootCNCap x1\<equiv> (case x1 of
|
||||
(bufferPtr, bufferSlot) \<Rightarrow> (do
|
||||
(nullCapPtr,_) \<leftarrow> provideCap NullCap;
|
||||
haskell_assert (nullCapPtr = CPtr 0) [];
|
||||
tcbBits \<leftarrow> return ( objBits (undefined ::tcb));
|
||||
tcbFrame \<leftarrow> liftM ptrFromPAddr $ allocRegion $ tcbBits;
|
||||
idleFrame \<leftarrow> liftM ptrFromPAddr $ allocRegion $ tcbBits;
|
||||
tcbCap \<leftarrow> doKernelOp $ createObject (fromAPIType TCBObject) tcbFrame 0;
|
||||
idleCap \<leftarrow> doKernelOp $ createObject (fromAPIType TCBObject) idleFrame 0;
|
||||
provideCap tcbCap;
|
||||
(_,rootCNSlot) \<leftarrow> provideCap rootCNCap;
|
||||
(_,rootVNSlot) \<leftarrow> provideCap NullCap;
|
||||
irqCap \<leftarrow> initInterruptController;
|
||||
provideCap irqCap;
|
||||
provideCap DomainCap;
|
||||
initVSpace rootCNSlot rootVNSlot;
|
||||
doKernelOp $ (do
|
||||
threadCRoot \<leftarrow> getThreadCSpaceRoot (capTCBPtr tcbCap);
|
||||
cteInsert rootCNCap rootCNSlot threadCRoot;
|
||||
threadVRoot \<leftarrow> getThreadVSpaceRoot (capTCBPtr tcbCap);
|
||||
rootVNCap \<leftarrow> getSlotCap rootVNSlot;
|
||||
cteInsert rootVNCap rootVNSlot threadVRoot;
|
||||
threadSet (\<lambda> t. t \<lparr> tcbIPCBuffer := bufferPtr \<rparr>)
|
||||
(capTCBPtr tcbCap);
|
||||
threadBuffer \<leftarrow> getThreadBufferSlot (capTCBPtr tcbCap);
|
||||
bufferCap \<leftarrow> getSlotCap bufferSlot;
|
||||
bufferCap' \<leftarrow> nullCapOnFailure $ deriveCap bufferSlot bufferCap;
|
||||
cteInsert bufferCap' bufferSlot threadBuffer;
|
||||
setPriority (capTCBPtr tcbCap) maxPriority
|
||||
od);
|
||||
configureIdleThread (capTCBPtr idleCap);
|
||||
doKernelOp $ setIdleThread (capTCBPtr idleCap);
|
||||
firstFreeSlot \<leftarrow> liftM (fst \<circ> head) $ gets initFreeSlotsL2;
|
||||
provideRegion $ BootRegion (CPtr 0) (firstFreeSlot - 1) BRInitCaps 0;
|
||||
return tcbCap
|
||||
od)
|
||||
)"
|
||||
|
||||
defs createUntypedCaps_def:
|
||||
"createUntypedCaps\<equiv> (do
|
||||
freeRegions \<leftarrow> getUntypedRegions;
|
||||
modify (\<lambda> st. st \<lparr> initFreeMemory := [], initBootMemory := [] \<rparr>);
|
||||
blocks \<leftarrow> return ( concat (map (uncurry makeBlockList) freeRegions));
|
||||
mapM_x storeLargeBlock blocks
|
||||
od)"
|
||||
|
||||
defs storeLargeBlock_def:
|
||||
"storeLargeBlock x0\<equiv> (case x0 of
|
||||
(addr, bits) \<Rightarrow> (do
|
||||
ptr \<leftarrow> return ( ptrFromPAddr addr);
|
||||
(cptr, _) \<leftarrow> provideCap (UntypedCap ptr bits 0);
|
||||
addRegionWithMerge (BootRegion cptr cptr BRLargeBlocks (bit bits)) bits
|
||||
od)
|
||||
)"
|
||||
|
||||
defs makeBlockList_def:
|
||||
"makeBlockList s e \<equiv>
|
||||
let
|
||||
n = finiteBitSize s;
|
||||
magnitudes = [0 .e. n - 1];
|
||||
makeLowBlock = (\<lambda> ((start, end), xs, ys) b.
|
||||
if start !! b \<and> start \<le> end
|
||||
then ((start + bit b, end), (start, b) # xs, ys)
|
||||
else ((start, end), xs, ys));
|
||||
makeHighBlock = (\<lambda> ((start, end), xs, ys) b.
|
||||
if (end + 1) !! b \<and> start \<le> end
|
||||
then ((start, end - bit b), xs, (end - bit b + 1, b) # ys)
|
||||
else ((start, end), xs, ys));
|
||||
makeBlocks = (\<lambda> v b. makeLowBlock (makeHighBlock v b) b);
|
||||
result = foldl makeBlocks ((s, e), [], []) magnitudes;
|
||||
returnVal = (\<lambda> (_, low, high). reverse high @ reverse low)
|
||||
in
|
||||
returnVal result"
|
||||
|
||||
defs countUntypedCaps_def:
|
||||
"countUntypedCaps\<equiv> (do
|
||||
freeRegions \<leftarrow> getUntypedRegions;
|
||||
return $ sum $ map (\<lambda> (b,t). length (makeBlockList b t)) freeRegions
|
||||
od)"
|
||||
|
||||
defs getUntypedRegions_def:
|
||||
"getUntypedRegions\<equiv> gets (\<lambda> st. initFreeMemory st @ initBootMemory st)"
|
||||
|
||||
defs createDeviceCaps_def:
|
||||
"createDeviceCaps\<equiv> (do
|
||||
devices \<leftarrow> doKernelOp $ doMachineOp getDeviceRegions;
|
||||
forM_x devices (\<lambda> (base, end). (do
|
||||
cap \<leftarrow> doKernelOp $ createDeviceCap (base, end);
|
||||
(cptr,_) \<leftarrow> provideCap cap;
|
||||
rawmagnitude \<leftarrow> return ( end - base);
|
||||
sz \<leftarrow> return ( find (\<lambda> sz. rawmagnitude = bit (pageBitsForSize sz))
|
||||
[minBound .e. maxBound]);
|
||||
magnitude \<leftarrow> (case sz of
|
||||
Some magnitude \<Rightarrow> return $ pageBitsForSize magnitude
|
||||
| None \<Rightarrow> haskell_fail []
|
||||
);
|
||||
provideRegion $ BootRegion cptr cptr BRDeviceCaps
|
||||
(fromIntegral base || fromIntegral magnitude)
|
||||
od))
|
||||
od)"
|
||||
|
||||
defs createSmallBlockCaps_def:
|
||||
"createSmallBlockCaps\<equiv> (do
|
||||
caps \<leftarrow> replicateM minSmallBlocks $ (do
|
||||
frame \<leftarrow> liftM ptrFromPAddr allocFrame;
|
||||
return $ UntypedCap frame pageBits 0
|
||||
od);
|
||||
storeSmallBlockCaps caps
|
||||
od)"
|
||||
|
||||
defs storeSmallBlockCaps_def:
|
||||
"storeSmallBlockCaps \<equiv> mapM_x storeSmallBlockCap"
|
||||
|
||||
defs storeSmallBlockCap_def:
|
||||
"storeSmallBlockCap cap\<equiv> (do
|
||||
(cptr, _) \<leftarrow> provideCap cap;
|
||||
dWord \<leftarrow> return ( fromIntegral pageBits);
|
||||
provideRegion $ BootRegion cptr cptr BRSmallBlocks dWord
|
||||
od)"
|
||||
|
||||
defs createFreeSlotRegions_def:
|
||||
"createFreeSlotRegions\<equiv> (do
|
||||
slots \<leftarrow> gets initFreeSlotsL2;
|
||||
modify (\<lambda> st. st \<lparr> initFreeSlotsL2 := [] \<rparr>);
|
||||
haskell_assert (length slots \<ge> minFreeSlots) $
|
||||
[] @ show (length slots) @
|
||||
[] @ show minFreeSlots;
|
||||
ranges \<leftarrow> return ( rangesBy (\<lambda> a b. a = b - 1) $ sort $ map fst slots);
|
||||
mapM_x (\<lambda> slots. provideRegion $
|
||||
BootRegion (head slots) (last slots) BRFreeSlots 0
|
||||
) ranges
|
||||
od)"
|
||||
|
||||
defs createEmptyRegions_def:
|
||||
"createEmptyRegions\<equiv> (do
|
||||
l1magnitude \<leftarrow> return ( bit (pageBits + rootCNodeSize));
|
||||
slots \<leftarrow> gets initFreeSlotsL1;
|
||||
modify (\<lambda> st. st \<lparr> initFreeSlotsL1 := [] \<rparr>);
|
||||
pageSize \<leftarrow> return ( 1 `~shiftL~` pageBits);
|
||||
ranges \<leftarrow> return ( rangesBy (\<lambda> a b. a + pageSize = b) $ sort $ map fst slots);
|
||||
mapM_x (\<lambda> slots. provideRegion $
|
||||
BootRegion (head slots) (last slots + pageSize - 1) BREmpty 0
|
||||
) ranges;
|
||||
provideRegion $ BootRegion l1magnitude maxBound BREmpty 0
|
||||
od)"
|
||||
|
||||
|
||||
consts
|
||||
newKSDomSchedule :: "(domain \<times> machine_word) list"
|
||||
|
|
|
|||
|
|
@ -133,7 +133,7 @@ defs deleteObjects_def:
|
|||
[];
|
||||
doMachineOp $ freeMemory (PPtr (fromPPtr ptr)) bits;
|
||||
ps \<leftarrow> gets ksPSpace;
|
||||
inRange \<leftarrow> return ( (\<lambda> x. x && (- mask bits) - 1 = fromPPtr ptr));
|
||||
inRange \<leftarrow> return ( (\<lambda> x. x && ((- mask bits) - 1) = fromPPtr ptr));
|
||||
map' \<leftarrow> return ( data_map_filterWithKey
|
||||
(\<lambda> x _. Not (inRange x))
|
||||
(psMap ps));
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -22,12 +22,60 @@ begin
|
|||
definition
|
||||
initKernelVM :: "unit kernel"
|
||||
where
|
||||
"initKernelVM \<equiv> ArchVSpaceDecls_H.initKernelVM"
|
||||
"initKernelVM \<equiv> ArchVSpaceDecls_H.mapKernelWindow"
|
||||
|
||||
definition
|
||||
initVSpace :: "machine_word \<Rightarrow> machine_word \<Rightarrow> unit kernel_init"
|
||||
initPlatform :: "unit kernel"
|
||||
where
|
||||
"initVSpace \<equiv> ArchVSpaceDecls_H.initVSpace"
|
||||
"initPlatform\<equiv> (do
|
||||
doMachineOp $ configureTimer;
|
||||
doMachineOp $ initL2Cache
|
||||
od)"
|
||||
|
||||
definition
|
||||
initCPU :: "unit kernel"
|
||||
where
|
||||
"initCPU \<equiv> ArchVSpaceDecls_H.activateGlobalPD"
|
||||
|
||||
definition
|
||||
createIPCBufferFrame :: "capability \<Rightarrow> vptr \<Rightarrow> capability kernel_init"
|
||||
where
|
||||
"createIPCBufferFrame \<equiv> ArchVSpaceDecls_H.createIPCBufferFrame"
|
||||
|
||||
definition
|
||||
createBIFrame :: "capability \<Rightarrow> vptr \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> capability kernel_init"
|
||||
where
|
||||
"createBIFrame \<equiv> ArchVSpaceDecls_H.createBIFrame"
|
||||
|
||||
definition
|
||||
createFramesOfRegion :: "capability \<Rightarrow> region \<Rightarrow> bool \<Rightarrow> vptr \<Rightarrow> unit kernel_init"
|
||||
where
|
||||
"createFramesOfRegion \<equiv> ArchVSpaceDecls_H.createFramesOfRegion"
|
||||
|
||||
definition
|
||||
createITPDPTs :: "capability \<Rightarrow> vptr \<Rightarrow> vptr \<Rightarrow> capability kernel_init"
|
||||
where
|
||||
"createITPDPTs \<equiv> ArchVSpaceDecls_H.createITPDPTs"
|
||||
|
||||
definition
|
||||
writeITPDPTs :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel_init"
|
||||
where
|
||||
"writeITPDPTs \<equiv> ArchVSpaceDecls_H.writeITPDPTs"
|
||||
|
||||
definition
|
||||
createITASIDPool :: "capability \<Rightarrow> capability kernel_init"
|
||||
where
|
||||
"createITASIDPool \<equiv> ArchVSpaceDecls_H.createITASIDPool"
|
||||
|
||||
definition
|
||||
writeITASIDPool :: "capability \<Rightarrow> capability \<Rightarrow> unit kernel"
|
||||
where
|
||||
"writeITASIDPool \<equiv> ArchVSpaceDecls_H.writeITASIDPool"
|
||||
|
||||
definition
|
||||
createDeviceFrames :: "capability \<Rightarrow> unit kernel_init"
|
||||
where
|
||||
"createDeviceFrames \<equiv> ArchVSpaceDecls_H.createDeviceFrames"
|
||||
|
||||
definition
|
||||
handleVMFault :: "machine_word \<Rightarrow> vmfault_type \<Rightarrow> ( fault , unit ) kernel_f"
|
||||
|
|
@ -49,15 +97,5 @@ lookupIPCBuffer :: "bool \<Rightarrow> machine_word \<Rightarrow> ((machine_word
|
|||
where
|
||||
"lookupIPCBuffer \<equiv> ArchVSpaceDecls_H.lookupIPCBuffer"
|
||||
|
||||
definition
|
||||
createInitPage :: "paddr \<Rightarrow> capability kernel"
|
||||
where
|
||||
"createInitPage \<equiv> ArchVSpaceDecls_H.createInitPage"
|
||||
|
||||
definition
|
||||
createDeviceCap :: "(paddr * paddr) \<Rightarrow> capability kernel"
|
||||
where
|
||||
"createDeviceCap \<equiv> ArchVSpaceDecls_H.createDeviceCap"
|
||||
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -1,11 +1,10 @@
|
|||
Built from git repo at /home/jbeeren/nfshome/work/fp/seL4/haskell by jbeeren
|
||||
|
||||
Generated from changeset:
|
||||
a3c1a39 Minor change to haskell implementation of armv_contextSwitch
|
||||
3105c61 Merge branch 'master' into context-switch
|
||||
|
||||
|
||||
Warning - uncomitted changes used:
|
||||
M src/SEL4/Kernel/VSpace/ARM.lhs
|
||||
?? ../api/
|
||||
?? ../arch/
|
||||
?? ../kernel.elf
|
||||
|
|
|
|||
Loading…
Reference in New Issue