1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(GD_GPL) 9% 10 11This module defines the high-level structures used to represent the 12state of the entire system, and the types and functions used to 13perform basic operations on the state. 14 15\begin{impdetails} 16 17We use the C preprocessor to select a target architecture. 18 19> {-# LANGUAGE CPP #-} 20 21\end{impdetails} 22 23> module SEL4.Model.StateData ( 24> module SEL4.Model.StateData, 25> module Control.Monad, get, gets, put, modify, 26> ) where 27 28The architecture-specific definitions are imported qualified with the "Arch" prefix. 29 30> import Prelude hiding (Word) 31> import qualified SEL4.Model.StateData.TARGET as Arch 32 33\begin{impdetails} 34 35> import SEL4.Config (numDomains) 36> import SEL4.API.Types 37> import {-# SOURCE #-} SEL4.Model.PSpace 38> import SEL4.Object.Structures 39> import SEL4.Machine 40> import SEL4.Machine.Hardware.TARGET (VMPageSize) 41 42> import Data.Array 43> import qualified Data.Set 44> import Data.Helpers 45> import Data.WordLib 46> import Control.Monad 47> import Control.Monad.State 48 49\end{impdetails} 50 51\subsection{Types} 52 53\subsubsection{Kernel State} 54 55The top-level kernel state structure is called "KernelState". It contains: 56 57> data KernelState = KState { 58 59\begin{itemize} 60\item the physical address space, of type "PSpace" (defined in \autoref{sec:model.pspace}); 61 62> ksPSpace :: PSpace, 63 64\item ghost state, i.e. meta-information about the kernel objects living in "PSpace"; 65 66> gsUserPages :: Word -> (Maybe VMPageSize), 67> gsCNodes :: Word -> (Maybe Int), 68> gsUntypedZeroRanges :: Data.Set.Set (Word, Word), 69 70\item the cyclic domain schedule; 71 72> ksDomScheduleIdx :: Int, 73> ksDomSchedule :: [DomainSchedule], 74 75\item the active security domain and the number to ticks remaining before it changes; 76 77> ksCurDomain :: Domain, 78> ksDomainTime :: Word, 79 80\item an array of ready queues, indexed by thread priority and domain (see "getQueue"); 81 82> ksReadyQueues :: Array (Domain, Priority) ReadyQueue, 83 84\item a bitmap for each domain; each bit represents the presence of a runnable thread for a specific priority 85 86> ksReadyQueuesL1Bitmap :: Array (Domain) Word, 87> ksReadyQueuesL2Bitmap :: Array (Domain, Int) Word, 88 89\item a pointer to the current thread's control block; 90 91> ksCurThread :: PPtr TCB, 92 93\item a pointer to the idle thread's control block; 94 95> ksIdleThread :: PPtr TCB, 96 97\item the required action of the scheduler next time it runs; 98 99> ksSchedulerAction :: SchedulerAction, 100 101\item the interrupt controller's state data; 102 103> ksInterruptState :: InterruptState, 104 105\item the number of preemption point runs where IRQs have not been checked 106 107> ksWorkUnitsCompleted :: Word, 108 109\item and some architecture-defined state data. 110 111> ksArchState :: Arch.KernelState } 112 113\end{itemize} 114 115Note that this definition of "KernelState" assumes a single processor. The behaviour of the kernel on multi-processor systems is not specified by this document. 116 117Note that the priority bitmap is split up into two levels. In order to check to see whether a priority has a runnable thread on a 32-bit system with a maximum priority of 255, we use the high 3 bits of the priority as an index into the level 1 bitmap. If the bit at that index is set, we use those same three bits to obtain a word from the level 2 bitmap. We then use the remaining 5 bits to index into that word. If the bit is set, the queue for that priority is non-empty. 118 119Note also that due the common case being scheduling high-priority threads, the level 2 bitmap array is reversed to improve cache locality. 120 121\subsubsection{Monads} 122 123Kernel functions are sequences of operations that transform a "KernelState" object. They are encapsulated in the monad "Kernel", which uses "StateT" to add a "KernelState" data structure to the monad that encapsulates the simulated machine, "MachineMonad". This allows functions to read and modify the kernel state. 124 125> type Kernel = StateT KernelState MachineMonad 126 127Note that there is no error-signalling mechanism available to functions in "Kernel". Therefore, all errors encountered in such functions are fatal, and will halt the kernel. See \autoref{sec:model.failures} for the definition of monads used for error handling. 128 129\subsubsection{Scheduler Queues} 130 131The ready queue is simply a list of threads that are ready to 132run. Each thread in this list is at the same priority level. 133 134> type ReadyQueue = [PPtr TCB] 135 136This is a standard Haskell singly-linked list independent of the 137thread control block structures. However, in a real implementation, it 138would most likely be embedded in the thread control blocks themselves. 139 140\subsection{Kernel State Functions} 141 142The following two functions are used to get and set the value of the 143current thread pointer which is stored in the kernel state. 144 145\begin{impdetails} 146 147These functions have the same basic form as many 148others in the kernel which fetch or set the value of some part of the 149state data. They make use of "gets" and "modify", two functions which 150each apply a given function to the current state --- either returning 151some value extracted from the state, or calculating a new state which 152replaces the previous one. 153 154\end{impdetails} 155 156> getCurThread :: Kernel (PPtr TCB) 157> getCurThread = gets ksCurThread 158 159> setCurThread :: PPtr TCB -> Kernel () 160> setCurThread tptr = modify (\ks -> ks { ksCurThread = tptr }) 161 162Similarly, these functions access the idle thread pointer, the ready queue for a given priority level (adjusted to account for the active security domain), the requested action of the scheduler, and the interrupt handler state. 163 164> getIdleThread :: Kernel (PPtr TCB) 165> getIdleThread = gets ksIdleThread 166 167> setIdleThread :: PPtr TCB -> Kernel () 168> setIdleThread tptr = modify (\ks -> ks { ksIdleThread = tptr }) 169 170> getQueue :: Domain -> Priority -> Kernel ReadyQueue 171> getQueue qdom prio = gets (\ks -> ksReadyQueues ks ! (qdom, prio)) 172 173> setQueue :: Domain -> Priority -> ReadyQueue -> Kernel () 174> setQueue qdom prio q = modify (\ks -> ks { ksReadyQueues = (ksReadyQueues ks)//[((qdom, prio),q)] }) 175 176> getSchedulerAction :: Kernel SchedulerAction 177> getSchedulerAction = gets ksSchedulerAction 178 179> setSchedulerAction :: SchedulerAction -> Kernel () 180> setSchedulerAction a = modify (\ks -> ks { ksSchedulerAction = a }) 181 182> getInterruptState :: Kernel InterruptState 183> getInterruptState = gets ksInterruptState 184 185> setInterruptState :: InterruptState -> Kernel () 186> setInterruptState a = modify (\ks -> ks { ksInterruptState = a }) 187 188> getWorkUnits :: Kernel Word 189> getWorkUnits = gets ksWorkUnitsCompleted 190 191> setWorkUnits :: Word -> Kernel () 192> setWorkUnits a = modify (\ks -> ks { ksWorkUnitsCompleted = a }) 193 194> modifyWorkUnits :: (Word -> Word) -> Kernel () 195> modifyWorkUnits f = modify (\ks -> ks { ksWorkUnitsCompleted = 196> f (ksWorkUnitsCompleted ks) }) 197 198TODO use this where update is restricted to arch state instead of fiddling in place 199 200> modifyArchState :: (Arch.KernelState -> Arch.KernelState) -> Kernel () 201> modifyArchState f = modify (\s -> s { ksArchState = f (ksArchState s) }) 202 203These functions access and modify the current domain and the number of ticks remaining until the current domain changes. 204 205> curDomain :: Kernel Domain 206> curDomain = gets ksCurDomain 207 208> nextDomain :: Kernel () 209> nextDomain = modify (\ks -> 210> let ksDomScheduleIdx' = (ksDomScheduleIdx ks + 1) `mod` length (ksDomSchedule ks) in 211> let next = ksDomSchedule ks !! ksDomScheduleIdx' 212> in ks { ksWorkUnitsCompleted = 0, 213> ksDomScheduleIdx = ksDomScheduleIdx', 214> ksCurDomain = dschDomain next, 215> ksDomainTime = dschLength next }) 216 217> getDomainTime :: Kernel Word 218> getDomainTime = gets ksDomainTime 219 220> decDomainTime :: Kernel () 221> decDomainTime = modify (\ks -> ks { ksDomainTime = ksDomainTime ks - 1 }) 222 223\subsection{Initial Kernel State} 224 225A new kernel state structure contains an empty physical address space, a set of empty scheduler queues, and undefined values for the other global variables, which must be set during the bootstrap sequence. 226 227> newKernelState :: PAddr -> (KernelState, [PAddr]) 228> newKernelState data_start = (state', frames) where 229> state' = KState { 230> ksPSpace = newPSpace, 231> gsUserPages = (\_ -> Nothing), 232> gsCNodes = (\_ -> Nothing), 233> gsUntypedZeroRanges = Data.Set.empty, 234> ksDomScheduleIdx = 0, 235> ksDomSchedule = [(0, 15), (2, 42), (1, 73)], 236> ksCurDomain = 0, 237> ksDomainTime = 15, 238> ksReadyQueues = 239> funPartialArray (const []) 240> ((0, 0), (fromIntegral numDomains, maxPriority)), 241> ksReadyQueuesL1Bitmap = funPartialArray (const 0) (0, fromIntegral numDomains), 242> ksReadyQueuesL2Bitmap = 243> funPartialArray (const 0) 244> ((0, 0), (fromIntegral numDomains, l2BitmapSize)), 245> ksCurThread = error "No initial thread", 246> ksIdleThread = error "Idle thread has not been created", 247> ksSchedulerAction = error "scheduler action has not been set", 248> ksInterruptState = error "Interrupt controller is uninitialised", 249> ksWorkUnitsCompleted = 0, 250> ksArchState = archState } 251> (archState, frames) = Arch.newKernelState data_start 252 253\subsection{Performing Machine Operations} 254 255The following function allows the machine monad to be directly accessed from kernel code. 256 257> doMachineOp :: MachineMonad a -> Kernel a 258> doMachineOp = lift 259 260\subsection{Miscellaneous Monad Functions} 261 262\subsubsection{Assertions and Undefined Behaviour} 263 264The function "assert" is used to state that a predicate must be true at a given point. If it is not, the behaviour of the kernel is undefined. The Haskell model will not terminate in this case. 265 266> assert :: Monad m => Bool -> String -> m () 267> assert p e = if p then return () else fail $ "Assertion failed: " ++ e 268 269The function "stateAssert" is similar to "assert", except that it reads the current state. This is typically used for more complex assertions that cannot be easily expressed in Haskell; in this case, the asserted function is "const True" in Haskell but is replaced with something stronger in the Isabelle translation. 270 271> stateAssert :: (KernelState -> Bool) -> String -> Kernel () 272> stateAssert f e = get >>= \s -> assert (f s) e 273 274The "capHasProperty" function is used with "stateAssert". As explained above, it is "const True" here, but is strengthened to actually check the capability in the translation to Isabelle. 275 276> capHasProperty :: PPtr CTE -> (Capability -> Bool) -> KernelState -> Bool 277> capHasProperty _ _ = const True 278 279\subsubsection{Searching a List} 280 281The function "findM" searches a list, returning the first item for which the given function returns "True". It is the monadic equivalent of "Data.List.find". 282 283> findM :: Monad m => (a -> m Bool) -> [a] -> m (Maybe a) 284> findM _ [] = return Nothing 285> findM f (x:xs) = do 286> r <- f x 287> if r then return $ Just x else findM f xs 288 289 290