CSpace

A thread’s CSpace (capability space) is the namespace through which it addresses capabilities. A CSpace is a tree of CNodes rooted at the thread’s CSpace root capability (slot 2 in the initial CSpace layout). The kernel resolves capability addresses by walking this tree using a guard-and-radix scheme inherited from seL4.

Global Slot Array

All live capabilities are stored in a single, boot-time allocated array of CapSlotStorage entries. CNodes do not embed capability payloads; they store CapRef indices into this global array.

Sizing

cap::init() allocates the array during boot based on available physical memory:

num_slots = clamp(free_frames / 4, 768, 131_072)

The floor of 768 covers the standard 6-service boot with test forks. Above approximately 3,000 frames the linear term dominates.

The array is allocated as contiguous physical frames mapped through the direct physical map. A companion bitmap tracks which slots are free.

Slot Storage

Each entry in the array stores both the capability payload and its metadata:

#[repr(C)]
pub struct CapSlotStorage {
    pub cap: Capability,       // 32 bytes
    pub meta: CapSlotMeta,     // CDT + untyped tracking + state
}
#[repr(C)]
pub struct CapSlotMeta {
    pub cdt_parent: CapSlot,      // CDT parent slot
    pub cdt_first_child: CapSlot, // CDT first child
    pub cdt_next: CapSlot,        // CDT next sibling
    pub cdt_prev: CapSlot,        // CDT previous sibling
    pub ut_first_child: CapSlot,  // Untyped child list head
    pub ut_next: CapSlot,         // Untyped child list next
    pub ut_parent: CapSlot,       // Parent untyped slot
    pub state: SlotState,         // Free | Occupied
}

CapSlot is u32. INVALID_SLOT = 0xFFFF_FFFF serves as the null marker.

The metadata carries two independent linked-list structures:

CDT links (cdt_parent, cdt_first_child, cdt_next, cdt_prev)

Track the Capability Derivation Tree.

Untyped links (ut_first_child, ut_next, ut_parent)

Track which objects were retyped from which untyped memory.

These structures are related but distinct. A retyped object has both a CDT parent (the source untyped capability that was invoked) and an untyped parent (the untyped memory region that physically backs it).

Slot Allocation

The allocator uses a bitmap with a NEXT_SLOT cursor for first-fit-with-wrap allocation. alloc_slot() returns None when all slots are exhausted. Slot pressure is a system-wide resource, not per-process.

CNode Structure

A CNode is a kernel object that stores an array of CapRef entries. Each CapRef is a 4-byte index into the global slot array.

Memory Layout

#[repr(C)]
pub struct CNode {
    pub header: KernelObject,  // 12 bytes (size_bits = log2 of slot count)
    pub guard_bits: u8,        //  1 byte
    _pad: [u8; 3],             //  3 bytes
    pub guard: u64,            //  8 bytes
    // CapRef[2^size_bits] follows contiguously in memory
}

The CapRef array begins immediately after the guard field and is accessed via pointer arithmetic.

Size Constraints

size_bits = 0

Default to 10 (1,024 slots)

size_bits 1-3

Rejected (InvalidArgument)

size_bits 4-16

Accepted as-is (16 to 65,536 slots)

size_bits > 16

Rejected (InvalidArgument)

CNode::init_at() writes the header, sets guard_bits = 0 and guard = 0 (flat mode), and fills every slot with CapRef::null() (INVALID_SLOT).

CapRef

#[repr(C)]
pub struct CapRef {
    pub slot: u32,  // index into global slot array
}

A null CapRef has slot = INVALID_SLOT = 0xFFFF_FFFF.

Because CNodes store references rather than embedded payloads:

  • Multiple CNodes can point to the same global slot via the same CapRef.

  • Move operations transfer CSpace visibility without copying capability state.

  • CDT and untyped tracking remain attached to the actual global slot.

Deleting a CNode entry (setting it to CapRef::null()) does not delete the capability. It only removes one CSpace-level reference to a global slot.

Address Resolution

Capability addresses are resolved by walking the CNode tree from a thread’s CSpace root. Each CNode level consumes a portion of the address bits.

Algorithm

