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

x64: haskell: updated most of haskell spec for new machine functions

This commit is contained in:
Joel Beeren 2017-03-16 14:18:10 +11:00
parent 42ff16ed4c
commit 05150477b9
8 changed files with 131 additions and 77 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
spec/haskell/src/SEL4/API/Invocation/X64.lhs
View File

@ -53,7 +53,8 @@ ASID pool structures, and on IO ports.
> pdptMapCap :: Capability,
> pdptMapCTSlot :: PPtr CTE,
> pdptMapPML4E :: PML4E,
> pdptMapPML4Slot :: PPtr PML4E }
> pdptMapPML4Slot :: PPtr PML4E,
> pdptMapVSpace :: PPtr PML4E }
> deriving Show
> data PageDirectoryInvocation
@ -64,7 +65,8 @@ ASID pool structures, and on IO ports.
> pdMapCap :: Capability,
> pdMapCTSlot :: PPtr CTE,
> pdMapPDPTE :: PDPTE,
> pdMapPDPTSlot :: PPtr PDPTE }
> pdMapPDPTSlot :: PPtr PDPTE,
> pdMapVSpace :: PPtr PML4E }
> deriving Show
> data PageTableInvocation
@ -75,7 +77,8 @@ ASID pool structures, and on IO ports.
> ptMapCap :: Capability,
> ptMapCTSlot :: PPtr CTE,
> ptMapPDE :: PDE,
> ptMapPDSlot :: PPtr PDE }
> ptMapPDSlot :: PPtr PDE,
> ptMapVSpace :: PPtr PML4E }
> deriving Show
IO page tables are contained in other IO page tables. The topmost one sits in a

118
spec/haskell/src/SEL4/Kernel/VSpace/X64.lhs
View File

