RTOS/seL4
1
0
Fork 0
forked from Imagelibrary/seL4
Code Pull Requests Activity

manual: more consistent terminology in sec 7.1

Browse Source 
Adjusting for VSpace object clarification and making sure terminology
is used consistently.

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
Gerwin Klein
2023-03-25 12:27:45 +11:00
parent e4c0e561d6
commit 59e751852c
1 changed files with 26 additions and 34 deletions
Download Patch File Download Diff File Expand all files Collapse all files

60
manual/parts/vspace.tex
View File

@@ -57,10 +57,10 @@ The rest of this section details the paging structures for each architecture.
\subsubsection{IA-32}
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.
On IA-32, the VSpace object is implemented by the \texttt{PageDirectory} object, 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
@@ -71,9 +71,9 @@ Structures at both levels are indexed by 10 bits in the virtual address.
\subsubsection{x64}
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.
On x86-64, the VSpace object is implemented by the \texttt{PML4} object. Three further levels of
paging structure are defined, as shown in the table below. All structures are indexed by 9 bits of
the virtual address.
\begin{tabularx}{\textwidth}{Xlll} \toprule
\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule
@@ -86,12 +86,9 @@ address.
\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.
Like IA-32, Arm AArch32 implements the VSpace object with a \texttt{PageDirectory} object which
covers the entire 4\,GiB address range. The second-level structures on AArch32 are
\texttt{PageTable} objects and cover 1\,MiB address ranges.
\begin{tabularx}{\textwidth}{Xlll} \toprule
\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule
@@ -102,8 +99,8 @@ 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.
Arm AArch64 processors have a four-level page-table structure. The VSpace object is implemented by the
\texttt{PageGlobalDirectory} object. All paging structures are indexed by 9 bits of the virtual address.
\begin{tabularx}{\textwidth}{Xlll} \toprule
\emph{Object} & \emph{Address Bits} & \emph{Level} & \emph{Methods} \\ \midrule
@@ -116,8 +113,8 @@ Arm AArch64 processors have a four-level page-table structure, where the VSpace
\subsection{RISC-V}
RISC-V provides the same paging structure for all levels, \texttt{PageTable}. The VSpace is then
realised as a \texttt{PageTable}.
RISC-V provides the same paging structure for all levels, \texttt{PageTable}. This means the VSpace
object is here also implemented by the \texttt{PageTable} object.
\subsubsection{RISC-V 32-bit}
@@ -147,27 +144,22 @@ of paging structures.
\subsection{Page}
A \obj{Page} object corresponds to a frame of physical memory that is used to
implement virtual memory pages in a virtual address space.
\obj{Frame} objects, used via \obj{Page} capabilities, correspond to frames of physical memory that
are used to 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 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
mapping permissions are specified with an argument of type
\texttt{seL4\_CapRights} given to the mapping function.
If the capability does not have
sufficient permissions to authorise the given mapping, then
the mapping permissions are silently downgraded. Specific mapping permissions are dependant on the
architecture and are documented in the \autoref{sec:api_reference} for each function.
The virtual address for a \obj{Page} mapping must be aligned to the size of the \obj{Page} and must
be mapped into a suitable paging structure object, which itself must already be mapped in.
To map a page readable, the corresponding \obj{Page} capability must have read permissions. To map
the page writeable, the capability must have write permissions. The requested mapping permissions
are specified with an argument of type \texttt{seL4\_CapRights} given to the mapping invocation. If
the capability does not have sufficient permissions to authorise the given mapping, the mapping
permissions are silently downgraded. Specific mapping permissions are dependent on the architecture
and are documented in the \autoref{sec:api_reference} for each function.
At minimum, each architecture defines \texttt{Map}, \texttt{Unmap} and
\texttt{GetAddress} methods for pages.
Methods for page objects for each architecture can be found in the \autoref{sec:api_reference}, and
Invocations for page capabilities for each architecture can be found in the \autoref{sec:api_reference}, and
are indexed per architecture in the table below.
\begin{tabularx}{\textwidth}{Xl} \toprule