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 <gerwin.klein@proofcraft.systems>

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.