manual/parts/objects.tex

9 A limited number of service primitives are provided by the microkernel;
10 more complex services may be implemented as applications on top of these
11 primitives. In this way, the functionality of the system can be extended
13 still supporting a potentially wide number of services for varied
21     \item[Threads] are an abstraction of CPU execution that supports
24     \item[Scheduling contexts] (MCS only) are an abstraction of CPU execuion time.
47 This chapter gives an overview of these services, describes how kernel
62 degree of assurance, as only those operations explicitly authorised by
72 address of the slot holding that capability.  This means, the seL4
73 capability model is an instance of a \emph{segregated} (or \emph{partitioned})
76 Capability spaces are implemented as a directed graph of kernel-managed
77 \emph{capability nodes} (\obj{CNode}s).  A \obj{CNode} is a table of
79 address of a capability in a capability space is the concatenation of the indices
80 of slots within \obj{CNodes} forming the path to the destination
84 also sent via IPC. This allows creation of applications with specific
85 access rights, the delegation of authority to another application, and
88 create a derived capability with a subset of the rights of the
90 capability can be used for partial delegation of authority.
94 been derived from the original capability being revoked. The propagation of
116 number of data words and possibly some capabilities. The structure and encoding
117 of these messages are described in detail in \autoref{ch:ipc}.
123 interpreted as a method invocation in a manner specific to the type of kernel
130 % making these prose descriptions of the system calls legitimate targets for
135 combinations and variants of the basic \emph{Send} and \emph{Receive} calls.  An
136 important variant is the \emph{Call} operation, which consists of a standard
137 \emph{Send} operation atomically followed by a variant of \emph{Receive} which
139 special resource instead of using the standard IPC mechanism; see
148 configuration, \emph{Wait} is a variant of \emph{Receive} that does not require
155     not require a capability to be used.  It forfeits the remainder of the
156     calling thread's timeslice and causes invocation of the kernel's scheduler.
159     the MCS configuration, this behaviour depends on the state of the scheduling
186 The remaining system calls are variants and combinations of
234     exists mostly for efficiency reasons, namely the common case of replying to
236     system call instead of two.  The transition from the reply to the receive
261 In this section we give a brief overview of the kernel-implemented
264 of kernel services is achieved by the creation,
265 manipulation, and combination of these kernel objects:
271     Each \obj{CNode} has a fixed number of slots,
272     always a power of two, determined when the \obj{CNode} is created. Slots
275     \item[Thread Control Blocks] (\obj{TCB}s; see \autoref{ch:threads}) represent a thread of
276     execution in seL4. Threads are the unit of execution that is
298     capabilities as part of the message.
306       is a word-size array of flags, each of which behaves like a binary semaphore. Operations
307       are \emph{signalling} a subset of flags in a single operation,
315     objects largely directly correspond to those of the hardware, and
317     Pool} and \obj{ASID Control} objects for tracking the status of
323     which allows for the creation of \obj{IRQHandler} capabilities.
324     An \obj{IRQHandler} capability permits the management of a specific
331     \item[Untyped Memory] (see \autoref{sec:kernmemalloc}) is the foundation of memory allocation
333     which allows the creation of new kernel objects. If the method
336     divided into a group of smaller untyped memory objects allowing
337     delegation of part (or all) of the system's memory.  We discuss
349 order to create new objects, and all objects consume a fixed amount of memory once
351 the specific amount of physical memory available to applications,
352 including being able to enforce isolation of physical memory access
355 hardware\footnote{The treatment of virtual ASIDs imposes a fixed number
356 of address spaces. This limitation is to be removed in future
357 versions of seL4.}, and so many denial-of-service attacks via resource
365 the initial thread in the form of capabilities to \obj{Untyped Memory}, and
369 \apifunc{seL4\_Untyped\_Retype}{untyped_retype} method; the created objects are termed \emph{children} of
374 all or part of the authority it possesses over this object to one or
375 more of its clients.
377 Untyped memory objects represent two different types of memory:
382 as determined by the hardware platform, and usage of these objects
389 in the creation of an ASID pool
393 \emph{device} memory) of a child untyped object is inherited from its
394 parent untyped object. That is, any child of a device untyped will
395 also be a device untyped. Developers cannot change the type attribute of an untyped.
407 Reusing a region of memory is allowed only
416 data structure, it is implemented as part of the CNode object and so
419 capabilities would be inserted into the CDT as children of the untyped
423 a \emph{watermark} recording how much of the region has previously been
425 an untyped memory region, the kernel will carry out one of two actions:
430 allocating new objects from the beginning of the region again.
439 object, the user removes all of the untyped memory object's
445 \subsection{Summary of Object Sizes}
457 the size of the resulting objects.
465     Type & Meaning of \texttt{size\_bits} & Size in Bytes  \\
467     \obj{CNode} & $\log_2$ number of slots & $2^\texttt{size\_bits} \cdot 2^\texttt{seL4\_SlotBits}$
475   \caption{\label{tab:objsize} Meaning of \texttt{size\_bits} for object types of
480 single \obj{Untyped Object} into multiple objects. The number of objects
482 objects must be of the same type, specified by the \texttt{type} argument. In
483 the case of variable-sized objects, each object must also be of the same size.
484 If the size of the memory area needed (calculated by the object size multiplied
485 by \texttt{num\_objects}) is greater than the remaining unallocated memory of