manual/parts/threads.tex

59 derived from the scheduling context object.
82 thread capability from which to use the MCP from. Threads can only set priorities and MCPs
127 In theory, sporadic servers provide temporal isolation -- preventing threads from exceeding their allocated budget -- by using the following algorithm:
132 amount of time consumed ($T - T_{s}$) and subtract that from the current replenishment being used.
139 While a thread is executing, it constantly drains the budget from the \texttt{rAmount} at the head of the
145 used. When a round-robin thread stops executing, budget is moved from the head to the tail
146 replenishment. Once the head budget is consumed, the thread is removed from the scheduling queue
174 Whenever a thread is executing it consumes the budget from its current scheduling context.  The
186 Threads can be unbound from a scheduling context with
187 \apifunc{seL4\_SchedContext\_UnbindObject}{schedcontext_unbindobject}.  This is distinct from
196 Like other objects, scheduling contexts are created from untyped memory using
223 does not possess the scheduling context, the thread will be removed from the call chain and the
251 Scheduling contexts can be unbound from all objects (notification objects and TCBs that are bound or
311 recovered from.  Consequently threads without standard exception handlers
329 from malicious or untrusted clients whose budget expires while the server is
360 Faults are delivered in such a way as to imitate a Call from the faulting
502 register API-ID is not returned in the fault message from the kernel on
515 functionality (i.e, API-ID from 0 to \texttt{seL4\_NumExclusiveBreakpoints} - 1).
568     \textbf{Meaning} & \textbf{IPC buffer location} \\ \midrule Data word from
651 \obj{VCPU}. Switching from regular execution mode into the guest execution mode is
663 disable the use of External Interrupt Exiting, as this would prevent the kernel from receiving
680 from the \obj{VCPU}.