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