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

manual: list all faults and fix style

Browse Source 
Signed-off-by: Ivan Velickovic <i.velickovic@unsw.edu.au>
This commit is contained in:
Ivan Velickovic
2024-06-24 10:37:26 +10:00
committed by Ivan Velickovic
parent d3d4cc6023
commit 1aa9ff8511
1 changed files with 13 additions and 5 deletions
Download Patch File Download Diff File Expand all files Collapse all files

18
manual/parts/threads.tex
View File

@@ -371,11 +371,19 @@ The register contents are transferred via the IPC buffer.
A thread's actions may result in a fault. Faults are delivered to the
thread's exception handler so that it can take the appropriate action.
The fault type is specified in the message label and is one of:
\texttt{seL4\_Fault\_CapFault}, \texttt{seL4\_Fault\_VMFault},
\texttt{seL4\_Fault\_UnknownSyscall}, \texttt{seL4\_Fault\_UserException},
\texttt{seL4\_Fault\_DebugException},
\texttt{seL4\_Fault\_TimeoutFault}, or \texttt{seL4\_Fault\_NullFault}
(indicating no fault occurred and this is a normal IPC message).
\begin{itemize}
\item \texttt{seL4\_Fault\_CapFault}
\item \texttt{seL4\_Fault\_VMFault}
\item \texttt{seL4\_Fault\_UnknownSyscall}
\item \texttt{seL4\_Fault\_UserException}
\item \texttt{seL4\_Fault\_TimeoutFault}
\item \texttt{seL4\_Fault\_NullFault} (indicating no fault occurred and this is a normal IPC message)
\item \texttt{seL4\_Fault\_VGICMaintenence}
\item \texttt{seL4\_Fault\_VPPIEvent}
\item \texttt{seL4\_Fault\_VCPUFault}
\item \texttt{seL4\_Fault\_DebugException}
\end{itemize}
Faults are delivered in such a way as to imitate a Call from the faulting
thread. This means that to send a fault message the fault endpoint