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

arm-hyp haskell: addres several FIXMES: 

- dropped InvokePageIO in favour of capVPisIOSpace flag on PageCap
- converted some objBits (undefined :: ...) to pteBits and pdeBits
- added invalid IOPDEs and IOPTEs encoded to 0
- added IOPTEs and IOPDEs to PSpaceStorable
- adjusted asidHighBits to drop one on enabling MMU
This commit is contained in:
Rafal Kolanski 2016-07-05 15:58:38 +10:00 committed by Alejandro Gomez-Londono
parent 298d4ea6fe
commit 884586da3f
8 changed files with 99 additions and 72 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
spec/haskell/src/SEL4/API/Invocation/ARM_HYP.lhs
View File

@ -36,9 +36,7 @@ This module makes use of the GHC extension allowing data types with no construct
There are five ARM-specific object types; however, only four of them may be invoked. These are the page table, page, ASID control, and ASID pool objects.
XXX ARMHYP The distinction between the non-SMMU invocations (internally grouped as ARMMMUInvocation!) and IOPT invocations is arbitrary, mostly to do with the ability to turn these on/off on different architectures. IOSpace can't be invoked on this architecture.
FIXME ARMHYP do we even want InvokePageIO? There is mapPageIO, IO pages can't be remapped, honestly they are frames to begin with (but then aren't the pages in InvokePage?), and they are unmapped in C going through normal unmap ... still want a split? see confusion with the caps and the isIOSpace flag
IO pages are invoked using InvokePage (cap contains a bit indicating it is an IO page).
> data Invocation
> = InvokePageTable PageTableInvocation
@ -52,7 +50,6 @@ FIXME ARMHYP do we even want InvokePageIO? There is mapPageIO, IO pages can't be
#ifdef CONFIG_ARM_SMMU
> | InvokeIOSpace IOSpaceInvocation
> | InvokeIOPageTable IOPageTableInvocation
> | InvokePageIO PageInvocationIO
#endif
> deriving Show

1
spec/haskell/src/SEL4/API/InvocationLabels/ARM_HYP.lhs
View File

@ -22,7 +22,6 @@ This module makes use of the GHC extension allowing data types with no construct
\subsection{ARM-Specific Invocation Labels}
FIXME ARMHYP remind me why IO page tables do not have remap
FIXME ARMHYP ARMPageMapIO is an inconsistant name (but coined by kernel team)
> data ArchInvocationLabel

14
spec/haskell/src/SEL4/Kernel/VSpace/ARM_HYP.lhs
View File

