Lines Matching refs:a
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.
21 manipulator of a virtual memory space needs the appropriate
28 Each architecture has a top-level paging structure (level 0) and a number of intermediate levels.
29 The top-level paging structure corresponds directly to the higher-level concept of a VSpace in seL4.
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,
35 a mapping operation will fail. Developers need to manually create and map all paging structures.
41 the capability being mapped, e.g. to map a level 1 paging structure at a specific virtual address,
42 the capability to the corresponding object is invoked with a map operation, where the top-level
50 API allows users more flexible policy options. For example, a process that has delegated a page
58 On IA-32, the VSpace is realised as a \texttt{PageDirectory}, which covers the entire 4\,GiB range
60 (\texttt{PageTable} objects) each cover a 4\,MiB range.
72 On x86-64, the VSpace is realised as a \texttt{PML4}. Three further levels of paging structure are
87 Like IA-32, Arm AArch32 realise the VSpace as a \texttt{PageDirectory}, which covers the entire
88 4\,GiB address range, and a second-level \texttt{PageTable}. The second-level structures on AArch32
91 Arm AArch32 processors have a two-level page-table structure.
92 The top-level page directory covers a range of 4\,GiB and each page table covers a 1\,MiB range.
103 Arm AArch64 processors have a four-level page-table structure, where the VSpace is realised as a
118 realised as a \texttt{PageTable}.
148 A \obj{Page} object corresponds to a frame of physical memory that is used to
149 implement virtual memory pages in a virtual address space.
151 The virtual address for a \obj{Page} mapping
153 the size of the \obj{Page} and must be mapped to a suitable VSpace, and every intermediate paging
155 To map a page readable, the capability
179 Each architecture also defines a range of page sizes. In the next section we show the available 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
251 capability that authorises the use of a subset of available address-space identifiers.
253 \obj{ASID Pool}. \obj{ASID Control} only has a single \texttt{MakePool} method for each
266 An \obj{ASID Pool} confers the right to create a subset of the available
267 maximum applications. For a VSpace to be usable by an application, it
268 must 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
327 To share a page, the capability to the