portugalfuturista/seL4
2
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

update some manual todos

Browse source 
Signed-off-by: Birg <bbrcknl@github.com>
This commit is contained in:
Birg 2023-11-17 17:42:39 +11:00 committed by Indan Zupancic
parent 94c5a0b53a
commit 391bfb15f8
7 changed files with 77 additions and 37 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

28
libsel4/arch_include/arm/interfaces/sel4arch.xml
View file

@ -85,11 +85,14 @@
cap_description="Capability to the I/O page table being operated on.">
<method id="ARMIOPageTableMap" name="Map">
<condition><config var="CONFIG_TK1_SMMU"/></condition>
<brief>
Map an IO page table into an IOSpace.
</brief>
<description>
TODO
<docref>See <autoref label="sec:iospace"/></docref>
</description>
<param dir="in" name="iospace" type="seL4_ARM_IOSpace"/>
<param dir="in" name="ioaddr" type="seL4_Word"/>
<param dir="in" name="iospace" type="seL4_ARM_IOSpace" description="The IOSpace to map the page table into."/>
<param dir="in" name="ioaddr" type="seL4_Word" description="Virtual address at which to map the page table."/>
<error name="seL4_DeleteFirst">
<description>
All required page tables are already mapped in <texttt text="iospace"/> at <texttt text="ioaddr"/>.
@ -109,8 +112,11 @@
</method>
<method id="ARMIOPageTableUnmap" name="Unmap">
<condition><config var="CONFIG_TK1_SMMU"/></condition>
<brief>
Unmap an IO page table from an IOSpace.
</brief>
<description>
TODO
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<error name="seL4_IllegalOperation">
<description>
@ -209,14 +215,18 @@
<method id="ARMPageMapIO" name="MapIO" manual_name="Map I/O">
<condition><config var="CONFIG_TK1_SMMU"/></condition>
<brief>
TODO
Map a page into an IOSpace.
</brief>
<description>
TODO
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<param dir="in" name="iospace" type="seL4_ARM_IOSpace"/>
<param dir="in" name="rights" type="seL4_CapRights_t"/>
<param dir="in" name="ioaddr" type="seL4_Word"/>
<param dir="in" name="iospace" type="seL4_ARM_IOSpace" description="The IOSpace to map the page into."/>
<param dir="in" name="rights" type="seL4_CapRights_t">
<description>
Rights for the mapping.<docref>Possible values for this type are given in <autoref label="sec:cap_rights"/> .</docref>
</description>
</param>
<param dir="in" name="ioaddr" type="seL4_Word" description="Virtual address at which to map page."/>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists in <texttt text="iospace"/> at <texttt text="ioaddr"/>.

24
libsel4/arch_include/x86/interfaces/sel4arch.xml
View file

@ -421,13 +421,25 @@
</method>
<method id="X86PageMapEPT" name="MapEPT" manual_name="Map EPT">
<condition><config var="CONFIG_VTX"/></condition>
<brief>
Map an extended page table.
</brief>
<description>
TODO
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<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"/>
<param dir="in" name="vspace" type="seL4_X86_EPTPML4" description="Capability to the VSpace which will
contain the mapping"/>
<param dir="in" name="vaddr" type="seL4_Word" description="Virtual address at which to map page."/>
<param dir="in" name="rights" type="seL4_CapRights_t">
<description>
Rights for the mapping. Possible values for this type are given in <autoref label='sec:cap_rights'/>.
</description>
</param>
<param dir="in" name="attr" type="seL4_X86_VMAttributes">
<description>
VM attributes for the mapping. Possible values for this type are given in <autoref label='ch:vspace'/>.
</description>
</param>
<error name="seL4_AlignmentError">
<description>
The <texttt text="vaddr"/> is not aligned to the page size of <texttt text="_service"/>.
@ -848,7 +860,7 @@
</error>
</method>
</interface>
<interface name="seL4_TCB" manual_name="TCB">
<interface name="seL4_TCB" manual_name="TCB" cap_description="Capability to the TCB which is being operated on.">
<method id="TCBSetEPTRoot" name="SetEPTRoot" manual_name="Set EPT Root" manual_label="set_eptroot">
<condition><config var="CONFIG_VTX"/></condition>
<brief>

