Object Model

Every resource managed by the kernel — threads, memory regions, IPC endpoints, address spaces — is represented as a kernel object. Access to kernel objects is mediated exclusively through capabilities; there is no other path.

Object Types

Kernite defines 12 object types:

Type Discriminant Description

Null

0

Empty placeholder. Null capabilities point to no object.

Untyped

1

Raw physical memory. Source of all other kernel objects via the retype operation. See CSpace.

Endpoint

2

Synchronous IPC channel. See Endpoints.

Notification

3

Asynchronous signaling word. See Notifications.

Tcb

4

Thread Control Block. Represents a schedulable thread. See Threads.

CNode

5

Capability storage node. An array of capability references forming part of a thread’s CSpace. See CSpace.

VSpace

6

Virtual address space (page table root). See Virtual Address Spaces.

Frame

7

Physical memory frame. Legacy path; new code uses MemoryObject.

IrqHandler

8

Hardware interrupt handler binding. Routes an IRQ to a notification.

IoPort

9

I/O port range (x86_64) or MMIO region (aarch64).

SchedContext

10

Scheduling parameters: budget, period, deadline, priority. Bound to a TCB.

MemoryObject

11

Page-granular memory abstraction with COW support. See Memory Objects.

The discriminant values are defined in cap/object.rs as the ObjectType enum:

#[repr(u8)]
pub enum ObjectType {
    Null = 0,
    Untyped = 1,
    Endpoint = 2,
    Notification = 3,
    Tcb = 4,
    CNode = 5,
    VSpace = 6,
    Frame = 7,
    IrqHandler = 8,
    IoPort = 9,
    SchedContext = 10,
    MemoryObject = 11,
}

KernelObject Header

Every kernel object begins with a KernelObject header:

#[repr(C)]
pub struct KernelObject {
    pub obj_type: ObjectType,  // 1 byte
    pub size_bits: u8,         // 1 byte
    pub ref_count: AtomicU32,  // 4 bytes
    pub _reserved: u32,        // 4 bytes
}
Field Type Size Purpose

obj_type

ObjectType

1 byte

Discriminant identifying the object type.

size_bits

u8

1 byte

Log2 of the object’s size in bytes. Meaning depends on type (e.g., CNode slot count, frame size).

ref_count

AtomicU32

4 bytes

Number of capabilities that reference this object.

_reserved

u32

4 bytes

Padding, reserved for future use.

The header uses #[repr©] layout. Object-specific data follows immediately after the header, so a pointer to any kernel object can be safely cast to *mut KernelObject to access the common fields.

KernelObject must be the first field of every kernel object struct. This invariant enables reference counting and type checking through raw pointer casts.

Object Creation

Kernel objects are created by retyping untyped memory. The Untyped::retype operation (syscall 9, invoke label 0x20) carves a region from an untyped memory capability and initializes it as a specific object type.

The creation flow:

  1. The caller invokes retype on an untyped capability, specifying the target object type, size, and destination CNode slots.

  2. The kernel validates alignment, size, and slot availability.

  3. For each requested object:

    1. A fresh global capability slot is allocated.

    2. Object storage is initialized at the appropriate physical address within the untyped region.

    3. A capability is written with CapRights::ALL, depth 0, and badge 0.

    4. The new slot is inserted as a child of the untyped in both the CDT and the untyped-child list.

    5. A CapRef is written into the destination CNode slot.

The retyped object has two structural parents:

  • Its derivation parent in the Capability Derivation Tree (CDT)

  • Its storage parent in the untyped-child tracking list

These are related but distinct structures. See Derivation Tree for details.

Reference Counting

Each kernel object carries an AtomicU32 reference count. The count represents the number of capability slots that reference this object.

Rules

  • A newly created object starts with ref_count = 1.

  • Capability::copy() and Capability::mint() increment the reference count.

  • Deleting a capability slot (CDT::delete_capability()) decrements the reference count.

  • When the count reaches zero, destroy_object() normally runs immediately. Exception: for Tcb objects, reaching zero sets pending_destroy and defers actual destruction until flush_deferred_current_release() runs after sched_ref drops to zero.

Atomic Ordering

Increments use fetch_add(1, AcqRel). Decrements use fetch_sub(1, AcqRel). Reads use load(Acquire).

The AcqRel ordering on modifications ensures that destruction observes all preceding writes from other cores.

Object Destruction

When the last capability reference to an object is released, destroy_object() performs type-specific cleanup:

Object Type Destruction Behavior

Endpoint

Wake all threads blocked in send and receive queues.

Notification

Wake any thread waiting on the notification.

Untyped

Free backing physical frames to the PMM.

Frame

Free the represented frame(s) to the PMM.

MemoryObject

Tear down reverse maps, free all backing pages to their respective sources (untyped or PMM).

CNode

Walk every stored CapRef and recursively delete each referenced capability.

VSpace

Run page table cleanup (unmap all entries, free page table pages).

Tcb

Thread cleanup. The scheduler holds a sched_ref on running TCBs; actual destruction is deferred until both the cap refcount and sched_ref reach zero. pending_destroy is set when the last cap is deleted; flush_deferred_current_release runs the actual destroy_object.

IrqHandler

Detach from the IRQ routing table.

IoPort

No cleanup required.

SchedContext

Unbind from TCB, remove from replenishment queue.

Null

No action.
CNode destruction triggers recursive capability deletion. Destroying a CNode therefore has authority consequences — it revokes access to every object referenced through that CNode.

Object Lifetime

Kernel objects are never returned to a general-purpose allocator. They remain owned by their parent untyped memory for the lifetime of the system. The untype operation can reclaim an object’s storage back to the parent untyped, but only when:

  • The object’s untyped parent matches the caller’s untyped capability

  • The object has no CDT children (no derived capabilities)

  • The object’s reference count is exactly 1

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

Diagram
TCB destruction is deferred. For Tcb objects the diagram above is not a single-step transition from "last capability deleted" to "Destroyed." Deletion sets pending_destroy, but destroy_object() runs only when flush_deferred_current_release() executes — after sched_ref drops to zero. See TCB Deferred Destruction below.

TCB Deferred Destruction

TCBs use a dual-refcount model to handle the window where the scheduler is actively running a thread whose last capability has been deleted.

sched_ref

Held by the scheduler while the TCB is the current thread on any CPU. Prevents destruction while the thread is on-CPU.

Cap refcount

Tracks the number of Tcb capabilities in existence. Managed by the standard KernelObject.ref_count.

Protocol:

  1. When the last Tcb capability is deleted, the cap refcount reaches zero. Instead of running destroy_object() immediately, the cap system sets pending_destroy = true on the TCB and returns.

  2. When the scheduler finishes with the thread (context switch away, or the thread was never running), it drops sched_ref.

  3. flush_deferred_current_release() checks pending_destroy and, if set, calls destroy_object() to perform actual cleanup (remove from scheduler queues, release bound SchedContext, unmap IPC buffer, etc.).

This ensures destroy_object() is never called while the thread is the current thread on a CPU, avoiding use-after-free in the scheduler’s fast path.

Related Pages

  • Capabilities — the fat capability structure and operations

  • CSpace — capability storage and address resolution

  • Memory Objects — the MemoryObject type in detail