@ -322,7 +322,7 @@ When a capability backing a virtual memory mapping is deleted, or when an explic
> if pt' == addrFromPPtr pdpt then return () else throw InvalidRoot
> _ -> throw InvalidRoot
> withoutFailure $ do
> flushPDPT vspace vaddr pdpt
> flushPDPT (addrFromPPtr vspace) asid
> storePML4E pmSlot InvalidPML4E
\subsubsection{Deleting a Page Directory}
@ -337,8 +337,9 @@ When a capability backing a virtual memory mapping is deleted, or when an explic
> if pd' == addrFromPPtr pd then return () else throw InvalidRoot
> _ -> throw InvalidRoot
> withoutFailure $ do
> doMachineOp invalidatePageStructureCache -- FIXME x64: hardware implement
> flushPD (addrFromPPtr vspace) asid
> storePDPTE pdptSlot InvalidPDPTE
> invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
\subsubsection{Deleting a Page Table}
@ -354,7 +355,7 @@ When a capability backing a virtual memory mapping is deleted, or when an explic
> withoutFailure $ do
> flushTable vspace vaddr pt
> storePDE pdSlot InvalidPDE
> doMachineOp invalidatePageStructureCache -- FIXME x64: hardware implement
> invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
\subsubsection{Unmapping a Frame}
@ -408,8 +409,31 @@ This helper function checks that the mapping installed at a given PT or PD slot
\subsection{Address Space Switching}
> setCurrentVSpaceRoot :: PAddr -> ASID -> MachineMonad ()
> setCurrentVSpaceRoot addr (ASID asid) = archSetCurrentVSpaceRoot addr (Word asid)
> getCurrentCR3 :: Kernel CR3
> getCurrentCR3 = gets (x64KSCurrentCR3 . ksArchState)
> setCurrentCR3 :: CR3 -> Kernel ()
> setCurrentCR3 cr3 = do
> modify (\s -> s { ksArchState = (ksArchState s) { x64KSCurrentCR3 = cr3 }})
> doMachineOp $ writeCR3 (cr3BaseAddress cr3) $ fromASID $ cr3pcid cr3
> invalidateLocalPageStructureCacheASID :: PAddr -> ASID -> Kernel ()
> invalidateLocalPageStructureCacheASID ptr asid = do
> curCR3 <- getCurrentCR3
> setCurrentCR3 (CR3 ptr asid)
> setCurrentCR3 curCR3
> invalidatePageStructureCacheASID :: PAddr -> ASID -> Kernel ()
> invalidatePageStructureCacheASID p a = invalidateLocalPageStructureCacheASID p a
> getCurrentVSpaceRoot :: Kernel PAddr
> getCurrentVSpaceRoot = do
> cur <- getCurrentCR3
> return $ cr3BaseAddress cur
> setCurrentVSpaceRoot :: PAddr -> ASID -> Kernel ()
> setCurrentVSpaceRoot vspace asid = setCurrentCR3 $ CR3 vspace asid
> -- FIXME x64: Currently we don't have global state for the CR3 so
> -- we can't test whether or not we should write to it. We should
@ -426,11 +450,14 @@ This helper function checks that the mapping installed at a given PT or PD slot
> capPML4BasePtr = pd }) -> do
> pd' <- findVSpaceForASID asid
> when (pd /= pd') $ throw InvalidRoot
> withoutFailure $ doMachineOp $ setCurrentVSpaceRoot (addrFromPPtr pd) asid
> -- update asid map
> curCR3 <- withoutFailure $ getCurrentCR3
> when (curCR3 /= CR3 (addrFromPPtr pd) asid) $
> withoutFailure $ setCurrentCR3 $ CR3 (addrFromPPtr pd) asid
> _ -> throw InvalidRoot)
> (\_ -> do
> globalPML4 <- gets (x64KSGlobalPML4 . ksArchState)
> doMachineOp $ setCurrentVSpaceRoot (addrFromKPPtr globalPML4) 0)
> setCurrentVSpaceRoot (addrFromKPPtr globalPML4) 0)
\subsection{Helper Functions}
@ -462,16 +489,14 @@ Note that implementations with separate high and low memory regions may also wis
%FIXME x64: needs review
> flushPDPT :: PPtr PML4E -> VPtr -> PPtr PDPTE -> Kernel ()
> flushPDPT _ _ _ = doMachineOp $ resetCR3
> flushAll :: PAddr -> ASID -> Kernel ()
> flushAll vspace asid = doMachineOp $ invalidateASID vspace (fromASID asid)
%FIXME x64: needs review
> flushPDPT :: PAddr -> ASID -> Kernel ()
> flushPDPT p a = flushAll p a
> flushPageDirectory :: PPtr PML4E -> VPtr -> PPtr PDE -> Kernel ()
> flushPageDirectory _ _ _ = doMachineOp $ resetCR3
> flushCacheRange :: PPtr a -> Int -> Kernel ()
> flushCacheRange _ _ = fail "not implemeneted"
> flushPD :: PAddr -> ASID -> Kernel ()
> flushPD p a = flushAll p a
%FIXME x64: needs review
@ -835,7 +860,8 @@ IOMap is related with label X64PageMapIO and IOUnmap is related with X64PageUnma
> pdptMapCap = ArchObjectCap $ cap { capPDPTMappedAddress = Just (asid, (VPtr vaddr)) },
> pdptMapCTSlot = cte,
> pdptMapPML4E = pml4e,
> pdptMapPML4Slot = pml4Slot }
> pdptMapPML4Slot = pml4Slot,
> pdptMapVSpace = vspace }
> (ArchInvocationLabel X64PDPTMap, _, _) -> throw TruncatedMessage
> (ArchInvocationLabel X64PDPTUnmap, _, _) -> do
> cteVal <- withoutFailure $ getCTE cte
@ -883,7 +909,8 @@ IOMap is related with label X64PageMapIO and IOUnmap is related with X64PageUnma
> pdMapCap = ArchObjectCap $ cap { capPDMappedAddress = Just (asid, (VPtr vaddr)) },
> pdMapCTSlot = cte,
> pdMapPDPTE = pdpte,
> pdMapPDPTSlot = pdptSlot }
> pdMapPDPTSlot = pdptSlot,
> pdMapVSpace = pml }
> (ArchInvocationLabel X64PageDirectoryMap, _, _) -> throw TruncatedMessage
> (ArchInvocationLabel X64PageDirectoryUnmap, _, _) -> do
> cteVal <- withoutFailure $ getCTE cte
@ -931,7 +958,8 @@ IOMap is related with label X64PageMapIO and IOUnmap is related with X64PageUnma
> ptMapCap = ArchObjectCap $ cap { capPTMappedAddress = Just (asid, (VPtr vaddr)) },
> ptMapCTSlot = cte,
> ptMapPDE = pde,
> ptMapPDSlot = pdSlot }
> ptMapPDSlot = pdSlot,
> ptMapVSpace = pml }
> (ArchInvocationLabel X64PageTableMap, _, _) -> throw TruncatedMessage
> (ArchInvocationLabel X64PageTableUnmap, _, _) -> do
> cteVal <- withoutFailure $ getCTE cte
@ -951,18 +979,18 @@ IOMap is related with label X64PageMapIO and IOUnmap is related with X64PageUnma
> decodeX64ASIDControlInvocation label args ASIDControlCap extraCaps =
> case (invocationType label, args, extraCaps) of
> (ArchInvocationLabel X64ASIDControlMakePool, index:depth:_,
> (untyped,parentSlot):(root,_):_) -> do
> (untyped,parentSlot):(croot,_):_) -> do
> asidTable <- withoutFailure $ gets (x64KSASIDTable . ksArchState)
> let free = filter (\(x,y) -> x <= (1 `shiftL` asidHighBits) - 1 && isNothing y) $ assocs asidTable
> when (null free) $ throw DeleteFirst
> let base = (fst $ head free) `shiftL` asidLowBits
> let pool = makeObject :: ASIDPool
> frame <- case untyped of
> UntypedCap {} | capBlockSize untyped == objBits pool -> do
> UntypedCap { capIsDevice = False } | capBlockSize untyped == objBits pool -> do
> ensureNoChildren parentSlot
> return $ capPtr untyped
> _ -> throw $ InvalidCapability 1
> destSlot <- lookupTargetSlot root (CPtr index) (fromIntegral depth)
> destSlot <- lookupTargetSlot croot (CPtr index) (fromIntegral depth)
> ensureEmptySlot destSlot
> return $ InvokeASIDControl $ MakePool {
> makePoolFrame = frame,
@ -1054,10 +1082,13 @@ Checking virtual address for page size dependent alignment:
> return $ []
> performPDPTInvocation :: PDPTInvocation -> Kernel ()
> performPDPTInvocation (PDPTMap cap ctSlot pml4e pml4Slot) = do
> performPDPTInvocation (PDPTMap cap ctSlot pml4e pml4Slot vspace) = do
> updateCap ctSlot cap
> storePML4E pml4Slot pml4e
> doMachineOp invalidatePageStructureCache
> asid <- case cap of
> ArchObjectCap (PageDirectoryCap _ (Just (a, _))) -> return a
> _ -> fail "should never happen"
> invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
>
> performPDPTInvocation (PDPTUnmap cap ctSlot) = do
> case capPDPTMappedAddress cap of
@ -1072,10 +1103,13 @@ Checking virtual address for page size dependent alignment:
> updateCap ctSlot (ArchObjectCap $ cap { capPDPTMappedAddress = Nothing })
> performPageDirectoryInvocation :: PageDirectoryInvocation -> Kernel ()
> performPageDirectoryInvocation (PageDirectoryMap cap ctSlot pdpte pdptSlot) = do
> performPageDirectoryInvocation (PageDirectoryMap cap ctSlot pdpte pdptSlot vspace) = do
> updateCap ctSlot cap
> storePDPTE pdptSlot pdpte
> doMachineOp invalidatePageStructureCache
> asid <- case cap of
> ArchObjectCap (PageDirectoryCap _ (Just (a, _))) -> return a
> _ -> fail "should never happen"
> invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
>
> performPageDirectoryInvocation (PageDirectoryUnmap cap ctSlot) = do
> case capPDMappedAddress cap of
@ -1091,10 +1125,13 @@ Checking virtual address for page size dependent alignment:
> performPageTableInvocation :: PageTableInvocation -> Kernel ()
> performPageTableInvocation (PageTableMap cap ctSlot pde pdSlot) = do
> performPageTableInvocation (PageTableMap cap ctSlot pde pdSlot vspace) = do
> updateCap ctSlot cap
> storePDE pdSlot pde
> doMachineOp invalidatePageStructureCache
> asid <- case cap of
> ArchObjectCap (PageTableCap _ (Just (a, _))) -> return a
> _ -> fail "should never happen"
> invalidatePageStructureCacheASID (addrFromPPtr vspace) asid
>
> performPageTableInvocation (PageTableUnmap cap slot) = do
> case capPTMappedAddress cap of
@ -1267,38 +1304,37 @@ The kernel model's x64 targets use an external simulation of the physical addres
>-- deleteIOPageTable _ = error "Not an IOPageTable capability" -}
> mapKernelWindow :: Kernel ()
> mapKernelWindow = error "Unimplemented . init code"
> mapKernelWindow :: Kernel ()
> mapKernelWindow = error "boot code unimplemented"
> activateGlobalVSpace :: Kernel ()
> activateGlobalVSpace = error "Unimplemented . init code"
> activateGlobalVSpace = error "boot code unimplemented"
> createIPCBufferFrame :: Capability -> VPtr -> KernelInit Capability
> createIPCBufferFrame = error "Unimplemented . init code"
> createIPCBufferFrame = error "boot code unimplemented"
> createBIFrame :: Capability -> VPtr -> Word32 -> Word32 -> KernelInit Capability
> createBIFrame = error "Unimplemented . init code"
> createBIFrame = error "boot code unimplemented"
> createFramesOfRegion :: Capability -> Region -> Bool -> KernelInit ()
> createFramesOfRegion = error "Unimplemented . init code"
> createFramesOfRegion = error "boot code unimplemented"
> createITPDPTs :: Capability -> VPtr -> VPtr -> KernelInit Capability
> createITPDPTs = error "Unimplemented . init code"
> createITPDPTs = error "boot code unimplemented"
> writeITPDPTs :: Capability -> Capability -> KernelInit ()
> writeITPDPTs = error "Unimplemented . init code"
> writeITPDPTs = error "boot code unimplemented"
> createITASIDPool :: Capability -> KernelInit Capability
> createITASIDPool = error "Unimplemented . init code"
> createITASIDPool = error "boot code unimplemented"
> writeITASIDPool :: Capability -> Capability -> Kernel ()
> writeITASIDPool = error "Unimplemented . init code"
> writeITASIDPool = error "boot code unimplemented"
> createDeviceFrames :: Capability -> KernelInit ()
> createDeviceFrames = error "Unimplemented . init code"
> createDeviceFrames = error "boot code unimplemented"
> vptrFromPPtr :: PPtr a -> KernelInit VPtr
> vptrFromPPtr (PPtr ptr) = do
> offset <- gets initVPtrOffset
> return $ (VPtr ptr) + offset
> vptrFromPPtr = error "boot code unimplemented"