Given a capability address cap_addr and a total address width addr_bits:

  1. Check recursion depth against MAX_RESOLVE_DEPTH = 8.

  2. Read the current CNode’s guard_bits and radix (from header.size_bits).

  3. Verify that bits_remaining >= guard_bits + radix.

  4. If guard_bits > 0, extract and compare the guard prefix from the most significant remaining bits. Fail with GuardMismatch if they differ.

  5. Extract the radix-width slice to compute a slot index.

  6. If no address bits remain, the resolution is complete — return the capability at this slot.

  7. If bits remain and the slot contains a CNode, recurse into that CNode with the remaining bits.

  8. If bits remain but the slot does not contain a CNode, fail with InvalidSlot.

Address Bit Interpretation

A capability address is consumed left-to-right as a sequence of guard-then-radix segments:

[guard₁][radix₁][guard₂][radix₂]...[guardₙ][radixₙ]

For example, a two-level CSpace with a 10-bit root CNode (guard_bits=0, size_bits=10) containing a 6-bit second-level CNode (guard_bits=0, size_bits=6) at slot 5:

Address: 0x0005_002A (16 bits)
         [  10 bits  ][ 6 bits ]
         [root index ][ L2 idx ]
         [    5      ][  42    ]

Resolution follows slot 5 in the root CNode to find the L2 CNode, then indexes slot 42 in L2.

Diagram

Error Types

Address resolution distinguishes specific failure modes:

InvalidSlot

Slot index out of bounds, or remaining bits but no CNode to follow.

SlotEmpty

The addressed slot contains CapRef::null().

GuardMismatch

The guard prefix in the address does not match the CNode’s guard value.

DepthExceeded

Resolution exceeded MAX_RESOLVE_DEPTH (8) levels.

Initial CSpace

The init task receives a statically-backed CNode with 4,096 slots (size_bits = 12). The kernel populates well-known slots during bootstrap:

Slot Name Description

0

CAP_SELF_TCB

Thread’s own TCB

1

CAP_SELF_VSPACE

Thread’s page table root

2

CAP_SELF_CSPACE

Thread’s CNode root

6

CAP_KBD_IOPORT

PS/2 keyboard I/O port (x86_64)

7

CAP_KBD_IRQ

PS/2 keyboard IRQ handler (x86_64)

8

CAP_COM1_IOPORT

COM1 serial I/O port

9

CAP_COM1_IRQ

COM1 IRQ handler

10

CAP_COM1_NOTIFICATION

COM1 IRQ notification

11

CAP_IRQ_CONTROL

IRQ control capability

12

CAP_INITRD_UNTYPED

Initrd device untyped

13

CAP_FB_UNTYPED

Framebuffer device untyped

15

CAP_PCI_IOPORT

PCI config space I/O port

16+

CAP_UNTYPED_START

Untyped memory capabilities (one per available region)

The aarch64 init CNode reuses the same three mandatory slots (0/1/2), then fills the I/O and untyped-range slots with MMIO-oriented objects (PL011 device untyped, interrupt handler).

Every other slot is an init-only convenience carved by init.rs; userland library code MUST NOT hardcode these positions.

Role-Based Capability Table (Children)

Child processes spawned by procmgr no longer receive a fixed slot map. Only the three mandatory slots are stable for every child:

Slot Name Description

0

CAP_SELF_TCB

Thread’s own TCB

1

CAP_SELF_VSPACE

Thread’s page table root

2

CAP_SELF_CSPACE

Thread’s CNode root

16+

CAP_UNTYPED_START

Untyped memory capabilities (procmgr-owned range)

All service endpoints (procmgr, vfs, namesrv, mmsrv, rsrcsrv, console, win32srv, …) arrive via a role capability table that the spawner builds and attaches to the new process. Userland resolves the capability by role, never by slot number.

Delivery: Auxv Tag

The spawner puts a pointer to a TronaCapTableV1 header on the child’s stack and exposes it through a single auxv entry:

Constant Value

AT_TRONA_CAP_TABLE

0x101C

TRONA_CAP_TABLE_MAGIC

0x43544153 ('SATC' little-endian)

TRONA_CAP_TABLE_VERSION

1

Each table row binds a role to a cursor-allocated CSpace slot plus the rights / flags that spawner policy granted.

Role ID Space

Range Meaning

0x0001-0x00FF

