content: %
  % Copyright 2014, General Dynamics C4 Systems
  %
  % SPDX-License-Identifier: GPL-2.0-only
  %
  
  Each thread has a virtual memory address space, possibly shared with other threads.
  
  The representation of the virtual address space is implementation-defined. On many architectures --- those with software-loaded TLBs, for example --- it will simply be a second CSpace structure, possibly identical to or a subtree of the thread's main CSpace. On others, such as those with hardware-defined page table structures, it must be constructed using implementation-defined kernel objects.
  
  \begin{impdetails}
  
  We use the C preprocessor to select a target architecture.
  
  > {-# LANGUAGE CPP #-}
  
  \end{impdetails}
  
  > module SEL4.Kernel.VSpace where
  
  \begin{impdetails}
  
  % {-# BOOT-IMPORTS: SEL4.Machine SEL4.Model SEL4.Object.Structures SEL4.API.Failures #-}
  % {-# BOOT-EXPORTS: lookupIPCBuffer isValidVTableRoot checkValidIPCBuffer #-}
  
  > import Prelude hiding (Word)
  > import SEL4.Machine
  > import SEL4.Model
  > import SEL4.Object
  > import SEL4.API.Failures
  > import SEL4.API.Types
  > import {-# SOURCE #-} SEL4.Kernel.Init
  > import Data.Word(Word32)
  
  \end{impdetails}
  
  The architecture-specific definitions are imported qualified with the "Arch" prefix.
  
  > import qualified SEL4.Kernel.VSpace.TARGET as Arch
  
  \subsection{Implementation-defined Functions}
  
  This module defines architecture-specific virtual memory management procedures. The operations required are:
  
  \begin{itemize}
  
  \item preparing the virtual memory environment, if any, that the kernel requires to run;
  
  > initKernelVM :: Kernel ()
  > initKernelVM = Arch.mapKernelWindow
  
  > initPlatform :: Kernel ()
  > initPlatform = do
  >   doMachineOp $ initIRQController
  >   doMachineOp $ configureTimer
  >   doMachineOp $ initL2Cache
  
  > initCPU :: Kernel ()
  > initCPU = Arch.activateGlobalVSpace
  
  
  > createIPCBufferFrame :: Capability -> VPtr -> KernelInit Capability
  > createIPCBufferFrame  = Arch.createIPCBufferFrame
  
  > createBIFrame :: Capability -> VPtr -> Word32 -> Word32 -> KernelInit Capability
  > createBIFrame  = Arch.createBIFrame
  
  > createFramesOfRegion :: Capability -> Region -> Bool -> KernelInit ()
  > createFramesOfRegion = Arch.createFramesOfRegion
  
  > createITPDPTs :: Capability -> VPtr -> VPtr -> KernelInit Capability
  > createITPDPTs = Arch.createITPDPTs
  
  > writeITPDPTs :: Capability -> Capability -> KernelInit ()
  > writeITPDPTs = Arch.writeITPDPTs
  
  > createITASIDPool :: Capability -> KernelInit Capability
  > createITASIDPool = Arch.createITASIDPool
  
  > writeITASIDPool :: Capability -> Capability -> Kernel ()
  > writeITASIDPool = Arch.writeITASIDPool
  
  > createDeviceFrames :: Capability -> KernelInit ()
  > createDeviceFrames = Arch.createDeviceFrames
  
  
  \item handling virtual memory faults, given the current thread, the faulting address, and a boolean value that is true for write accesses;
  
  > handleVMFault :: PPtr TCB -> VMFaultType -> KernelF Fault ()
  > handleVMFault = Arch.handleVMFault
  
  \item determining whether a given capability is a valid VSpace root;
  
  > isValidVTableRoot :: Capability -> Bool
  > isValidVTableRoot = Arch.isValidVTableRoot
  
  \item determining whether a given capability is a valid IPC buffer frame that can contain the given virtual address;
  
  > checkValidIPCBuffer :: VPtr -> Capability -> KernelF SyscallError ()
  > checkValidIPCBuffer = Arch.checkValidIPCBuffer
  
  \item locating the IPC buffer for a given thread;
  
  > lookupIPCBuffer :: Bool -> PPtr TCB -> Kernel (Maybe (PPtr Word))
  > lookupIPCBuffer = Arch.lookupIPCBuffer
  
  \item determining the virtual address of user process in kernel init
  
  > vptrFromPPtr :: PPtr a -> KernelInit VPtr
  > vptrFromPPtr = Arch.vptrFromPPtr
  
  \end{itemize}
  
  