Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-09 08:49:54 +00:00
Code Issues Packages Projects Releases Wiki Activity

manual: clarify VSpace as top-level paging structure

Browse Source 
This change updates the vspace chapter to separate the high-level concept of a VSpace from the
architectually defined objects. It also updates the various names for the vspace parameter to all be
vspace.
This commit is contained in:
Anna Lyons
2018-05-10 13:36:46 +10:00
parent 804fc54942
commit 17b901d79f
4 changed files with 61 additions and 32 deletions
Download Patch File Download Diff File Expand all files Collapse all files

12
libsel4/arch_include/arm/interfaces/sel4arch.xml
View File

@@ -22,7 +22,7 @@
and installs a reference to the invoked
<texttt text='PageTable'/> in a specified slot in the <texttt text="PageDirectory"/>.
</description>
<param dir="in" name="pd" type="seL4_CPtr"
<param dir="in" name="vspace" type="seL4_CPtr"
description="Capability to the VSpace which will contain the mapping."/>
<param dir="in" name="vaddr" type="seL4_Word"
description="Virtual address to map the page into."/>
@@ -63,7 +63,7 @@
corresponding to the given address. If the required paging structures are not present
this operation will fail, returning a seL4_FailedLookup error.
</description>
<param dir="in" name="pd" type="seL4_CPtr"
<param dir="in" name="vspace" type="seL4_CPtr"
description="Capability to the VSpace which will contain the mapping."/>
<param dir="in" name="vaddr" type="seL4_Word"
description="Virtual address to map the page into."/>
@@ -85,7 +85,7 @@
<description>
Changes the permissions of an existing mapping.
</description>
<param dir="in" name="pd" type="seL4_CPtr"
<param dir="in" name="vspace" type="seL4_CPtr"
description="Capability to the VSpace which will contain the mapping."/>
<param dir="in" name="rights" type="seL4_CapRights_t">
<description>
@@ -218,10 +218,10 @@
Assign an ASID Pool.
</brief>
<description>
Assigns an ASID to the VSpace associated with the <texttt text="Page Directory"/> passed in as an argument.
Assigns an ASID to the VSpace passed in as an argument.
</description>
<param dir="in" name="vroot" type="seL4_CPtr"
description="The page directory that is being assigned to an ASID pool. Must not already be assigned to an ASID pool."/>
<param dir="in" name="vspace" type="seL4_CPtr"
description="The VSpace that is being assigned to an ASID pool. Must not already be assigned to an ASID pool."/>
</method>
</interface>
<interface name="seL4_ARM_VCPU" manual_name="VCPU">

25
libsel4/arch_include/riscv/interfaces/sel4arch.xml
View File

@@ -39,13 +39,13 @@
<interface name="seL4_RISCV_PageTable" manual_name="Page Table" cap_description="Capability to the page table to invoke.">
<method id="RISCVPageTableMap" name="Map" manual_label="pagetable_map">
<brief>
Map a page table into a higher-level page table.
Map a page table at a specific virtual address.
</brief>
<description>
<docref>See <autoref label="ch:vspace"/></docref>
Starting from the VSpace, map the page table object at any unpopulated level for the provided virtual address. If all paging structures and mappings are present for this virtual address, return an seL4_DeleteFirst error.
</description>
<param dir="in" name="pt" type="seL4_RISCV_PageTable">
<description>Higher-level page table to map the lower-level page table into.</description>
<param dir="in" name="vspace" type="seL4_RISCV_PageTable">
<description>VSpace to map the lower-level page table into.</description>
</param>
<param dir="in" name="vaddr" type="seL4_Word">
<description>Virtual address at which to map the page table.</description>
@@ -72,13 +72,14 @@
Map a page into a page table.
</brief>
<description>
Takes a <texttt text="Page Table"/> capability as an argument and installs a reference
Takes a VSpace, or top-level <texttt text="Page Table"/>,
capability as an argument and installs a reference
to the given <texttt text="Page"/> in the page table slot corresponding to the given address.
If the required paging structures are not present
this operation will fail, returning a seL4_FailedLookup error.
</description>
<param dir="in" name="pt" type="seL4_RISCV_PageTable">
<description>Page table to map the page into.</description>
<param dir="in" name="vspace" type="seL4_RISCV_PageTable">
<description>VSpace to map the page into.</description>
</param>
<param dir="in" name="vaddr" type="seL4_Word">
<description>Virtual address at which to map the page.</description>
@@ -102,8 +103,8 @@
<description>
Changes the permissions of an existing mapping.
</description>
<param dir="in" name="pt" type="seL4_RISCV_PageTable">
<description>Page table to remap the page into.</description>
<param dir="in" name="vspace" type="seL4_RISCV_PageTable">
<description>VSpace to remap the page into.</description>
</param>
<param dir="in" name="rights" type="seL4_CapRights_t">
<description>
@@ -168,11 +169,11 @@
Assign an ASID Pool.
</brief>
<description>
Assigns an ASID to the VSpace associated with the <texttt text="Page Directory"/> passed in as an argument.
Assigns an ASID to the VSpace passed in as an argument.
</description>
<param dir="in" name="vroot" type="seL4_CPtr">
<param dir="in" name="vspace" type="seL4_CPtr">
<description>
The top level page table that is being assigned to an ASID pool. Must not already be assigned
The top-level <texttt text="PageTable" /> that is being assigned to an ASID pool. Must not already be assigned
to an ASID pool.
</description>
</param>

