From bfd342f980e0bd46eeede5cb318de9df2e24ee57 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Mon, 23 Sep 2024 21:26:54 +1000 Subject: [PATCH] aarch64 haskell+design: update exec spec to use semi-lazy FPU switching Signed-off-by: Corey Lewis --- spec/design/m-skel/AARCH64/MachineTypes.thy | 4 +- spec/design/skel/AARCH64/ArchTCB_H.thy | 4 +- spec/design/skel/AARCH64/ArchThread_H.thy | 1 + spec/design/skel/AARCH64/FPU_H.thy | 19 +++++++ spec/design/skel/AARCH64/Hardware_H.thy | 2 +- spec/design/skel/Retype_H.thy | 2 +- spec/design/skel/Structures_H.thy | 2 + spec/design/skel/TCB_H.thy | 1 + spec/design/skel/Thread_H.thy | 1 + spec/haskell/SEL4.cabal | 1 + spec/haskell/src/SEL4/API/Invocation.lhs | 4 ++ .../src/SEL4/Kernel/Hypervisor/AARCH64.hs | 18 +++---- spec/haskell/src/SEL4/Kernel/Thread.lhs | 12 ++++- .../haskell/src/SEL4/Kernel/Thread/AARCH64.hs | 6 +++ .../src/SEL4/Machine/Hardware/AARCH64.hs | 15 ++++-- .../src/SEL4/Machine/RegisterSet/AARCH64.hs | 10 ++-- .../src/SEL4/Model/StateData/AARCH64.hs | 4 +- spec/haskell/src/SEL4/Object/FPU/AARCH64.hs | 54 +++++++++++++++++++ spec/haskell/src/SEL4/Object/Instances.lhs | 1 + spec/haskell/src/SEL4/Object/ObjectType.lhs | 2 + .../src/SEL4/Object/ObjectType/AARCH64.hs | 7 +-- spec/haskell/src/SEL4/Object/Structures.lhs | 16 ++++++ .../src/SEL4/Object/Structures/AARCH64.hs | 5 ++ spec/haskell/src/SEL4/Object/TCB.lhs | 17 ++++++ spec/haskell/src/SEL4/Object/TCB/AARCH64.hs | 11 ++++ 25 files changed, 188 insertions(+), 31 deletions(-) create mode 100644 spec/design/skel/AARCH64/FPU_H.thy create mode 100644 spec/haskell/src/SEL4/Object/FPU/AARCH64.hs diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy index 8c518e2c8f..b30c896846 100644 --- a/spec/design/m-skel/AARCH64/MachineTypes.thy +++ b/spec/design/m-skel/AARCH64/MachineTypes.thy @@ -26,7 +26,7 @@ text \ 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 (*<*) @@ -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" diff --git a/spec/design/skel/AARCH64/ArchTCB_H.thy b/spec/design/skel/AARCH64/ArchTCB_H.thy index 39085e3663..b18ea5c2c6 100644 --- a/spec/design/skel/AARCH64/ArchTCB_H.thy +++ b/spec/design/skel/AARCH64/ArchTCB_H.thy @@ -5,7 +5,9 @@ *) theory ArchTCB_H -imports TCBDecls_H +imports + TCBDecls_H + FPU_H begin context Arch begin arch_global_naming (H) diff --git a/spec/design/skel/AARCH64/ArchThread_H.thy b/spec/design/skel/AARCH64/ArchThread_H.thy index 3cb95f63f9..0450df8db6 100644 --- a/spec/design/skel/AARCH64/ArchThread_H.thy +++ b/spec/design/skel/AARCH64/ArchThread_H.thy @@ -13,6 +13,7 @@ imports TCBDecls_H ArchVSpaceDecls_H ArchHypervisor_H + FPU_H begin context Arch begin arch_global_naming (H) diff --git a/spec/design/skel/AARCH64/FPU_H.thy b/spec/design/skel/AARCH64/FPU_H.thy new file mode 100644 index 0000000000..a5fb57f6c5 --- /dev/null +++ b/spec/design/skel/AARCH64/FPU_H.thy @@ -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 diff --git a/spec/design/skel/AARCH64/Hardware_H.thy b/spec/design/skel/AARCH64/Hardware_H.thy index 9c1e2074f1..366f8ba550 100644 --- a/spec/design/skel/AARCH64/Hardware_H.thy +++ b/spec/design/skel/AARCH64/Hardware_H.thy @@ -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 \ diff --git a/spec/design/skel/Retype_H.thy b/spec/design/skel/Retype_H.thy index 6d325434e8..6ed9c02303 100644 --- a/spec/design/skel/Retype_H.thy +++ b/spec/design/skel/Retype_H.thy @@ -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 diff --git a/spec/design/skel/Structures_H.thy b/spec/design/skel/Structures_H.thy index 833ba5f48c..87a164b281 100644 --- a/spec/design/skel/Structures_H.thy +++ b/spec/design/skel/Structures_H.thy @@ -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 diff --git a/spec/design/skel/TCB_H.thy b/spec/design/skel/TCB_H.thy index 5c9b070e1c..cb1473f135 100644 --- a/spec/design/skel/TCB_H.thy +++ b/spec/design/skel/TCB_H.thy @@ -22,6 +22,7 @@ arch_requalify_consts (H) msgRegisters fromVPtr postModifyRegisters + postSetFlags sanitiseRegister getSanitiseRegisterInfo diff --git a/spec/design/skel/Thread_H.thy b/spec/design/skel/Thread_H.thy index 7464c3c6aa..e78cda95c8 100644 --- a/spec/design/skel/Thread_H.thy +++ b/spec/design/skel/Thread_H.thy @@ -31,6 +31,7 @@ requalify_consts (aliasing) configureIdleThread switchToIdleThread switchToThread + prepareNextDomain context begin global_naming global diff --git a/spec/haskell/SEL4.cabal b/spec/haskell/SEL4.cabal index a23531ee62..3232861b9e 100644 --- a/spec/haskell/SEL4.cabal +++ b/spec/haskell/SEL4.cabal @@ -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 diff --git a/spec/haskell/src/SEL4/API/Invocation.lhs b/spec/haskell/src/SEL4/API/Invocation.lhs index 6997554773..de4819c427 100644 --- a/spec/haskell/src/SEL4/API/Invocation.lhs +++ b/spec/haskell/src/SEL4/API/Invocation.lhs @@ -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} diff --git a/spec/haskell/src/SEL4/Kernel/Hypervisor/AARCH64.hs b/spec/haskell/src/SEL4/Kernel/Hypervisor/AARCH64.hs index cd9e2790d7..82242c4f9b 100644 --- a/spec/haskell/src/SEL4/Kernel/Hypervisor/AARCH64.hs +++ b/spec/haskell/src/SEL4/Kernel/Hypervisor/AARCH64.hs @@ -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) diff --git a/spec/haskell/src/SEL4/Kernel/Thread.lhs b/spec/haskell/src/SEL4/Kernel/Thread.lhs index e3215bd567..68e0292c5a 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread.lhs +++ b/spec/haskell/src/SEL4/Kernel/Thread.lhs @@ -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 @@ -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 @@ -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 () diff --git a/spec/haskell/src/SEL4/Kernel/Thread/AARCH64.hs b/spec/haskell/src/SEL4/Kernel/Thread/AARCH64.hs index 9329e5a30d..3aad6af2ec 100644 --- a/spec/haskell/src/SEL4/Kernel/Thread/AARCH64.hs +++ b/spec/haskell/src/SEL4/Kernel/Thread/AARCH64.hs @@ -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" @@ -36,3 +39,6 @@ switchToIdleThread = do activateIdleThread :: PPtr TCB -> Kernel () activateIdleThread _ = return () + +prepareNextDomain :: Kernel () +prepareNextDomain = switchLocalFpuOwner Nothing diff --git a/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs b/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs index 2e452b472b..ceeeffb7e1 100644 --- a/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs +++ b/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs @@ -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 -} diff --git a/spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs b/spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs index 7bf4414118..03c684deb5 100644 --- a/spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs +++ b/spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs @@ -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 @@ -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) diff --git a/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs b/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs index 037fd06e5b..6fdaea0fe6 100644 --- a/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs +++ b/spec/haskell/src/SEL4/Model/StateData/AARCH64.hs @@ -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 @@ -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; diff --git a/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs b/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs new file mode 100644 index 0000000000..08114ac63f --- /dev/null +++ b/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs @@ -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) diff --git a/spec/haskell/src/SEL4/Object/Instances.lhs b/spec/haskell/src/SEL4/Object/Instances.lhs index eb20a91117..e06b7c74dc 100644 --- a/spec/haskell/src/SEL4/Object/Instances.lhs +++ b/spec/haskell/src/SEL4/Object/Instances.lhs @@ -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 diff --git a/spec/haskell/src/SEL4/Object/ObjectType.lhs b/spec/haskell/src/SEL4/Object/ObjectType.lhs index 8fc24967ab..6a8ffb8e0d 100644 --- a/spec/haskell/src/SEL4/Object/ObjectType.lhs +++ b/spec/haskell/src/SEL4/Object/ObjectType.lhs @@ -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} @@ -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 $ [] > diff --git a/spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs b/spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs index b71e018100..b55a5ce762 100644 --- a/spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs +++ b/spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs @@ -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) @@ -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 diff --git a/spec/haskell/src/SEL4/Object/Structures.lhs b/spec/haskell/src/SEL4/Object/Structures.lhs index d3d1263e40..5cd0c0eefe 100644 --- a/spec/haskell/src/SEL4/Object/Structures.lhs +++ b/spec/haskell/src/SEL4/Object/Structures.lhs @@ -283,6 +283,10 @@ The TCB is used to store various data about the thread's current state: > tcbSchedPrev :: Maybe (PPtr TCB), > tcbSchedNext :: Maybe (PPtr TCB), +\item the thread's feature flags, currently only used for fpuDisabled + +> tcbFlags :: TcbFlags, + \item and any arch-specific TCB contents > tcbArch :: ArchTCB } @@ -492,3 +496,15 @@ Various operations on the free index of an Untyped cap. > data TcbQueue = TcbQueue { > tcbQueueHead :: Maybe (PPtr TCB), > tcbQueueEnd :: Maybe (PPtr TCB) } + +\subsubsection{TCB Flags} + +> type TcbFlags = Word + +> data TcbFlag +> = NoFlag +> | ArchFlag ArchTcbFlag + +> tcbFlagToWord :: TcbFlag -> Word +> tcbFlagToWord NoFlag = 0x0 +> tcbFlagToWord (ArchFlag archFlag) = archTcbFlagToWord archFlag diff --git a/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs b/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs index aa1d6ec3ac..2bbe4dc10b 100644 --- a/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs +++ b/spec/haskell/src/SEL4/Object/Structures/AARCH64.hs @@ -70,6 +70,11 @@ atcbContextSet uc atcb = atcb { atcbContext = uc } atcbContextGet :: ArchTCB -> UserContext atcbContextGet = atcbContext +data ArchTcbFlag = FpuDisabled + +archTcbFlagToWord :: ArchTcbFlag -> Word +archTcbFlagToWord (FpuDisabled) = 0x1 + {- ASID Pools -} diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs index 20b8195638..7e142cd3c9 100644 --- a/spec/haskell/src/SEL4/Object/TCB.lhs +++ b/spec/haskell/src/SEL4/Object/TCB.lhs @@ -85,6 +85,7 @@ There are eleven types of invocation for a thread control block. All require wri > TCBBindNotification -> decodeBindNotification cap extraCaps > TCBUnbindNotification -> decodeUnbindNotification cap > TCBSetTLSBase -> decodeSetTLSBase args cap +> TCBSetFlags -> decodeSetFlags args cap > _ -> throw IllegalOperation \subsubsection{Reading, Writing and Copying Registers} @@ -377,6 +378,14 @@ This is to ensure that the source capability is not made invalid by the deletion > setTLSBaseNewBase = tls_base } > decodeSetTLSBase _ _ = throw TruncatedMessage +> decodeSetFlags :: [Word] -> Capability -> +> KernelF SyscallError TCBInvocation +> decodeSetFlags (flagsClear:flagsSet:_) cap = do +> return $ SetFlags { +> setFlagsTCB = capTCBPtr cap, +> setFlagsClear = flagsClear, +> setFlagsSet = flagsSet } +> decodeSetFlags _ _ = throw TruncatedMessage \subsection[invoke]{Performing TCB Invocations} @@ -545,6 +554,14 @@ Modifying the current thread may require rescheduling because modified registers > when (tcb == cur) rescheduleRequired > return [] +> invokeTCB (SetFlags tcb flagsClear flagsSet) = +> withoutPreemption $ do +> flags <- threadGet tcbFlags tcb +> let newFlags = (flags .&. complement flagsClear) .|. flagsSet +> setFlags tcb newFlags +> Arch.postSetFlags tcb newFlags +> return [] + \subsection{Decoding Domain Invocations} The domain cap is invoked to set the domain of a given TCB object to a given value. diff --git a/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs b/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs index f96ed14f96..113e012784 100644 --- a/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs +++ b/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs @@ -20,11 +20,13 @@ import SEL4.Machine(PPtr) import SEL4.Model import SEL4.Object.Structures import SEL4.Object.Instances() +import SEL4.API.Types import SEL4.API.Failures import SEL4.API.Invocation.AARCH64 import SEL4.Machine.RegisterSet(setRegister, UserMonad, VPtr(..)) import qualified SEL4.Machine.RegisterSet as RegisterSet(Register(..)) import SEL4.Machine.RegisterSet.AARCH64(Register(..), Word) +import SEL4.Object.FPU.AARCH64 import Data.Bits import Data.Maybe import Data.Word(Word8) @@ -51,3 +53,12 @@ getSanitiseRegisterInfo t = do postModifyRegisters :: PPtr TCB -> PPtr TCB -> UserMonad () postModifyRegisters _ _ = return () + +postSetFlags :: PPtr TCB -> TcbFlags -> Kernel () +postSetFlags t flags = + when (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) (fpuRelease t) + +prepareSetDomain :: PPtr TCB -> Domain -> Kernel () +prepareSetDomain t newDom = do + curDom <- curDomain + when (curDom /= newDom) (fpuRelease t)