17
libsel4/include/interfaces/sel4.xml
View file

@ -806,15 +806,13 @@
<method id="TCBSetTLSBase" name="SetTLSBase" manual_name="Set TLS Base" manual_label="tcb_settlsbase">
<brief>
Set the TLS base of the target TCB. This intended for use on architectures where the register
used for TLS can only be written to in privilidged mode
Set the TLS base of the target TCB.
</brief>
<description>
An invocation for setting the Thread Local Storage (TLS) base address. This ensures that across all platforms, the TLSBase register is viewed as being completely mutable, just like all of the general purpose registers, even on platforms where modification is a privileged operation.
</description>
<return>
</return>
<param dir="in" name="tls_base" type="seL4_Word"
description="The TLS base to set"/>
description="The TLS base to set."/>
<error name="seL4_IllegalOperation">
<description>
The <texttt text="_service"/> is a CPtr to a capability of the wrong type.
@ -1334,7 +1332,7 @@
</method>
</interface>
<interface name="seL4_SchedControl">
<interface name="seL4_SchedControl" cap_description="Capability to a scheduling control object.">
<method id="SchedControlConfigureFlags" name="ConfigureFlags" manual_name="ConfigureFlags" manual_label="schedcontrol_configureflags">
<condition><config var="CONFIG_KERNEL_MCS"/></condition>
@ -1377,7 +1375,7 @@
</interface>
<interface name="seL4_SchedContext">
<interface name="seL4_SchedContext" cap_description="Capability to the scheduling context which is being operated on.">
<method id="SchedContextBind" name="Bind"
manual_name="Bind" manual_label="schedcontext_bind">
@ -1505,8 +1503,11 @@
The caller must have a maximum control priority greater than or equal to the threads priority.
</brief>
<description>
TODO
Capability to the scheduling context which is being operated on.
</description>
<return>
See <autoref label="sec:scheduling_contexts"/>
</return>
<param dir="out" name="consumed" type="seL4_Time"/>
<error name="seL4_IllegalOperation">
<description>

9
libsel4/include/sel4/syscalls_mcs.h
View file

@ -224,6 +224,10 @@ seL4_Yield(void);
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_Wait(seL4_CPtr src, seL4_Word *sender);
@ -246,6 +250,10 @@ seL4_Wait(seL4_CPtr src, seL4_Word *sender);
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>
* @endxmlonly
*/
LIBSEL4_INLINE_FUNC seL4_MessageInfo_t
seL4_NBWait(seL4_CPtr src, seL4_Word *sender);
@ -269,7 +277,6 @@ seL4_NBWait(seL4_CPtr src, seL4_Word *sender);
* sender, or the notification word of the
* notification object that was signalled.
* This parameter is ignored if `NULL`.
*
* @return A `seL4_MessageInfo_t` structure
* @xmlonly
* <docref>as described in <autoref label="sec:messageinfo"/></docref>

22
libsel4/sel4_arch_include/x86_64/interfaces/sel4arch.xml
View file

