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