42
spec/haskell/src/SEL4/Machine/Hardware/X64.lhs
View File

@ -43,8 +43,6 @@ The machine monad contains a platform-specific opaque pointer, used by the exter
> type IRQ = Platform.IRQ
> type CR3 = Platform.CR3
> type IOPort = Word16
> toPAddr = Platform.PAddr
@ -240,19 +238,11 @@ caches must be done separately.
\subsubsection{Address Space Setup}
> setCurrentCR3 :: CR3 -> MachineMonad ()
> setCurrentCR3 cr3 = Platform.writeCR3 cr3
> writeCR3 :: PAddr -> Word64 -> MachineMonad ()
> writeCR3 vspace asid = Platform.writeCR3 vspace asid
> getCurrentCR3 :: MachineMonad CR3
> getCurrentCR3 = do
> cbptr <- ask
> liftIO $ Platform.readCR3 cbptr
> archSetCurrentVSpaceRoot :: PAddr -> Word -> MachineMonad ()
> archSetCurrentVSpaceRoot pd asid =
> setCurrentCR3 $ Platform.X64CR3 pd asid
> resetCR3 = error "Unimplemented"
> resetCR3 :: MachineMonad ()
> resetCR3 = Platform.resetCR3
\subsubsection{Memory Barriers}
@ -270,6 +260,12 @@ caches must be done separately.
> invalidatePageStructureCache :: MachineMonad ()
> invalidatePageStructureCache = invalidateTLBEntry 0
> invalidateASID :: PAddr -> Word64 -> MachineMonad ()
> invalidateASID vspace asid = Platform.invalidateASID vspace asid
> invalidateTranslationSingleASID :: PAddr -> Word64 -> MachineMonad ()
> invalidateTranslationSingleASID vspace asid = Platform.invalidateTranslationSingleASID vspace asid
\subsubsection{Page Table Structure}
The x64 architecture defines a four-level hardware-walked page table. The kernel must write entries to this table in the defined format to construct address spaces for user-level tasks.
@ -631,11 +627,21 @@ IRQ parameters
%FIXME: review how deeply we need to model this.
> data X64IRQState = X64IRQState
> data X64IRQState =
> IRQFree
> | IRQReserved
> | IRQMSI {
> msiBus :: Word,
> msiDev :: Word,
> msiFunc :: Word,
> msiHandle :: Word }
> | IRQIOAPIC {
> irqIOAPIC :: Word,
> irqPin :: Word,
> irqLevel :: Word,
> irqPolarity :: Word,
> irqMasked :: Bool }
> irqStateIRQIOAPICNew = error "Unimplemented . FIXME see structures.bf"
> irqStateIRQMSINew = error "Unimplemented . FIXME see structures.bf"
> updateIRQState :: IRQ -> X64IRQState -> MachineMonad ()
> updateIRQState _ _ = error "Unimplemented"

