adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

init commit for imx31-new-qemu support

This commit is contained in:
Gao Xin 2014-12-23 14:27:04 +11:00 committed by Gerwin Klein
parent 8302e4960a
commit d87fdb30ea
11 changed files with 828 additions and 916 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
haskell/SEL4.cabal
View File

@ -25,7 +25,7 @@ Library
exposed-modules: SEL4
SEL4.Machine.Target
build-depends: mtl, base, array, containers
build-depends: mtl==2.1.3.1, base, array, containers
if flag(FFI)
-- be fixed.
build-depends: unix
@ -42,6 +42,7 @@ Library
SEL4.API.Types.Universal
SEL4.API.Invocation
SEL4.Kernel
SEL4.Kernel.BootInfo
SEL4.Kernel.VSpace
SEL4.Kernel.CSpace
SEL4.Kernel.Init

6
haskell/src/SEL4/API/Failures.lhs
View File

@ -42,6 +42,12 @@ The procedure for handling faults is defined in \autoref{sec:kernel.faulthandler
> userExceptionErrorCode :: Word }
> deriving Show
\subsection{Kernel Init Failure}
Data type InitFailure can be thrown during SysInit
> data InitFailure = InitFailure
\subsection{System Call Errors}
The following data type defines the set of errors that can be returned from a kernel object method call.

112
haskell/src/SEL4/API/Types.lhs
View File

@ -28,7 +28,7 @@ We use the C preprocessor to select a target architecture. Also, this file makes
> import SEL4.Machine
> import Data.Bits
> import Data.Word(Word8)
> import Data.Word(Word8 , Word32)
\end{impdetails}
@ -203,86 +203,44 @@ The top-level structure is "BootInfo", which contains an IPC buffer pointer,
information about the initial untyped capabilities, and an array of virtual
address space regions.
> data BootInfo = BootInfo {
> biIPCBuffer :: VPtr,
> -- insert (length biRegions) here
> biRegions :: [BootRegion] }
> deriving Show
> newtype Region = Region { fromRegion :: (PPtr Word, PPtr Word) }
> deriving (Show, Eq)
> wordsFromBootInfo :: BootInfo -> [Word]
> wordsFromBootInfo bi = [
> fromVPtr $ biIPCBuffer bi,
> fromIntegral $ length $ biRegions bi ]
> ++ (concat $ map wordsFromBootRegion $ biRegions bi)
> ptrFromPAddrRegion :: (PAddr, PAddr) -> Region
> ptrFromPAddrRegion (start, end) = Region (ptrFromPAddr start, ptrFromPAddr end)
Each region descriptor has start and end pointers (with the latter pointing to
the last address in the region, rather than the first address after it), a
type, and some data whose use depends on the type.
> newtype SlotRegion = SlotRegion (Word, Word)
> deriving (Show, Eq)
> data BootRegion = BootRegion {
> brBase :: CPtr,
> brEnd :: CPtr,
> brType :: BootRegionType,
> brData :: Word }
> deriving Show
> data BIDeviceRegion = BIDeviceRegion {
> bidrBasePAddr :: PAddr,
> bidrFrameSizeBits :: Word32,
> bidrFrameCaps :: SlotRegion }
> deriving (Show, Eq)
> wordsFromBootRegion :: BootRegion -> [Word]
> wordsFromBootRegion br = [
> fromCPtr $ brBase br,
> fromCPtr $ brEnd br,
> fromIntegral $ fromEnum $ brType br,
> brData br ]
> data BIFrameData = BIFrameData {
> bifNodeID :: Word32, --Word?
> bifNumNodes :: Word32, --Int?
> bifNumIOPTLevels :: Word32, --Int?
> bifIPCBufVPtr :: VPtr,
> bifNullCaps :: [Word],
> bifSharedFrameCaps :: [Word],
> bifUIFrameCaps :: [Word],
> bifUIPTCaps :: [Word],
> bifUntypedObjCaps :: [Word],
> bifUntypedObjPAddrs :: [PAddr],
> bifUntypedObjSizeBits :: [Word8], --combine these into one list?
> bifITCNodeSizeBits :: Word8,
> bifNumDeviceRegions :: Word32,
> bifDeviceRegions :: [BIDeviceRegion] }
> deriving (Show, Eq)
The boot regions are of various types, and are used for three separate purposes: describing what \emph{can} appear in a specific region of the address space, describing what \emph{is} in the initial task's address space, and describing the structure of the capability table. Regions with different purposes may overlap as noted below.
> data BootRegionType
\begin{description}
\item[Empty] regions are not used by capabilities or virtual memory mappings in the initial task's address space.
> = BREmpty
\item[RootTask] regions contain the root task's mapped text or data, backed by one or more page-sized frames.
> | BRRootTask
\item[CapsOnly] regions cannot be used for virtual memory mappings, but are still usable for capabilities. This may be, for example, because the kernel maps its own data at these addresses, or because the hardware MMU does not implement addressing of the region. This may overlap any region other than "BRRootTask".
> | BRCapsOnly
\item[NodeL1] appears once, and represents the area covered by the initial thread's root page table node. The data word contains the radix of the node.
> | BRNodeL1
\item[NodeL2] regions represent second-level nodes in the initial capability table. Again, the data word contains the radix of the node. They all occur within the "BRNodeL1" region.
> | BRNodeL2
Regions of any of the types below only appear in "BRNodeL2" regions.
\item[FreeSlots] regions contain empty capability slots accessible in the root task's CSpace, which may be used to bootstrap the system's capability management. The data word gives the CSpace depth required by the Retype call to locate the CNode containing the slots.
> | BRFreeSlots
\item[InitCaps] is the region containing the root task's six guaranteed initial capabilities; it always appears exactly once with a base address of zero. Address 0 contains a null capability (which should not be replaced with a valid one). It is followed by the initial thread's TCB, CSpace root, VSpace root, and reply endpoint, and then .
> | BRInitCaps
\item[SmallBlocks] regions are filled with untyped memory objects of a single size, generally the platform's standard page size. The minimum number of page-sized untyped blocks that will be provided to the root task by the kernel is fixed at compile time. The data word contains the block size, in address bits.
> | BRSmallBlocks
\item[LargeBlocks] regions are filled with untyped memory objects of varying sizes. The kernel provides large blocks for any physical memory not already covered by other memory regions. The blocks are in order from smallest to largest, with at most one of each size; the sizes present have the corresponding bits in the region's data word set. In spite of the name, some of these blocks may have sizes less than one page. There may be multiple large block regions.
> | BRLargeBlocks
\item[DeviceCaps] regions each contain the capabilities required to access one hardware device. The meaning of the data word is implementation-defined.
> | BRDeviceCaps
\end{description}
> deriving (Show, Enum)
> data InitData = InitData {
> initFreeMemory :: [Region], -- Filled in initFreemem
> initSlotPosCur :: Word, --Word?
> initSlotPosMax :: Word, -- Filled in makeRootCNode ?
> initBootInfo :: BIFrameData,
> initBootInfoFrame :: PAddr } --PAddr?
> deriving (Show, Eq)

186
haskell/src/SEL4/Kernel/BootInfo.lhs Normal file
View File

