manual/parts/objects.tex

66 object (such as a thread control block) and carries access rights that
121 message will be transferred through the kernel to another thread.
124 object. For example, invoking a thread control block (TCB) capability with a
125 correctly formatted message will suspend the target thread.
156     calling thread's timeslice and causes invocation of the kernel's scheduler.
158     the calling thread will immediately be scheduled with a fresh timeslice.  In
164     ready to receive the message immediately, the sending thread will block
168     \item[\apifunc{seL4\_Recv}{sel4_recv}] (``receive'') is used by a thread to
194     dropped.  The sending thread continues execution.  As with
197     \item[\apifunc{seL4\_NBRecv}{sel4_nbrecv}] is used by a thread to check for
205     some important differences.  The call blocks the sending thread until its
212     When the sent message is delivered to another thread via an \obj{Endpoint},
222     the calling thread is blocked until a capability to the reply object is
228     slot in the replying thread's TCB.  It has exactly the same behaviour as
245     \item[\apifunc{seL4\_NBWait}{sel4_nbwait}] (MCS only) is used by a thread to
275     \item[Thread Control Blocks] (\obj{TCB}s; see \autoref{ch:threads}) represent a thread of
285        control thread's access to CPU time.
288     communication between threads. IPC is synchronous: A thread
334     succeeds, the calling thread gains access to capabilities to the
363 thread (with an appropriate address and capability space).
365 the initial thread in the form of capabilities to \obj{Untyped Memory}, and
367 bootstrap the initial thread.  These \obj{Untyped Memory} regions can then be split into
388 \item Frame objects retyped from device untyped objects cannot be set as thread IPC buffers, or used