5
spec/haskell/src/SEL4/Machine/Hardware/X64/PC99.hs
View File

@ -131,15 +131,16 @@ foreign import ccall unsafe "qemu_store_word_phys"
-- PC99 stubs
data CR3 = X64CR3 { cr3BaseAddress :: PAddr, cr3pcid :: Word }
writeCR3 = error "Unimplemented"
readCR3 = error "Unimplemented"
resetCR3 = error "Unimplemented"
invalidateTLB = error "Unimplemented"
mfence = error "Unimplemented"
addrFromKPPtr = error "Unimplemented" -- FIXME two kernel windows
pptrBase = error "Unimplemented" -- FIXME two kernel windows
hwASIDInvalidate = error "Unimplemented"
invalidateASID = error "Unimplemented"
invalidateTranslationSingleASID = error "unimplemented"
getFaultAddress :: Ptr CallbackData -> IO VPtr

3
spec/haskell/src/SEL4/Model/StateData/X64.lhs
View File

@ -39,7 +39,8 @@ This module contains the architecture-specific kernel global data for the X86-64
> x64KSGlobalPML4 :: PPtr PML4E,
> x64KSGlobalPDPTs :: [PPtr PDPTE],
> x64KSGlobalPDs :: [PPtr PDE],
> x64KSGlobalPTs :: [PPtr PTE]}
> x64KSGlobalPTs :: [PPtr PTE],
> x64KSCurrentCR3 :: CR3}
> newKernelState :: PAddr -> (KernelState, [PAddr])
> newKernelState _ = error "No initial state defined for x64"