@ -29,14 +29,21 @@
<member name="gs_base"/>
</struct>
<interface name="seL4_X86_PDPT" manual_name="PDPT">
<interface name="seL4_X86_PDPT" manual_name="PDPT" cap_description="Capability to the PDPT being operated on.">
<method id="X86PDPTMap" name="Map">
<brief>
Map a page directory page table.
</brief>
<description>
TODO
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<param dir="in" name="pml4" type="seL4_X64_PML4"/>
<param dir="in" name="vaddr" type="seL4_Word"/>
<param dir="in" name="attr" type="seL4_X86_VMAttributes"/>
<param dir="in" name="pml4" type="seL4_X64_PML4" description="Capability to the VSpace which will contain the mapping."/>
<param dir="in" name="vaddr" type="seL4_Word" description="Virtual address at which to map page."/>
<param dir="in" name="attr" type="seL4_X86_VMAttributes">
<description>
VM attributes for the mapping. Possible values for this type are given in <autoref label='ch:vspace'/>.
</description>
</param>
<error name="seL4_DeleteFirst">
<description>
A mapping already exists for this level in <texttt text="vspace"/> at <texttt text="vaddr"/>.
@ -66,8 +73,11 @@
</error>
</method>
<method id="X86PDPTUnmap" name="Unmap">
<brief>
Unmap a page directory page table.
</brief>
<description>
TODO
<docref>See <autoref label="ch:vspace"/></docref>
</description>
<error name="seL4_IllegalOperation">
<description>

12
manual/parts/objects.tex
View file

@ -21,7 +21,7 @@ The basic services seL4 provides are as follows:
\item[Threads] are an abstraction of CPU execution that supports
running software;
\item[Scheduling contexts] (MCS only) are an abstraction of CPU execuion time.
\item[Scheduling contexts] (MCS only) are an abstraction of CPU execution time.
\item[Address spaces] are virtual memory spaces that each contain an
application. Applications are limited to accessing memory in their
@ -69,7 +69,7 @@ Conceptually, a capability resides in an application's \emph{capability
space}; an address in this space refers to a \emph{slot} which may or
may not contain a capability. An application may refer to
a capability---to request a kernel service, for example---using the
address of the slot holding that capability. This means, the seL4
address of the slot holding that capability. This means, the seL4
capability model is an instance of a \emph{segregated} (or \emph{partitioned})
capability system, where capabilities are managed by the kernel.
@ -114,7 +114,7 @@ The seL4 kernel provides a message-passing service for communication between
threads. This mechanism is also used for communication with kernel-provided
services. There is a standard message format, each message containing a
number of data words and possibly some capabilities. The structure and encoding
of these messages are described in detail in \autoref{ch:ipc}.
of these messages are described in detail in \autoref{ch:ipc}.
Threads send messages by invoking capabilities within their capability space.
When an endpoint, notification or reply capability is invoked in this way, the
@ -305,11 +305,11 @@ manipulation, and combination of these kernel objects:
provide a simple signalling mechanism. A \obj{Notification}
is a word-size array of flags, each of which behaves like a binary semaphore. Operations
are \emph{signalling} a subset of flags in a single operation,
polling to check any flags,
polling to check any flags,
and blocking until any are signalled. Notification capabilities
can be signal-only or wait-only.
\item[Virtual Address Space Objects] (see \autoref{ch:vspace})
\item[Virtual Address Space Objects] (see \autoref{ch:vspace})
are used to construct a virtual
address space (or VSpace) for one or more threads. These
objects largely directly correspond to those of the hardware, and
@ -321,7 +321,7 @@ manipulation, and combination of these kernel objects:
and acknowledge interrupts from hardware devices.
Initially, there is a capability to \obj{IRQControl},
which allows for the creation of \obj{IRQHandler} capabilities.
An \obj{IRQHandler} capability permits the management of a specific
An \obj{IRQHandler} capability permits the management of a specific
interrupt source associated with a specific device.
It is delegated to
a device driver to access an interrupt source. The \obj{IRQHandler}

2
manual/parts/threads.tex
View file

@ -88,7 +88,7 @@ affinity values are compatible across different platforms.
seL4 uses a preemptive, tickless scheduler with 256 priority levels (0 --- 255). All threads have
a maximum controlled priority (MCP) and a priority, the latter being the effective priority of the
thread.
When a thread modifies a another threads priority (including itself) it must provide a
When a thread modifies another thread's priority (including itself) it must provide a
thread capability from which to use the MCP from. Threads can only set priorities and MCPs
to be less than or equal to the provided thread's MCP.
The initial task starts with an MCP and priority as the highest priority in the system (\texttt{seL4\_MaxPrio}).