manual/parts/threads.tex

15 time is also represented by the thread abstraction.
16 A thread is represented in seL4 by its thread control block
19 With MCS, a scheduling context is represented by a scheduling context object
28 (see  \autoref{ch:ipc}), which is used to pass extra arguments during IPC
30 registers. While it is not compulsory that a thread has an IPC buffer,
35 %FIXME: there is much more information held in the TCB!
42 \autoref{sec:kernmemalloc}). A newly created thread is initially inactive. It
43 is configured by setting its CSpace and VSpace with the
57 corresponding to the affinity of the thread. For master, this is set using
58 \apifunc{seL4\_TCB\_SetAffinity}{tcb_setaffinity}, while on the MCS kernel the affinity is
71 automatically suspended when the last capability to their \obj{TCB} is
73 % an example of which is demonstrated in \nameref{ex:second_thread}.
91 Of threads eligible for scheduling, the highest priority thread in a runnable state is chosen.
107 Access to CPU execution time is controlled through scheduling context objects.
115 an admission test. As a result the set of all parameters is not neccesserily schedulable. If
117 round-robin scheduling is applied once the budget is expired.
119 A scheduling context that is eligible to be picked by the scheduler, i.e has budget available, is
121 and sporadic threads.  For round-robin threads, the budget is charged each time the current node's
122 scheduling context is changed, until it is depleted and then refilled immediately.
131 \item When a thread stops executing (blocks or is preempted), schedule a replenishment at $T_{s} + p$ for the
137 of the time it is eligible for use (\emph{rTime}) and the amount that replenishment is for
139 While a thread is executing, it constantly drains the budget from the \texttt{rAmount} at the head of the
140 replenishment list. If the \texttt{rTime} is in the future, the thread bound to that
141 scheduling context is placed in a queue of threads waiting for more budget.
144 budget is charged. Round-robin threads have two refills only, both of which are always ready to be
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
153 \item The maximum number of refills in a single scheduling context is determined by the size
156 limits the number of refills for that specific scheduling context. This value is added to the base
157 value of 2 and is limited by the size of the scheduling context.
166 Given the number of replenishments is limited, if a node's SC changes and the outgoing SC does not
167 have enough space to store the new replenishment, space is created by removing the current
168 replenishment which can result in preemption if the next replenishment is not yet available.
171 replenishment queue. However, the scheduling overhead will be higher as the replenishment list is
174 Whenever a thread is executing it consumes the budget from its current scheduling context.  The
176 block until the next replenishment is ready to be used.
181 one kernel entry.  When a thread is bound to a scheduling context, if it is in a runnable state and
182 the scheduling context is active, it will be added to the scheduler.
187 \apifunc{seL4\_SchedContext\_UnbindObject}{schedcontext_unbindobject}.  This is distinct from
200 on a single node.  A scheduling control cap for each node is provided to the initial task at run
201 time.  Threads run on the node that their scheduling context is configured for.  Scheduling context
206 The kernel does not conduct any schedulability tests, as task admission is left to user-level policy
218 context is donated to the passive thread. The generated reply cap ensures that the callee is merely
219 borrowing the scheduling context: when the reply cap is consumed by a reply message being sent the
220 scheduling context will be returned to the caller.  If the reply cap is revoked, and the callee
222 a deep call chain and a reply cap in the middle of the call chain is revoked, such that the callee
224 scheduling context will remain where it is.  If the receiver does not provide a reply object to
230 scheduling context, B's reply cap to A is revoked, then the scheduling context will remain with C.
231 However, a call chain will remain between A and C, such that if C's reply cap is revoked, or
238 is no guarantee that the scheduling context will return, which increases book keeping complexity but allows
240 does not guarantee the return of a scheduling context: this is an inherently trusted operation as the
245 \apifunc{seL4\_SchedContext\_UnbindObject}{schedcontext_unbindobject}.  If a signal is delivered to
247 the scheduling context that is bound to the notification object.  The scheduling context is returned
261 Of threads eligible for scheduling, the highest priority thread in a runnable state is chosen.
268 however when a thread executes is determined by thread priority.  Consequently,
269 access to CPU is a function of thread MCPs, scheduling contexts and the
272 the highest priority thread will always run, however it is up to the system
273 designer to make sure the entire system is schedulable.
280 exception handler and a \emph{timeout} exception handler, where the latter is MCS
290 This address is then used to lookup the handler endpoint, and the capability to
291 the endpoint is installed into the threads' kernel CNode.  For threads without
294 handler capability is validated. The kernel does not perform another lookup,
295 but checks that the capability is an endpoint with the correct rights.
304 The standard exception handler is used when a fault is triggered by a thread
307 make any more progress until the page is mapped.  If a thread experiences a
308 fault that would trigger the standard exception handler while it is set to a
310 This is because without action by another thread, standard exceptions cannot be
321 The handling of timeout faults is not compulsory: if a thread does not have a
323 running when it's budget is replenished.  This allows temporally sensitive
329 from malicious or untrusted clients whose budget expires while the server is
334 If a reply message is sent to a nested server and a scheduling context without
353 The fault type is specified in the message label and is one of:
358 (indicating no fault occurred and this is a normal IPC message).
362 must have Write and either Grant or GrantReply permissions. If this is not the
363 case, a double fault happens (generally the thread is simply suspended).
376 is called on a capability that does not exist, is not an endpoint or notification capability or does not have
402 number that is unknown to seL4.
404 of the faulting thread is passed to the thread's exception handler so that it
405 may, for example, emulate the system call if a thread is being
411 message length is non-zero, the faulting thread's register set will be
413 registers updated is controlled with the length field of the message
425 message length is non-zero, the faulting thread's register set will be
427 registers updated is controlled with the length field of the message
436 is configured to include them (when CONFIG\_HARDWARE\_DEBUG\_API is set). The hardware
437 debugging extensions API is supported on the following subset of the platforms that the
450 Information on the available hardware debugging resources is presented in the form of the following constants:
457 On this platform therefore, \texttt{seL4\_NumHWBreakpoints} is defined as 10.
468 set only on ARM platforms. The API-ID of the first exclusive breakpoint is given
475 on ARM platforms. The API-ID of the first exclusive watchpoint is given
483 x86 platforms. The API-ID of the first dual-function monitor is given
502 register API-ID is not returned in the fault message from the kernel on
510 threads when configured to do so (when CONFIG\_HARDWARE\_DEBUG\_API is set). To
513 The caller is expected to select an API-ID that corresponds to
523 If \texttt{bp\_was\_consumed} is \texttt{true}, the caller should not
533 is currently configured (if any) for single-stepping will be the implicit
558 timeout fault handler that is not a null capability.  They allow a timeout
604 The fixed schedule is compiled into the kernel via the constant
608 is active.
618 Hardware execution virtualisation is supported on specific arm and x86 platforms. The interface is exposed through a series
624 additional machine registers and other pieces of state a \obj{VCPU} object is introduced to act
632 a \obj{VCPU} to a \obj{TCB} is done by an invocation on the \obj{VCPU} only, and not the \obj{TCB}.
636 the underlying architecture specific harwdare mechanisms is required to use these objects, and
637 such familiarity is therefore assumed in description.
641 When a \obj{TCB} has a bound \obj{VCPU} it is allowed to have the mode portion of the
649 A \obj{TCB} with a bound \obj{VCPU} has two execution modes; one is the original thread just as
650 if there was no bound \obj{VCPU}, and the other is the guest mode execution using the
651 \obj{VCPU}. Switching from regular execution mode into the guest execution mode is
653 it is scheduled thereafter, to execute using the higher privileged mode controlled by the \obj{VCPU}.
658 \obj{VCPU} state and execution is controlled through the \apifunc{seL4\_VCPU\_ReadVMCS}{x86_vcpu_readvmcs}
661 merely does enough validation on the parameters to ensure the \obj{VCPU} is not configured
662 to run in such a way as to violate any kernel properties. For example, it is not possible to
666 Memory access of the guest execution mode is controlled by requiring the use of Extended
672 continuing to provide translation when the TCB is executing in its normal mode.
679 if the I/O port capability is deleted for any reason the access will be correspondingly removed