Skip to content

Commit

Permalink
aarch64 haskell+design: update exec spec to use semi-lazy FPU switching
Browse files Browse the repository at this point in the history
Signed-off-by: Corey Lewis <[email protected]>
  • Loading branch information
corlewis committed Sep 24, 2024
1 parent f6ca1f8 commit bfd342f
Show file tree
Hide file tree
Showing 25 changed files with 188 additions and 31 deletions.
4 changes: 2 additions & 2 deletions spec/design/m-skel/AARCH64/MachineTypes.thy
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ text \<open>

section "Types"

#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 decls_only NOT UserContext UserMonad Word getRegister setRegister newContext FPUState newFPUState
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 decls_only NOT UserContext UserMonad Word getRegister setRegister getFPUState setFPUState newContext FPUState newFPUState

#INCLUDE_HASKELL SEL4/Object/Structures/AARCH64.hs CONTEXT AARCH64 ONLY VPPIEventIRQ VirtTimer
(*<*)
Expand All @@ -40,7 +40,7 @@ context Arch begin arch_global_naming
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 instanceproofs
#INCLUDE_HASKELL SEL4/Object/Structures/AARCH64.hs CONTEXT AARCH64 instanceproofs ONLY VPPIEventIRQ VirtTimer
(*>*)
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 bodies_only NOT getRegister setRegister newContext newFPUState
#INCLUDE_HASKELL SEL4/Machine/RegisterSet/AARCH64.hs CONTEXT AARCH64 bodies_only NOT getRegister setRegister getFPUState setFPUState newContext newFPUState

section "Machine State"

Expand Down
4 changes: 3 additions & 1 deletion spec/design/skel/AARCH64/ArchTCB_H.thy
Original file line number Diff line number Diff line change
Expand Up @@ -5,7 +5,9 @@
*)

theory ArchTCB_H
imports TCBDecls_H
imports
TCBDecls_H
FPU_H
begin

context Arch begin arch_global_naming (H)
Expand Down
1 change: 1 addition & 0 deletions spec/design/skel/AARCH64/ArchThread_H.thy
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ imports
TCBDecls_H
ArchVSpaceDecls_H
ArchHypervisor_H
FPU_H
begin

context Arch begin arch_global_naming (H)
Expand Down
19 changes: 19 additions & 0 deletions spec/design/skel/AARCH64/FPU_H.thy
Original file line number Diff line number Diff line change
@@ -0,0 +1,19 @@
(*
* Copyright 2024, Proofcraft Pty Ltd
*
* SPDX-License-Identifier: GPL-2.0-only
*)

chapter "FPU"

theory FPU_H
imports
Hardware_H
TCBDecls_H
begin
context Arch begin arch_global_naming (H)

#INCLUDE_HASKELL SEL4/Object/FPU/AARCH64.hs CONTEXT AARCH64_H ArchInv=Arch

end
end
2 changes: 1 addition & 1 deletion spec/design/skel/AARCH64/Hardware_H.thy
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ context Arch begin arch_global_naming (H)
pptrUserTop kernelELFBase kernelELFBaseOffset kernelELFPAddrBase \
addrFromKPPtr ptTranslationBits vmFaultTypeFSR setVSpaceRoot \
setIRQTrigger \
config_ARM_PA_SIZE_BITS_40 fpuThreadDeleteOp isFpuEnable \
config_ARM_PA_SIZE_BITS_40 readFpuState writeFpuState enableFpu disableFpu isFpuEnable \
hcrVCPU hcrNative sctlrDefault vgicHCREN gicVCPUMaxNumLR sctlrEL1VM \
get_gic_vcpu_ctrl_hcr set_gic_vcpu_ctrl_hcr get_gic_vcpu_ctrl_vmcr \
set_gic_vcpu_ctrl_vmcr get_gic_vcpu_ctrl_apr set_gic_vcpu_ctrl_apr \
Expand Down
2 changes: 1 addition & 1 deletion spec/design/skel/Retype_H.thy
Original file line number Diff line number Diff line change
Expand Up @@ -26,7 +26,7 @@ requalify_consts (aliasing)
hasCancelSendRights sameRegionAs isPhysicalCap
sameObjectAs updateCapData maskCapRights
createObject capUntypedPtr capUntypedSize
performInvocation decodeInvocation prepareThreadDelete
performInvocation decodeInvocation prepareThreadDelete prepareSetDomain

