portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

haskell: make latex document build

Browse source
This commit is contained in:
Gerwin Klein 2015-05-22 15:17:08 +10:00
parent 0b8627b012
commit 2f08fce48b
1 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
haskell/src/SEL4/Kernel/VSpace/ARM.lhs
View file

@ -75,8 +75,10 @@ Function mapKernelWindow will create a virtialll address space for the initial t
An abstract version looks like:
\begin{verbatim}
allMemory <- doMachineOp getMemoryRegions
mapM_ mapKernelRegion allMemory
\end{verbatim}
However we assume that the result of getMemoryRegions is actually [0,1<<24] and do the following
@ -111,9 +113,8 @@ However we assume that the result of getMemoryRegions is actually [0,1<<24] and
> placeNewObject (PPtr $ fromPPtr $ head globalPTs) (makeObject :: PTE) ptSize
> storePDE slot pde
In c-code we need to Detype the armGlobalPagetTable which is c-equvilance to memzero(armKSGlobalPT,1 << PT_SIZE_BITS)
FIXME: We might still need to map vector table
In C code we need to detype the armGlobalPagetTable which is C equivalent to
\verb+memzero(armKSGlobalPT,1 << PT_SIZE_BITS)+
> mapGlobalsFrame
> kernelDevices <- doMachineOp getKernelDevices