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

Add a glossary to the manual

Browse Source 
Add a glossary with seL4-specific terms and their
definitions.
Remove chapter number from bibliography
Tweak Makefile for glossary

Signed-off-by: Birgit Brecknell <bbrcknl@gmail.com>
This commit is contained in:
Birgit Brecknell
2024-03-20 14:31:02 +11:00
committed by Matthew Brecknell
parent 43607edb68
commit f6656e2c78
7 changed files with 152 additions and 19 deletions
Download Patch File Download Diff File Expand all files Collapse all files

3
manual/Makefile
View File

@@ -228,6 +228,7 @@ clean:
*.out *.ps *-diff.tex *.mps .log *.pdf *.tgz *~ *.lof *.lot env.tex
rm -rf ${DoxygenOutput} ${GeneratedLatexDir} ${GeneratedMarkdownDir}
rm -rf ${Stage}
rm -rf *.acn *.glo *.gls *.ilg *.ist
tar: clean
( p=`pwd` && d=`basename "$$p"` && cd .. && \
@@ -291,6 +292,8 @@ references.bib: $(addsuffix .tex, $(Targets))
${Q}if ! test -e $*.bbl || test $(Bib) -nt $*.bbl; then rm -f $*.bbl; fi
@echo "====> LaTeX first pass: $(<)"
${Q}$(LaTeX) $< >.log || if egrep -q $(Error) $*.log ; then cat .log; rm $@; false ; fi
@echo "====> Glossary: $(<)"
${Q}makeindex -s manual.ist -o manual.gls manual.glo
${Q}if egrep -q $(Rerun_Bib) $*.log ; then echo "====> BibTex" && $(BibTeX) $* > /dev/null && echo "====> LaTeX BibTeX pass" && $(LaTeX) >.log $< ; fi
${Q}if egrep -q $(Rerun) $*.log ; then echo "====> LaTeX rerun" && $(LaTeX) >.log $<; fi
${Q}if egrep -q $(Rerun) $*.log ; then echo "====> LaTeX rerun" && $(LaTeX) >.log $<; fi

11
manual/manual.tex
View File

@@ -13,6 +13,11 @@
\usepackage{url}
% Glossary
\usepackage[acronym,toc]{glossaries}
\input{parts/glossary}
\makeglossaries
% Setting this to true turns on the `draft' watermark
\newif \ifDraft \Draftfalse
%\Drafttrue
@@ -45,7 +50,7 @@
\usepackage{verbatim}
\usepackage[small,bf,up,width=0.75\textwidth]{caption}
\usepackage[htt]{hyphenat}
\usepackage[nottoc,numbib]{tocbibind}
\usepackage[nottoc]{tocbibind}
\renewcommand{\captionfont}{\small}
\renewcommand{\chapterautorefname}{Chapter}
@@ -184,6 +189,10 @@ for details.
\label{sec:api_reference}
\input{parts/api}
% glossary
\printglossaries
\glsaddallunused
% Bibliography
\cleardoublepage
\bibliographystyle{plainnat}

116
manual/parts/glossary.tex Normal file
View File

@@ -0,0 +1,116 @@
%
% Copyright 2014, General Dynamics C4 Systems
%
% SPDX-License-Identifier: GPL-2.0-only
%
\newglossaryentry{asid}{
name=ASID,
description={Address Space Identifier. Depending on architecture, the kernel provides software ASIDs, which are associated with VSpace root objects, and define the virtual address space of a thread. They are mapped to hardware ASIDs on demand when the architecture supports these. Multiple threads may be in the same address space}
}
\newglossaryentry{badge}{
name=Badge,
description={A badge is a piece of extra information stored in a capability, mostly used for endpoint and notification capabilities. It can be used by applications to identify caps previously handed out to clients}
}
\newglossaryentry{cap}{
name=Capability,
description={The main access control concept in seL4. A capability conceptually is a reference to a kernel object together with a set of access rights. Most seL4 capabilities store additional bits of information. Some of this additional information may be exposed to the user, but the bulk of it is kernel-internal book-keeping information. Capabilities are stored in CNodes and TCBs}
}
\newglossaryentry{cdt}{
name=CDT,
description={Capability Derivation Tree. A kernel-internal data structure that tracks the child/parent relationship between capabilities. Capabilities to new objects are children of the Untyped capability the object was created from. Capabilities can also be copied and result in either child or sibling capabilities, depending on the operation that was used and the depth of the existing derivation tree. The revoke operation will delete all children of the invoked capability}
}
\newglossaryentry{cnode}{
name=CNode,
description={Capability Node. Kernel-controlled storage that holds capabilities. Capability nodes can be created in different sizes and be shared between CSpaces}
}
\newglossaryentry{cptr}{
name=CPtr,
description={Capability Pointer. A user-level reference to a capability, relative to a specified root CNode or the thread’s CSpace root}
}
\newglossaryentry{cspace}{
name=CSpace,
description={A directed graph of CNodes. The CSpace of a thread defines the set of capabilities it has access to. The root of the graph is the CNode capability in the CSpace slot of the thread. The edges of the graph are the CNode capabilities residing in the CNodes spanned by this root}
}
\newglossaryentry{endpoint}{
name=Endpoint,
description={IPC is facilitated by small kernel objects known as endpoints, which act as general communication ports. Invocations on endpoint objects are used to send and receive IPC messages}
}
\newglossaryentry{guard}{
name=Guard,
description={Guard of a CNode capability. From the user’s perspetive the CSpace of a thread is organised as a guarded page table. The kernel will resolve user capability pointers into internal capability slot pointers. The guard of one link/edge in the CSpace graph defines a sequence of bits that will be stripped from the user-level capability pointer before resolving resumes at the next CNode}
}
\newglossaryentry{iommu}{
name=IOMMU,
description={Input–Output Memory Management Unit. Applies virtual address translation and memory protection to DMA capable I/O devices}
}
\newglossaryentry{iopagetable}{
name=IOPageTable,
description={This object represents a node in the multilevel page-table structure used by IOMMU hardware to translate hardware memory accesses}
}
\newglossaryentry{iospace}{
name=IOSpace,
description={This object represents the address space associated with a hardware device. It represents the right to modify a device’s address space. See \autoref{ch:io}}
}
\newglossaryentry{ipc}{
name=IPC,
description={Inter Process Communication is facilitated by endpoints, which act as general communication ports. Invocations on endpoint objects are used to send and receive messages}
}
\newglossaryentry{irqcontrol}{
name=IRQControl,
description={A single capability from which IRQHandler capabilities to all IRQ numbers in the system can be derived. This capability can be moved between CSpaces and CSlots but cannot be duplicated. Revoking this capability removes all IRQHandlers}
}
\newglossaryentry{irqhandler}{
name=IRQHandler,
description={Capabilities that represent the ability of a thread to handle a certain interrupt. See \autoref{ch:io}}
}
\newglossaryentry{notificationobject}{
name=Notification Object,
description={A word-size array of flags that provides a non-blocking signalling mechanism similar to a binary semaphore. Operations are signalling a subset of flags in a single operation, polling to check any flags, and blocking until any are signalled. Notification capabilities can be signal-only or wait-only}
}
\newglossaryentry{replyobject}{
name=Reply Object,
description={(MCS only) A reply object is a vessel for tracking reply messages, used to send a reply message and
wake up the caller}
}
\newglossaryentry{schedulingcontext}{
name=Scheduling Context,
description={(MCS only) An abstraction of CPU execution time}
}
\newglossaryentry{tcb}{
name=TCB,
description={Thread Control Block. The kernel object that stores management data for threads, such as the thread's CSpace, VSpace, thread state, or user registers}
}
\newglossaryentry{untypedmemory}{
name=Untyped Memory,
description={Memory that can be used to create kernel objects via the \apifunc{seL4\_Untyped\_Retype}{untyped_retype} invocation. It is the foundation of memory allocation in the seL4 kernel. See \autoref{sec:kernmemalloc}}
}
\newglossaryentry{vm}{
name=VM,
description={Virtual Memory. The concept of translating virtual memory addresses to physical frames. See \autoref{ch:vspace}}
}
\newglossaryentry{vspace}{
name=VSpace,
description={Virtual Address Space. In analogy to CSpace, the virtual memory space of a thread. See \autoref{ch:vspace}}
}

26
manual/parts/io.tex
View File

@@ -92,7 +92,7 @@ by the given \obj{IO Port} capability in order for the method to succeed.
The I/O port methods return error codes upon failure.
A \texttt{seL4\_IllegalOperation} code is returned if port access is
attempted outside the range allowed by the \obj{IO Port} capability.
attempted outside the range allowed by the \obj{IO Port} capability.
Since invocations that
read from I/O ports are required to return two values -- the value read
and the error code -- a structure containing two members, \texttt{result}
@@ -135,7 +135,7 @@ mapped into the I/O address space. A \obj{Page} can be mapped into
either a \obj{VSpace} or an \obj{IOSpace} but never into both at the same time.
\obj{IOSpace} and \obj{VSpace} fault handling differ significantly.
\obj{VSpace} page faults are redirected to the thread's exception handler (see \autoref{sec:faults}),
\obj{VSpace} page faults are redirected to the thread's exception handler (see \autoref{sec:faults}),
which can take the
appropriate action and restart the thread at the faulting instruction.
There is no concept of an exception handler for an \obj{IOSpace}. Instead, faulting
@@ -148,7 +148,7 @@ CSpace. An \obj{IOSpace} capability for a specific device is created by
using the \apifunc{seL4\_CNode\_Mint}{cnode_mint} method, passing the
PCI identifier of the device as the low 16 bits of the \texttt{badge} argument, and
a Domain ID as the high 16 bits of the \texttt{badge} argument.
PCI identifiers are explained fully in the PCI specification
PCI identifiers are explained fully in the PCI specification
\cite{Shanley:PCISA}, but are briefly described here. A PCI identifier is
a 16-bit quantity. The first 8 bits identify the bus that the device is on.
The next 5 bits are the device identifier: the number of the device on
@@ -162,14 +162,14 @@ unsupported value is chosen.
The IOMMU page-table structure has three levels.
Page tables are mapped into an \obj{IOSpace} using the \apifunc{seL4\_X86\_IOPageTable\_Map}{x86_io_page_table_map} method.
This method takes the \obj{IOPageTable} to map, the \obj{IOSpace} to map into
This method takes the \obj{IOPageTable} to map, the \obj{IOSpace} to map into
and the address to map at. Three levels of page tables must be mapped before
a frame can be mapped successfully. A frame is mapped with the
\apifunc{seL4\_X86\_Page\_MapIO}{x86_page_map_io} method whose parameters are analogous to
the corresponding method that maps \obj{Page}s into \obj{VSpaces} (see \autoref{ch:vspace}),
the corresponding method that maps \obj{Page}s into \obj{VSpaces} (see \autoref{ch:vspace}),
namely \apifunc{seL4\_X86\_Page\_Map}{x86_page_map}.
Unmapping is accomplished with the usual unmap (see \autoref{ch:vspace}) API
Unmapping is accomplished with the usual unmap (see \autoref{ch:vspace}) API
call,
\apifunc{seL4\_X86\_Page\_Unmap}{x86_page_unmap}.
@@ -191,7 +191,7 @@ with an identifier (StreamID) that is used to direct the transaction through a
SMMU translation context bank (CB). A translation context bank can perform
address translation, memory protection and memory attribute transformation.
The standard specifies different types of address translations that correspond
to stages in the ArmV8 virtual memory system architecture such as either
to stages in the ArmV8 virtual memory system architecture such as either
non-secure EL0, EL1 first and second stage translations, Hyp mode translations
or secure mode translations. It is possible to associate different StreamIDs
with the same context bank and it is possible to share address translation
@@ -218,7 +218,7 @@ context banks, bind context banks to page translation structures, implement
SMMU fault handling and also perform explicit TLB maintenance.
This allows system software to ensure that a device is only able to access and
modify memory contents that it has been explicitly given access to and allow
devices to be presented with a virtualized address space for performing DMA.
devices to be presented with a virtualised address space for performing DMA.
All the StreamIDs and context banks are accessible via capabilities. Control
capabilities are used to create capabilities referring to each StreamID and
@@ -248,7 +248,7 @@ enabled, and seL4 is operating in EL2, the SMMU only does stage 2 translations.
Four capabilities types provide access to SMMU resources:
\begin{description}
\item[\obj{seL4\_ARM\_SID}] A capability granting access to a single
\item[\obj{seL4\_ARM\_SID}] A capability granting access to a single
transaction stream, which can be used to bind and unbind a stream to a
single context bank.
\item[\obj{seL4\_ARM\_CB}] A capbility representing a single specific context
@@ -280,7 +280,7 @@ tasks in the system.
\item[\apifunc{seL4\_ARM\_SIDControl\_GetSID}{arm_sid_controlgetsid}] uses the
\obj{seL4\_ARM\_SIDControl} capability to create a new \obj{seL4\_ARM\_SID}
capability that represents a single StreamID. This new capbility is placed
in the provided slot. It is expected that whatever thread controls an
in the provided slot. It is expected that whatever thread controls an
\obj{seL4\_ARM\_SIDControl} capability knows about how StreamIDs are
allocated in a system.
\end{description}
@@ -380,7 +380,7 @@ Similarly, deleting a VSpace\_cap that contains assigned context bank number wil
Deleting the last ARM\_SID cap will:
\begin{itemize}
\item Perform an \apifunc{seL4\_ARM\_SID\_UnbindCB}{arm_sid_unbindcb},
\item Perform an \apifunc{seL4\_ARM\_SID\_UnbindCB}{arm_sid_unbindcb},
(deleting the copy of the assigned \obj{seL4\_ARM\_CB} cap)
\item Disable the stream ID.
\end{itemize}
@@ -470,7 +470,7 @@ which can be used to identify its context bank ID.
\obj{seL4\_ARM\_SIDControl} cap (controlling stream ID distributions) are trusted.
\item SMMU interrupts are handled as same as other IRQs, i,e, the kernel does not
treat the SMMU IRQs special, reporting the interrupt via IRQ notifications.
\item The kernel provides a API for reading the global fault registers:
\item The kernel provides a API for reading the global fault registers:
\apifunc{seL4\_ARM\_SIDControl\_GetFault}{arm_sid_controlgetfault}. Because
the IRQ notification can only deliver information via the badge, the owner
of the StreamControl\_cap can retrieve more information via this API.
@@ -483,7 +483,7 @@ which can be used to identify its context bank ID.
cap holder (the \obj{seL4\_ARM\_CB} cap holder).
\item Once the fault handling is done, the server can call
\apifunc{seL4\_ARM\_CB\_CBClearFault}{arm_cb_clearfault} to clear the fault
status on a context bank, and
status on a context bank, and
\apifunc{seL4\_ARM\_SIDControl\_ClearFault}{arm_sid_controlclearfault}
to clear the fault status on SMMU.
\end{itemize}