4
spec/haskell/src/SEL4/Object/Interrupt/X64.lhs
View File

@ -87,7 +87,7 @@ This module defines the machine-specific interrupt handling routines for x64.
> performIRQControl (ArchInv.IssueIRQHandlerIOAPIC (IRQ irq) destSlot srcSlot ioapic
> pin level polarity vector) = withoutPreemption $ do
> doMachineOp $ Arch.ioapicMapPinToVector ioapic pin level polarity vector
> irqState <- doMachineOp $ Arch.irqStateIRQIOAPICNew ioapic pin level polarity (1::Word) (0::Word)
> irqState <- return $ Arch.IRQIOAPIC ioapic pin level polarity True
> doMachineOp $ Arch.updateIRQState irq irqState
> -- do same thing as generic path in performIRQControl in Interrupt.lhs
> setIRQState IRQSignal (IRQ irq)
@ -96,7 +96,7 @@ This module defines the machine-specific interrupt handling routines for x64.
>
> performIRQControl (ArchInv.IssueIRQHandlerMSI (IRQ irq) destSlot srcSlot pciBus
> pciDev pciFunc handle) = withoutPreemption $ do
> irqState <- doMachineOp $ Arch.irqStateIRQMSINew pciBus pciDev pciFunc handle
> irqState <- return $ Arch.IRQMSI pciBus pciDev pciFunc handle
> doMachineOp $ Arch.updateIRQState irq irqState
> -- do same thing as generic path in performIRQControl in Interrupt.lhs
> setIRQState IRQSignal (IRQ irq)

