aarch64 haskell: flush API, including perform
Still missing decodeInvocation, but should otherwise be complete, including machine ops. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
2215c411a1
commit
4c7294452b
|
@ -30,13 +30,24 @@ import SEL4.Machine.RegisterSet.AARCH64 (Register(..), VCPUReg(..))
|
|||
-- ASID pool structures.
|
||||
|
||||
data Invocation
|
||||
= InvokePageTable PageTableInvocation
|
||||
= InvokeVSpaceRoot VSpaceRootInvocation
|
||||
| InvokePageTable PageTableInvocation
|
||||
| InvokePage PageInvocation
|
||||
| InvokeASIDControl ASIDControlInvocation
|
||||
| InvokeASIDPool ASIDPoolInvocation
|
||||
| InvokeVCPU VCPUInvocation
|
||||
deriving Show
|
||||
|
||||
data VSpaceRootInvocation
|
||||
= VSpaceRootFlush {
|
||||
vsFlushType :: FlushType,
|
||||
vsFlushStart :: VPtr,
|
||||
vsFlushEnd :: VPtr,
|
||||
vsFlushPStart :: PAddr,
|
||||
vsFlushSpace :: PPtr PTE,
|
||||
vsFlushASID :: ASID }
|
||||
deriving Show
|
||||
|
||||
data PageTableInvocation
|
||||
= PageTableUnmap {
|
||||
ptUnmapCap :: ArchCapability,
|
||||
|
@ -58,6 +69,13 @@ data PageInvocation
|
|||
| PageUnmap {
|
||||
pageUnmapCap :: ArchCapability,
|
||||
pageUnmapCapSlot :: PPtr CTE }
|
||||
| PageFlush {
|
||||
pageFlushType :: FlushType,
|
||||
pageFlushStart :: VPtr,
|
||||
pageFlushEnd :: VPtr,
|
||||
pageFlushPStart :: PAddr,
|
||||
pageFlushSpace :: PPtr PTE,
|
||||
pageFlushASID :: ASID }
|
||||
deriving Show
|
||||
|
||||
data ASIDControlInvocation
|
||||
|
@ -75,6 +93,10 @@ data ASIDPoolInvocation
|
|||
assignASIDCTSlot :: PPtr CTE }
|
||||
deriving Show
|
||||
|
||||
data FlushType
|
||||
= Clean | Invalidate | CleanInvalidate | Unify
|
||||
deriving Show
|
||||
|
||||
{- VCPUs -}
|
||||
|
||||
type HyperReg = VCPUReg
|
||||
|
|
|
@ -19,11 +19,19 @@ module SEL4.API.InvocationLabels.AARCH64 where
|
|||
-- FIXME AARCH64: review enum arch_invocation_label in C, the list is quite
|
||||
-- different between ARM and RISCV64
|
||||
data ArchInvocationLabel
|
||||
= ARMPageTableMap
|
||||
= ARMVSpaceClean_Data
|
||||
| ARMVSpaceInvalidate_Data
|
||||
| ARMVSpaceCleanInvalidate_Data
|
||||
| ARMVSpaceUnify_Instruction
|
||||
| ARMPageTableMap
|
||||
| ARMPageTableUnmap
|
||||
| ARMPageMap
|
||||
| ARMPageUnmap
|
||||
| ARMPageGetAddress
|
||||
| ARMPageClean_Data
|
||||
| ARMPageInvalidate_Data
|
||||
| ARMPageCleanInvalidate_Data
|
||||
| ARMPageUnify_Instruction
|
||||
| ARMASIDControlMakePool
|
||||
| ARMASIDPoolAssign
|
||||
| ARMVCPUSetTCB
|
||||
|
|
|
@ -220,6 +220,19 @@ invalidateTLBByASID asid = do
|
|||
when (isJust maybeVMID) $
|
||||
doMachineOp $ invalidateTranslationASID $ fromIntegral $ fromJust maybeVMID
|
||||
|
||||
doFlush :: FlushType -> VPtr -> VPtr -> PAddr -> MachineMonad ()
|
||||
doFlush flushType vstart vend pstart =
|
||||
-- the address calculations that happen here on ARM_HYP are at the caller side in AARCH64
|
||||
case flushType of
|
||||
Clean -> cleanCacheRange_RAM vstart vend pstart
|
||||
Invalidate -> invalidateCacheRange_RAM vstart vend pstart
|
||||
CleanInvalidate -> cleanInvalidateCacheRange_RAM vstart vend pstart
|
||||
Unify -> do
|
||||
cleanCacheRange_PoU vstart vend pstart
|
||||
dsb
|
||||
invalidateCacheRange_I vstart vend pstart
|
||||
branchFlushRange vstart vend pstart
|
||||
isb
|
||||
|
||||
{- Unmapping and Deletion -}
|
||||
|
||||
|
@ -654,6 +667,14 @@ decodeARMMMUInvocation _ _ _ _ (VCPUCap {}) _ = fail "decodeARMMMUInvocation: no
|
|||
|
||||
{- Invocation Implementations -}
|
||||
|
||||
performVSpaceRootInvocation :: VSpaceRootInvocation -> Kernel ()
|
||||
performVSpaceRootInvocation (VSpaceRootFlush flushType vstart vend pstart space asid) = do
|
||||
let start = VPtr $ fromPPtr $ ptrFromPAddr pstart
|
||||
let end = start + (vend - vstart)
|
||||
when (start < end) $ do
|
||||
doMachineOp $ doFlush flushType start end pstart
|
||||
|
||||
|
||||
performPageTableInvocation :: PageTableInvocation -> Kernel ()
|
||||
performPageTableInvocation (PageTableMap cap ctSlot pte ptSlot) = do
|
||||
updateCap ctSlot cap
|
||||
|
@ -696,6 +717,12 @@ performPageInvocation (PageGetAddr ptr) = do
|
|||
msgLabel = 0 }
|
||||
setMessageInfo ct msgInfo
|
||||
|
||||
performPageInvocation (PageFlush flushType vstart vend pstart space asid) = do
|
||||
let start = VPtr $ fromPPtr $ ptrFromPAddr pstart
|
||||
let end = start + (vend - vstart)
|
||||
when (start < end) $ do
|
||||
doMachineOp $ doFlush flushType start end pstart
|
||||
|
||||
|
||||
performASIDControlInvocation :: ASIDControlInvocation -> Kernel ()
|
||||
performASIDControlInvocation (MakePool frame slot parent base) = do
|
||||
|
@ -726,6 +753,7 @@ performASIDPoolInvocation (Assign asid poolPtr ctSlot) = do
|
|||
performARMMMUInvocation :: ArchInv.Invocation -> KernelP [Word]
|
||||
performARMMMUInvocation i = withoutPreemption $ do
|
||||
case i of
|
||||
InvokeVSpaceRoot oper -> performVSpaceRootInvocation oper
|
||||
InvokePageTable oper -> performPageTableInvocation oper
|
||||
InvokePage oper -> performPageInvocation oper
|
||||
InvokeASIDControl oper -> performASIDControlInvocation oper
|
||||
|
|
|
@ -209,6 +209,25 @@ sfence = error "Unimplemented - machine op"
|
|||
invalidateTranslationASID :: Word -> MachineMonad ()
|
||||
invalidateTranslationASID vmID = error "unimplemented - machine op"
|
||||
|
||||
cleanInvalidateCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
|
||||
cleanInvalidateCacheRange_RAM vstart vend pstart = error "Unimplemented - machine op"
|
||||
|
||||
cleanCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
|
||||
cleanCacheRange_RAM vstart vend pstart = error "Unimplemented - machine op"
|
||||
|
||||
cleanCacheRange_PoU :: VPtr -> VPtr -> PAddr -> MachineMonad ()
|
||||
cleanCacheRange_PoU vstart vend pstart = error "Unimplemented - machine op"
|
||||
|
||||
invalidateCacheRange_RAM :: VPtr -> VPtr -> PAddr -> MachineMonad ()
|
||||
invalidateCacheRange_RAM vstart vend pstart = error "Unimplemented - machine op"
|
||||
|
||||
invalidateCacheRange_I :: VPtr -> VPtr -> PAddr -> MachineMonad ()
|
||||
invalidateCacheRange_I vstart vend pstart = error "Unimplemented - machine op"
|
||||
|
||||
branchFlushRange :: VPtr -> VPtr -> PAddr -> MachineMonad ()
|
||||
branchFlushRange vstart vend pstart = error "Unimplemented - machine op"
|
||||
|
||||
|
||||
{- FPU status/control registers -}
|
||||
|
||||
enableFpuEL01 :: MachineMonad ()
|
||||
|
|
Loading…
Reference in New Issue