12
libsel4/arch_include/x86/interfaces/sel4arch.xml
View File

@@ -29,7 +29,7 @@
<description>
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<param dir="in" name="vroot" type="seL4_CPtr"
<param dir="in" name="vspace" type="seL4_CPtr"
description='Capability to the VSpace which will contain the mapping'/>
<param dir="in" name="vaddr" type="seL4_Word"
description='Virtual address to map the page into.'/>
@@ -75,7 +75,7 @@
and installs a reference to the invoked
<texttt text='PageTable'/> in a specified slot in the <texttt text="PageDirectory"/>.
</description>
<param dir="in" name="vroot" type="seL4_CPtr"
<param dir="in" name="vspace" type="seL4_CPtr"
description='Capability to the VSpace which will contain the mapping'/>
<param dir="in" name="vaddr" type="seL4_Word"
description='Virtual address to map the page into.'/>
@@ -134,7 +134,7 @@
corresponding to the given address. If the required paging structures are not present
this operation will fail, returning a seL4_FailedLookup error.
</description>
<param dir="in" name="vroot" type="seL4_CPtr"
<param dir="in" name="vspace" type="seL4_CPtr"
description='Capability to the VSpace which will contain the mapping'/>
<param dir="in" name="vaddr" type="seL4_Word"
description='Virtual address to map the page into.'/>
@@ -156,7 +156,7 @@
<description>
Changes the permissions of an existing mapping.
</description>
<param dir="in" name="vroot" type="seL4_CPtr"
<param dir="in" name="vspace" type="seL4_CPtr"
description='Capability to the VSpace which will contain the mapping'/>
<param dir="in" name="rights" type="seL4_CapRights_t">
<description>
@@ -211,7 +211,7 @@
<param dir="out" name="paddr" type="seL4_Word"/>
</method>
<method id="X86PageMapEPT" name="MapEPT" condition="defined(CONFIG_VTX)" manual_name="Map EPT">
<param dir="in" name="vroot" type="seL4_X86_EPTPML4"/>
<param dir="in" name="vspace" type="seL4_X86_EPTPML4"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="rights" type="seL4_CapRights_t"/>
<param dir="in" name="attr" type="seL4_X86_VMAttributes"/>
@@ -250,7 +250,7 @@
Assigns an ASID to the VSpace associated with the <texttt text="Page Directory"/> passed in as an argument.
</description>
<cap_param append_description='The ASID pool which is being assigned to. Must not be full. Each ASID pool can contain 1024 entries.'/>
<param dir="in" name="vroot" type="seL4_CPtr" description='The page directory that is being assigned to an ASID pool. Must not already be assigned to an ASID pool.'/>
<param dir="in" name="vspace" type="seL4_CPtr" description='The page directory that is being assigned to an ASID pool. Must not already be assigned to an ASID pool.'/>
</method>
</interface>

44
manual/parts/vspace.tex
View File

