manual/parts/vspace.tex

9 A virtual address space in seL4 is called a VSpace. In a similar
10 way to a CSpace (see \autoref{ch:cspace}), a VSpace is composed of objects
14 Common to every architecture is the \obj{Page}, representing a frame of physical memory.
30 For each architecture, the VSpace is realised as a different object, as determined by the
34 or a specifically sized frame of memory, can be mapped. If the previous level is not mapped,
37 for that level, is hardware defined.
42 the capability to the corresponding object is invoked with a map operation, where the top-level
43 structure is passed as an argument.
45 In general, the top-level structure has no invocations for mapping, but is used as an argument to
58 On IA-32, the VSpace is realised as a \texttt{PageDirectory}, which covers the entire 4\,GiB range
72 On x86-64, the VSpace is realised as a \texttt{PML4}. Three further levels of paging structure are
103 ARM AArch64 processors have a four-level page-table structure, where the VSpace is realised as a
117 RISC-V provides the same paging structure for all levels, \texttt{PageTable}. The VSpace is then
148 A \obj{Page} object corresponds to a frame of physical memory that is used to
157 that is being invoked must have read permissions. To map the page
247 For internal kernel book-keeping purposes, there is a fixed maximum
250 capability. The \obj{ASID Control} capability is used to generate a
252 This newly created capability is called an
268 must be assigned to an ASID. This is done using a capability to an
282 \texttt{seL4\_x86\_VMAttributes} is used to specify the cache behaviour of the