10
spec/haskell/src/SEL4/Object/ObjectType/X64.lhs
View File

@ -71,12 +71,12 @@ IOPTs
X64 has two writable user data caps
> -- FIXME x64: io_space_capdata_get_domainID
> ioSpaceGetDomainID :: Word -> Word16
> ioSpaceGetDomainID _ = error "Not implemented"
>-- ioSpaceGetDomainID :: Word -> Word16
>-- ioSpaceGetDomainID _ = error "Not implemented"
> -- FIXME x64: io_space_capdata_get_PCIDevice
> ioSpaceGetPCIDevice :: Word -> Maybe IOASID
> ioSpaceGetPCIDevice _ = error "Not implemented"
>-- -- FIXME x64: io_space_capdata_get_PCIDevice
>-- ioSpaceGetPCIDevice :: Word -> Maybe IOASID
>-- ioSpaceGetPCIDevice _ = error "Not implemented"
> -- FIXME x64: io_port_capdata_get_firstPort
> ioPortGetFirstPort :: Word -> Word16

17
spec/haskell/src/SEL4/Object/Structures/X64.lhs
View File

@ -24,8 +24,8 @@ This module makes use of the GHC extension allowing declaration of types with no
> import SEL4.Machine.RegisterSet
> import SEL4.Machine.Hardware.X64
> import Data.Array
> import Data.Word (Word16, Word64)
> import Data.Bits
> import Data.Word(Word64)
\end{impdetails}
@ -84,9 +84,9 @@ This module makes use of the GHC extension allowing declaration of types with no
> deriving Show
> archObjSize :: ArchKernelObject -> Int
> archObjSize a = case a of
> archObjSize a = case a of
> KOASIDPool _ -> pageBits
> KOPTE _ -> 3
> KOPTE _ -> 3
> KOPDE _ -> 3
> KOPDPTE _ -> 3
> KOPML4E _ -> 3
@ -108,7 +108,7 @@ present on all platforms is stored here.
> atcbContext = newContext }
> atcbContextSet :: UserContext -> ArchTCB -> ArchTCB
> atcbContextSet uc at = at { atcbContext = uc }
> atcbContextSet uc atcb = atcb { atcbContext = uc }
>
> atcbContextGet :: ArchTCB -> UserContext
> atcbContextGet = atcbContext
@ -122,7 +122,7 @@ An ASID pool is an array of pointers to page directories. This is used to implem
An ASID is an unsigned word. Note that it is a \emph{virtual} address space identifier, and does not correspond to any hardware-defined identifier.
> newtype ASID = ASID Word64
> newtype ASID = ASID { fromASID :: Word64 }
> deriving (Show, Eq, Ord, Enum, Real, Integral, Num, Bits, Ix, Bounded)
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.
@ -142,3 +142,10 @@ ASIDs are mapped to address space roots by a global two-level table. The actual
> asidHighBitsOf :: ASID -> ASID
> asidHighBitsOf asid = (asid `shiftR` asidLowBits) .&. mask asidHighBits
> data CR3 = CR3 {
> cr3BaseAddress :: PAddr,
> cr3pcid :: ASID }
> deriving (Show, Eq)