@ -468,7 +468,7 @@ FIXME ARMHYP checks contiguous hint here, but that should be built into the getO
> mapM (flip storePTE InvalidPTE) slots
> doMachineOp $
> cleanCacheRange_PoU (VPtr $ fromPPtr $ (head slots))
> (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined :: PTE)) - 1 ))
> (VPtr $ (fromPPtr (last slots)) + (bit pteBits - 1))
> (addrFromPPtr (head slots))
> ARMSection -> do
> let p = lookupPDSlot pd vptr
@ -484,7 +484,7 @@ FIXME ARMHYP checks contiguous hint here, but that should be built into the getO
> mapM (flip storePDE InvalidPDE) slots
> doMachineOp $
> cleanCacheRange_PoU (VPtr $ fromPPtr $ (head slots))
> (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined :: PDE)) - 1))
> (VPtr $ (fromPPtr (last slots)) + (bit pdeBits - 1))
> (addrFromPPtr (head slots))
> withoutFailure $ flushPage size pd asid vptr
@ -1024,7 +1024,6 @@ FIXME ARMHYP MOVE THESE, they are dispatched via ObjectType/ decodeInvocation an
> decodeARMMMUInvocation label _ _ _ cap@(VCPUCap {}) extraCaps = error "FIXME ARMHYP TODO VCPU"
#ifdef CONFIG_ARM_SMMU
> decodeARMMMUInvocation label _ _ _ cap@(IOSpaceCap {}) extraCaps = error "FIXME ARMHYP TODO IOSpace"
> decodeARMMMUInvocation label _ _ _ cap@(IOPageDirectoryCap {}) extraCaps = error "FIXME ARMHYP IO"
> decodeARMMMUInvocation label _ _ _ cap@(IOPageTableCap {}) extraCaps = error "FIXME ARMHYP IO"
#endif
@ -1082,7 +1081,6 @@ notion of the largest permitted object size, and checks it appropriately.
#ifdef CONFIG_ARM_SMMU
> InvokeIOSpace _ -> error "FIXME ARMHYP TODO IOSpace"
> InvokeIOPageTable _ -> error "FIXME ARMHYP TODO IO"
> InvokePageIO _ -> error "FIXME ARMHYP TODO IO"
#endif
> return $ []
@ -1147,7 +1145,7 @@ the PT/PD is consistent.
> mapM (flip storePTE pte) slots
> doMachineOp $
> cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots)
> (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined::PTE)) - 1))
> (VPtr $ (fromPPtr (last slots)) + (bit pteBits - 1))
> (addrFromPPtr (head slots))
> when tlbFlush $ invalidateTLBByASID asid
> Right (pde, slots) -> do
@ -1155,7 +1153,7 @@ the PT/PD is consistent.
> mapM (flip storePDE pde) slots
> doMachineOp $
> cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots)
> (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined::PDE)) - 1))
> (VPtr $ (fromPPtr (last slots)) + (bit pdeBits - 1))
> (addrFromPPtr (head slots))
> when tlbFlush $ invalidateTLBByASID asid
>
@ -1164,7 +1162,7 @@ the PT/PD is consistent.
> mapM (flip storePTE pte) slots
> doMachineOp $
> cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots)
> (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined::PTE)) - 1))
> (VPtr $ (fromPPtr (last slots)) + (bit pteBits - 1))
> (addrFromPPtr (head slots))
> when tlbFlush $ invalidateTLBByASID asid
>
@ -1173,7 +1171,7 @@ the PT/PD is consistent.
> mapM (flip storePDE pde) slots
> doMachineOp $
> cleanCacheRange_PoU (VPtr $ fromPPtr $ head slots)
> (VPtr $ (fromPPtr (last slots)) + (bit (objBits (undefined::PDE)) - 1))
> (VPtr $ (fromPPtr (last slots)) + (bit pdeBits - 1))
> (addrFromPPtr (head slots))
> when tlbFlush $ invalidateTLBByASID asid
>

43
spec/haskell/src/SEL4/Machine/Hardware/ARM_HYP.lhs
View File

