manual/parts/objects.tex

26     \item[Address spaces] are virtual memory spaces that each contain an
27     application. Applications are limited to accessing memory in their
331     \item[Untyped Memory] (see \autoref{sec:kernmemalloc}) is the foundation of memory allocation
332     in the seL4 kernel.  Untyped memory capabilities have a single method
335     newly-created objects. Additionally, untyped memory objects can be
336     divided into a group of smaller untyped memory objects allowing
337     delegation of part (or all) of the system's memory.  We discuss
338     memory management in general in the following sections.
345 The seL4 microkernel does not dynamically allocate memory for kernel objects.
346 Instead, objects must be explicitly created from application-controlled memory
348 explicit authority to memory (through these \obj{Untyped Memory} capabilities) in
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
360 At boot time, seL4 pre-allocates the memory required for the kernel
364 The kernel then hands all remaining memory to
370 the original untyped memory object.
377 Untyped memory objects represent two different types of memory:
378 general purpose memory, or device memory.
379 \emph{General purpose} memory can be untyped into any other object
380 type and used for any operation on untyped memory provided by the kernel.
381 \emph{Device memory} covers memory regions reserved for devices
387 untyped objects; developers cannot, for example, create an endpoint from device memory.
393 \emph{device} memory) of a child untyped object is inherited from its
407 Reusing a region of memory is allowed only
409 objects inside that memory.  The kernel tracks
418 creates new kernel objects by retyping untyped memory, the newly created
420 memory capability.
425 an untyped memory region, the kernel will carry out one of two actions:
438 By calling \apifunc{seL4\_CNode\_Revoke}{cnode_revoke} on the original capability to an untyped memory
439 object, the user removes all of the untyped memory object's
441 memory region.  Thus, after this invocation there are no valid references
448 When retyping untyped memory it is useful to know how much memory the
452 have variables sizes. When retyping untyped memory into \obj{CNode}s
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