diff --git a/manual/parts/threads.tex b/manual/parts/threads.tex index 1cd3aab25..f57ea2117 100644 --- a/manual/parts/threads.tex +++ b/manual/parts/threads.tex @@ -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