@ -71,7 +71,7 @@ ARM virtual memory faults are handled by one of two trap handlers: one for data
> = ARMDataAbort
> | ARMPrefetchAbort
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
> | ARMVCPUFault Word -- FIXME ARMHYP do we care about hsr for VCPU fault? hsr gets passed in from the asm code in the exception handler, there's no way to get it after
> | ARMVCPUFault { vcpuFaultHSR :: Word }
> | ARMVGICMaintenanceFault -- FIXME ARMHYP do we want any parameters?
#endif
> deriving Show
@ -542,12 +542,12 @@ hardware can be configured to omit the first level entirely if all second
levels are stored contiguously. We use this configuration to preserve the usual
page table/directory nomenclature.
> -- FIXME ARMHYP what about stored_hw_asid? XN? AF? SH? HAP? MemAttr? TEX? etc?
> -- FIXME ARMHYP global (SH) is never used so I don't know what a global page's SH would look like
> -- FIXME ARMHYP what happened to parity and domain?
seL4 does not use hardware domains or parity on ARM hypervisor systems.
> data PDE
> = InvalidPDE -- FIXME ARMHYP where is stored_hw_asid?
> = InvalidPDE
> | PageTablePDE {
> pdeTable :: PAddr }
> | SectionPDE {
@ -635,6 +635,8 @@ FIXME ARMHYP ask somebody what the most convenient refinement would be
> data VMAttributes = VMAttributes {
> armPageCacheable, armParityEnabled, armExecuteNever :: Bool }
Convenient references to size and log of size of PDEs and PTEs.
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
With hypervisor extensions enabled, page table and page directory entries occupy
@ -649,20 +651,21 @@ With hypervisor extensions enabled, page table and page directory entries occupy
#else /* CONFIG_ARM_HYPERVISOR_SUPPORT */
ARM page directories and page tables occupy four frames and one quarter of a frame, respectively.
FIXME ARMHYP define pteBits and pdeBits in terms of objBits of the right kind of object
FIXME ARMHYP in C, we might want to call them PD\_INDEX\_BITS instead of PD\_BITS - tell Adrian
FIXME ARMHYP in C, rename in progress such that PD\_INDEX\_BITS is used instead of PD\_BITS
> pteBits = (2 :: Int)
> pdeBits = (2 :: Int)
> pdBits = (12 :: Int) + pdeBits
> ptBits = (8 :: Int) + pteBits
FIXME ARMHYP this is a bit silly: in the C code we have pdBits be 12 and ptBits 8,
not the size of the whole thing. In fact, in the haskell we often have to shift pdBits right by the size of the PDE, which get by calling objBits on a new PDE...
FIXME ARMHYP therefore pdeBits and pteBits are not used much outside of here
#endif /* CONFIG_ARM_HYPERVISOR_SUPPORT */
> pteSize :: Int
> pteSize = bit pteBits
> pdeSize :: Int
> pdeSize = bit pdeBits
> cacheLineBits = Platform.cacheLineBits
> cacheLine = Platform.cacheLine
@ -674,12 +677,12 @@ FIXME ARMHYP therefore pdeBits and pteBits are not used much outside of here
> ioptBits = pageBits
FIXME ARMHYP this is really platform code (TK1), move there
FIXME ARMHYP this is so very very verbose, but there is no way to know if we will care about the differences between a page table IOPDE entry and a 4M section one.
FIXME ARMHYP TODO we want to have invalid PDE and PTEs
Note that InvalidIOPDE and InvalidPTE do not exist in C, as there is no valid bit. What actually happens is that a non-read, non-write entry is considered invalid. In pracice, the kernel writes an IOPTE/IOPDE of all zeros here.
> data IOPDE -- FIXME ARMHYP where is InvalidIOPDE?
> = PageTableIOPDE {
> data IOPDE
> = InvalidIOPDE
> | PageTableIOPDE {
> iopdeFrame :: PAddr,
> iopdeRead :: Bool,
> iopdeWrite :: Bool,
@ -691,7 +694,13 @@ FIXME ARMHYP TODO we want to have invalid PDE and PTEs
> iopdeNonsecure :: Bool }
> deriving (Show, Eq)
> iopteBits = 2 :: Int
> iopdeBits = 2 :: Int
> iopteSize = bit iopteBits :: Int
> iopdeSize = bit iopdeBits :: Int
> wordFromIOPDE :: IOPDE -> Word
> wordFromIOPDE InvalidIOPDE = 0
> wordFromIOPDE (PageTableIOPDE addr r w ns) = bit 28 .|.
> ((fromIntegral addr .&. 0xfffffc00) `shiftR` 10) .|.
> (if r then bit 31 else 0) .|.
@ -703,8 +712,9 @@ FIXME ARMHYP TODO we want to have invalid PDE and PTEs
> (if w then bit 30 else 0) .|.
> (if ns then bit 29 else 0)
> data IOPTE -- FIXME ARMHYP where is InvalidIOPTE
> = PageIOPTE {
> data IOPTE
> = InvalidIOPTE
> | PageIOPTE {
> iopteFrame :: PAddr,
> iopteRead :: Bool,
> iopteWrite :: Bool,
@ -712,6 +722,7 @@ FIXME ARMHYP TODO we want to have invalid PDE and PTEs
> deriving (Show, Eq)
> wordFromIOPTE :: IOPTE -> Word
> wordFromIOPTE InvalidIOPTE = 0
> wordFromIOPTE (PageIOPTE addr r w ns) = 0 .|.
> ((fromIntegral addr .&. 0xfffff000) `shiftR` 12) .|.
> (if r then bit 31 else 0) .|.

10
spec/haskell/src/SEL4/Model/StateData/ARM_HYP.lhs
View File

@ -48,14 +48,16 @@ There are three ARM-specific global data elements:
\item the global page directory, which is copied to initialise new page directories, and also as the hardware page table root when the current thread has no valid root.
\end{itemize}
FIXME ARMHYP there is no sign of armKSASIDMap - what is it??
it is the representation in ghost state of storing hwasids into the last invalid entry of a PD
seL4 stores the hardware ASID into the last (invalid) entry of a page
directory, which the user cannot map. This allows fast changes to hardware
ASIDs for a given address space. To represent this, we use a ghost state
armKSASIDMap to map from page directories to hardware ASIDs.
FIXME ARMHYP there is no sign of armKSKernelVSpace - ghost state
FIXME ARMHYP has no global PD and PTs, but the more complicated stage 1 translation for its own address space set up at boot time and then never used again ... it is unclear if we should model this at this time... see arm/32/model/statedata.c ... it is only set up during kernel boot. ARM_HYP doesn't really have a global PD that gets copied everywhere
FIXME ARMHYP missing IO ASID to PD map for SMMU (not yet in C)
FIXME ARMHYP where are SMMU globals if any?
FIXME ARMHYP ksCurCPU will be renamed
> data KernelState = ARMKernelState {
> armKSGlobalsFrame :: PPtr Word,

29
spec/haskell/src/SEL4/Object/Instances/ARM_HYP.lhs
View File

@ -8,6 +8,12 @@
% @TAG(GD_GPL)
%
\begin{impdetails}
> {-# LANGUAGE CPP, EmptyDataDecls, GeneralizedNewtypeDeriving #-}
\end{impdetails}
This module defines instances of "PSpaceStorable" for ARM-specific kernel objects. This includes page table and page directory entries, and ASID pools.
> module SEL4.Object.Instances.ARM_HYP where
@ -18,6 +24,9 @@ This module defines instances of "PSpaceStorable" for ARM-specific kernel object
> import SEL4.Object.Structures
> import SEL4.Model
> import Data.Helpers
#ifdef CONFIG_ARM_SMMU
> import SEL4.Machine.Hardware.ARM_HYP(IOPTE(..), IOPDE(..))
#endif
\end{impdetails}
@ -35,6 +44,22 @@ This module defines instances of "PSpaceStorable" for ARM-specific kernel object
> KOArch (KOPTE p) -> return p
> _ -> typeError "PTE" o
#ifdef CONFIG_ARM_SMMU
> instance PSpaceStorable IOPDE where
> makeObject = InvalidIOPDE
> injectKO = KOArch . KOIOPDE
> projectKO o = case o of
> KOArch (KOIOPDE p) -> return p
> _ -> typeError "IOPDE" o
> instance PSpaceStorable IOPTE where
> makeObject = InvalidIOPTE
> injectKO = KOArch . KOIOPTE
> projectKO o = case o of
> KOArch (KOIOPTE p) -> return p
> _ -> typeError "IOPTE" o
#endif
> instance PSpaceStorable ASIDPool where
> makeObject = ASIDPool $
> funPartialArray (const Nothing) (0,1023)
@ -43,7 +68,5 @@ This module defines instances of "PSpaceStorable" for ARM-specific kernel object
> KOArch (KOASIDPool e) -> return e
> _ -> typeError "ASID pool" o
FIXME ARMHYP not looked at these at all, assuming type error will happen when we try store/load an object type we haven't indicated is PSpaceStorable
FIXME ARMHYP we want these for IOPTE IOPDE and maybe VCPU
FIXME ARMHYP maybe add VCPU

32
spec/haskell/src/SEL4/Object/ObjectType/ARM_HYP.lhs
View File

@ -68,7 +68,6 @@ ASID capabilities can be copied without modification.
#ifdef CONFIG_ARM_SMMU
> deriveCap _ (c@IOSpaceCap {}) = return c
> deriveCap _ (c@IOPageTableCap {}) = error "FIXME ARMHYP TODO IO"
> deriveCap _ (c@IOPageDirectoryCap {}) = throw IllegalOperation -- FIXME ARMHYP missing in C
#endif /* CONFIG_ARM_SMMU */
None of the ARM-specific capabilities have a user writeable data word.
@ -114,7 +113,7 @@ Deletion of any mapped frame capability requires the page table slot to be locat
> finaliseCap (cap@PageCap { capVPMappedAddress = Just (a, v),
> capVPSize = s, capVPBasePtr = ptr }) _ =
#ifdef CONFIG_ARM_SMMU
> if isIOSpaceFrame(cap)
> if capVPisIOSpace cap
> then error "FIXME ARMHYP TODO IO"
> else
#endif
@ -137,7 +136,11 @@ All other capabilities need no finalisation action.
\subsection{Recycling Capabilities}
> resetMemMapping :: ArchCapability -> ArchCapability
#ifdef CONFIG_ARM_SMMU
> resetMemMapping (PageCap p rts sz io _) = PageCap p rts sz io Nothing
#else
> resetMemMapping (PageCap p rts sz _) = PageCap p rts sz Nothing
#endif
> resetMemMapping (PageTableCap ptr _) = PageTableCap ptr Nothing
> resetMemMapping (PageDirectoryCap ptr _) = PageDirectoryCap ptr Nothing
#ifdef CONFIG_ARM_SMMU
@ -207,7 +210,6 @@ All other capabilities need no finalisation action.
#ifdef CONFIG_ARM_SMMU
> recycleCap _ (IOSpaceCap {}) = error "FIXME ARMHYP TODO IOSpace"
> recycleCap _ (IOPageTableCap {}) = error "FIXME ARMHYP TODO IOSpace"
> recycleCap _ (IOPageDirectoryCap {}) = error "FIXME ARMHYP IOPageDirectoryCap can't be recycled" -- but reachable in C in this function
#endif
> hasRecycleRights :: ArchCapability -> Bool
@ -268,7 +270,12 @@ Create an architecture-specific object.
> createObject :: ObjectType -> PPtr () -> Int -> Kernel ArchCapability
> createObject t regionBase _ =
> let funupd = (\f x v y -> if y == x then v else f y) in
> let pointerCast = PPtr . fromPPtr
> let pointerCast = PPtr . fromPPtr in
#ifndef CONFIG_ARM_SMMU
> let mkPageCap = \sz -> PageCap (pointerCast regionBase) VMReadWrite sz Nothing
#else
> let mkPageCap = \sz -> PageCap (pointerCast regionBase) VMReadWrite sz False Nothing
#endif
> in case t of
> Arch.Types.APIObjectType _ ->
> fail "Arch.createObject got an API type"
@ -277,29 +284,25 @@ Create an architecture-specific object.
> modify (\ks -> ks { gsUserPages =
> funupd (gsUserPages ks)
> (fromPPtr regionBase) (Just ARMSmallPage)})
> return $! PageCap (pointerCast regionBase)
> VMReadWrite ARMSmallPage Nothing
> return $! mkPageCap ARMSmallPage
> Arch.Types.LargePageObject -> do
> createPageObject regionBase 4
> modify (\ks -> ks { gsUserPages =
> funupd (gsUserPages ks)
> (fromPPtr regionBase) (Just ARMLargePage)})
> return $! PageCap (pointerCast regionBase)
> VMReadWrite ARMLargePage Nothing
> return $! mkPageCap ARMLargePage
> Arch.Types.SectionObject -> do
> createPageObject regionBase 8
> modify (\ks -> ks { gsUserPages =
> funupd (gsUserPages ks)
> (fromPPtr regionBase) (Just ARMSection)})
> return $! PageCap (pointerCast regionBase)
> VMReadWrite ARMSection Nothing
> return $! mkPageCap ARMSection
> Arch.Types.SuperSectionObject -> do
> createPageObject regionBase 12
> modify (\ks -> ks { gsUserPages =
> funupd (gsUserPages ks)
> (fromPPtr regionBase) (Just ARMSuperSection)})
> return $! PageCap (pointerCast regionBase)
> VMReadWrite ARMSuperSection Nothing
> return $! mkPageCap ARMSuperSection
> Arch.Types.PageTableObject -> do
> let ptSize = ptBits - objBits (makeObject :: PTE)
> let regionSize = (1 `shiftL` ptBits)
@ -342,7 +345,6 @@ Create an architecture-specific object.
#ifdef CONFIG_ARM_SMMU
> IOSpaceCap {} -> error "FIXME ARMHYP TODO IOSpace"
> IOPageTableCap {} -> error "FIXME ARMHYP TODO IO"
> IOPageDirectoryCap {} -> error "FIXME ARMHYP TODO IO"
#endif
> _ -> decodeARMMMUInvocation label args capIndex slot cap extraCaps
@ -358,8 +360,6 @@ Create an architecture-specific object.
> withoutPreemption $ error "FIXME ARMHYP TODO IOSpace"
> ArchInv.InvokeIOPageTable _ ->
> withoutPreemption $ error "FIXME ARMHYP TODO IO"
> ArchInv.InvokePageIO _ ->
> withoutPreemption $ error "FIXME ARMHYP TODO IO"
#endif
> _ -> performARMMMUInvocation i
@ -377,7 +377,6 @@ Create an architecture-specific object.
#ifdef CONFIG_ARM_SMMU
> capUntypedPtr (IOSpaceCap {}) = error "FIXME ARMHYP TODO IOSpace"
> capUntypedPtr (IOPageTableCap { capIOPTBasePtr = PPtr p }) = PPtr p
> capUntypedPtr (IOPageDirectoryCap { capIOPDBasePtr = PPtr p }) = PPtr p
#endif
@ -395,6 +394,5 @@ FIXME ARMHYP if none of the IO or VCPU caps are physical, then capUntypedSize ne
#ifdef CONFIG_ARM_SMMU
> capUntypedSize (IOSpaceCap {}) = 0 -- invalid, use C default
> capUntypedSize (IOPageTableCap {}) = bit ioptBits
> capUntypedSize (IOPageDirectoryCap {}) = 0 -- invalid, use C default
#endif

37
spec/haskell/src/SEL4/Object/Structures/ARM_HYP.lhs
View File

@ -34,8 +34,6 @@ This module makes use of the GHC extension allowing declaration of types with no
There are six ARM-specific capability types: the global ASID control capability, ASID pools, page tables, page directories, and pages.
FIXME ARMHYP frame caps in C have an isIOSpace property - add this here, or add a separate PageIOCap (IOPageCap?) that simply encodes / decodes to the right thing?
> data ArchCapability
> = ASIDPoolCap {
> capASIDPool :: PPtr ASIDPool,
@ -45,6 +43,7 @@ FIXME ARMHYP frame caps in C have an isIOSpace property - add this here, or add
> capVPBasePtr :: PPtr Word,
> capVPRights :: VMRights,
> capVPSize :: VMPageSize,
> capVPisIOSpace :: Bool,
> capVPMappedAddress :: Maybe (ASID, VPtr) }
> | PageTableCap {
> capPTBasePtr :: PPtr PTE,
@ -60,40 +59,36 @@ FIXME ARMHYP frame caps in C have an isIOSpace property - add this here, or add
> | IOSpaceCap {
> capIOSpaceModuleID :: Word16,
> capIOSpaceClientID :: Word16 }
> | IOPageDirectoryCap {
> capIOPDBasePtr :: PPtr IOPDE,
> capIOPDMappedAddress :: Maybe (ASID) } -- FIXME ARMHYP where is mapped address? note that this ASID is in a different namespace (IOMMU not MMU) - stable, deviceID by convention
> | IOPageTableCap {
> capIOPTBasePtr :: PPtr IOPTE,
> capIOPTMappedAddress :: Maybe (ASID, VPtr) } -- FIXME ARMHYP Vptr or PAddr?
> capIOPTMappedAddress :: Maybe (ASID, VPtr) }
#endif
> deriving (Eq, Show)
\subsection{Kernel Objects}
The ARM kernel stores one ARM-specific type of object in the PSpace: ASID pools, which are second level nodes in the global ASID table.
FIXME ARMHYP how does the above comment possibly relate to the ArchKernelObject datatype? fix comment
FIXME ARMHYP TODO IOPTE needs to go here for sure, but what about VCPU? if it was clear what these did, one could decide
The ARM kernel stores some ARM-specific types of objects in the PSpace, such as ASID pools, which are second level nodes in the global ASID table.
> data ArchKernelObject
> = KOASIDPool ASIDPool
> | KOPTE PTE
> | KOPDE PDE
#ifdef CONFIG_ARM_SMMU
> | KOIOPTE IOPTE
> | KOIOPDE IOPDE
#endif
> deriving Show
FIXME ARMHYP add IOPTE and IOPDE to ArchKernelObject? - YES VCPU - MAYBE
FIXME ARMHYP add VCPU to ArchKernelObject? MAYBE
> archObjSize :: ArchKernelObject -> Int
> archObjSize a = case a of
> KOASIDPool _ -> pageBits
#ifndef CONFIG_ARM_HYPERVISOR_SUPPORT
> KOPTE _ -> 2
> KOPDE _ -> 2
#else
> KOPTE _ -> 3
> KOPDE _ -> 3
> KOPTE _ -> pteBits
> KOPDE _ -> pdeBits
#ifdef CONFIG_ARM_SMMU
> KOIOPTE _ -> iopteBits
> KOIOPDE _ -> iopdeBits
#endif
\subsection{ASID Pools}
@ -110,10 +105,14 @@ An ASID is an unsigned word. Note that it is a \emph{virtual} address space iden
ASIDs are mapped to address space roots by a global two-level table. The actual ASID values are opaque to the user, as are the sizes of the levels of the tables; ASID allocation calls will simply return an error once the available ASIDs are exhausted.
FIXME ARMHYP unclear if bit manipulation still correct - we lose one bit down to 7 for isIOSpace, and then 6 after deviceUntyped patch - make it 7/6 (with/without IOMMU)
FIXME ARMHYP after device untyped patch this will be 6 and 7 respectively
> asidHighBits :: Int
#ifdef CONFIG_ARM_HYPERVISOR_SUPPORT
> asidHighBits = 7 -- isIOSpace takes away one bit
#else
> asidHighBits = 8
#endif
> asidLowBits :: Int
> asidLowBits = 10