@ -0,0 +1,186 @@
% @LICENSE(OKL_CORE)
This module contains functions that maintaining the bootinfo structure for init-thread .
> module SEL4.Kernel.BootInfo where
\begin{impdetails}
> import Data.Bits
> import Control.Monad.State
> import SEL4.API.Types
> import SEL4.Object.Structures
> import SEL4.Machine
> import SEL4.Model.StateData
> import {-# SOURCE #-} SEL4.Kernel.Init
\subsection{Constant}
> biCapNull :: Word
> biCapNull = 0
> itASID :: ASID
> itASID = 1
> biCapITTCB :: Word
> biCapITTCB = 1
> biCapITCNode :: Word
> biCapITCNode = 2
> biCapITPD :: Word
> biCapITPD = 3
> biCapIRQControl :: Word
> biCapIRQControl = 4
> biCapASIDControl :: Word
> biCapASIDControl = 5
> biCapITASIDPool :: Word
> biCapITASIDPool = 6
> biCapIOPort :: Word
> biCapIOPort = 7
> biCapIOSpace :: Word
> biCapIOSpace = 8
> biCapBIFrame :: Word
> biCapBIFrame = 9
> biCapITIPCBuf :: Word
> biCapITIPCBuf = 10
> biCapDynStart :: Word
> biCapDynStart = 11
> biFrameSizeBits :: Int
> biFrameSizeBits = pageBits
Warning: rootCNodeSizeBits should be rootCNodeSize + objBits (undefined::CTE)
> rootCNodeSizeBits :: Int
> rootCNodeSizeBits = 12 -- FIXME: duplication (maybe, check)
\subsection{Default Bootinfo}
> nopBIFrameData :: BIFrameData
> nopBIFrameData = BIFrameData {
> bifNodeID = 0, -- Initialized in createIPCBufferFrame
> bifNumNodes = 0, -- Initialized in createIPCBufferFrame
> bifNumIOPTLevels = 0, -- Initialized with 0 if fine
> bifIPCBufVPtr =0, -- Initialized in createIPCBufferFrame
> bifNullCaps = [],
> bifSharedFrameCaps = [], -- ARM no multikernel
> bifUIFrameCaps = [], -- Initialized in createFramesOfRegion
> bifUIPTCaps = [], -- Initialized in createITPDPTs
> bifUntypedObjCaps = [],
> bifUntypedObjPAddrs = [],
> bifUntypedObjSizeBits = [],
> bifITCNodeSizeBits = fromIntegral rootCNodeSizeBits, -- Initialized here is fine
> bifNumDeviceRegions = 0,
> bifDeviceRegions = []
> }
Functions for serialize BIFrameData into Memory
> data SerialData = SerialData {ptrCursor::PPtr Word,value::Word}
> type Serializer = StateT SerialData MachineMonad
> serializeStore :: Word -> Int -> Serializer ()
> serializeStore value intsize = do
> forM_ [0 .. intsize-1] $ \size -> do
Warning: For little endian system we should use this size instead of intsize - size - 1
> byte <- return $ (value `shiftR` (8 * (intsize - size -1))) .&. ((bit 8) - 1)
> serializeByte byte
> serializeByte :: Word -> Serializer ()
> serializeByte input = do
> ptr <- gets ptrCursor
> byte <- gets value
> value <- return $ input .|. ((fromIntegral byte) `shiftL` 8)
> if (ptr .&. 3) == 3
> then do
> lift $ storeWordVM ((ptr `shiftR` 2) `shiftL` 2) value
> modify (\st -> st {ptrCursor = ptr + 1, value = 0})
> else
> modify (\st -> st {ptrCursor = ptr + 1, value = value})
> paddingTo :: PPtr Word -> Serializer()
> paddingTo pptr = do
> ptr <- gets ptrCursor
> (flip mapM_) [ptr .. pptr-1] $ \_ -> (serializeByte 0)
> maxBIUntypedCaps :: Word
> maxBIUntypedCaps = 167
> maxBIDeviceRegions :: Word
> maxBIDeviceRegions = 200
> serialBIDeviceRegion :: BIDeviceRegion -> Serializer ()
> serialBIDeviceRegion biDeviceRegion = do
> serializeStore (fromPAddr $ bidrBasePAddr biDeviceRegion) 4
> serializeStore (fromIntegral $ bidrFrameSizeBits biDeviceRegion) 4
> slotRegion <- return $ bidrFrameCaps biDeviceRegion
> let (a,b) = case slotRegion of SlotRegion (a,b) -> (a,b)
> serializeStore a 4
> serializeStore b 4
> return ()
The function syncBIFrame is used as the last step in KernelInit.
It will write boot info back into the memory.
> syncBIFrame :: KernelInit ()
> syncBIFrame = do
> frameData <- gets $ initBootInfo
> frame <- gets $ initBootInfoFrame
> doKernelOp $ doMachineOp $ do
> (flip runStateT) (SerialData {ptrCursor = ptrFromPAddr $ frame,value = 0}) $ do
> serializeStore (fromIntegral (bifNodeID frameData)) 4
> serializeStore (fromIntegral (bifNumNodes frameData)) 4
> serializeStore (fromIntegral (bifNumIOPTLevels frameData)) 4
> serializeStore (fromIntegral $ fromVPtr $ (bifIPCBufVPtr frameData)) 4
> let serializeRange = \ls -> if ls == []
> then do
> serializeStore 0 4
> serializeStore 0 4
> else do
> serializeStore (head ls) 4
> serializeStore (last ls) 4
> serializeRange $ bifNullCaps frameData
> serializeRange $ bifSharedFrameCaps frameData
> serializeRange $ bifUIFrameCaps frameData
> serializeRange $ bifUIPTCaps frameData
> serializeRange $ bifUntypedObjCaps frameData
> ptr <- gets ptrCursor
> ptr <- return $ ptr + (PPtr $ maxBIUntypedCaps `shiftL` 2)
> untypedAddrs <- return $ bifUntypedObjPAddrs frameData
> (flip mapM_) untypedAddrs $ \addr -> do
> serializeStore (fromPAddr addr) 4
> paddingTo ptr
> ptr <- return $ ptr + (PPtr maxBIUntypedCaps)
> untypedSizeBits <- return $ bifUntypedObjSizeBits frameData
> (flip mapM_) untypedSizeBits $ \bits -> do
> serializeStore (fromIntegral bits) 1
> paddingTo ptr
> serializeStore (fromIntegral $ bifITCNodeSizeBits frameData) 1
> serializeStore (fromIntegral $ bifNumDeviceRegions frameData) 4
> (flip mapM_) (bifDeviceRegions frameData) $ \region -> do
> serialBIDeviceRegion region
> return ()
The KernelInit monad can fail - however, we do not care what type of failure occurred, only that a failure has happened.
> isAligned x n = x .&. mask n == 0

814
haskell/src/SEL4/Kernel/Init.lhs
View File

@ -12,28 +12,31 @@ This module contains functions that create a new kernel state and set up the add
> module SEL4.Kernel.Init(
> initKernel, newKernelState,
> KernelInit, allocRegion, allocFrame, provideCap, provideRegion,
> doKernelOp
> KernelInit, doKernelOp, allocRegion,allocFrame,provideCap
> ) where
\begin{impdetails}
% {-# BOOT-IMPORTS: SEL4.Machine SEL4.Model SEL4.Object.Structures SEL4.API.Types Control.Monad.State #-}
% {-# BOOT-EXPORTS: #InitData KernelInit allocRegion allocFrame provideCap provideRegion doKernelOp #-}
% {-# BOOT-IMPORTS: SEL4.Machine SEL4.Model SEL4.API.Failures SEL4.Object.Structures SEL4.API.Types Control.Monad.State Control.Monad.Error #-}
% {-# BOOT-EXPORTS: #InitData KernelInit allocRegion allocFrame provideCap doKernelOp #-}
> import SEL4.Config
> import SEL4.API.Types
> import SEL4.API.Failures
> import SEL4.Model
> import SEL4.Object
> import SEL4.Machine
> import SEL4.Kernel.Thread
> import SEL4.Kernel.VSpace
> import SEL4.Machine.Hardware.ARM (pageBitsForSize)
> import SEL4.Object.Structures (maxPriority)
> import SEL4.Kernel.BootInfo
>-- import SEL4.Machine.Hardware.ARM (pageBitsForSize)
>-- import SEL4.Object.Structures (maxPriority)
> import Data.Bits
> import Data.List
> import Control.Monad.State(StateT, runStateT, lift)
>-- import Data.List
> import Control.Monad.State(StateT, runStateT)
> import Control.Monad.Error
> import Data.Word(Word8)
\end{impdetails}
@ -41,640 +44,320 @@ This module contains functions that create a new kernel state and set up the add
The first thread in the system is created by the kernel; its address space contains capabilities to change thread domains and to use all of the machine's physical resources, minus any physical memory which is used by the kernel's static data and code.
\subsubsection{Initial Address Space}
The initial address space layout needs to be balanced between using superpages to cover as much memory as possible, to allow greater flexibility for creating large mappings; and providing a reasonable number of small objects, to make the root server's address space easy to manage reliably.
So, the initial address space is constructed as follows:
\begin{itemize}
\item The kernel creates a root CNode, of a user-configurable size. It is given a guard of whatever size is necessary to make each slot in the root CNode cover the same amount of the address space as the architecture's virtual page size. The address space covered by this node is recorded as a "BRNodeL1" region in the boot region list.
\item The kernel creates a second-level CNode from a page-sized block of memory, and give it the necessary guard to allow it to be mapped in the first slot of the root node. The slots in this CNode are used for capabilities created in the following steps. If the kernel runs out of slots, a new CNode will be created and mapped the same way in an unused root node slot. For each such CNode, a "BRNodeL2" region is added to the boot region list.
\item The initial task's thread capability, address space root capabilities, interrupt control capability, architecture-specific initial capabilities and domain capability are mapped into its address space at well-known locations starting at capability address 1. The capability at address 0 is always invalid. These capabilities' locations are recorded as a "BRInitCaps" region in the boot region list.
\item Architecture-specific frame capabilities are created for the code and data of the initial task, and are placed in the corresponding slots in the root CNode. These are then mapped into the virtual address space using an architecture-defined mechanism. "BRRootTask" regions are created to specify the locations of the mapped pages.
\item Two extra virtual memory pages are allocated and mapped, using the same mechanism as the root task's code and data. The boot region list is copied into one of the pages; its location will be passed to the initial thread in a register. The second page will become the initial thread's IPC buffer.
\item From the remaining physical memory, the kernel creates a configurable number of untyped \emph{small blocks} of size equal to the machine's smallest virtual page size, and records their locations with one or more "BRSmallBlocks" regions.
\item Virtual memory capabilities are created for each memory-mapped IO device in the system. For each device, a "BRDeviceCaps" region is created to locate the capabilities used by the device.
\item The kernel ensures that the number of free slots that will remain after the following step is not less than a configurable minimum. If necessary, a new CNode is allocated.
\item All remaining physical memory is divided into aligned power-of-two-sized untyped blocks. The kernel creates capabilities for these blocks, arranged in groups. Each group has no more than one capability of each size, arranged in order of increasing size; for each group, a "BRLargeBlocks" region is created, and the region's data word used as a bit field that indicates which sizes are present in the group.
\item Finally, the kernel creates "BRFreeSlots" regions for any unused slots in the second-level CNodes, "BREmpty" regions for any unused areas of the CSpace, and "BRCapsOnly" regions for any areas of the virtual address space that cannot be allocated to user-level tasks.
\end{itemize}
Implementations that require separate CSpace and VSpace structures will provide caps in the initial CSpace for all frames used to back the initial VSpace. Otherwise, the initial VSpace root will be a copy of the initial CSpace root. In both cases, the CSpace address of each mapped frame capability will be equal to the virtual address of the page it backs.
\subsection{Framework}
\subsubsection{Kernel Initialisation Monad}
The various kernel initialisation functions run in a monad that extends the usual kernel state structures with additional information about the bootstrapping process. In particular, they are able to allocate memory from a list of free frames, and provide the user with capabilities and metadata about the capabilities.
> data InitData = InitData {
> initFreeSlotsL1 :: [(CPtr, PPtr CTE)],
> initFreeSlotsL2 :: [(CPtr, PPtr CTE)],
> initFreeMemory :: [(PAddr, PAddr)],
> initBootMemory :: [(PAddr, PAddr)],
> initRegions :: [BootRegion] }
The KernelInit monad can fail - however, we do not care what type of failure occurred, only that a failure has happened.
> type KernelInit = StateT InitData Kernel
> type KernelInit = ErrorT InitFailure (StateT InitData Kernel)
> doKernelOp :: Kernel a -> KernelInit a
> doKernelOp = lift
> runInit :: [(PAddr, PAddr)] ->
> [(PAddr, PAddr)] ->
> KernelInit (VPtr, (VPtr, PPtr Word), Capability) ->
> Kernel (BootInfo, VPtr, PPtr Word, Capability)
> runInit freeMemory bootMemory doInit = do
> let initData = InitData {
> initFreeSlotsL1 = [],
> initFreeSlotsL2 = [],
> initFreeMemory = freeMemory,
> initBootMemory = bootMemory,
> initRegions = [] }
> ((bufferPtr, (infoVPtr, infoPPtr), tcbCap), initData') <-
> runStateT doInit initData
> let bootInfo = BootInfo bufferPtr $ initRegions initData'
> return (bootInfo, infoVPtr, infoPPtr, tcbCap)
> doKernelOp = lift . lift
\subsubsection{Allocating Frames and Pages}
The following function allocates a region of physical memory. The region size is specified as a power of two, and the allocated region must be size-aligned.
> minNum4kUntypedObj :: Int
> minNum4kUntypedObj = 12
> maxNumFreememRegions :: Int
> maxNumFreememRegions = 2
> getAPRegion :: PAddr -> KernelInit [Region]
> getAPRegion kernelFrameEnd = do
> memRegions <- doKernelOp $ doMachineOp getMemoryRegions
> subRegions <- return $ (flip map) memRegions (\x ->
> let (s,e) = x in
> if s < kernelFrameEnd then (kernelFrameEnd,e) else (s,e)
> )
> return $ map ptrFromPAddrRegion subRegions
> initFreemem :: PAddr -> Region -> KernelInit ()
> initFreemem kernelFrameEnd uiRegion = do
> memRegions <- getAPRegion kernelFrameEnd
> let region = fromRegion uiRegion
> let fst' = fst . fromRegion
> let snd' = snd . fromRegion
> let subUI = \r ->
> if fst region >= fst' r && snd region <= snd' r --assumes uiRegion within one region
> then [(fst' r, fst region), (fst region, snd' r)]
> else [(fst' r, snd' r)]
> let freeRegions = concat $ map subUI memRegions
> let freeRegions' = take maxNumFreememRegions $ freeRegions ++
> (if (length freeRegions < maxNumFreememRegions)
> then replicate (maxNumFreememRegions - length freeRegions) (PPtr 0, PPtr 0)
> else [])
> modify (\st -> st { initFreeMemory = map Region freeRegions' })
> allocRegion :: Int -> KernelInit PAddr
> allocRegion bits = do
> freeMem <- gets initFreeMemory
> case isUsable `break` freeMem of
> (small, (b, t):rest) -> do
> let result = align b
> let below = if result == b then [] else [(b, result - 1)]
> let above = if result + s - 1 == t then [] else [(result + s, t)]
> modify (\st -> st { initFreeMemory = small++below++above++rest })
> return result
> _ -> fail "Unable to allocate memory"
> case isAlignedUsable `break` freeMem of
> (small, r:rest) -> do
> let (b, t) = fromRegion r
> let (result, region) = if align b == b then (b, Region (b + s, t)) else (t - s, Region (b, t - s))
> modify (\st -> st { initFreeMemory = small++ [region] ++rest })
> return $ addrFromPPtr result
> (_, []) ->
> case isUsable `break` freeMem of
> (small, r':rest) -> do
> let (b, t) = fromRegion r'
> let result = align b
> let below = if result == b then [] else [Region (b, result - 1)]
> let above = if result + s - 1 == t then [] else [Region (result + s, t)]
> modify (\st -> st { initFreeMemory = small++below++above++rest })
> return $ addrFromPPtr result
> _ -> fail "Unable to allocate memory"
> where
> s = 1 `shiftL` bits
> align b = (((b - 1) `shiftR` bits) + 1) `shiftL` bits
> isUsable (b, t) = let r = align b in r >= b && r + s - 1 <= t
> isUsable reg = let r = (align . fst . fromRegion) reg in
> r >= (fst $ fromRegion reg) && r + s - 1 <= (snd $ fromRegion reg)
> isAlignedUsable reg =
> let
> b = fst $ fromRegion reg;
> t = snd $ fromRegion reg;
> (r, q) = (align b, align t)
> in (r == b || q == t) && t - b >= s
Most allocations are frame-sized, so for convenience there is an "allocFrame" function.
> allocFrame :: KernelInit PAddr
> allocFrame = allocRegion pageBits
The following function allocates and maps a virtual memory page.
> allocPage :: KernelInit (VPtr, PPtr Word, PPtr CTE)
> allocPage = do
> frame <- allocFrame
> let clr = (fromPPtr (ptrFromPAddr frame) `shiftR` pageBits)
> .&. mask pageColourBits
> (cptr, slot) <- allocRootSlotWithColour clr
> doKernelOp $ do
> cap <- createInitPage frame
> let byteLength = 1 `shiftL` pageBits
> doMachineOp $ clearMemory (ptrFromPAddr frame) byteLength
> insertInitCap slot cap
> return $ (VPtr $ fromCPtr cptr, ptrFromPAddr frame, slot)
The following function creates a capability for a frame, without modifying the contents of the frame. The frame is to be mapped at a given virtual address, and will be inserted into the initial capability space in the corresponding location. Depending on the architecture, this frame capability will either represent the mapping directly, or be copied into an architecture-specific page table structure after that structure is created later in the boot sequence.
> mapForInitTask :: PAddr -> VPtr -> KernelInit ()
> mapForInitTask frame page = do
> slot <- requestRootSlot $ CPtr $ fromVPtr page
> doKernelOp $ do
> cap <- createInitPage frame
> insertInitCap slot cap
\subsubsection{Creating Root CNode Slots}
This function is called once to allocate a root-level CNode and make its slots available.
> makeRootCNode :: KernelInit Capability
> makeRootCNode = do
> let slotBits = objBits (undefined::CTE)
> let levelBits = rootCNodeSize
> let levelSize = 1 `shiftL` levelBits
> frame <- liftM ptrFromPAddr $ allocRegion (levelBits + slotBits)
> rootCNCap <- doKernelOp $
> createObject (fromAPIType CapTableObject) frame levelBits
> let rootCNCap' = rootCNCap {
> capCNodeGuardSize = finiteBitSize frame - pageBits - levelBits }
> rootSlots <- mapM (\n -> doKernelOp $ do
> slot <- locateSlot (capCNodePtr rootCNCap') n
> let cptr = CPtr $ n `shiftL` pageBits
> return (cptr, slot)) [0..levelSize - 1]
> modify (\st -> st { initFreeSlotsL1 = rootSlots })
> provideRegion $ BootRegion
> (CPtr 0) (CPtr $ (1 `shiftL` (pageBits+levelBits)) - 1)
> BRNodeL1 $ fromIntegral levelBits
> return rootCNCap'
\subsubsection{Allocating Root CNode Slots}
The slots in the root CNode are shared by second-level CNodes and the root task's virtual memory mappings. Other than the first second-level CNode, which must start at virtual address 0, the CNodes can be placed in any available slot, but the memory mappings for the initial task's executable require specific addresses.
Slots for CNodes are allocated with "allocRootSlot", which simply returns the first available slot.
> allocRootSlot :: KernelInit (CPtr, PPtr CTE)
> allocRootSlot = do
> freeSlots <- gets initFreeSlotsL1
> case freeSlots of
> result:rest -> do
> modify (\st -> st { initFreeSlotsL1 = rest })
> return result
> _ -> fail "No free root CNode slots remaining"
Virtual memory pages that are not part of the initial executable can be mapped anywhere, as long as the user-level mapping and the kernel's mapping have the same colour (to prevent cache aliasing issues). The "allocRootSlotWithColour" function allocates the first slot of the requested colour. The number of possible colours depends on the platform-defined constant "pageColourBits".
> allocRootSlotWithColour :: Word -> KernelInit (CPtr, PPtr CTE)
> allocRootSlotWithColour c = do
> freeSlots <- gets initFreeSlotsL1
> let matchingSlots = filter (\slot ->
> fromCPtr (fst slot) `shiftR` pageBits
> .&. mask pageColourBits == c) freeSlots
> case matchingSlots of
> result:_ -> do
> modify (\st -> st { initFreeSlotsL1 = delete result freeSlots })
> return result
> _ -> fail $ "No free root slots of colour " ++ show c ++ " remaining"
The initial task's executable must be mapped at the address it was linked at; the "requestRootSlot" function is used to allocate the corresponding root slots. It will fail if the requested slot has already been used or does not exist.
> requestRootSlot :: CPtr -> KernelInit (PPtr CTE)
> requestRootSlot addr = do
> freeSlots <- gets initFreeSlotsL1
> let (requested,others) = partition (\x -> fst x == addr) freeSlots
> case requested of
> [(_,result)] -> do
> modify (\st -> st { initFreeSlotsL1 = others })
> return result
> [] -> fail $ "Requested root CNode slot is not free: " ++ show addr
> _ -> fail "Unreachable: multiple matches for requested slot"
\subsubsection{Creating CNodes}
This function creates a frame full of new capability slots and adds them to the free list.
> makeSlots :: KernelInit ()
> makeSlots = do
> let slotBits = objBits (undefined::CTE)
> let slotSize = 1 `shiftL` slotBits
> let levelBits = pageBits - slotBits
> let levelSize = 1 `shiftL` levelBits
> frame <- liftM ptrFromPAddr allocFrame
> (cptr,slot) <- allocRootSlot
> node <- doKernelOp $ do
> cap <- createObject (fromAPIType CapTableObject)
> frame levelBits
> let cap' = cap { capCNodeGuardSize = pageBits - levelBits }
> insertInitCap slot cap'
> return $ capCNodePtr cap'
> let newSlots = map
> (\n -> (cptr + CPtr n, node + (slotSize * PPtr n)))
> [0..levelSize - 1]
> oldSlots <- gets initFreeSlotsL2
> modify (\st -> st { initFreeSlotsL2 = oldSlots ++ newSlots })
> provideRegion $ BootRegion
> cptr (cptr - 1 + (CPtr $ 1 `shiftL` levelBits))
> BRNodeL2 $ fromIntegral levelBits
\subsubsection{Allocating Slots}
This function allocates a slot and writes an initial capability into it (with no MDB parents or children). If there are no free slots remaining, it creates more. It returns a CSpace pointer to the created capability.
> provideCap :: Capability -> KernelInit (CPtr, PPtr CTE)
> provideCap cap = do
> freeSlots <- gets initFreeSlotsL2
> when (freeSlots == []) makeSlots
> freeSlots <- gets initFreeSlotsL2
> case freeSlots of
> (cptr,slot):rest -> do
> modify (\st -> st { initFreeSlotsL2 = rest })
> unless (isNullCap cap) $ doKernelOp $ insertInitCap slot cap
> return (cptr, slot)
> _ -> fail "No free slots, even after makeSlots"
\subsubsection{Creating Boot Regions}
This function adds a boot region to the initial boot info. In a real implementation it would be written to the boot info page at this point; to keep this code simple we add regions to a list and write them all at once.
> provideRegion :: BootRegion -> KernelInit ()
> provideRegion r = addRegionWithMerge r 0
These functions also add a boot region, but check for the case where the new boot region can be merged with the last existing region to avoid consuming any additional space. The condition for merging of large block mappings is complex - it requires that the all bits in the size bitmap in the second region are at higher locations than those in the first. For convenience, an integer is supplied and the check made is whether the bits lie respectively below and above this cutoff point.
> mergeBRs :: BootRegion -> BootRegion -> Int -> Maybe BootRegion
> mergeBRs (BootRegion a b BRLargeBlocks s) (BootRegion c d BRLargeBlocks t) n
> | (b == c - 1) && (s .&. mask n == s) && (t .&. mask n == 0)
> = Just (BootRegion a d BRLargeBlocks (s .|. t))
> | otherwise
> = Nothing
> mergeBRs (BootRegion a b BRSmallBlocks s) (BootRegion c d BRSmallBlocks t) _
> | (b == c - 1) && (s == t)
> = Just (BootRegion a d BRSmallBlocks s)
> | otherwise
> = Nothing
> mergeBRs (BootRegion a b BRRootTask s) (BootRegion c d BRRootTask t) _
> | (b == c - 1) && (s == t)
> = Just (BootRegion a d BRRootTask s)
> | otherwise
> = Nothing
> mergeBRs
> (BootRegion b1 t1 BRDeviceCaps d1) (BootRegion b2 t2 BRDeviceCaps d2) _
> | (t1 == b2 - 1) && (s1 == s2) &&
> (d1 `shiftR` s1 == (d2 `shiftR` s1) - n1)
> = Just (BootRegion b1 t2 BRDeviceCaps d1)
> | otherwise
> = Nothing
> where
> n1 = fromCPtr $ t1 - b1 + 1
> s1 = fromIntegral $ d1 .&. mask 8
> s2 = fromIntegral $ d2 .&. mask 8
> mergeBRs _ _ _ = Nothing
> addRegionWithMerge :: BootRegion -> Int -> KernelInit ()
> addRegionWithMerge r n = do
> regions <- gets initRegions
> modify (\st -> st { initRegions = tryMergeList regions })
> where
> tryMergeList xs = case xs of
> [] -> [r]
> _ -> case mergeBRs (last xs) r n of
> Nothing -> xs ++ [r]
> Just r' -> init xs ++ [r']
\subsection{Bootstrapping the Kernel}
The kernel is bootstrapped by calling "initKernel". The arguments are the address of the initial thread's entry point, a list of frames to be mapped in the initial thread's address space, the offset to be subtracted from the initial frame addresses to obtain the corresponding virtual addresses, a list of frames reserved by the kernel, and a list of frames that are used by the kernel's bootstrapping code.
> initKernel :: VPtr -> [PAddr] -> VPtr -> [PAddr] -> [PAddr] ->
> Kernel ()
> initKernel :: VPtr -> [PAddr] -> VPtr -> [PAddr] -> [PAddr] -> Kernel ()
> initKernel entry initFrames initOffset kernelFrames bootFrames = do
Define some useful constants.
> let pageSize = bit pageBits
> let wordSize = finiteBitSize entry
> let uiRegion = coverOf $ map (\x -> Region (ptrFromPAddr x, (ptrFromPAddr x) + bit (pageBits) - 1)) initFrames
> let kernelRegion = coverOf $ map (\x -> Region (ptrFromPAddr x, (ptrFromPAddr x) + bit (pageBits) - 1)) kernelFrames
> let kePPtr = fst $ fromRegion $ uiRegion
> let kfEndPAddr = addrFromPPtr kePPtr
> (startPPtr,endPPtr) <- return $ fromRegion uiRegion
> let vptrStart = (VPtr (fromPAddr $ addrFromPPtr $ startPPtr )) + initOffset
> let vptrEnd = (VPtr (fromPAddr $ addrFromPPtr $ endPPtr + 1)) + initOffset
Determine the available memory regions.
> allMemory <- doMachineOp getMemoryRegions
> let allFrames = concat $
> map (\(s, e) -> [s, s+pageSize .. s+(e-s) - 1])
> allMemory
\begin{impdetails}
Configure the physical address space model. This is an implementation detail specific to the Haskell model, and is not relevant on real hardware.
> initPSpace $ map (\(s, e) -> (ptrFromPAddr s, ptrFromPAddr e))
> allMemory
> --FIXME
Reserve the PSpace regions used by the kernel and the root task. This must be done first, since some of these reserved regions will be turned into kernel objects by "initKernelVM", below. Again, this is specific to the Haskell model's implementation and is not relevant on real hardware.
Warning: Currenlty we assume that the bootFrames (probably get from qemu) is always []
> mapM (\p -> reserveFrame (ptrFromPAddr p) True) kernelFrames
Warning: We used to reserve the PSpace regions used by the kernel and the root task. This must be done first, since some of these reserved regions will be turned into kernel objects by "initKernelVM", below. Again, this is specific to the Haskell model's implementation and is not relevant on real hardware.
> mapM (\p -> reserveFrame (ptrFromPAddr p) True) $ kernelFrames ++ bootFrames
\end{impdetails}
\begin{impdetails}
Set up the kernel's VM environment.
> initKernelVM
Make sure the lists of initial task and kernel frames are valid.
\end{impdetails}
> when (null initFrames)
> $ fail "initFrames must not be empty"
> when (null kernelFrames)
> $ fail "kernelFrames must not be empty"
\begin{impdetails}
FIX ME: is the follwing still necessary in haskell?
> unless (distinct initFrames)
> $ fail "initFrames must be distinct"
> unless (distinct kernelFrames)
> $ fail "kernelFrames must be distinct"
> initCPU
> initPlatform
> when (0 `elem` initFrames)
> $ fail "initFrames must not contain 0"
> when (0 `elem` kernelFrames)
> $ fail "kernelFrames must not contain 0"
\end{impdetails}
> unless (and $ map (flip elem allFrames) initFrames)
> $ fail "initFrames must only use available physical memory"
> unless (and $ map (flip elem allFrames) kernelFrames)
> $ fail "kernelFrames must only use available physical memory"
> when (or $ map (flip elem initFrames) kernelFrames)
> $ fail "kernelFrames and initFrames must not overlap"
> unless (and $ map (flip elem kernelFrames) bootFrames)
> $ fail "bootFrames must all appear in kernelFrames"
> unless (distinct allFrames)
> $ fail "memory regions must not overlap"
Move into the "KernelInit" monad. Arguments in nopInitData are not correct, BIFrameInfo will get initialized later.
> unless (isAligned (fromVPtr initOffset) pageBits)
> $ fail "initOffset not aligned"
> unless (and $ map (\b -> isAligned b pageBits) initFrames)
> $ fail "initFrames not aligned"
> unless (and $ map (\b -> isAligned b pageBits) kernelFrames)
> $ fail "kernelFrames not aligned"
> unless (distinct bootFrames)
> $ fail "boot regions must not overlap"
> unless (and $ map (\(s, e) -> (e-s) < bit wordSize
> && bit pageBits <= (e-s))
> allMemory) $ fail "memory regions wrong sizes"
> runInit $ do
> initFreemem kfEndPAddr uiRegion
> rootCNCap <- makeRootCNode
> initInterruptController rootCNCap biCapIRQControl
> let ipcBufferVPtr = vptrEnd
> ipcBufferCap <- createIPCBufferFrame rootCNCap ipcBufferVPtr
> let biFrameVPtr = vptrEnd + (1 `shiftL` pageBits)
> createBIFrame rootCNCap biFrameVPtr 0 1
> createFramesOfRegion rootCNCap uiRegion True initOffset
> itPDCap <- createITPDPTs rootCNCap vptrStart biFrameVPtr
> writeITPDPTs rootCNCap itPDCap
Reserve the frames used by the kernel and the root task.
Create and Init initial thread's ASID pool
> let emptyFrames =
> filter (flip notElem ([0] ++ initFrames ++ kernelFrames)) allFrames
> itAPCap <- createITASIDPool rootCNCap
> doKernelOp $ writeITASIDPool itAPCap itPDCap
Create a list of all remaining free memory regions.
> createIdleThread
> let freeGroups = rangesBy (\a b -> a + pageSize == b)
> (sort emptyFrames)
> let freeMemory =
> map (\fs -> (head fs, last fs + pageSize - 1)) freeGroups
> let bootGroups = rangesBy (\a b -> a + pageSize == b) bootFrames
> let bootMemory =
> map (\fs -> (head fs, last fs + pageSize - 1)) bootGroups
Create InitialThread and switch to it
Move into the "KernelInit" monad.
> createInitialThread rootCNCap itPDCap ipcBufferCap entry ipcBufferVPtr biFrameVPtr
> (bootInfo, infoVPtr, infoPPtr, tcbCap) <-
> runInit freeMemory bootMemory $ do
>-- createUntypedObject rootCNCap Region (KernelBase,KernelBase)
Create the root cnode.
Create Device Frames
> rootCNCap <- makeRootCNode
> createDeviceFrames rootCNCap
Create a second-level CNode. It is not needed yet, but must be created at this point to avoid allocating the first root CNode slot (with address 0) to a virtual memory page.
Searilize BIFrame into memory
> makeSlots
> syncBIFrame
Map the initial task's frames and create boot regions for them.
We should clean cache, but we did not have a good interface so far.
> let initMappings = map
> (\f -> (f, (VPtr$fromIntegral f) - initOffset)) initFrames
> (buffer, infoPtrs) <- mapTaskRegions initMappings
>-- doKernelOp $ doMachineOp $ cleanCache
Create the basic set of initial capabilities.
> runInit :: KernelInit () -> Kernel ()
> runInit oper = do
> let initData = InitData {
> initFreeMemory = [],
> initSlotPosCur = 0,
> initSlotPosMax = bit (pageBits), -- The CNode Size is pageBits + (objSize cte)
> initBootInfo = nopBIFrameData,
> initBootInfoFrame = 0 }
> (flip runStateT) initData $ do
> result <- runErrorT oper
> either (\_ -> fail $ "initFailure") return result
> return ()
> tcbCap <- createInitCaps rootCNCap buffer
createInitalThread, setup caps in initial thread, set idleThread to be the curerntThread and switch to the initialThread.
Create capabilities for the hardware devices and a small number of frame-sized untyped objects.
> createInitialThread :: Capability -> Capability -> Capability -> VPtr -> VPtr -> VPtr-> KernelInit ()
> createInitialThread rootCNCap itPDCap ipcBufferCap entry ipcBufferVPtr biFrameVPtr = do
> let tcbBits = objBits (makeObject::TCB)
> tcb' <- allocRegion tcbBits
> let tcbPPtr = ptrFromPAddr tcb'
> doKernelOp $ do
> placeNewObject tcbPPtr (makeObject::TCB) 0
> srcSlot <- locateSlot (capCNodePtr rootCNCap) biCapITCNode
> destSlot <- getThreadCSpaceRoot tcbPPtr
> cteInsert rootCNCap srcSlot destSlot
> srcSlot <- locateSlot (capCNodePtr rootCNCap) biCapITPD
> destSlot <- getThreadVSpaceRoot tcbPPtr
> cteInsert itPDCap srcSlot destSlot
> srcSlot <- locateSlot (capCNodePtr rootCNCap) biCapITIPCBuf
> destSlot <- getThreadBufferSlot tcbPPtr
> cteInsert ipcBufferCap srcSlot destSlot
> threadSet (\t-> t{tcbIPCBuffer = ipcBufferVPtr}) tcbPPtr
> activateInitialThread tcbPPtr entry biFrameVPtr
> createSmallBlockCaps
> createDeviceCaps
Insert thread into rootCNodeCap
If there are not enough free slots remaining for both the capabilities to the remaining unallocated memory and a minimal number of initial free slots, then reserve another page full of slots.
> cap <- return $ ThreadCap tcbPPtr
> slot <- locateSlot (capCNodePtr rootCNCap) biCapITTCB
> insertInitCap slot cap
> return ()
> untypedCount <- countUntypedCaps
> freeSlotCount <- liftM length $ gets initFreeSlotsL2
> when (freeSlotCount < untypedCount + minFreeSlots) $ do
> makeSlots
create idle thread and set the Current Thread to Idle Thread
FIX ME: Seems we need to setCurThread and setSchedulerAction here, otherwise errors raised.
Reserving more slots may, in rare circumstances, increase the untyped cap count; this will happen if the free blocks are all more than double the size of a frame. Also, calling "makeSlots" may not produce enough free slots if "minFreeSlots" is too large. We assert that there are sufficient free slots to avoid these situations.
> createIdleThread :: KernelInit ()
> createIdleThread = do
> paddr <- allocRegion $ objBits (makeObject :: TCB)
> let tcbPPtr = ptrFromPAddr paddr
> doKernelOp $ do
> placeNewObject tcbPPtr (makeObject::TCB) 0
> modify (\s -> s {ksIdleThread = tcbPPtr})
> setCurThread tcbPPtr
> setSchedulerAction ResumeCurrentThread
> configureIdleThread tcbPPtr
> untypedCount' <- countUntypedCaps
> freeSlotCount' <- liftM length $ gets initFreeSlotsL2
> assert (freeSlotCount' >= untypedCount' + minFreeSlots) $
> "Couldn't reserve enough free slots"
> createUntypedObject :: Capability -> Region -> KernelInit ()
> createUntypedObject rootCNodeCap bootMemReuseReg = do
> let regStart = (fst . fromRegion)
> let regStartPAddr = (addrFromPPtr . regStart)
> let regEnd = (snd . fromRegion)
> let regEndPAddr = (addrFromPPtr . regEnd)
> slotBefore <- gets initSlotPosCur
> mapM_ (\i -> provideUntypedCap rootCNodeCap i (fromIntegral pageBits) slotBefore)
> [regStartPAddr bootMemReuseReg, (regStartPAddr bootMemReuseReg + bit pageBits) .. (regEndPAddr bootMemReuseReg - 1)]
> currSlot <- gets initSlotPosCur
> mapM_ (\_ -> do
> paddr <- allocRegion pageBits
> provideUntypedCap rootCNodeCap paddr (fromIntegral pageBits) slotBefore)
> [(currSlot - slotBefore) .. (fromIntegral minNum4kUntypedObj - 1)]
> freemem <- gets initFreeMemory
> (flip mapM) (take maxNumFreememRegions freemem)
> (\reg -> do
> (\f -> foldM f reg [4 .. (finiteBitSize (undefined::Word)) - 2])
> (\reg bits -> do
> reg' <- (if not (isAligned (regStartPAddr reg) (bits + 1))
> && (regEndPAddr reg) - (regStartPAddr reg) >= bit bits
> then do
> provideUntypedCap rootCNodeCap (regStartPAddr reg) (fromIntegral bits) slotBefore
> return $ Region (regStart reg + bit bits, regEnd reg)
> else return reg)
> if not (isAligned (regEndPAddr reg') (bits + 1)) && (regEndPAddr reg') - (regStartPAddr reg') >= bit bits
> then do
> provideUntypedCap rootCNodeCap (regEndPAddr reg' - bit bits) (fromIntegral bits) slotBefore
> return $ Region (regStart reg', regEnd reg' - bit bits)
> else return reg' )
> )
> let emptyReg = Region (PPtr 0, PPtr 0)
> let freemem' = replicate maxNumFreememRegions emptyReg
> slotAfter <- gets initSlotPosCur
> modify (\s -> s { initFreeMemory = freemem',
> initBootInfo = (initBootInfo s) {
> bifUntypedObjCaps = [slotBefore .. slotAfter] }})
> syncBIFrame
Create untyped capabilities to the remainder of available unallocated memory.
> createUntypedCaps
Create boot regions for any remaining ranges of free slots. After this, it is no longer possible to create new capabilities, as there are no free slots, and no frames left to create more slots.
> createFreeSlotRegions
Create empty regions corresponding to any free L1 frames.
> createEmptyRegions
> return (fst buffer, infoPtrs, tcbCap)
The boot data page is filled in.
> let bootInfoWords = wordsFromBootInfo bootInfo
> let intSize = finiteBitSize (undefined::Word) `div` 8
> assert (length bootInfoWords * intSize < 1 `shiftL` pageBits) $
> "Boot info must fit in one page: " ++ show bootInfo
> zipWithM_ storeWordUser
> [infoPPtr, infoPPtr+(PPtr $ fromIntegral intSize)..] bootInfoWords
Finally, the initial thread's context is set up with the entry point and the location of the boot information page, and then activated.
> activateInitialThread (capTCBPtr tcbCap) entry infoVPtr
\subsubsection{Initial Virtual Memory Mappings}
The initial thread's virtual address space contains a set of frames loaded by the boot loader, and two additional pages allocated by the kernel. Those frames are used for the initial thread's IPC buffer and for storing the "BootInfo" structure, respectively.
> mapTaskRegions :: [(PAddr, VPtr)] ->
> KernelInit ((VPtr, PPtr CTE), (VPtr, PPtr Word))
> mapTaskRegions :: [(PAddr,VPtr)] -> KernelInit ((VPtr,PPtr CTE),(VPtr,PPtr Word))
> mapTaskRegions taskMappings = do
> mapM (uncurry mapForInitTask) taskMappings
> (bufferPtr,_,bufferSlot) <- allocPage
> (infoVPtr,infoPPtr,_) <- allocPage
> let pages = sort $ map snd taskMappings
> let pageSize = 1 `shiftL` pageBits
> let pageGroups = [bufferPtr]:[infoVPtr]:
> rangesBy (\a b -> a + pageSize == b) pages
> let rootTaskRegions =
> map (\ps -> BootRegion
> (CPtr $ fromVPtr $ head ps)
> (CPtr $ fromVPtr $ last ps + pageSize - 1)
> BRRootTask (fromIntegral pageBits))
> $ pageGroups
> mapM_ provideRegion rootTaskRegions
> return ((bufferPtr, bufferSlot), (infoVPtr, infoPPtr))
> fail $ "mapTaskRegions is not Implemented" ++ show taskMappings
\subsubsection{Initial Capabilities}
Make the root cnode, alloc (cptr,slot) from allocRootSlot and insert root cnode cap into its self
The first seven addresses in the initial thread capability space always contain a set of basic capabilities: a null capability at address 0, followed by the initial thread's TCB, CSpace and VSpace roots, and reply endpoint, the interrupt control capability, and the domain capability.
Specific allocRegion for convenience, since most allocations are frame-sized.
This function is responsible for placing those seven capabilities in the initial CSpace, and for creating the corresponding objects (other than the CSpace root, which already exists). It returns the TCB capability, which is needed later on to activate the thread.
> allocFrame :: KernelInit PAddr
> allocFrame = allocRegion pageBits
> createInitCaps :: Capability -> (VPtr, PPtr CTE) -> KernelInit Capability
> createInitCaps rootCNCap (bufferPtr, bufferSlot) = do
> makeRootCNode :: KernelInit Capability
> makeRootCNode = do
> let slotBits = objBits (undefined::CTE)
> let levelBits = rootCNodeSize
> let levelSize = (1::Int) `shiftL` levelBits
> frame <- liftM ptrFromPAddr $ allocRegion (levelBits + slotBits)
> rootCNCap <- doKernelOp $ createObject (fromAPIType CapTableObject) frame levelBits
> slot <- doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapITCNode
> doKernelOp $ insertInitCap slot rootCNCap
> return rootCNCap
Place a null capability in slot 0. The slot's contents should already be null; this is really only done to ensure that slot 0 isn't allocated to something else.
> (nullCapPtr,_) <- provideCap NullCap
> assert (nullCapPtr == CPtr 0) "Null cap must be at CPtr 0"
Create the root task and idle thread TCBs.
> let tcbBits = objBits (undefined :: TCB)
> tcbFrame <- liftM ptrFromPAddr $ allocRegion $ tcbBits
> idleFrame <- liftM ptrFromPAddr $ allocRegion $ tcbBits
> tcbCap <- doKernelOp $ createObject (fromAPIType TCBObject) tcbFrame 0
> idleCap <- doKernelOp $ createObject (fromAPIType TCBObject) idleFrame 0
Place the initial TCB in the root thread.
> provideCap tcbCap
Place the root CNode and VNode capabilities in the CSpace.
> (_,rootCNSlot) <- provideCap rootCNCap
> (_,rootVNSlot) <- provideCap NullCap
Set up the interrupt controller.
> irqCap <- initInterruptController
> provideCap irqCap
Grant the right to set domains.
> provideCap DomainCap
Set up the VSpace. After this it is no longer safe to create new VSpace mappings (as this function may have searched the root CNode for mapped pages, and copied the mappings to a separate VSpace structure).
> initVSpace rootCNSlot rootVNSlot
Insert the CSpace and VSpace roots in the initial TCB, and set its IPC buffer pointer and priority.
> doKernelOp $ do
> threadCRoot <- getThreadCSpaceRoot (capTCBPtr tcbCap)
> cteInsert rootCNCap rootCNSlot threadCRoot
> threadVRoot <- getThreadVSpaceRoot (capTCBPtr tcbCap)
> rootVNCap <- getSlotCap rootVNSlot
> cteInsert rootVNCap rootVNSlot threadVRoot
> threadSet (\t -> t { tcbIPCBuffer = bufferPtr })
> (capTCBPtr tcbCap)
> threadBuffer <- getThreadBufferSlot (capTCBPtr tcbCap)
> bufferCap <- getSlotCap bufferSlot
> bufferCap' <- nullCapOnFailure $ deriveCap bufferSlot bufferCap
> cteInsert bufferCap' bufferSlot threadBuffer
> setPriority (capTCBPtr tcbCap) maxPriority
Configure and set the idle thread.
> configureIdleThread (capTCBPtr idleCap)
> doKernelOp $ setIdleThread (capTCBPtr idleCap)
The task now has its six initial capabilities: null, initial TCB, initial CSpace and VSpace roots, reply endpoint, and interrupt controller, in that order. There may also be additional architecture-specific capabilities created during "initVSpace". Create a boot region to point at them.
> firstFreeSlot <- liftM (fst . head) $ gets initFreeSlotsL2
> provideRegion $ BootRegion (CPtr 0) (firstFreeSlot - 1) BRInitCaps 0
> return tcbCap
\subsubsection{Large Untyped Objects}
The large untyped objects are created from any physical memory that remains above the small block area, which generally occupies the first 1MB. This function may be called multiple times if the physical memory is not contiguous.
> createUntypedCaps :: KernelInit ()
> createUntypedCaps = do
> freeRegions <- getUntypedRegions
> modify (\st -> st { initFreeMemory = [], initBootMemory = [] })
> let blocks = concat (map (uncurry makeBlockList) freeRegions)
> mapM_ storeLargeBlock blocks
> storeLargeBlock :: (PAddr, Int) -> KernelInit ()
> storeLargeBlock (addr, bits) = do
> let ptr = ptrFromPAddr addr
> (cptr, _) <- provideCap (UntypedCap ptr bits 0)
> addRegionWithMerge (BootRegion cptr cptr BRLargeBlocks (bit bits)) bits
Given the base and top addresses of a contiguous region of unallocated memory, this function generates a list of size-aligned blocks of memory.
> makeBlockList :: PAddr -> PAddr -> [(PAddr, Int)]
> makeBlockList s e = returnVal result
> where
> n = finiteBitSize s
> sizes = [0 .. n - 1]
> makeLowBlock ((start, end), xs, ys) b =
> if start `testBit` b && start <= end
> then ((start + bit b, end), (start, b) : xs, ys)
> else ((start, end), xs, ys)
> makeHighBlock ((start, end), xs, ys) b =
> if (end + 1) `testBit` b && start <= end
> then ((start, end - bit b), xs, (end - bit b + 1, b) : ys)
> else ((start, end), xs, ys)
> makeBlocks v b = makeLowBlock (makeHighBlock v b) b
> result = foldl makeBlocks ((s, e), [], []) sizes
> returnVal (_, low, high) = reverse high ++ reverse low
In order to reserve enough capability slots for the initial free slots and the untyped object capabilities, the number of untyped capabilities that will be generated must be predicted. If the result is too large, then more slots will be allocated before calling "createUntypedCaps".
> countUntypedCaps :: KernelInit Int
> countUntypedCaps = do
> freeRegions <- getUntypedRegions
> return $ sum $ map (\(b,t) -> length (makeBlockList b t)) freeRegions
The available untyped regions include all free memory, and also all kernel memory that is used by the bootstrapping code. The latter cannot be allocated during kernel initialisation, but is usable by user-level code once the system has started.
> getUntypedRegions :: KernelInit [(PAddr, PAddr)]
> getUntypedRegions = gets (\st -> initFreeMemory st ++ initBootMemory st)
\subsubsection{Device Capabilities}
For each memory-mapped device in the system, the kernel provides the necessary capabilities to access the device's memory region, and creates a boot region structure pointing at those capabilities. The boot region's data word contains the base address and size of the device region, to allow user level device drivers to identify the devices (based on some platform-specific memory layout, or addresses provided by other devices).
> createDeviceCaps :: KernelInit ()
> createDeviceCaps = do
> devices <- doKernelOp $ doMachineOp getDeviceRegions
> forM_ devices $ \(base, end) -> do
> cap <- doKernelOp $ createDeviceCap (base, end)
> (cptr,_) <- provideCap cap
> let rawsize = end - base
> let sz = find (\sz -> rawsize == bit (pageBitsForSize sz))
> [minBound .. maxBound]
> size <- case sz of
> Just size -> return $ pageBitsForSize size
> Nothing -> fail "Couldn't find appropriate size for device"
> provideRegion $ BootRegion cptr cptr BRDeviceCaps
> (fromIntegral base .|. fromIntegral size)
\subsubsection{Small Untyped Objects}
A small fixed number of page-sized untyped objects is created from the free memory left over after kernel initialisation. These are intended for use by the initial task during bootstrapping.
> createSmallBlockCaps :: KernelInit ()
> createSmallBlockCaps = do
> caps <- replicateM minSmallBlocks $ do
> frame <- liftM ptrFromPAddr allocFrame
> return $ UntypedCap frame pageBits 0
> storeSmallBlockCaps caps
> storeSmallBlockCaps :: [Capability] -> KernelInit ()
> storeSmallBlockCaps = mapM_ storeSmallBlockCap
> storeSmallBlockCap :: Capability -> KernelInit ()
> storeSmallBlockCap cap = do
> (cptr, _) <- provideCap cap
> let dWord = fromIntegral pageBits
> provideRegion $ BootRegion cptr cptr BRSmallBlocks dWord
\subsubsection{Free Slots}
After all of the initial capabilities have been created, there are some free slots left over. Boot regions are created for these free slots, to inform the user of their location. There must be a minimal number of free slots available, to allow the initial thread to bootstrap its capability management.
> createFreeSlotRegions :: KernelInit ()
> createFreeSlotRegions = do
> slots <- gets initFreeSlotsL2
> modify (\st -> st { initFreeSlotsL2 = [] })
> assert (length slots >= minFreeSlots) $
> "There are " ++ show (length slots) ++
> " slots remaining, but there must be at least " ++ show minFreeSlots
> let ranges = rangesBy (\a b -> a == b - 1) $ sort $ map fst slots
> mapM_ (\slots -> provideRegion $
> BootRegion (head slots) (last slots) BRFreeSlots 0
> ) ranges
\subsubsection{Empty Regions}
Any regions of the capability space that are not allocated to the initial thread are marked as empty regions. This includes any unallocated slots in the root CNode, and the remainder of the valid address space.
> createEmptyRegions :: KernelInit ()
> createEmptyRegions = do
> let l1size = bit (pageBits + rootCNodeSize)
> slots <- gets initFreeSlotsL1
> modify (\st -> st { initFreeSlotsL1 = [] })
> let pageSize = 1 `shiftL` pageBits
> let ranges = rangesBy (\a b -> a + pageSize == b) $ sort $ map fst slots
> mapM_ (\slots -> provideRegion $
> BootRegion (head slots) (last slots + pageSize - 1) BREmpty 0
> ) ranges
> provideRegion $ BootRegion l1size maxBound BREmpty 0
> provideCap :: Capability -> Capability -> KernelInit ()
> provideCap rootCNodeCap cap = do
> currSlot <- gets initSlotPosCur
> maxSlot <- gets initSlotPosMax
> when (currSlot >= maxSlot) $ throwError InitFailure
> slot <- doKernelOp $ locateSlot (capCNodePtr rootCNodeCap) currSlot
> doKernelOp $ insertInitCap slot cap
> modify (\st -> st { initSlotPosCur = currSlot + 1 })
> provideUntypedCap :: Capability -> PAddr -> Word8 -> Word -> KernelInit ()
> provideUntypedCap rootCNodeCap pptr sizeBits slotPosBefore = do
> currSlot <- gets initSlotPosCur
> let i = currSlot - slotPosBefore
> untypedObjs <- gets (bifUntypedObjPAddrs . initBootInfo)
> assert (length untypedObjs == fromIntegral i) "Untyped Object List is inconsistent"
> untypedObjs' <- gets (bifUntypedObjSizeBits . initBootInfo)
> assert (length untypedObjs' == fromIntegral i) "Untyped Object List is inconsistent"
> bootInfo <- gets initBootInfo
> let bootInfo' = bootInfo { bifUntypedObjPAddrs = untypedObjs ++ [pptr],
> bifUntypedObjSizeBits = untypedObjs' ++ [sizeBits] }
> modify (\st -> st { initBootInfo = bootInfo' })
> syncBIFrame
> provideCap rootCNodeCap $ UntypedCap {
> capPtr = ptrFromPAddr pptr,
> capBlockSize = fromIntegral sizeBits,
> capFreeIndex = 0 }
\subsection{Helper Functions}
Various functions in this module use "rangesBy" to split a sorted list into contiguous ranges, given a function that determines whether two adjacent items are contiguous. This is similar to "Data.List.groupBy", but does not assume that the comparison function "adj" is transitive; instead, the comparison function's arguments are always adjacent items in the input list.
@ -688,11 +371,18 @@ Various functions in this module use "rangesBy" to split a sorted list into cont
> where
> r = rangesBy adj (y:xs)
> coverOf :: [Region] -> Region
> coverOf [] = Region (0xffffffff,0)
> coverOf [x] = x
> coverOf (x:xs) = Region (ln, hn)
> where
> (l,h) = fromRegion x;
> (ll,hh) = fromRegion $ coverOf xs;
> ln = if l <= ll then l else ll;
> hn = if h <= hh then hh else h
> distinct :: Eq a => [a] -> Bool
> distinct [] = True
> distinct (x:xs) = (notElem x xs && distinct xs)
> isAligned :: (Num a, Bits a) => a -> Int -> Bool
> isAligned x n = x .&. mask n == 0

47
haskell/src/SEL4/Kernel/VSpace.lhs
View File

@ -31,6 +31,7 @@ We use the C preprocessor to select a target architecture.
> import SEL4.Model
> import SEL4.Object
> import SEL4.API.Failures
> import SEL4.API.Types
> import {-# SOURCE #-} SEL4.Kernel.Init
\end{impdetails}
@ -48,12 +49,42 @@ This module defines architecture-specific virtual memory management procedures.
\item preparing the virtual memory environment, if any, that the kernel requires to run;
> initKernelVM :: Kernel ()
> initKernelVM = Arch.initKernelVM
> initKernelVM = Arch.mapKernelWindow
\item creating the initial address space, given the slot containing the root CSpace capability and an empty slot in which the root VSpace capability should be placed;
> initPlatform :: Kernel ()
> initPlatform = do
> doMachineOp $ configureTimer
> initL2Cache
> initL2Cache = return ()
> initCPU :: Kernel ()
> initCPU = Arch.activateGlobalPD
> createIPCBufferFrame :: Capability -> VPtr -> KernelInit Capability
> createIPCBufferFrame = Arch.createIPCBufferFrame
> createBIFrame = Arch.createBIFrame
> createFramesOfRegion :: Capability -> Region -> Bool -> VPtr -> KernelInit ()
> createFramesOfRegion = Arch.createFramesOfRegion
> createITPDPTs :: Capability -> VPtr -> VPtr -> KernelInit Capability
> createITPDPTs = Arch.createITPDPTs
> writeITPDPTs :: Capability -> Capability -> KernelInit ()
> writeITPDPTs = Arch.writeITPDPTs
> createITASIDPool :: Capability -> KernelInit Capability
> createITASIDPool = Arch.createITASIDPool
> writeITASIDPool :: Capability -> Capability -> Kernel ()
> writeITASIDPool = Arch.writeITASIDPool
> createDeviceFrames :: Capability -> KernelInit ()
> createDeviceFrames = Arch.createDeviceFrames
> initVSpace :: PPtr CTE -> PPtr CTE -> KernelInit ()
> initVSpace = Arch.initVSpace
\item handling virtual memory faults, given the current thread, the faulting address, and a boolean value that is true for write accesses;
@ -75,13 +106,5 @@ This module defines architecture-specific virtual memory management procedures.
> lookupIPCBuffer :: Bool -> PPtr TCB -> Kernel (Maybe (PPtr Word))
> lookupIPCBuffer = Arch.lookupIPCBuffer
\item and creating new capabilities to virtual memory pages and devices mapped by the bootstrap code.
> createInitPage :: PAddr -> Kernel Capability
> createInitPage = Arch.createInitPage
>
> createDeviceCap :: (PAddr, PAddr) -> Kernel Capability
> createDeviceCap = Arch.createDeviceCap
\end{itemize}

559
haskell/src/SEL4/Kernel/VSpace/ARM.lhs
View File

@ -23,6 +23,7 @@ This module defines the handling of the ARM hardware-defined page tables.
> import SEL4.Model.StateData.ARM
> import SEL4.Object.Instances()
> import SEL4.API.Invocation
> import SEL4.Kernel.BootInfo
> import {-# SOURCE #-} SEL4.Object.CNode
> import {-# SOURCE #-} SEL4.Object.TCB
> import {-# SOURCE #-} SEL4.Kernel.Init
@ -32,6 +33,7 @@ This module defines the handling of the ARM hardware-defined page tables.
> import Data.Maybe
> import Data.List
> import Data.Array
> import Data.Word(Word32)
\end{impdetails}
@ -64,72 +66,47 @@ The idle thread executes a short loop that drains the CPU's write buffer and the
> , 0xeafffffc -- b 1b
> ]
The "initKernelVM" function is called at the beginning of the kernel's bootstrap sequence. It initialises the kernel's global page directory and page table, and sets it as the active page table. This assumes that the MMU is either disabled, or enabled with the kernel mapped at the same addresses it will use while running.
\subsection{Creating the vspace for the initial thread}
> initKernelVM :: Kernel ()
> initKernelVM = do
> createGlobalPD
> allMemory <- doMachineOp getMemoryRegions
> mapM_ mapKernelRegion allMemory
> kernelDevices <- doMachineOp getKernelDevices
> mapM_ mapKernelDevice kernelDevices
> createGlobalsFrame
> mapGlobalsFrame
> activateGlobalPD
Function mapKernelWindow will create a virtialll address space for the initial thread
The "initVSpace" function creates and populates the initial task's VSpace structures. Page-sized initial mappings are copied from the initial task's CSpace.
> mapKernelWindow :: Kernel ()
> mapKernelWindow = do
> initVSpace :: PPtr CTE -> PPtr CTE -> KernelInit ()
> initVSpace cRootSlot vRootSlot = do
An abstract version looks like:
Because the kernel reserves all virtual addresses above "kernelBase" for its own use, it specifies this region as a "BRCapsOnly" region; that is, user tasks may use it for capabilities, but not for virtual memory mappings.
allMemory <- doMachineOp getMemoryRegions
mapM_ mapKernelRegion allMemory
> provideRegion $ BootRegion
> (CPtr $ fromVPtr kernelBase) maxBound BRCapsOnly 0
However we assume that the result of getMemoryRegions is actually [0,1<<24] and do the following
Create and populate the initial task's virtual address space.
> vRoot <- createInitialRoot vRootSlot
> cRoot <- doKernelOp $ getSlotCap cRootSlot
> populateInitialRoot vRoot cRoot
>
> doKernelOp $ doMachineOp cleanCaches_PoU
The global PD contains all of the kernel mappings, including direct-mapped physical memory, IO mappings for the timer and interrupt controller, the trap vectors, and the user-accessible globals frame. The global PTs are also initialised at this point.
> createGlobalPD :: Kernel ()
> createGlobalPD = do
> globalPD <- gets $ armKSGlobalPD . ksArchState
> deleteObjects (PPtr $ fromPPtr globalPD) pdBits
> placeNewObject (PPtr $ fromPPtr globalPD) (makeObject :: PDE)
> (pdBits `shiftR` (objBits (makeObject :: PDE)))
> globalPTs <- gets $ armKSGlobalPTs . ksArchState
> deleteObjects (PPtr $ fromPPtr $ head globalPTs) pageBits
> placeNewObject (PPtr $ fromPPtr $ head globalPTs) (makeObject :: PTE)
> (pageBits `shiftR` (objBits (makeObject :: PTE)))
> return ()
> activateGlobalPD :: Kernel ()
> activateGlobalPD = do
> doMachineOp cleanCaches_PoU
> globalPD <- gets $ armKSGlobalPD . ksArchState
> doMachineOp $ do
> setCurrentPD $ addrFromPPtr globalPD
> invalidateTLB
The kernel creates mappings for all physical memory regions in the global page directory before switching to it. This implementation requires each region to be at least one 1MB section in size.
> mapKernelRegion :: (PAddr, PAddr) -> Kernel ()
> mapKernelRegion (phys, physEnd) = do
> let size = physEnd - phys
> let vbase = kernelBase `shiftR` pageBitsForSize (ARMSection)
> let pdeBits = objBits (undefined :: PDE)
> assert (size >= bit (pageBitsForSize ARMSection))
> "Kernel regions must be at least 1MB"
> let pteBits = objBits (undefined :: PTE)
> let ptSize = ptBits - pteBits
> let pdSize = pdBits - pdeBits
> globalPD <- gets $ armKSGlobalPD . ksArchState
> if (size < bit (pageBitsForSize ARMSuperSection))
> then forM_ [phys, phys + bit (pageBitsForSize ARMSection) ..
> phys + size - 1] $ \phys -> do
> let virt = VPtr $ fromPPtr $ ptrFromPAddr phys
> globalPTs <- gets $ armKSGlobalPTs . ksArchState
> deleteObjects (PPtr $ fromPPtr globalPD) pdBits
> placeNewObject (PPtr $ fromPPtr globalPD) (makeObject :: PDE) pdSize
> forM_ [vbase, vbase+16 .. (bit pageBits) - 16 - 1] $ \v -> do
> let offset = fromVPtr v
> let virt = v `shiftL` pageBitsForSize (ARMSection)
> let phys = addrFromPPtr $ PPtr $ fromVPtr virt
> let pde = SuperSectionPDE {
> pdeFrame = phys,
> pdeParity = True,
> pdeCacheable = True,
> pdeGlobal = True,
> pdeExecuteNever = False,
> pdeRights = VMKernelOnly }
> let slots = map (\n -> globalPD + PPtr (n `shiftL` pdeBits))
> [offset .. offset + 15]
> (flip $ mapM_ ) slots (\slot -> storePDE slot pde)
> forM_ [(bit pageBits) - 16, (bit pageBits) - 2] $ \v -> do
> let offset = fromVPtr v
> let virt = v `shiftL` pageBitsForSize (ARMSection)
> let phys = addrFromPPtr $ PPtr $ fromVPtr virt
> let pde = SectionPDE {
> pdeFrame = phys,
> pdeParity = True,
@ -138,212 +115,297 @@ The kernel creates mappings for all physical memory regions in the global page d
> pdeGlobal = True,
> pdeExecuteNever = False,
> pdeRights = VMKernelOnly }
> let offset = fromVPtr virt `shiftR` pageBitsForSize ARMSection
> let slot = globalPD + PPtr (offset `shiftL` pdeBits)
> storePDE slot pde
> else forM_ [phys, phys + bit (pageBitsForSize ARMSuperSection) ..
> phys + size - 1] $ \phys -> do
> let virt = VPtr $ fromPPtr $ ptrFromPAddr phys
> let pde = SuperSectionPDE {
> pdeFrame = phys,
> pdeParity = True,
> pdeCacheable = True,
> pdeGlobal = True,
> pdeExecuteNever = False,
> pdeRights = VMKernelOnly }
> let offset = fromVPtr virt `shiftR` pageBitsForSize ARMSection
> let slots = map (\n -> globalPD + PPtr (n `shiftL` pdeBits))
> [offset .. offset + 15]
> mapM_ (flip storePDE pde) slots
> let paddr = addrFromPPtr $ PPtr $ fromPPtr $ head globalPTs
> let pde = PageTablePDE {pdeTable = paddr ,pdeParity = True, pdeDomain = 0}
> let slot = globalPD + PPtr (((bit pageBits) - 1) `shiftL` pdeBits)
> deleteObjects (PPtr $ fromPPtr $ head globalPTs) ptBits
> placeNewObject (PPtr $ fromPPtr $ head globalPTs) (makeObject :: PTE) ptSize
> storePDE slot pde
The "mapKernelFrame" helper function is used when mapping the globals frame, kernel IO devices, and the trap frame.
In c-code we need to Detype the armGlobalPagetTable which is c-equvilance to memzero(armKSGlobalPT,1 << PT_SIZE_BITS)
> mapKernelFrame :: PAddr -> VPtr -> VMRights -> VMAttributes -> Kernel ()
> mapKernelFrame paddr vptr rights attributes = do
> assert (vptr >= kernelBase) "mapKernelFrame: must be in kernel area"
> pd <- gets $ armKSGlobalPD . ksArchState
> let pdSlot = lookupPDSlot pd vptr
> pde <- getObject pdSlot
> let pteBits = objBits (undefined :: PTE)
> let ptIndex = fromVPtr $ vptr `shiftR` 12 .&. 0xff
> ptSlot <- case pde of
> PageTablePDE {} -> do
> let pt = ptrFromPAddr $ pdeTable pde
> return $ pt + (PPtr $ ptIndex `shiftL` pteBits)
> InvalidPDE {} -> do
> ptFrame <- allocKernelPT
> let pde = PageTablePDE {
> pdeTable = addrFromPPtr ptFrame,
> pdeParity = True,
> pdeDomain = 0 }
> storePDE pdSlot pde
> return $ PPtr $ fromPPtr ptFrame + (ptIndex `shiftL` pteBits)
> _ -> fail "mapKernelFrame: section already mapped"
> pte <- getObject ptSlot
> case pte of
> InvalidPTE {} -> do
> let pte' = SmallPagePTE {
> pteFrame = paddr,
> pteCacheable = armPageCacheable attributes,
> pteGlobal = True,
> pteExecuteNever = False,
> pteRights = rights }
> storePTE ptSlot pte'
> _ -> fail "mapKernelFrame: frame already mapped"
FIX ME: We might still need to map vector table
The "allocKernelPT" helper function is used when "mapKernelFrame" needs to allocate a new page table. It returns a table taken from from a small statically-allocated pool.
> mapGlobalsFrame
> kernelDevices <- doMachineOp getKernelDevices
> mapM_ mapKernelDevice kernelDevices
> allocKernelPT :: Kernel (PPtr PTE)
> allocKernelPT = do
> pts <- gets $ armKSGlobalPTs . ksArchState
> case pts of
> [] -> fail "mapKernelFrame: no more global PTs"
> (pt:pts') -> do
> modify (\ks -> ks {
> ksArchState = (ksArchState ks) { armKSGlobalPTs = pts' } })
> return pt
Any IO devices used directly by the kernel --- generally including the interrupt controller, one of the timer devices, and optionally a serial port for debugging --- must be mapped in the global address space. This implementation limits device mappings to one page; it may need to be extended to support multiple-page mappings.
> mapKernelDevice :: (PAddr, PPtr Word) -> Kernel ()
> mapKernelDevice (addr, ptr) = do
> let vptr = VPtr $ fromPPtr ptr
> mapKernelFrame addr vptr VMKernelOnly $ VMAttributes False False False
> mapKernelFrame addr vptr VMKernelOnly $ VMAttributes False False True
The globals frame is a user-readable frame mapped at a well-known location, "globalsBase", in the kernel's virtual memory region.
> createGlobalsFrame :: Kernel ()
> createGlobalsFrame = do
> globals <- gets $ armKSGlobalsFrame . ksArchState
> deleteObjects (PPtr $ fromPPtr globals) pageBits
> reserveFrame (PPtr $ fromPPtr globals) True
> let offset = fromVPtr $ idleThreadStart - globalsBase
> doMachineOp $ zipWithM_ storeWord
> [globals + PPtr offset, globals + PPtr offset + 4 ..]
> idleThreadCode
> activateGlobalPD :: Kernel ()
> activateGlobalPD = do
> globalPD <- gets $ armKSGlobalPD . ksArchState
> doMachineOp $ do
> setCurrentPD $ addrFromPPtr globalPD
> invalidateTLB
Insert an entry into the global PD for the globals frame.
Function pair "createITPDPTs" + "writeITPDPTs" init the memory space for the initial thread
> createITPDPTs :: Capability -> VPtr -> VPtr -> KernelInit Capability
> createITPDPTs rootCNCap vptrStart biFrameVPtr = do
> let pdSize = pdBits - objBits (makeObject :: PDE)
> let ptSize = ptBits - objBits (makeObject :: PTE)
> pdPPtr <- allocRegion pdBits
> doKernelOp $ placeNewObject (ptrFromPAddr pdPPtr) (makeObject::PDE) pdSize -- create a pageDirectory
> pdCap <- return $ ArchObjectCap $ PageDirectoryCap (ptrFromPAddr pdPPtr) (Just itASID)
> slot <- doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapITPD
> doKernelOp $ insertInitCap slot $ pdCap
> slotBefore <- gets $ initSlotPosCur
> let btmVPtr = vptrStart `shiftR` (pdSize + pageBits) `shiftL` (pdSize + pageBits)
> let step = 1 `shiftL` (ptSize + pageBits)
> let topVPtr = biFrameVPtr + (bit biFrameSizeBits) - 1
> forM_ [btmVPtr,btmVPtr + step .. topVPtr] $ \vptr -> do
> ptPPtr <- allocRegion ptBits
> doKernelOp $ placeNewObject (ptrFromPAddr ptPPtr) (makeObject::PTE) ptSize -- create a pageTable
> provideCap rootCNCap $ ArchObjectCap $ PageTableCap (ptrFromPAddr ptPPtr) (Just (itASID, vptr))
> slotAfter <- gets initSlotPosCur
> bootInfo <- gets initBootInfo
> let bootInfo' = bootInfo { bifUIPTCaps = [slotBefore .. slotAfter - 1] }
> modify (\s -> s { initBootInfo = bootInfo' })
> return pdCap
> writeITPDPTs :: Capability -> Capability -> KernelInit ()
> writeITPDPTs rootCNCap pdCap =
> case pdCap of
> ArchObjectCap cap -> do
> doKernelOp $ copyGlobalMappings $ capPDBasePtr cap
> ptSlots <- gets $ bifUIPTCaps . initBootInfo
> doKernelOp $ do
> (flip mapM) ptSlots (\pos-> do
> slot <- locateSlot (capCNodePtr rootCNCap) pos
> cte <- getCTE slot
> mapITPTCap pdCap (cteCap cte)
> )
> frameSlots <- gets $ bifUIFrameCaps . initBootInfo
> doKernelOp $ do
> (flip mapM) frameSlots (\pos -> do
> slot <- locateSlot (capCNodePtr rootCNCap) pos
> cte <- getCTE slot
> mapITFrameCap pdCap (cteCap cte))
> slot <- locateSlot (capCNodePtr rootCNCap) biCapITIPCBuf
> cte <- getCTE slot
> mapITFrameCap pdCap (cteCap cte)
> slot <- locateSlot (capCNodePtr rootCNCap) biCapBIFrame
> cte <- getCTE slot
> mapITFrameCap pdCap (cteCap cte)
> _ -> fail $ (show pdCap) ++ " is not an ArchObjectCap."
Function pair "createITASIDPool" + "writeITASIDPool" init the asidpool cap for the initial thread
> createITASIDPool :: Capability -> KernelInit Capability
> createITASIDPool rootCNCap = do
> apPPtr <- allocRegion $ objBits (undefined :: ASIDPool)
> doKernelOp $ placeNewObject (ptrFromPAddr apPPtr) (makeObject::ASIDPool) 0
> slot <- doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapITASIDPool
> asidPoolCap <- return $ ArchObjectCap $ ASIDPoolCap (ptrFromPAddr apPPtr) 0
> doKernelOp $ insertInitCap slot asidPoolCap
> slot <- doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapASIDControl
> asidControlCap <- return $ ArchObjectCap $ ASIDControlCap
> doKernelOp $ insertInitCap slot asidControlCap
> return asidPoolCap
> writeITASIDPool :: Capability -> Capability -> Kernel ()
> writeITASIDPool apCap pdCap = do
> apPtr <- case apCap of
> ArchObjectCap (ASIDPoolCap ptr _) -> return ptr
> _ -> fail "WrieITASIDPool:should never happen"
> pdPtr <- case pdCap of
> ArchObjectCap (PageDirectoryCap ptr _) -> return ptr
> _ -> fail "WriteITASIDPool:should never happen"
> ASIDPool ap <- getObject apPtr
> let ap' = ap//[(itASID, Just pdPtr)]
> setObject apPtr (ASIDPool ap')
> asidTable <- gets (armKSASIDTable . ksArchState)
> let asidTable' = asidTable//[(asidHighBitsOf itASID, Just apPtr)]
> modify (\s -> s {
> ksArchState = (ksArchState s) { armKSASIDTable = asidTable' }})
>
Function "mapITPTCap" is used to store a pde into the pd of the initial thread
> mapITPTCap :: Capability -> Capability -> Kernel ()
> mapITPTCap pdCap ptCap = do
> pd <- case pdCap of
> ArchObjectCap (PageDirectoryCap ptr _) -> return ptr
> _ -> fail "mapITPTCap:should never happen"
> ptCap' <- case ptCap of
> ArchObjectCap c -> return c
> _ -> fail "mapITPTCap:should never happen"
> (pt,vptr) <- case ptCap' of
> PageTableCap { capPTBasePtr = pt',
> capPTMappedAddress = Just (_, vptr') }
> -> return (pt', vptr')
> _ -> fail $ "mapITPTCap:This shouldn't happen. PageTableCap expected instead of" ++ (show ptCap)
> let offset = fromVPtr $ vptr `shiftR` pageBitsForSize ARMSection
> let targetSlot = pd + (PPtr $ offset `shiftL` 2) -- array entry size
> let pde = PageTablePDE {
> pdeTable = addrFromPPtr pt,
> pdeParity = True,
> pdeDomain = 0 }
> storePDE targetSlot pde
Function "mapITFrameCap" maps pte into pt of the initial thread.
> mapITFrameCap :: Capability -> Capability -> Kernel ()
> mapITFrameCap pdCap frameCap = do
> pd' <- case pdCap of
> ArchObjectCap (PageDirectoryCap ptr _) -> return ptr
> _ -> fail $ "mapITFrameCap: expect PDCap , get:" ++ (show pdCap)
> frameCap' <- case frameCap of
> ArchObjectCap c -> return c
> _ -> fail $ "mapITFrameCap: expect FrameCap, get:" ++ (show frameCap)
> (frame,vptr) <- case frameCap' of
> PageCap { capVPBasePtr = frame',
> capVPMappedAddress = Just (_, vptr') }
> -> return (frame', vptr')
> _ -> fail $ "This shouldn't happen, PageCap expected instead of " ++ (show frameCap)
> let offset = fromVPtr $ vptr `shiftR` pageBitsForSize ARMSection
> let pd = pd' + (PPtr $ offset `shiftL` 2)
> pde <- getObject pd
> pt <- case pde of
> PageTablePDE { pdeTable = ref } -> return $ ptrFromPAddr ref
> _ -> fail $ "This shouldn't happen,expect PageTablePDE at " ++ (show pd) ++ "instead of " ++ (show pde)
> let offset = fromVPtr $ ((vptr .&.(mask $ pageBitsForSize ARMSection))
> `shiftR` pageBitsForSize ARMSmallPage)
> let targetSlot = pt + (PPtr $ offset `shiftL` 2) -- slot size
> let pte = SmallPagePTE {
> pteFrame = addrFromPPtr frame,
> pteCacheable = True,
> pteGlobal = False,
> pteExecuteNever = False,
> pteRights = VMReadWrite }
> storePTE targetSlot pte
Function "createIPCBufferFrame" will create IpcBuffer frame of the initial thread.
The address of this ipcbuffer starts from the end of uiRegion
> createIPCBufferFrame :: Capability -> VPtr -> KernelInit Capability
> createIPCBufferFrame rootCNCap vptr = do
> pptr <- allocFrame
> doKernelOp $ doMachineOp $ clearMemory (ptrFromPAddr pptr) (1 `shiftL` pageBits)
> cap <- createITFrameCap (ptrFromPAddr pptr) vptr (Just itASID) False
> slot <- doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapITIPCBuf
> doKernelOp $ insertInitCap slot cap
> bootInfo <- gets (initBootInfo)
> let bootInfo' = bootInfo { bifIPCBufVPtr = vptr}
> modify (\s -> s {initBootInfo = bootInfo' })
> return cap
Function "createBIFrame" will create the biframe cap for the initial thread
> createBIFrame :: Capability -> VPtr -> Word32 -> Word32 -> KernelInit Capability
> createBIFrame rootCNCap vptr nodeId numNodes = do
> pptr <- allocFrame
> bootInfo <- gets initBootInfo
> let bootInfo' = bootInfo { bifNodeID = nodeId,
> bifNumNodes = numNodes }
> modify (\s -> s {
> initBootInfo = bootInfo',
> initBootInfoFrame = pptr,
> initSlotPosCur = biCapDynStart
> })
> doKernelOp $ doMachineOp $ clearMemory (ptrFromPAddr pptr) (1 `shiftL` pageBits)
> cap <- createITFrameCap (ptrFromPAddr pptr) vptr (Just itASID) False
> slot <- doKernelOp $ locateSlot (capCNodePtr rootCNCap) biCapBIFrame
> doKernelOp $ insertInitCap slot cap
> return cap
> createITFrameCap :: PPtr Word -> VPtr -> Maybe ASID -> Bool -> KernelInit Capability
> createITFrameCap pptr vptr asid large = do
> let sz = if large then ARMLargePage else ARMSmallPage
> let addr = case asid of
> Just asid' -> Just (asid', vptr)
> Nothing -> Nothing
> let frame = PageCap {
> capVPBasePtr = pptr,
> capVPRights = VMReadWrite,
> capVPSize = sz,
> capVPMappedAddress = addr }
> return $ ArchObjectCap $ frame
> createFramesOfRegion :: Capability -> Region -> Bool -> VPtr -> KernelInit ()
> createFramesOfRegion rootCNCap region doMap pvOffset = do
> curSlotPos <- gets initSlotPosCur
> (startPPtr, endPPtr) <- return $ fromRegion region
> forM_ [startPPtr,startPPtr + (bit pageBits) .. endPPtr] $ \ptr -> do
> let paddr = fromPAddr $ addrFromPPtr ptr
> frameCap <- if doMap then
> createITFrameCap ptr ((VPtr paddr) + pvOffset ) (Just itASID) False
> else createITFrameCap ptr 0 Nothing False
> provideCap rootCNCap frameCap
> slotPosAfter <- gets initSlotPosCur
> bootInfo <- gets initBootInfo
> let bootInfo' = bootInfo { bifUIFrameCaps = [curSlotPos .. slotPosAfter - 1] }
> modify (\s -> s { initBootInfo = bootInfo' })
Function "mapGlobalsFrame" inserts an entry into the global PD for the globals frame.
> mapGlobalsFrame :: Kernel ()
> mapGlobalsFrame = do
> globalsFrame <- gets $ armKSGlobalsFrame . ksArchState
> mapKernelFrame (addrFromPPtr globalsFrame) globalsBase VMReadOnly $
> VMAttributes True True False
> VMAttributes True True True
Create the initial thread's page directory and allocate an ASID for it. Returns the page directory capability, which it also stores in the given slot.
> createInitialRoot :: PPtr CTE -> KernelInit Capability
> createInitialRoot slot = do
> let asid = 1
> initPDFrame <- allocRegion pdBits
> let initPD = ptrFromPAddr initPDFrame
> let rootCap = ArchObjectCap $ PageDirectoryCap {
> capPDBasePtr = initPD,
> capPDMappedASID = Just asid }
> doKernelOp $ do
> placeNewObject (ptrFromPAddr initPDFrame) (makeObject :: PDE)
> (pdBits `shiftR` (objBits (makeObject :: PDE)))
> copyGlobalMappings initPD
> insertInitCap slot rootCap
>
> initASIDPoolFrame <- allocRegion $ objBits (undefined :: ASIDPool)
> let initASIDPoolPtr = ptrFromPAddr initASIDPoolFrame
> let ASIDPool emptyASIDPool = (makeObject :: ASIDPool)
> let initASIDPool = ASIDPool $ emptyASIDPool//[(asid .&. mask asidLowBits, Just initPD)]
> doKernelOp $ do
> placeNewObject (ptrFromPAddr initASIDPoolFrame) initASIDPool 0
> asidTable <- gets (armKSASIDTable . ksArchState)
> let asidTable' =
> asidTable//[(asidHighBitsOf asid, Just initASIDPoolPtr)]
> modify (\s -> s {
> ksArchState = (ksArchState s) { armKSASIDTable = asidTable' }})
> provideCap $ ArchObjectCap $ ASIDControlCap
> provideCap $ ArchObjectCap $ ASIDPoolCap {
> capASIDPool = initASIDPoolPtr,
> capASIDBase = 0 }
>
> return rootCap
The "mapKernelFrame" helper function is used when mapping the globals frame, kernel IO devices, and the trap frame. We simply store pte into our globalPT
Map all of the frame capabilities in the initial capability space into the virtual address space.
> mapKernelFrame :: PAddr -> VPtr -> VMRights -> VMAttributes -> Kernel ()
> mapKernelFrame paddr vaddr vmrights attributes = do
> let idx = fromVPtr $ (vaddr .&. (mask $ pageBitsForSize ARMSection)
> `shiftR` pageBitsForSize ARMSmallPage)
> globalPT <- getARMGlobalPT
> let pte = SmallPagePTE {
> pteFrame = paddr,
> pteCacheable = armPageCacheable attributes,
> pteGlobal = True,
> pteExecuteNever = False,
> pteRights = vmrights }
> let base = PPtr $ fromPPtr globalPT
> storePTE (PPtr ((fromPPtr globalPT) + (idx `shiftL` 2))) pte
> populateInitialRoot :: Capability -> Capability -> KernelInit ()
> populateInitialRoot vRoot cRoot = do
> let asid = fromJust $ capPDMappedASID $ capCap vRoot
> let ArchObjectCap pdCap = vRoot
> let pd = capPDBasePtr pdCap
> getARMGlobalPT :: Kernel (PPtr PTE)
> getARMGlobalPT = do
> pt <- gets (head . armKSGlobalPTs . ksArchState)
> return pt
The CSpace root should resolve the right number of bits for its slots to cover the same region as the corresponding slots in page tables.
> case cRoot of
> CNodeCap {} -> return ()
> _ -> fail "Initial CSpace cap is not valid"
> assert (capCNodeGuard cRoot == 0) $
> "populateInitialRoot: CSpace root guard must be 0"
> assert (capCNodeBits cRoot + capCNodeGuardSize cRoot + pageBits ==
> finiteBitSize (undefined::Word)) $
> "populateInitialRoot: CSpace region must match page table region"
Any frame capabilities present in the node are mapped into the VSpace.
> forM_ [0 .. 1 `shiftL` capCNodeBits cRoot - 1] $ \index -> do
> cSlot <- doKernelOp $ locateSlot (capCNodePtr cRoot) index
> cte <- doKernelOp $ getObject cSlot
> case cteCap cte of
> ArchObjectCap (pageCap@PageCap {}) -> do
> assert (capVPSize pageCap == ARMSmallPage) $
> "Initial frames must all be small-page sized"
> let vaddr = VPtr $ index `shiftL` pageBits
> let pageCap' = pageCap {
> capVPMappedAddress = Just (asid, vaddr) }
> let cte' = cte { cteCap = ArchObjectCap pageCap' }
> doKernelOp $ setObject cSlot cte'
> mapUserFrame pd asid
> (addrFromPPtr $ capVPBasePtr pageCap) vaddr
> _ -> return ()
> allocUserPT :: ASID -> VPtr -> KernelInit (PPtr PTE)
> allocUserPT asid vaddr = do
> initPTFrame <- allocRegion ptBits
> doKernelOp $ placeNewObject (ptrFromPAddr initPTFrame)
> (makeObject :: PTE) (ptBits `shiftR` (objBits (makeObject :: PTE)))
> let initPT = ptrFromPAddr initPTFrame
> provideCap $ ArchObjectCap $ PageTableCap {
> capPTBasePtr = initPT,
> capPTMappedAddress = Just (asid, vaddr) }
> return initPT
> mapUserFrame :: PPtr PDE -> ASID -> PAddr -> VPtr -> KernelInit ()
> mapUserFrame pd asid paddr vptr = do
> assert (vptr < kernelBase) "mapUserFrame: must not be in kernel area"
> let pdSlot = lookupPDSlot pd vptr
> pde <- doKernelOp $ getObject pdSlot
> let pteBits = objBits (undefined :: PTE)
> let ptIndex = fromVPtr $ vptr `shiftR` 12 .&. 0xff
> ptSlot <- case pde of
> PageTablePDE {} -> do
> let pt = ptrFromPAddr $ pdeTable pde
> return $ pt + (PPtr $ ptIndex `shiftL` pteBits)
> InvalidPDE {} -> do
> ptFrame <- allocUserPT asid vptr
> let pde = PageTablePDE {
> pdeTable = addrFromPPtr ptFrame,
> pdeParity = True,
> pdeDomain = 0 }
> doKernelOp $ storePDE pdSlot pde
> return $ PPtr $ fromPPtr ptFrame + (ptIndex `shiftL` pteBits)
> _ -> fail "mapUserFrame: section already mapped"
> doKernelOp $ do
> pte <- getObject ptSlot
> case pte of
> InvalidPTE {} -> do
> let pte' = SmallPagePTE {
> pteFrame = paddr,
> pteCacheable = True,
> pteGlobal = False,
> pteExecuteNever = False,
> pteRights = VMReadWrite }
> storePTE ptSlot pte'
> _ -> fail "mapUserFrame: frame already mapped"
> createDeviceFrames :: Capability -> KernelInit ()
> createDeviceFrames rootCNodeCap = do
> deviceRegions <- doKernelOp $ doMachineOp getDeviceRegions
> (flip mapM_) deviceRegions (\(start,end) -> do
> frameSize <- return $ if (isAligned start (pageBitsForSize ARMSection))
> && isAligned end (pageBitsForSize ARMSection)
> then ARMSection else ARMSmallPage
> slotBefore <- gets initSlotPosCur
> (flip mapM_) [start, (start + (bit (pageBitsForSize frameSize))) .. (end - 1)]
> (\f -> do
> frameCap <- createITFrameCap (ptrFromPAddr f) 0 Nothing (frameSize == ARMSection)
> provideCap rootCNodeCap frameCap)
> slotAfter <- gets initSlotPosCur
> let biDeviceRegion = BIDeviceRegion {
> bidrBasePAddr = start,
> bidrFrameSizeBits = fromIntegral $ pageBitsForSize frameSize,
> bidrFrameCaps = SlotRegion (slotBefore, slotAfter) }
> devRegions <- gets (bifDeviceRegions . initBootInfo)
> let devRegions' = devRegions ++ [biDeviceRegion]
> bootInfo <- gets (initBootInfo)
> let bootInfo' = bootInfo { bifDeviceRegions = devRegions' }
> modify (\st -> st { initBootInfo = bootInfo' })
> --syncBIFrame
> )
> bInfo <- gets (initBootInfo)
> let bInfo' = bInfo { bifNumDeviceRegions = (fromIntegral . length . bifDeviceRegions) bInfo }
> modify (\st -> st { initBootInfo = bInfo' })
\subsubsection{Creating a New Address Space}
@ -769,25 +831,6 @@ Note that implementations with separate high and low memory regions may also wis
> return ()
> checkValidIPCBuffer _ _ = throw IllegalOperation
The following two functions are used by the bootstrap code to create the initial thread's virtual memory mappings and the system's device capabilities.
> createInitPage :: PAddr -> Kernel Capability
> createInitPage addr = do
> let ptr = ptrFromPAddr addr
> reserveFrame ptr False
> return $ ArchObjectCap $ PageCap ptr VMReadWrite ARMSmallPage Nothing
>
> createDeviceCap :: (PAddr, PAddr) -> Kernel Capability
> createDeviceCap (addr, end) = do
> let wptr = ptrFromPAddr addr
> let rawsize = end - addr
> let sz = find (\sz -> rawsize == bit (pageBitsForSize sz))
> [minBound .. maxBound]
> size <- case sz of
> Just size -> return size
> Nothing -> fail "Couldn't find appropriate size for device"
> return $ ArchObjectCap $ PageCap wptr VMReadWrite size Nothing
ARM memory mappings may be read-only or read-write; on newer revisions of the ARM they may also be marked non-executable. Write-only mappings are not possible.
> maskVMRights :: VMRights -> CapRights -> VMRights

2
haskell/src/SEL4/Machine/Hardware.lhs
View File

@ -55,6 +55,8 @@ Depending on the architecture, real physical addresses may be the same as the ad
> addrFromPPtr :: PPtr a -> PAddr
> addrFromPPtr = Arch.addrFromPPtr
> fromPAddr = Arch.fromPAddr
\subsubsection{Interrupts}
An interrupt request from an external device, or from the CPU's timer, is represented by the type "IRQ".

1
haskell/src/SEL4/Model/Failures.lhs
View File

@ -40,6 +40,7 @@ All four of the failure types must have an instance of the "Error" class to be u
> instance Error Fault
> instance Error SyscallError
> instance Error LookupFailure
> instance Error InitFailure
\subsection{Failure Handling}

6
haskell/src/SEL4/Model/PSpace.lhs
View File

@ -75,7 +75,7 @@ The default definitions are sufficient for most kernel objects. There is one exc
> loadObject :: (Monad m) => Word -> Word -> Maybe Word ->
> KernelObject -> m a
> loadObject ptr ptr' next obj = do
> unless (ptr == ptr') $ fail "no object at address given in pspace"
> unless (ptr == ptr') $ fail $ "no object at address given in pspace,target=" ++ (show ptr) ++",lookup=" ++ (show ptr')
> val <- projectKO obj
> alignCheck ptr (objBits val)
> sizeCheck ptr next (objBits val)
@ -84,7 +84,7 @@ The default definitions are sufficient for most kernel objects. There is one exc
> updateObject :: (Monad m) => a -> KernelObject -> Word ->
> Word -> Maybe Word -> m KernelObject
> updateObject val oldObj ptr ptr' next = do
> unless (ptr == ptr') $ fail "no object at address given in pspace"
> unless (ptr == ptr') $ fail $ "no object at address given in pspace,target=" ++ (show ptr) ++",lookup=" ++ (show ptr')
> liftM (asTypeOf val) $ projectKO oldObj -- for the type error
> alignCheck ptr (objBits val)
> sizeCheck ptr next (objBits val)
@ -230,7 +230,7 @@ No type checks are performed when deleting objects; "deleteObjects" simply delet
> "Object deletion would leave dangling pointers"
> doMachineOp $ freeMemory (PPtr (fromPPtr ptr)) bits
> ps <- gets ksPSpace
> let inRange = (\x -> x .&. (- mask bits) - 1 == fromPPtr ptr)
> let inRange = (\x -> x .&. ((- mask bits) - 1) == fromPPtr ptr)
> let map' = Data.Map.filterWithKey
> (\x _ -> not (inRange x))
> (psMap ps)

8
haskell/src/SEL4/Object/Interrupt.lhs
View File

@ -141,20 +141,22 @@ When the last IRQ handler capability for a given IRQ is deleted, the capability
This function is called during bootstrap to set up the initial state of the interrupt controller. It allocates a frame and converts its contents to capability slots, which are used as a table endpoints that are notified of incoming interrupts. It also sets the global interrupt controller state, which contains a pointer to each slot and a Boolean flag indicating whether a handler capability has been generated for each IRQ. An interrupt controller capability is provided to the initial thread.
> initInterruptController :: KernelInit Capability
> initInterruptController = do
> initInterruptController :: Capability -> Word -> KernelInit Capability
> initInterruptController rootCNCap biCapIRQC= do
> frame <- allocFrame
> doKernelOp $ do
> assert (length [minBound..(maxBound::IRQ)]
> `shiftL` (objBits (makeObject :: CTE)) <= bit pageBits)
> "Interrupt vector slots must fit in one frame"
> placeNewObject (ptrFromPAddr frame) (makeObject :: CTE)
> (bit pageBits `shiftR` objBits (makeObject :: CTE))
> (pageBits - objBits (makeObject :: CTE))
> doMachineOp $ mapM_ (maskInterrupt True) [minBound .. maxBound]
> let irqTable = funArray $ const IRQInactive
> setInterruptState $ InterruptState (ptrFromPAddr frame) irqTable
> timerIRQ <- doMachineOp configureTimer
> setIRQState IRQTimer timerIRQ
> slot <- locateSlot (capCNodePtr rootCNCap) biCapIRQC
> insertInitCap slot IRQControlCap
> return IRQControlCap
\subsubsection{Handling Interrupts}