Untyped Memory

Untyped memory is the raw physical memory from which all kernel objects are created. The kernel does not have a general-purpose heap allocator; instead, every kernel object (endpoints, TCBs, CNodes, VSpaces, MemoryObjects) is carved from an untyped region via the retype operation. This design, inherited from seL4, makes all kernel memory usage explicit and auditable.

UntypedMemory Structure

#[repr(C)]
pub struct UntypedMemory {
    pub header: KernelObject,       // obj_type = Untyped (1)
    pub phys_addr: PhysAddr,        // physical address of the region
    pub size_bits: u8,              // log2 of region size (e.g., 20 = 1 MB)
    pub watermark: u64,             // next allocation offset within the region
    pub is_device: bool,            // device memory (non-cacheable, non-zeroable)
    pub alloc_lock: SpinLock,       // protects watermark + free_list for concurrent MO_COMMIT
    pub free_list_head: u64,        // head of intrusive free list (phys addr)
    pub free_list_count: u32,       // pages on the free list
}

size_bits

The region covers 2^size_bits bytes. Common values: 12 (4 KB), 20 (1 MB), 30 (1 GB).

watermark

Byte offset of the next allocation within the region. Advances forward on retype, never backwards unless reset.

is_device

Device untyped (MMIO regions). Can only be retyped into Frame or Untyped. Not zero-filled.

free_list_head

Intrusive free list for reclaimed pages. Each free page stores the next pointer at its virtual address via the direct physical map.

Retype Operation

UNTYPED_RETYPE (invoke label 0x20) carves typed kernel objects from an untyped region.

Arguments

Argument Description

Argument	Description
`new_type`	Target object type (Endpoint, CNode, Tcb, VSpace, Frame, Untyped, etc.).
`size_bits`	Size parameter (meaning depends on type: CNode slot count, frame size, etc.).
`num_objects`	Number of objects to create.
`dest_cnode`	Destination CNode capability address.
`dest_offset`	Starting slot index within the destination CNode.

new_type

Target object type (Endpoint, CNode, Tcb, VSpace, Frame, Untyped, etc.).

size_bits

Size parameter (meaning depends on type: CNode slot count, frame size, etc.).

num_objects

Number of objects to create.

dest_cnode

Destination CNode capability address.

dest_offset

Starting slot index within the destination CNode.

Algorithm

Validate device constraint: device untyped can only produce Frame or Untyped.
Compute object size: type-specific size calculation (see Object Sizes).
Validate destination range: dest_offset + num_objects must be within the CNode’s slot count. All destination slots must be empty.
Check available space: watermark + total_size must not exceed 2^size_bits.
Align the watermark: round up to type-specific alignment (see Alignment Rules).
For each object:
1. Allocate physical address: phys_addr + watermark, advance watermark by object size.
2. Initialize the object in memory (zero-fill for RAM-backed, type-specific init).
3. Allocate a fresh global capability slot.
4. Write a capability with CapRights::ALL, depth 0, badge 0.
5. Insert the new slot as a CDT child of the untyped capability.
6. Insert the new slot into the untyped-child list (UntypedTracker::add_child).
7. Write a CapRef into the destination CNode slot.

Security Invariant

Newly retyped RAM-backed frames are zero-filled before exposure to userspace. This prevents information leakage from previous owners of the physical memory.

Object Sizes

Object size computation is type-specific:

Object Type Size

Object Type	Size
`Endpoint`	`size_of::<Endpoint>()` (includes 128-entry NBSend ring buffer).
`Notification`	`size_of::<Notification>()`.
`CNode`	`size_of::<CNode>() + (2^effective_bits * size_of::<CapRef>())`. The `effective_bits` function maps `size_bits = 0` to default 10, rejects < 4 and > 16.
`Tcb`	`size_of::<Tcb>()` (large: includes FPU save area, IPC message buffer, recv wait links).
`VSpace`	`VSPACE_OBJECT_SIZE` = `PAGE_SIZE + VSPACE_TRACKING_SIZE`. First page is the hardware page table root; remainder is embedded `VSpaceTracking`.
`Frame`	`2^max(size_bits, 12)`. Minimum 4 KB (one page).
`Untyped`	`2^size_bits`. Creates a sub-untyped.
`MemoryObject`	`required_bytes(page_count)`, rounded up to page alignment. The struct itself is small; radix tree nodes are allocated separately from PMM.
`SchedContext`	`size_of::<SchedContext>()`.
`IrqHandler`	`size_of::<IrqHandler>()`.
`IoPort`	`size_of::<IoPortRange>()`.

Endpoint

size_of::<Endpoint>() (includes 128-entry NBSend ring buffer).

Notification

size_of::<Notification>().

CNode

size_of::<CNode>() + (2^effective_bits * size_of::<CapRef>()). The effective_bits function maps size_bits = 0 to default 10, rejects < 4 and > 16.

Tcb

size_of::<Tcb>() (large: includes FPU save area, IPC message buffer, recv wait links).

VSpace

VSPACE_OBJECT_SIZE = PAGE_SIZE + VSPACE_TRACKING_SIZE. First page is the hardware page table root; remainder is embedded VSpaceTracking.

Frame

2^max(size_bits, 12). Minimum 4 KB (one page).

Untyped

2^size_bits. Creates a sub-untyped.

MemoryObject

required_bytes(page_count), rounded up to page alignment. The struct itself is small; radix tree nodes are allocated separately from PMM.

SchedContext

size_of::<SchedContext>().

IrqHandler

size_of::<IrqHandler>().

IoPort

size_of::<IoPortRange>().

Alignment Rules