context begin global_naming global

Expand Down
2 changes: 2 additions & 0 deletions spec/design/skel/Structures_H.thy
Original file line number Diff line number Diff line change
Expand Up @@ -24,11 +24,13 @@ arch_requalify_types (H)
arch_kernel_object
asid
arch_tcb
arch_tcb_flag

arch_requalify_consts (H)
archObjSize
nullPointer
newArchTCB
archTcbFlagToWord
fromPPtr
PPtr
atcbContextGet
Expand Down
1 change: 1 addition & 0 deletions spec/design/skel/TCB_H.thy
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ arch_requalify_consts (H)
msgRegisters
fromVPtr
postModifyRegisters
postSetFlags
sanitiseRegister
getSanitiseRegisterInfo

Expand Down
1 change: 1 addition & 0 deletions spec/design/skel/Thread_H.thy
Original file line number Diff line number Diff line change
Expand Up @@ -31,6 +31,7 @@ requalify_consts (aliasing)
configureIdleThread
switchToIdleThread
switchToThread
prepareNextDomain

context begin global_naming global

Expand Down
1 change: 1 addition & 0 deletions spec/haskell/SEL4.cabal
Original file line number Diff line number Diff line change
Expand Up @@ -214,6 +214,7 @@ Library
SEL4.Object.Instances.AARCH64
SEL4.Object.VCPU.AARCH64
SEL4.Object.TCB.AARCH64
SEL4.Object.FPU.AARCH64
SEL4.Model.StateData.AARCH64
SEL4.Model.PSpace.AARCH64
SEL4.Machine.RegisterSet.AARCH64
Expand Down
4 changes: 4 additions & 0 deletions spec/haskell/src/SEL4/API/Invocation.lhs
Original file line number Diff line number Diff line change
Expand Up @@ -83,6 +83,10 @@ The following data type defines the set of possible TCB invocation operations. T
> | SetTLSBase {
> setTLSBaseTCB :: PPtr TCB,
> setTLSBaseNewBase :: Word }
> | SetFlags {
> setFlagsTCB :: PPtr TCB,
> setFlagsClear :: Word,
> setFlagsSet :: Word }
> deriving Show

\subsubsection{CNode Invocations}
Expand Down
18 changes: 6 additions & 12 deletions spec/haskell/src/SEL4/Kernel/Hypervisor/AARCH64.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,19 +13,13 @@ import SEL4.Object.Structures
import SEL4.API.Failures
import SEL4.Kernel.FaultHandler
import SEL4.API.Failures.AARCH64
import SEL4.Machine.Hardware.AARCH64 (HypFaultType(..),isFpuEnable,getESR)
import SEL4.Machine.Hardware.AARCH64 (HypFaultType(..),getESR)
import Data.Bits

handleHypervisorFault :: PPtr TCB -> HypFaultType -> Kernel ()
handleHypervisorFault thread (ARMVCPUFault hsr) = do
fpu_enabled <- doMachineOp isFpuEnable
-- the C code makes extra checks on hsr to get to this branch, but the
-- handling of lazy FPU switching is out of scope of verification at this
-- time, so we omit the entire branch where an FPU fault could occur
if not fpu_enabled
then error "Lazy FPU switch is outside of current verification scope"
else if hsr == 0x2000000 -- UNKNOWN_FAULT
then do
esr <- doMachineOp getESR
handleFault thread (UserException (esr .&. mask 32) 0)
else handleFault thread (ArchFault $ VCPUFault $ fromIntegral hsr)
if hsr == 0x2000000 -- UNKNOWN_FAULT
then do
esr <- doMachineOp getESR
handleFault thread (UserException (esr .&. mask 32) 0)
else handleFault thread (ArchFault $ VCPUFault $ fromIntegral hsr)
12 changes: 10 additions & 2 deletions spec/haskell/src/SEL4/Kernel/Thread.lhs
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ We use the C preprocessor to select a target architecture.
\begin{impdetails}

