From e4c0e561d6f30fa9287769e85df390b97648962b Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sat, 25 Mar 2023 12:11:55 +1100 Subject: [PATCH] manual: describe VSpace objects more explicitly Rework the intro to the VSpace section for slightly improved clarity and a more explicit definition of the distinctions between VSpace and VSpace object, and between frame object and page capability. Addresses #564 Signed-off-by: Gerwin Klein --- manual/parts/vspace.tex | 70 +++++++++++++++++++++-------------------- 1 file changed, 36 insertions(+), 34 deletions(-) diff --git a/manual/parts/vspace.tex b/manual/parts/vspace.tex index c5b53080c..239a6b011 100644 --- a/manual/parts/vspace.tex +++ b/manual/parts/vspace.tex @@ -6,50 +6,52 @@ \chapter{\label{ch:vspace}Address Spaces and Virtual Memory} -A virtual address space in seL4 is called a VSpace. In a similar -way to a CSpace (see \autoref{ch:cspace}), a VSpace is composed of objects -provided by the microkernel. Unlike CSpaces, these objects for managing -virtual memory largely correspond to those of the hardware. Consequently, -each architecture defines its own objects for the top-level VSpace and further intermediate paging structures. -Common to every architecture is the \obj{Page}, representing a frame of physical memory. -The kernel also includes \obj{ASID Pool} and -\obj{ASID Control} objects for tracking the status of address spaces. +A virtual address space in seL4 is called a VSpace. Similarly to a CSpace (see \autoref{ch:cspace}), +a VSpace is composed of objects provided by the kernel. Unlike CSpaces, objects for managing virtual +memory correspond to those of the hardware and each architecture defines its own object types for +paging structures. Also unlike CSpaces, we call only the top-level paging structure a VSpace object. +It provides the top-level authority to the VSpace. -These VSpace-related objects are sufficient to implement the -hardware data structures required to create, manipulate, and destroy -virtual memory address spaces. It should be noted that, as usual, the -manipulator of a virtual memory space needs the appropriate -capabilities to the required objects. +Common to all architectures is the \obj{Frame}, representing a frame of physical memory. Frame +objects are manipulated via \obj{Page} capabilities, which represents both authority to the frame, +as well as to the virtual memory mapping, i.e.\ the page, when mapped. The kernel also provides +\obj{ASID Pool} objects and \obj{ASID Control} invocations for tracking the status of address space +identifiers for VSpaces. + +These VSpace-related objects are sufficient to implement the hardware data structures required to +create, manipulate, and destroy virtual memory address spaces. As usual, the manipulator of a +virtual memory space needs the appropriate capabilities to the required objects. \section{Objects} \subsection{Hardware Virtual Memory Objects} Each architecture has a top-level paging structure (level 0) and a number of intermediate levels. -The top-level paging structure corresponds directly to the higher-level concept of a VSpace in seL4. -For each architecture, the VSpace is realised as a different object, as determined by the -architectural details. +When referring to it generically, we call this top-level paging structure the VSpace object. The +seL4 object type that implements the VSpace object is architecture dependent. For instance on +AArch32, a VSpace is represented by the PageDirectory object and on x64 by a PML4 object. -In general, each paging structure at each level contains slots where the next level paging structure, -or a specifically sized frame of memory, can be mapped. If the previous level is not mapped, -a mapping operation will fail. Developers need to manually create and map all paging structures. -The size and type of structure at each level, and the number of bits in the virtual address resolved -for that level, is hardware defined. +In general, each paging structure at each level contains slots where either the next level paging +structure or a frame of memory can be mapped. The level of the paging structure determines the size +of the frame. The size and type of structure at each level, and the number of bits in the virtual +address resolved for that level are hardware defined. -seL4 provides methods for operating on these -hardware paging structures including mapping and cache operations. Mapping operations are invoked on -the capability being mapped, e.g. to map a level 1 paging structure at a specific virtual address, -the capability to the corresponding object is invoked with a map operation, where the top-level -structure is passed as an argument. +The seL4 kernel provides methods for operating on these hardware paging structures including mapping +and cache operations. Mapping operations are invoked on the capability to the object being mapped. +For example, to map a level 2 paging structure at a specific virtual address, we can invoke the map +operation on the capability to the level 2 object and provide the virtual address as well as the +capability to the level 1 object as arguments. -In general, the top-level structure has no invocations for mapping, but is used as an argument to -several other virtual-memory related object invocations. -For some architectures, the top-level page table can be invoked for cache operations. -By making these cache related operations invocations on page directory capabilities in addition to -the page capabilities themselves, the -API allows users more flexible policy options. For example, a process that has delegated a page -directory can conduct cache operations on all frames mapped from that capability without access -to those capabilities directly. +If the previous level (level 1 in the example) is not itself already mapped, the mapping operation +will fail. Developers need to create and map all paging structures, the kernel does not +automatically create intermediate levels. + +In general, the VSpace object (the top-level paging structure) has no invocations for mapping, but +is used as an argument to several other virtual-memory related object invocations. For some +architectures, the VSpace object provides cache operation invocations. This allows simpler +policy options: a process that has delegated a VSpace capability (e.g.\ to a page directory on +AArch32) can conduct cache operations on all frames mapped from that capability without needing +access to those capabilities directly. The rest of this section details the paging structures for each architecture.