The watermark is rounded up to type-specific alignment before each object:

Type Alignment

Type	Alignment
CNode	`align_of::<CNode>()` (8 bytes on 64-bit).
VSpace	`PAGE_SIZE` (4,096 bytes) — hardware page table root must be page-aligned.
Frame	Object size (power-of-2 alignment matches the frame size).
MemoryObject	`PAGE_SIZE` (struct + radix tree nodes are page-aligned).
All others	Object size.

CNode

align_of::<CNode>() (8 bytes on 64-bit).

VSpace

PAGE_SIZE (4,096 bytes) — hardware page table root must be page-aligned.

Frame

Object size (power-of-2 alignment matches the frame size).

MemoryObject

PAGE_SIZE (struct + radix tree nodes are page-aligned).

All others

Object size.

Dual Tracking

Each retyped object is tracked in two independent linked lists:

CDT (Capability Derivation Tree): The new capability slot is a CDT child of the untyped capability slot. This enables revocation: revoking the untyped capability destroys all objects created from it.
Untyped-child list: The ut_first_child / ut_next links in CapSlotMeta form a separate singly-linked list per untyped. This allows has_children() and reset() to check whether the untyped has live objects without walking the entire CDT.

Free-List Reclamation

When an MO decommits a page that was allocated from an untyped source, the frame is returned to the untyped’s free list rather than to the PMM:

The decommitted frame’s physical address is written as the next pointer at the frame’s virtual address (via direct map).
The frame is linked at the head of free_list_head.
free_list_count is incremented.

Subsequent MO_COMMIT operations on the same untyped check the free list before advancing the watermark, providing O(1) frame reuse.

The alloc_lock protects both the free list and watermark for concurrent access from multiple MO_COMMIT operations (lock ordering: mo.commit_lock → ut.alloc_lock).

Device Untyped

Untyped regions backed by device memory (MMIO ranges) have is_device = true.

Restrictions:

Can only be retyped into Frame or Untyped.
Frames from device untyped are not zero-filled (device MMIO has side effects on read/write).
Device frames are typically mapped with ENTRY_CACHE_DISABLE or write-through caching in the VSpace.

Common uses: framebuffer memory, virtio device MMIO regions, PCI ECAM config space.

Untype and Reset

Untype

Reclaims a single object back to its parent untyped. The untype() operation refuses unless:

The object’s ut_parent matches the caller’s untyped slot.
The object has no CDT children (no derived capabilities).
The object’s reference count is exactly 1.

If the conditions hold, CDT::revoke() runs the full revocation and deletion path on the object’s slot.

Reset

UntypedTracker::reset() clears the watermark back to zero, making the entire region available for retyping again. Reset is only permitted when the untyped-child list is empty (no live objects).

Reset does not free the untyped’s physical memory or modify any external state. It simply resets the allocation pointer.

Initial Untyped Distribution

During boot, the kernel creates untyped capabilities for all available physical memory regions reported by the boot info. These are placed in the init task’s CSpace starting at CAP_UNTYPED_START (slot 16).

Each memory map entry of type Usable produces one untyped capability. The size_bits is set to match the region size. Device memory regions (framebuffer, initrd) produce device untyped capabilities.

The init task (and later, mmsrv) distributes untyped memory to child processes by retyping smaller sub-untypeds or by committing pages through MemoryObjects.

Error Conditions and Edge Cases

Retype Errors

Error Cause

Error	Cause
`InvalidOperation`	Device untyped retyped into non-Frame/non-Untyped type.
`InvalidArgument`	CNode `size_bits` outside valid range (1-3 or >16).
`InvalidSlot`	Destination slot range exceeds CNode capacity.
`SlotOccupied`	One or more destination slots are not empty.
`NotEnoughMemory`	Watermark + total_size exceeds the untyped region.
`OutOfSlots`	Global capability slot array is exhausted.

InvalidOperation

Device untyped retyped into non-Frame/non-Untyped type.

InvalidArgument

CNode size_bits outside valid range (1-3 or >16).

InvalidSlot

Destination slot range exceeds CNode capacity.

SlotOccupied

One or more destination slots are not empty.

NotEnoughMemory

Watermark + total_size exceeds the untyped region.

OutOfSlots

Global capability slot array is exhausted.

Exhaustion

When an untyped’s watermark reaches the end of the region, no more objects can be retyped from it. The watermark never moves backwards except via explicit reset().

If the free-list has reclaimed pages, MO_COMMIT can still allocate from the free list even when the watermark is exhausted. However, UNTYPED_RETYPE does not use the free list — it only advances the watermark.

Partial Retype

If a retype request asks for multiple objects and fails partway (e.g., slot 3 of 5 is occupied):

The validation pass checks all destination slots before allocating anything.
If validation passes, all objects are created atomically.
There is no partial creation — either all objects are created or none.

Concurrent MO_COMMIT on Same Untyped

Multiple threads can call MO_COMMIT on MemoryObjects backed by the same untyped simultaneously. The alloc_lock on the untyped serializes watermark advances and free-list pops. Lock ordering: mo.commit_lock → ut.alloc_lock.

Device Untyped Peculiarities

Device frames are not zero-filled (device MMIO may have side effects on read/write).
Device frames cannot be used as MemoryObject data pages (only as direct VSpace frame mappings).
Retyping device untyped into any type other than Frame or Untyped returns InvalidOperation.

Object Model — object creation lifecycle
Capabilities — CDT parent tracking during retype
CSpace — destination CNode slot installation
Design Patterns — memory allocation patterns
Memory Objects — MO commit uses untyped as primary frame source
Capability Invocations — UNTYPED_RETYPE label 0x20