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