% {-# BOOT-IMPORTS: SEL4.Model SEL4.Machine SEL4.Object.Structures SEL4.Object.Instances() SEL4.API.Types #-}
% {-# BOOT-EXPORTS: setDomain setMCPriority setPriority getThreadState setThreadState setBoundNotification getBoundNotification doIPCTransfer isRunnable restart suspend doReplyTransfer tcbSchedEnqueue tcbSchedDequeue rescheduleRequired timerTick possibleSwitchTo tcbQueueEmpty tcbQueuePrepend tcbQueueAppend tcbQueueInsert tcbQueueRemove #-}
% {-# BOOT-EXPORTS: setDomain setMCPriority setPriority setFlags getThreadState setThreadState setBoundNotification getBoundNotification doIPCTransfer isRunnable restart suspend doReplyTransfer tcbSchedEnqueue tcbSchedDequeue rescheduleRequired timerTick possibleSwitchTo tcbQueueEmpty tcbQueuePrepend tcbQueueAppend tcbQueueInsert tcbQueueRemove #-}

> import Prelude hiding (Word)
> import SEL4.Config
Expand Down Expand Up @@ -308,7 +308,9 @@ has the highest runnable priority in the system on kernel entry (unless idle).
> scheduleChooseNewThread :: Kernel ()
> scheduleChooseNewThread = do
> domainTime <- getDomainTime
> when (domainTime == 0) $ nextDomain
> when (domainTime == 0) $ do
> Arch.prepareNextDomain
> nextDomain
> chooseThread
> setSchedulerAction ResumeCurrentThread

Expand Down Expand Up @@ -457,6 +459,12 @@ The following function is used to alter a thread's domain.
> when runnable $ tcbSchedEnqueue tptr
> when (tptr == curThread) $ rescheduleRequired

\subsubsection{Changing a thread's flags}

> setFlags :: PPtr TCB -> TcbFlags -> Kernel ()
> setFlags tptr flags = do
> threadSet (\t -> t { tcbFlags = flags }) tptr

\subsubsection{Changing a thread's MCP}

> setMCPriority :: PPtr TCB -> Priority -> Kernel ()
Expand Down
6 changes: 6 additions & 0 deletions spec/haskell/src/SEL4/Kernel/Thread/AARCH64.hs
Original file line number Diff line number Diff line change
Expand Up @@ -19,12 +19,15 @@ import {-# SOURCE #-} SEL4.Kernel.Init
import {-# SOURCE #-} SEL4.Object.TCB (asUser, threadGet)
import SEL4.Machine.RegisterSet.AARCH64(Register(..))
import SEL4.Object.VCPU.AARCH64
import SEL4.Object.Structures.AARCH64
import SEL4.Object.FPU.AARCH64

switchToThread :: PPtr TCB -> Kernel ()
switchToThread tcb = do
tcbobj <- getObject tcb
vcpuSwitch (atcbVCPUPtr $ tcbArch tcbobj)
setVMRoot tcb
lazyFpuRestore tcb

configureIdleThread :: PPtr TCB -> KernelInit ()
configureIdleThread _ = error "Unimplemented init code"
Expand All @@ -36,3 +39,6 @@ switchToIdleThread = do

activateIdleThread :: PPtr TCB -> Kernel ()
activateIdleThread _ = return ()

prepareNextDomain :: Kernel ()
prepareNextDomain = switchLocalFpuOwner Nothing
15 changes: 12 additions & 3 deletions spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs
Original file line number Diff line number Diff line change
Expand Up @@ -387,11 +387,20 @@ debugPrint str = liftIO $ putStrLn str

{- FPU Operations -}

fpuThreadDeleteOp :: Word -> MachineMonad ()
fpuThreadDeleteOp tcbPtr = error "Unimplemented callback"
readFpuState :: MachineMonad AARCH64.FPUState
readFpuState = error "Unimplemented - machine op"

writeFpuState :: AARCH64.FPUState -> MachineMonad ()
writeFpuState _ = error "Unimplemented - machine op"

enableFpu :: MachineMonad ()
enableFpu = error "Unimplemented - machine op"

disableFpu :: MachineMonad ()
disableFpu = error "Unimplemented - machine op"

isFpuEnable :: MachineMonad Bool
isFpuEnable = error "Unimplemented - lazy FPU switch abstracted as machine op"
isFpuEnable = error "Unimplemented - machine op"

{- GIC VCPU interface -}

Expand Down
10 changes: 7 additions & 3 deletions spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs
Original file line number Diff line number Diff line change
Expand Up @@ -118,8 +118,7 @@ data FPUState = FPUState { fpuRegs :: Array Int Data.Word.Word64

-- The representation of the user-level context of a thread is an array of
-- machine words, indexed by register name for the user registers, plus the
-- state of the FPU. There are no operations on the FPU state apart from save
-- and restore at kernel entry and exit.
-- state of the FPU.
data UserContext = UC { fromUC :: Array Register Word,
fpuState :: FPUState }
deriving Show
Expand All @@ -134,8 +133,13 @@ newFPUState = FPUState (funPartialArray (const 0) (0,63)) 0 0
newContext :: UserContext
newContext = UC ((funArray $ const 0)//initContext) newFPUState

-- Functions are provided to get and set a single register.
-- Functions are provided to get and set a single register, or to get and set the FPU state.

getRegister r = gets $ (! r) . fromUC

setRegister r v = modify (\ uc -> UC (fromUC uc //[(r, v)]) (fpuState uc))

getFPUState :: State UserContext FPUState
getFPUState = gets fpuState

setFPUState fc = modify (\ uc -> UC (fromUC uc) fc)
4 changes: 3 additions & 1 deletion spec/haskell/src/SEL4/Model/StateData/AARCH64.hs
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ module SEL4.Model.StateData.AARCH64 where
import Prelude hiding (Word)
import SEL4.Machine
import SEL4.Machine.Hardware.AARCH64 (PTE(..), PT_Type, config_ARM_PA_SIZE_BITS_40)
import SEL4.Object.Structures
import SEL4.Object.Structures.AARCH64

import Data.Array
Expand Down Expand Up @@ -41,7 +42,8 @@ data KernelState = ARMKernelState {
armKSGlobalUserVSpace :: PPtr PTE,
armHSCurVCPU :: Maybe (PPtr VCPU, Bool),
armKSGICVCPUNumListRegs :: Int,
gsPTTypes :: Word -> Maybe PT_Type
gsPTTypes :: Word -> Maybe PT_Type,
armKSCurFPUOwner :: Maybe (PPtr TCB)
}

-- counting from 0 at bottom, i.e. number of levels = maxPTLevel + 1;
Expand Down
54 changes: 54 additions & 0 deletions spec/haskell/src/SEL4/Object/FPU/AARCH64.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
--
-- Copyright 2024, Proofcraft Pty Ltd
--
-- SPDX-License-Identifier: GPL-2.0-only
--

{-# LANGUAGE CPP #-}

module SEL4.Object.FPU.AARCH64 where

import SEL4.Machine
import SEL4.Model
import SEL4.Object.Structures
import SEL4.Machine.Hardware.AARCH64
import SEL4.Machine.RegisterSet.AARCH64
import SEL4.Model.StateData.AARCH64
import {-# SOURCE #-} SEL4.Object.TCB(asUser, threadGet)

import Data.Bits
import Data.Maybe

saveFpuState :: PPtr TCB -> Kernel ()
saveFpuState tcbPtr = do
fpuState <- doMachineOp readFpuState
asUser tcbPtr (setFPUState fpuState)

loadFpuState :: PPtr TCB -> Kernel ()
loadFpuState tcbPtr = do
fpuState <- asUser tcbPtr getFPUState
doMachineOp (writeFpuState fpuState)

switchLocalFpuOwner :: Maybe (PPtr TCB) -> Kernel ()
switchLocalFpuOwner newOwner = do
doMachineOp enableFpu
curFpuOwner <- gets (armKSCurFPUOwner . ksArchState)
when (isJust curFpuOwner) (saveFpuState (fromJust curFpuOwner))
if isJust newOwner
then loadFpuState (fromJust newOwner)
else doMachineOp disableFpu
modifyArchState (\s -> s { armKSCurFPUOwner = newOwner })

fpuRelease :: PPtr TCB -> Kernel ()
fpuRelease tcbPtr = do
curFpuOwner <- gets (armKSCurFPUOwner . ksArchState)
when (curFpuOwner /= Just tcbPtr) (switchLocalFpuOwner Nothing)

lazyFpuRestore :: PPtr TCB -> Kernel ()
lazyFpuRestore tcbPtr = do
flags <- threadGet tcbFlags tcbPtr
if (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0)
then doMachineOp disableFpu
else do
doMachineOp enableFpu
switchLocalFpuOwner (Just tcbPtr)
1 change: 1 addition & 0 deletions spec/haskell/src/SEL4/Object/Instances.lhs
Original file line number Diff line number Diff line change
Expand Up @@ -140,6 +140,7 @@ By default, new threads are unable to change the security domains of other threa
> tcbBoundNotification = Nothing,
> tcbSchedPrev = Nothing,
> tcbSchedNext = Nothing,
> tcbFlags = 0,
> tcbArch = newArchTCB }
> injectKO = KOTCB
> projectKO o = case o of
Expand Down
2 changes: 2 additions & 0 deletions spec/haskell/src/SEL4/Object/ObjectType.lhs
Original file line number Diff line number Diff line change
Expand Up @@ -45,6 +45,7 @@ We use the C preprocessor to select a target architecture.
The architecture-specific definitions are imported qualified with the "Arch" prefix.

> import qualified SEL4.Object.ObjectType.TARGET as Arch
> import qualified SEL4.Object.TCB.TARGET as Arch(prepareSetDomain)

\subsection{Creating Capabilities}

Expand Down Expand Up @@ -461,6 +462,7 @@ This function just dispatches invocations to the type-specific invocation functi
> performInvocation _ _ (InvokeTCB invok) = invokeTCB invok
>
> performInvocation _ _ (InvokeDomain thread domain) = withoutPreemption $ do
> Arch.prepareSetDomain thread domain
> setDomain thread domain
> return $ []
>
Expand Down
7 changes: 2 additions & 5 deletions spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs
Original file line number Diff line number Diff line change
Expand Up @@ -23,6 +23,7 @@ import SEL4.Object.Structures
import SEL4.Kernel.VSpace.AARCH64
import SEL4.Object.VCPU.AARCH64
import {-# SOURCE #-} SEL4.Object.TCB
import SEL4.Object.FPU.AARCH64

import Data.Bits
import Data.Word(Word16)
Expand Down Expand Up @@ -246,13 +247,9 @@ capUntypedSize (VCPUCap {}) = bit vcpuBits

-- Thread deletion requires associated FPU cleanup

fpuThreadDelete :: PPtr TCB -> Kernel ()
fpuThreadDelete threadPtr =
doMachineOp $ fpuThreadDeleteOp (fromPPtr threadPtr)

prepareThreadDelete :: PPtr TCB -> Kernel ()
prepareThreadDelete thread = do
fpuThreadDelete thread
fpuRelease thread
tcbVCPU <- archThreadGet atcbVCPUPtr thread
case tcbVCPU of
Just ptr -> dissociateVCPUTCB ptr thread
Expand Down
Loading

0 comments on commit bfd342f

Please sign in to comment.