System roles — well-known endpoints/notifications/untypeds defined in lib/trona/uapi/consts/kernel.rs (ROLE_PROCMGR_CONTROL, ROLE_VFS_CLIENT, ROLE_MMSRV_CLIENT, ROLE_CONSOLE_CLIENT, ROLE_SIGNAL_NTFN, ROLE_PCI_IOPORT, ROLE_SC_CAP, …).

0x0100-0x0FFF (LOCAL_ROLE_BASE..LOCAL_ROLE_END)

Local roles — process-local identifiers reserved by the spawner; not portable across deployments.

0x1000+

Reserved for future raw / authority roles.

Lookup happens at runtime through trona::caps::* helpers — callers ask for a role and get back a resolved Capability, or None when the role was not provisioned. There are no hardcoded slot numbers anywhere in the child image.

Rights Bits (CAP_TBL_RIGHT_*)

Bit Name Meaning

0x01

READ

Row is readable (baseline for every live entry).

0x02

WRITE

Allows operations that mutate receiver state.

0x04

GRANT

Allows forwarding the capability via CNODE_COPY with GRANT.

0x08

INVOKE

Allows syscall 9 Invoke through this capability.

0x10

BADGE

Row carries a badge; receiver must treat source as an authenticated client.

0x20

DEVICE

Capability points at device-class memory (MMIO / I/O port / device untyped).

Flags Bits (CAP_TBL_FLAG_*)

Bit Name Meaning

0x01

BADGED

Row was minted with a non-zero badge.

0x02

RAW

Authority-grade capability (e.g. ROLE_MMSRV_AUTHORITY_RAW) — libraries must refuse to leak it.

0x04

OPTIONAL

Absence is legal; callers must tolerate None.

0x08

NOTIFICATION

Underlying object is a Notification, not an Endpoint.

0x10

UNTYPED

Untyped memory.

0x20

DEVICE_UT

Device untyped (non-zeroed on retype).

0x40

IO_PORT

IoPort capability (x86_64 port range, aarch64 MMIO window).

The BADGED / RAW / NOTIFICATION combinations let trona::caps pick the right runtime wrapper — a NOTIFICATION row returns a Notification, a plain endpoint row returns an Endpoint, and RAW gates access to authority-only operations.

Error Conditions and Edge Cases

Global Slot Exhaustion

When alloc_slot() returns None, no new capabilities can be created. This affects copy, mint, save_caller, and retype — all operations that allocate global slots.

Slot count is fixed at boot (clamp(free_frames / 4, 768, 131_072)). A system with heavy capability derivation (deep fork chains, many services) can exhaust slots before physical memory. There is no runtime slot expansion.

Multi-Level Resolution Failure Modes

Address resolution can fail at any level in the CNode tree:

Error Scenario

GuardMismatch

The address bits intended as the guard prefix do not match the CNode’s guard value. Common cause: using a flat-mode address against a guarded CNode (or vice versa).

DepthExceeded

The CNode tree is deeper than MAX_RESOLVE_DEPTH (8). This prevents infinite loops in malformed CSpace trees but limits maximum CSpace depth.

InvalidSlot

The address has remaining bits but the current slot does not contain a CNode — resolution cannot continue. Also returned when the slot index exceeds the CNode’s capacity.

SlotEmpty

The addressed slot contains CapRef::null(). The address is valid but nothing is stored there.

CNode Destruction Cascade

Destroying a CNode object triggers recursive capability deletion:

  1. destroy_object(CNode) iterates every CapRef in the CNode.

  2. For each non-null CapRef, CDT::delete_capability() runs the full deletion lifecycle.

  3. If a deleted capability is itself a CNode, its destruction triggers another recursive walk.

Recursion depth is bounded by MAX_RESOLVE_DEPTH (8) and MAX_DERIVATION_DEPTH (64). In practice, CNode trees rarely exceed 2-3 levels.

Deleting a CNode that contains the only references to critical objects (endpoints, VSpaces) will destroy those objects. This is the intended authority model: CNode ownership implies authority over everything it names.

Slot 0 Is Not Special

Slot 0 in a CNode is a valid, usable slot. The init CSpace places CAP_SELF_TCB at slot 0 by convention, not by kernel requirement. A CNode with all slots occupied at indices 0 through num_slots - 1 is fully valid.