aarch64 haskell+design: update exec spec to use semi-lazy FPU switching

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

spec/design/m-skel/AARCH64/MachineTypes.thy

@@ -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
 (*<*)
@@ -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"
 

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)

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)

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

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 \

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
 

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

spec/design/skel/TCB_H.thy

@@ -22,6 +22,7 @@ arch_requalify_consts (H)
   msgRegisters
   fromVPtr
   postModifyRegisters
+  postSetFlags
   sanitiseRegister
   getSanitiseRegisterInfo
 

spec/design/skel/Thread_H.thy

@@ -31,6 +31,7 @@ requalify_consts (aliasing)
   configureIdleThread
   switchToIdleThread
   switchToThread
+  prepareNextDomain
 
 context begin global_naming global
 

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

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}

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)

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 ()

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

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 -}
 

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)

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;

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)

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

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 $ []
 >

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