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 11\chapter{\label{ch:vspace}Address Spaces and Virtual Memory} 12 13A virtual address space in seL4 is called a VSpace. In a similar 14way to a CSpace (see \autoref{ch:cspace}), a VSpace is composed of objects 15provided by the microkernel. Unlike CSpaces, these objects for managing 16virtual memory largely correspond to those of the hardware. Consequently, 17each architecture defines its own objects for the top-level VSpace and further intermediate paging structures. 18Common to every architecture is the \obj{Page}, representing a frame of physical memory. 19The kernel also includes \obj{ASID Pool} and 20\obj{ASID Control} objects for tracking the status of address spaces. 21 22These VSpace-related objects are sufficient to implement the 23hardware data structures required to create, manipulate, and destroy 24virtual memory address spaces. It should be noted that, as usual, the 25manipulator of a virtual memory space needs the appropriate 26capabilities to the required objects. 27 28\section{Objects} 29 30\subsection{Hardware Virtual Memory Objects} 31 32Each architecture has a top-level paging structure (level 0) and a number of intermediate levels. 33The top-level paging structure corresponds directly to the higher-level concept of a VSpace in seL4. 34For each architecture, the VSpace is realised as a different object, as determined by the 35architectural details. 36 37In general, each paging structure at each level contains slots where the next level paging structure, 38or a specifically sized frame of memory, can be mapped. If the previous level is not mapped, 39a mapping operation will fail. Developers need to manually create and map all paging structures. 40The size and type of structure at each level, and the number of bits in the virtual address resolved 41for that level, is hardware defined. 42 43seL4 provides methods for operating on these 44hardware paging structures including mapping and cache operations. Mapping operations are invoked on 45the capability being mapped, e.g. to map a level 1 paging structure at a specific virtual address, 46the capability to the corresponding object is invoked with a map operation, where the top-level 47structure is passed as an argument. 48 49In general, the top-level structure has no invocations for mapping, but is used as an argument to 50several other virtual-memory related object invocations. 51For some architectures, the top-level page table can be invoked for cache operations. 52By making these cache related operations invocations on page directory capabilities in addition to 53the page capabilities themselves, the 54API allows users more flexible policy options. For example, a process that has delegated a page 55directory can conduct cache operations on all frames mapped from that capability without access 56to those capabilities directly. 57 58The rest of this section details the paging structures for each architecture. 59 60\subsubsection{IA-32} 61 62On IA-32, the VSpace is realised as a \texttt{PageDirectory}, which covers the entire 4\,GiB range 63in the 32-bit address space, and forms the top-level paging structure. Second level page-tables 64(\texttt{PageTable} objects) each cover a 4\,MiB range. 65Structures at both levels are indexed by 10 bits in the virtual address. 66 67\begin{tabularx}{\textwidth}{Xlll} \toprule 68\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule 69\texttt{PageDirectory} & 22---31 & 0 & \autoref{group__x86__seL4__X86__PageDirectory} \\ 70\texttt{PageTable} & 12---21 & 1 & \autoref{group__x86__seL4__X86__PageTable} \\ 71\bottomrule 72\end{tabularx} 73 74\subsubsection{x64} 75 76On x86-64, the VSpace is realised as a \texttt{PML4}. Three further levels of paging structure are 77defined, as shown in the table below. All structures are indexed with 9 bits of the virtual 78address. 79 80\begin{tabularx}{\textwidth}{Xlll} \toprule 81\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule 82\texttt{PML4} & 39---47 & 0 & None \\ 83\texttt{PDPT} & 30---38 & 1 & \autoref{group__x86__64__seL4__X86__PDPT} \\ 84\texttt{PageDirectory} & 21---29 & 2 & \autoref{group__x86__seL4__X86__PageDirectory} \\ 85\texttt{PageTable} & 12---20 & 3 & \autoref{group__x86__seL4__X86__PageTable} \\ 86\bottomrule 87\end{tabularx} 88 89\subsubsection{AArch32} 90 91Like IA-32, ARM AArch32 realise the VSpace as a \texttt{PageDirectory}, which covers the entire 924\,GiB address range, and a second-level \texttt{PageTable}. The second-level structures on AArch32 93cover 1\,MiB address ranges. 94 95ARM AArch32 processors have a two-level page-table structure. 96The top-level page directory covers a range of 4\,GiB and each page table covers a 1\,MiB range. 97 98\begin{tabularx}{\textwidth}{Xlll} \toprule 99\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule 100\texttt{PageDirectory} & 20---31 & 0 & \autoref{group__aarch32__seL4__ARM__PageDirectory} \\ 101\texttt{PageTable} & 12---19 & 1 & \autoref{group__arm__seL4__ARM__PageTable} \\ 102\bottomrule 103\end{tabularx} 104 105\subsubsection{AArch64} 106 107ARM AArch64 processors have a four-level page-table structure, where the VSpace is realised as a 108\texttt{PageGlobalDirectory}. All paging structures are index by 9 bits of the virtual address. 109 110\begin{tabularx}{\textwidth}{Xlll} \toprule 111\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule 112 \texttt{PageGlobalDirectory} & 39---47 & 0 & \autoref{group__aarch64__seL4__ARM__PageGlobalDirectory} \\ 113 \texttt{PageUpperDirectory} & 30---38 & 1 & \autoref{group__aarch64__seL4__ARM__PageUpperDirectory} \\ 114\texttt{PageDirectory} & 21---29 & 2 & \autoref{group__aarch64__seL4__ARM__PageDirectory} \\ 115\texttt{PageTable} & 12---20 & 3 & \autoref{group__arm__seL4__ARM__PageTable} \\ 116\bottomrule 117\end{tabularx} 118 119\subsection{RISC-V} 120 121RISC-V provides the same paging structure for all levels, \texttt{PageTable}. The VSpace is then 122realised as a \texttt{PageTable}. 123 124\subsubsection{RISC-V 32-bit} 125 12632-bit RISC-V \texttt{PageTables} are indexed by 10 bits of virtual address. 127 128\begin{tabularx}{\textwidth}{Xlll} \toprule 129\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule 130\texttt{PageTable} & 22---31 & 0 & \autoref{group__riscv__seL4__RISCV__PageTable} \\ 131\texttt{PageTable} & 12---21 & 1 & \autoref{group__riscv__seL4__RISCV__PageTable} \\ 132\bottomrule 133\end{tabularx} 134 135\subsubsection{RISC-V 64-bit} 136 13764-bit RISC-V follows the SV39 model, where \texttt{PageTables} are indexed by 9 bits of virtual address. 138Although RISC-V allows 139for multiple different numbers of paging levels, currently seL4 only supports exactly three levels 140of paging structures. 141 142\begin{tabularx}{\textwidth}{Xlll} \toprule 143\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule 144\texttt{PageTable} & 30---38 & 0 & \autoref{group__riscv__seL4__RISCV__PageTable} \\ 145\texttt{PageTable} & 21---29 & 1 & \autoref{group__riscv__seL4__RISCV__PageTable} \\ 146\texttt{PageTable} & 12---20 & 2 & \autoref{group__riscv__seL4__RISCV__PageTable} \\ 147\bottomrule 148\end{tabularx} 149 150\subsection{Page} 151 152A \obj{Page} object corresponds to a frame of physical memory that is used to 153implement virtual memory pages in a virtual address space. 154 155The virtual address for a \obj{Page} mapping 156must be aligned to 157the size of the \obj{Page} and must be mapped to a suitable VSpace, and every intermediate paging 158structure required. 159To map a page readable, the capability 160to the page 161that is being invoked must have read permissions. To map the page 162writeable, the capability must have write permissions. The requested 163mapping permissions are specified with an argument of type 164\texttt{seL4\_CapRights} given to the mapping function. 165If the capability does not have 166sufficient permissions to authorise the given mapping, then 167the mapping permissions are silently downgraded. Specific mapping permissions are dependant on the 168architecture and are documented in the \autoref{sec:api_reference} for each function. 169 170At minimum, each architecture defines \texttt{Map}, \texttt{Unmap},\texttt{Remap} and 171\texttt{GetAddress} methods for pages. 172Methods for page objects for each architecture can be found in the \autoref{sec:api_reference}, and 173are indexed per architecture in the table below. 174 175\begin{tabularx}{\textwidth}{Xl} \toprule 176\emph{Architectures} & \emph{Methods} \\ \midrule 177IA32, X64 & \autoref{group__x86__seL4__X86__Page} \\ 178AArch32, AArch64 & \autoref{group__arm__seL4__ARM__Page} \\ 179 RISC-V & \autoref{group__riscv__seL4__RISCV__Page} \\ 180\bottomrule 181\end{tabularx} 182 183Each architecture also defines a range of page sizes. In the next section we show the available page 184sizes, as well as the \emph{mapping level}, which refers to 185the level of the paging structure at which this page must be mapped. 186 187\subsubsection{AArch32 page sizes} 188 189\begin{tabularx}{\textwidth}{Xll} \toprule 190 \emph{Constant} & \emph{Size} & \emph{Mapping level} \\ \midrule 191 \texttt{seL4\_PageBits} & 4\,KiB & 1 \\ 192 \texttt{seL4\_LargePageBits} & 64\,KiB & 1 \\ 193 \texttt{seL4\_SectionBits} & 1\,MiB & 0 \\ 194 \texttt{seL4\_SuperSectionBits} & 16\,MiB & 0 \\ 195 \bottomrule 196\end{tabularx} 197 198Mappings for sections and super sections consume 16 slots in the page table and page directory 199respectively. 200 201\subsubsection{AArch64 page sizes} 202 203\begin{tabularx}{\textwidth}{Xll} \toprule 204 \emph{Constant} & \emph{Size} & \emph{Mapping level} \\ \midrule 205 \texttt{seL4\_PageBits} & 4\,KiB & 3 \\ 206 \texttt{seL4\_LargePageBits} & 2\,MiB & 2 \\ 207 \texttt{seL4\_HugePageBits} & 1\,GiB & 1 \\ 208 \bottomrule 209\end{tabularx} 210 211\subsubsection{IA-32 page sizes} 212 213\begin{tabularx}{\textwidth}{Xll} \toprule 214 \emph{Constant} & \emph{Size} & \emph{Mapping level} \\ \midrule 215 \texttt{seL4\_PageBits} & 4\,KiB & 1 \\ 216 \texttt{seL4\_LargePageBits} & 4\,MiB & 0 \\ 217 \bottomrule 218\end{tabularx} 219 220\subsubsection{X64 page sizes} 221 222\begin{tabularx}{\textwidth}{Xll} \toprule 223 \emph{Constant} & \emph{Size} & \emph{Mapping level} \\ \midrule 224 \texttt{seL4\_PageBits} & 4\,KiB & 3 \\ 225 \texttt{seL4\_LargePageBits} & 2\,MiB & 2 \\ 226 \texttt{seL4\_HugePageBits} & 1\,GiB & 1 \\ 227 \bottomrule 228\end{tabularx} 229 230\subsubsection{RISC-V 32-bit page sizes} 231 232\begin{tabularx}{\textwidth}{Xll} \toprule 233 \emph{Constant} & \emph{Size} & \emph{Mapping level} \\ \midrule 234 \texttt{seL4\_PageBits} & 4\,KiB & 1 \\ 235 \texttt{seL4\_LargePageBits} & 4\,MiB & 0 \\ 236 \texttt{seL4\_HugePageBits} & 512\,MiB & 0 \\ 237 \bottomrule 238\end{tabularx} 239 240\subsubsection{RISC-V 64-bit page sizes} 241 242\begin{tabularx}{\textwidth}{Xll} \toprule 243 \emph{Constant} & \emph{Size} & \emph{Mapping level} \\ \midrule 244 \texttt{seL4\_PageBits} & 4\,KiB & 2 \\ 245 \texttt{seL4\_LargePageBits} & 2\,MiB & 1 \\ 246 \texttt{seL4\_HugePageBits} & 1\,GiB & 0 \\ 247 \bottomrule 248\end{tabularx} 249 250\subsection{ASID Control} 251 252For internal kernel book-keeping purposes, there is a fixed maximum 253number of applications the system can support. In order to manage 254this limited resource, the microkernel provides an \obj{ASID Control} 255capability. The \obj{ASID Control} capability is used to generate a 256capability that authorises the use of a subset of available address-space identifiers. 257This newly created capability is called an 258\obj{ASID Pool}. \obj{ASID Control} only has a single \texttt{MakePool} method for each 259architecture, listed in the table below. 260 261\begin{tabularx}{\textwidth}{Xl} \toprule 262\emph{Architectures} & \emph{Methods} \\ \midrule 263IA32, X64 & \autoref{group__x86__seL4__X86__ASIDControl} \\ 264AArch32, AArch64 & \autoref{group__arm__seL4__ARM__ASIDControl} \\ 265RISC-V & \autoref{group__riscv__seL4__RISCV__ASIDControl} \\ 266\bottomrule 267\end{tabularx} 268 269\subsection{ASID Pool} 270 271An \obj{ASID Pool} confers the right to create a subset of the available 272maximum applications. For a VSpace to be usable by an application, it 273must be assigned to an ASID. This is done using a capability to an 274\obj{ASID Pool}. The \obj{ASID Pool} object has a single method, \texttt{Assign}, for each 275architecture: 276 277\begin{tabularx}{\textwidth}{Xl} \toprule 278\emph{Architectures} & \emph{Methods} \\ \midrule 279IA32, X64 & \autoref{group__x86__seL4__X86__ASIDPool} \\ 280AArch32, AArch64 & \autoref{group__arm__seL4__ARM__ASIDPool} \\ 281RISC-V & \autoref{group__riscv__seL4__RISCV__ASIDPool} \\ 282\bottomrule 283\end{tabularx} 284 285\section{Mapping Attributes} 286A parameter of type \texttt{seL4\_ARM\_VMAttributes} or 287\texttt{seL4\_x86\_VMAttributes} is used to specify the cache behaviour of the 288page being mapped; possible values for ARM that can be bitwise OR'd together are 289shown in \autoref{tbl:vmattr_arm} \ifxeightsix and an enumeration of valid values 290for IA-32 are shown in \autoref{tbl:vmattr_ia32}\fi. 291 292\begin{table}[htb] 293 \begin{center} 294 \begin{tabularx}{\textwidth}{p{0.33\textwidth}X} 295 \toprule 296 Attribute & Meaning \\ 297 \midrule 298 \texttt{seL4\_ARM\_PageCacheable} & Enable data in this mapping 299 to be cached \\ 300 \texttt{seL4\_ARM\_ParityEnabled} & Enable parity checking for 301 this mapping\\ 302 \texttt{seL4\_ARM\_ExecuteNever} & Map this memory as non-executable \\ 303 \bottomrule 304 \end{tabularx} 305 \caption{\label{tbl:vmattr_arm} Virtual memory attributes for ARM page 306 table entries.} 307 \end{center} 308\end{table} 309 310\begin{table}[htb] 311 \begin{center} 312 \begin{tabularx}{\textwidth}{p{0.33\textwidth}X} 313 \toprule 314 Attribute & Meaning \\ 315 \midrule 316 \texttt{seL4\_x86\_WriteBack} & Read and writes are cached \\ 317 \texttt{seL4\_x86\_CacheDisabled} & Prevent data in this mapping 318 from being cached \\ 319 \texttt{seL4\_x86\_WriteThrough} & Enable write through cacheing for this mapping \\ 320 \texttt{seL4\_x86\_WriteCombining} & Enable write combining for this mapping \\ 321 \bottomrule 322 \end{tabularx} 323 \caption{\label{tbl:vmattr_ia32} Virtual memory attributes for x86 page 324 table entries.} 325 \end{center} 326\end{table} 327 328\section{Sharing Memory} 329 330seL4 does not allow \obj{Page Table}s to be shared, but does allow 331pages to be shared between address spaces. 332To share a page, the capability to the 333\obj{Page} must first be 334duplicated using the \apifunc{seL4\_CNode\_Copy}{cnode_copy} method and the new copy must 335be used in the \apifunc{seL4\_ARM\_Page\_Map}{arm_page_map} \ifxeightsix or \apifunc{seL4\_x86\_Page\_Map}{x86_page_map} \fi method that maps the page into the second 336address space. Attempting to map the same capability 337twice will result in an error. 338 339 340\section{Page Faults} 341 342Page faults are reported to the exception handler of the executed thread. 343See \autoref{sec:vm-fault}. 344