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 contains definitions of the types and functions that the kernel uses for interaction with the hardware, such as performing memory accesses and controlling virtual memory mappings.
12
13The functions and types in this module are required for all architectures. Specific architectures may define additional functions and types in their respective modules.
14
15\begin{impdetails}
16
17We use the C preprocessor to select a target architecture. Also, this file makes use of the GHC extension allowing derivation of arbitrary type classes for types defined with "newtype".
18
19> {-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-}
20
21\end{impdetails}
22
23> module SEL4.Machine.Hardware where
24
25\begin{impdetails}
26
27> import Prelude hiding (Word)
28> import SEL4.Machine.RegisterSet
29> import Control.Monad(liftM)
30
31> import Data.Ix
32
33\end{impdetails}
34
35The architecture-specific definitions are imported qualified with the "Arch" prefix.
36
37> import qualified SEL4.Machine.Hardware.TARGET as Arch
38
39\subsection{Types}
40
41\subsubsection{Hardware Monad}
42
43Each simulator must define a monad that encapsulates the state of the underlying hardware.
44
45> type MachineMonad = Arch.MachineMonad
46
47> initL2Cache :: MachineMonad ()
48> initL2Cache = return ()
49
50\subsubsection{Physical Addresses}
51
52Depending on the architecture, real physical addresses may be the same as the addresses the kernel uses to access kernel objects, or they may be offset by a constant. The "PAddr" type is used to represent a real physical address; functions are provided that convert between this and the kernel pointer type, "PPtr".
53
54> type PAddr = Arch.PAddr
55
56> ptrFromPAddr :: PAddr -> PPtr a
57> ptrFromPAddr = Arch.ptrFromPAddr
58
59> addrFromPPtr :: PPtr a -> PAddr
60> addrFromPPtr = Arch.addrFromPPtr
61
62> fromPAddr = Arch.fromPAddr
63
64\subsubsection{Interrupts}
65
66An interrupt request from an external device, or from the CPU's timer, is represented by the type "IRQ".
67
68> newtype IRQ = IRQ Arch.IRQ
69>     deriving (Enum, Bounded, Ord, Ix, Eq, Show)
70
71The maximum and minimum IRQ are given explicit constant names here. In Haskell, these are extracted from instantiation of IRQ into the Bounded class. In the formalisation, these constants are specified directly.
72
73> minIRQ :: IRQ
74> minIRQ = minBound
75
76> maxIRQ :: IRQ
77> maxIRQ = maxBound
78
79\subsubsection{Virtual Memory and Hypervisor Faults}
80
81Most architectures provide some information about virtual memory and hypervisor faults in hardware registers. Other information is implied by the hardware's choice between a set of different trap handlers. The latter is represented in this model by the following data types.
82
83> type VMFaultType = Arch.VMFaultType
84
85> type HypFaultType = Arch.HypFaultType
86
87\subsection{Hardware Operations}
88
89The simulator must define several operations on the underlying hardware. These operations are used by the kernel to determine the configuration of the hardware, and to perform privileged operations such as virtual memory and interrupt management.
90
91\subsubsection{Hardware Configuration}
92
93These operations are used to determine the configuration of the machine:
94
95\begin{itemize}
96\item the number of address bits covered by a virtual page;
97
98> pageBits :: Int
99> pageBits = Arch.pageBits
100
101\item the start and end addresses (plus one) of the regions of the physical address space occupied by free physical memory (ie, physical memory other than the kernel code and stack);
102
103> getMemoryRegions :: MachineMonad [(PAddr, PAddr)]
104> getMemoryRegions = Arch.getMemoryRegions
105
106\item the start and end addresses (plus one) of the regions of the physical address space occupied by memory-mapped I/O devices that are not accessed by the kernel;
107
108> getDeviceRegions :: MachineMonad [(PAddr, PAddr)]
109> getDeviceRegions = Arch.getDeviceRegions
110
111\item and the base addresses, kernel-accessible addresses and sizes (in address bits) of the memory-mapped I/O devices that the kernel uses internally.
112
113> getKernelDevices :: MachineMonad [(PAddr, PPtr Word)]
114> getKernelDevices = Arch.getKernelDevices
115
116\end{itemize}
117
118\subsubsection{Memory Accesses}
119
120These operations load or store a word in the physical address space.
121
122> loadWord :: PPtr Word -> MachineMonad Word
123> loadWord = Arch.loadWord
124
125> storeWord :: PPtr Word -> Word -> MachineMonad ()
126> storeWord = Arch.storeWord
127
128This storeWord operation is for caching virtual memory/page table writes in simulator environments. (Instead on relying on PTE/PDE values in PSpace)
129
130> storeWordVM :: PPtr Word -> Word -> MachineMonad ()
131> storeWordVM = Arch.storeWordVM
132
133\subsubsection{Virtual Memory Management}
134
135Before a user task is given direct access to the contents of a memory region, the region must be cleared, to avoid leaking information belonging to the kernel or another user task. This is an architecture-specific operation because it may require a cache flush.
136
137> clearMemory :: PPtr Word -> Int -> MachineMonad ()
138> clearMemory = Arch.clearMemory
139
140This function is called to free a region of user-memory after use.
141
142> freeMemory :: PPtr Word -> Int -> MachineMonad ()
143> freeMemory = Arch.freeMemory
144
145The following constant is used to determine the correct page colouring when allocating the initial task's IPC buffer; it is the number of bits of the virtual page number that are significant in determining the page colour. It is zero if there are no page colouring restrictions.
146
147> pageColourBits :: Int
148> pageColourBits = Arch.pageColourBits
149
150\subsubsection{Interrupts}
151
152After receiving an Interrupt event, or at preemption points, the kernel calls this function to check for any pending interrupts which might preempt the kernel. If there are any, it returns the one with highest priority. In a real kernel, this would be implemented by briefly enabling interrupts.
153
154> getActiveIRQ :: Bool -> MachineMonad (Maybe IRQ)
155> getActiveIRQ inPreempt = liftM (liftM IRQ) (Arch.getActiveIRQ inPreempt)
156
157This function is used to enable or disable a specific interrupt, either when its handler is set or cleared, or when an IRQ has been forwarded to a user level handler and not yet acknowledged. If the argument is "True", delivery of the specified interrupt to the kernel will be disabled; otherwise it will be enabled.
158
159> maskInterrupt :: Bool -> IRQ -> MachineMonad ()
160> maskInterrupt mask' (IRQ irq) = Arch.maskInterrupt mask' irq
161
162This function is used by the kernel to acknowledge an interrupt, after it has been handled by the kernel or forwarded to user level. If a user level handler is called, the interrupt will be disabled before calling this function.
163
164> ackInterrupt :: IRQ -> MachineMonad ()
165> ackInterrupt (IRQ irq) = Arch.ackInterrupt irq
166
167This function is used to init interrupt chip
168
169> initIRQController :: MachineMonad ()
170> initIRQController = Arch.initIRQController
171
172
173\subsubsection{Timers}
174
175The timer interval is set at boot time by calling this function. It returns the IRQ that is used for timer interrupts.
176
177> configureTimer :: MachineMonad IRQ
178> configureTimer = liftM IRQ Arch.configureTimer
179
180The kernel calls this function after handling a timer interrupt, but before acknowledging it. It should take whatever action is necessary to clear the interrupt and reset the timer.
181
182> resetTimer :: MachineMonad ()
183> resetTimer = Arch.resetTimer
184
185\subsubsection{Debugging}
186
187This operation prints a debugging message to the console.
188
189> debugPrint :: String -> MachineMonad ()
190> debugPrint = Arch.debugPrint
191
192\subsection{User Context Operations}
193
194There are also two functions that perform specific operations on the register set. These are used to fetch and set the program counter. We must use functions here, rather than aliases for register names, because the handling of these registers may differ significantly depending on the architecture and the type of fault. These functions:
195
196\begin{itemize}
197\item fetch the address of the instruction that is currently executing, from the user level thread's point of view (such as a system call instruction, or an instruction which accesses virtual memory and has faulted);
198
199> getRestartPC :: UserMonad Word
200> getRestartPC = Arch.getRestartPC
201
202\item and set the address of the next instruction to be executed, which by default is the instruction after the current one.
203
204> setNextPC :: Word -> UserMonad ()
205> setNextPC = Arch.setNextPC
206
207\end{itemize}
208
209The value read by "getRestartPC" should also appear in "frameRegisters", while the value set by "setNextPC" should not be directly accessible to user level code. This is necessary even if the hardware uses a single physical register for both values. It ensures that "CopyRegisters" reads the current instruction address and sets the next instruction address, no matter how the thread last entered the kernel.
210
211\subsection{Constants}
212
213The constant "nullPointer" is a physical pointer guaranteed to be invalid.
214
215> nullPointer :: PPtr a
216> nullPointer = PPtr 0
217
218