@@ -14,7 +14,7 @@ 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 top-level and intermediate paging structures.
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.
@@ -30,8 +30,13 @@ capabilities to the required objects.
\subsection{Hardware Virtual Memory Objects}
Each architecture has a top-level paging structure (level 0) and a number of intermediate levels.
In general, each level contains slots where the next level paging structure, or a frame of memory,
can be mapped. If the previous level is not mapped, a mapping operation will fail.
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.
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.
@@ -54,8 +59,10 @@ The rest of this section details the paging structures for each architecture.
\subsubsection{IA-32}
IA-32 processors have a two-level page-table structure.
The top-level page directory covers a 4\,GiB range and each page table covers a 4\,MiB range.
On IA-32, the VSpace is realised as a \texttt{PageDirectory}, which covers the entire 4\,GiB range
in the 32-bit address space, and forms the top-level paging structure. Second level page-tables
(\texttt{PageTable} objects) each cover a 4\,MiB range.
Structures at both levels are indexed by 10 bits in the virtual address.
\begin{tabularx}{\textwidth}{Xlll} \toprule
\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule
@@ -66,7 +73,9 @@ The top-level page directory covers a 4\,GiB range and each page table covers a
\subsubsection{x64}
% TODO describe
On x86-64, the VSpace is realised as a \texttt{PML4}. Three further levels of paging structure are
defined, as shown in the table below. All structures are indexed with 9 bits of the virtual
address.
\begin{tabularx}{\textwidth}{Xlll} \toprule
\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule
@@ -79,6 +88,10 @@ The top-level page directory covers a 4\,GiB range and each page table covers a
\subsubsection{AArch32}
Like IA-32, ARM AArch32 realise the VSpace as a \texttt{PageDirectory}, which covers the entire
4\,GiB address range, and a second-level \texttt{PageTable}. The second-level structures on AArch32
cover 1\,MiB address ranges.
ARM AArch32 processors have a two-level page-table structure.
The top-level page directory covers a range of 4\,GiB and each page table covers a 1\,MiB range.
@@ -91,6 +104,9 @@ The top-level page directory covers a range of 4\,GiB and each page table covers
\subsubsection{AArch64}
ARM AArch64 processors have a four-level page-table structure, where the VSpace is realised as a
\texttt{PageGlobalDirectory}. All paging structures are index by 9 bits of the virtual address.
\begin{tabularx}{\textwidth}{Xlll} \toprule
\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule
\texttt{PageGlobalDirectory} & 39---47 & 0 & \autoref{group__aarch64__seL4__ARM__PageGlobalDirectory} \\
@@ -100,9 +116,15 @@ The top-level page directory covers a range of 4\,GiB and each page table covers
\bottomrule
\end{tabularx}
\subsection{RISC-V}
RISC-V provides the same paging structure for all levels, \texttt{PageTable}. The VSpace is then
realised as a \texttt{PageTable}.
\subsubsection{RISC-V 32-bit}
32-bit RISC-V \texttt{PageTables} are indexed by 10 bits of virtual address.
\begin{tabularx}{\textwidth}{Xlll} \toprule
\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule
\texttt{PageTable} & 22---31 & 0 & \autoref{group__riscv__seL4__RISCV__PageTable} \\
@@ -112,6 +134,11 @@ The top-level page directory covers a range of 4\,GiB and each page table covers
\subsubsection{RISC-V 64-bit}
64-bit RISC-V follows the SV39 model, where \texttt{PageTables} are indexed by 9 bits of virtual address.
Although RISC-V allows
for multiple different numbers of paging levels, currently seL4 only supports exactly three levels
of paging structures.
\begin{tabularx}{\textwidth}{Xlll} \toprule
\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule
\texttt{PageTable} & 30---38 & 0 & \autoref{group__riscv__seL4__RISCV__PageTable} \\
@@ -127,8 +154,9 @@ implement virtual memory pages in a virtual address space.
The virtual address for a \obj{Page} mapping
must be aligned to
the size of the \obj{Page} and must be mapped to a suitable \obj{Page Directory}
or \obj{Page Table}. To map a page readable, the capability
the size of the \obj{Page} and must be mapped to a suitable VSpace, and every intermediate paging
structure required.
To map a page readable, the capability
to the page
that is being invoked must have read permissions. To map the page
writeable, the capability must have write permissions. The requested