Kernel objects are held in a boot-sized metadata arena. The default reference configuration supports 65,536 live objects and one million capability slots. Limits are configurable before boot and immutable afterward.
| Object | Purpose |
|---|---|
Untyped |
authority over an aligned physical-memory interval |
Frame4K / Frame2M |
mappable memory frame |
PageTable |
one level of an address-space tree |
VSpace |
address-space root and mapping epoch |
CNode |
capability slot array |
Domain |
quota/accounting container for one protection domain |
Thread |
schedulable context |
Endpoint |
synchronous IPC rendezvous |
Reply |
kernel-only one-shot reply authority bound to a server thread |
Notification |
asynchronous bit notification |
Irq |
interrupt source and mask/ack state |
IoRegion |
bounded port-I/O or MMIO authority |
IommuDomain |
DMA translation domain |
Device |
PCI requester identity and reset authority |
Timer |
notification deadline |
DebugPort |
development-only diagnostic authority |
Every object has an internal (index: u32, generation: u32) identity. Reusing an
arena slot increments the generation; stale references fail rather than naming a
new object.
A capability is an unforgeable kernel record containing:
- object identity and generation;
- object type;
- immutable rights;
- optional badge;
- parent derivation reference;
- revocation epoch; and
- object-type-specific guard data.
Users name capabilities with a 64-bit CapPtr path through their root CNode.
CapPtr is not an object pointer and reveals no kernel address.
Common rights are Read, Write, Grant, GrantReply, Control, Map,
Execute, and Debug. Each object defines its meaningful subset. Minting can
remove rights or add a badge; it cannot add rights. Moving preserves rights and
invalidates the source slot atomically.
- Every occupied slot names one live object generation.
- A child’s rights are a subset of its parent’s rights.
- Only the kernel creates root authority.
- A badge cannot increase authority.
- A capability operation either completes entirely or leaves all slots unchanged.
- Revocation removes every live descendant existing at the selected epoch.
- Object destruction requires zero capabilities, zero mappings, no queued IPC, and no in-flight machine action referencing the object.
The derivation structure uses a bounded intrusive metadata tree. Revocation is restartable: each syscall performs bounded work and returns a continuation token when more descendants remain. This prevents a hostile capability tree from monopolizing the kernel.
The root task receives Untyped capabilities for usable physical ranges not
retained by the kernel. Untyped.Retype:
- validates alignment, size, object count, and non-overlap;
- reserves object metadata;
- zeroes any memory that could become user visible;
- creates typed objects; and
- installs capabilities into empty destination slots atomically.
Retyping never converts MMIO or firmware-reserved memory into ordinary frames. An untyped interval cannot be simultaneously retyped into overlapping objects. Reclaim requires destruction of every descendant object.
Endpoints provide synchronous rendezvous with FIFO ordering within effective priority. Supported operations are:
Send: enqueue or transfer a one-way message;Recv: receive or block;Call: send and block with a one-shot reply object;Reply: reply to the server thread’s current caller;ReplyRecv: reply and atomically wait for the next request.
The fast path carries:
- a 32-bit protocol/message tag;
- four 64-bit words in registers;
- a sender badge; and
- up to two capability transfers described in the UTCB.
The per-thread user communication buffer (UTCB) carries up to 64 additional words, transfer-slot paths, fault records, and protocol metadata. Large payloads use shared frame grants.
- The sender needs
Grantto transfer a derived capability. - The receiver chooses empty destination slots before blocking.
- Rights are intersected with the sender-specified mask.
- A failed transfer delivers neither message nor partial capabilities.
- Reply objects are kernel-created, never installed in a CNode, non-transferable, single-use, and destroyed on reply, caller cancellation, or server death.
- A server thread has at most one active reply. Receiving another
Callbefore consuming it is rejected;ReplyRecvis the normal server loop. - Sender identity is represented by the receiver-minted endpoint badge; global process IDs are not trusted for authorization.
A notification contains a 64-bit pending bitmap and a wait queue. Signaling ORs bits; waiting atomically consumes the current bits or blocks. IRQ and timer objects signal notifications.
Notifications do not carry capabilities or arbitrary messages. This separation keeps interrupt delivery asynchronous while RPC remains typed and synchronous.
Call donates the caller’s effective priority to the receiving server while the
reply object is live. Donation:
- is bounded to eight nested call edges;
- tracks a visited-thread bitmap to reject cycles;
- is removed on reply, timeout, cancellation, or server death; and
- never changes the thread’s base priority.
If the bound would be exceeded, Call fails with E_DEPTH before mutating queues.
The rule prevents common priority inversion without requiring unbounded graph
reasoning in the kernel.
A thread is in exactly one state:
Inactive
Ready(cpu)
Running(cpu)
BlockedSend(endpoint)
BlockedRecv(endpoint)
BlockedReply(reply)
BlockedNotification(notification)
Faulted(fault_id)
Suspended
Dead
A thread appears in at most one queue, and Running(cpu) is bijective with the
CPU’s current-thread field. Transition helpers remove the old queue membership
before installing the new state.
Each thread owns:
- saved integer and FPU contexts;
- one quota/accounting domain;
- a VSpace and root CNode capability reference;
- UTCB address and validated mapping generation;
- base/effective priority and affinity;
- fault endpoint capability.
User exceptions become messages to the thread’s fault endpoint:
- fault kind and architecture error code;
- RIP, RSP, RFLAGS, and fault address when relevant;
- access type;
- VSpace mapping epoch; and
- a non-transferable fault-reply token.
The pager may map memory and resume with validated registers, terminate the
thread, or forward policy to procd. A stale fault token cannot resume a later
fault.
Kernel-mode page faults, invalid internal object references, and failed invariant checks are fail-stop kernel faults.
The first executable fault-policy transition is accepted in Thermite. It proves that a valid live user thread with a fault endpoint receives an exact generation-tagged fault action carrying vector/error, decoded page access, CR2, and VSpace epoch; absence of the endpoint terminates the thread without creating a reply generation. Fatal architectural vectors, kernel exceptions, corrupt page-fault metadata, missing thread state, invalid frames/vectors, overflow, and stop requests produce an exact reason and latch fail-stop state with rescheduling cleared. The same transition classifies timer, reschedule, TLB, device, quarantine, and spurious events without conflating those actions with fault delivery.
The accepted claim ends at the returned state/action pair. Current-thread and endpoint lookup, fault-token object allocation, scheduler queue mutation, platform masking/acknowledgement, TLB invalidation, and the concrete frame-to- event/action-to-machine bridge are still later verified transitions. See M1 exception-dispatch policy.
The platform-to-core boundary now has an accepted safe-slice decoder for the
exact saved exception-frame layouts. It validates the 21-word kernel or 23-word
user shape, selectors, return-address class, restricted RFLAGS, vector, and user
stack tail before constructing ExceptionEvent. Captured CR2, vector, error,
and privilege origin come only from their proved common-entry offsets. The
verified function calls the accepted Thermite policy in the same crate, and any
malformed slice fail-stops before a recoverable action can be returned.
This closes value normalization, not pointer ownership: the eventual dispatcher must still prove the RDI range before creating the slice, snapshot per-CPU/current- thread context under the kernel lock, and execute the returned action. See M1 exception-frame bridge.
The platform side now has an accepted exact 93-byte front end for the raw RDI
frame pointer. Under explicit readable-frame and returning-scalar obligations,
it performs the conditional six-word kernel/eight-word user reads and transports
CR2, error, RIP, RFLAGS, optional user RSP, vector, CS, and SS through six SysV
scalars. The direct Verus model proves the frame and RBX are unchanged, RSP
advances exactly eight bytes over the inherited return address, and the tail
target is exactly 0xffffffff80011200. The scalar inherits the correct
dispatcher-entry SysV alignment and returns through the common-entry return
address without another stack write. The readable return target is fixed to the
common-entry continuation at 0xffffffff80011038. Three runtime consumers and
three fixed-address links reproduce; thirteen artifact/proof negatives fail. See
M1 dispatcher-front capsule.
This component alone is not the platform-to-core transition. The scalar and per-CPU wrapper checkpoints below subsequently join these values to a verified adapter while retaining this front end's narrow raw-read contract.
The common-entry caller now discharges the dispatcher front's concrete
frame-memory obligations in one direct-Verus composition. A registered stack
interval covers the worst-case aligned call word at entry_rsp - 144, the
128-byte saved-register block, the 40-byte normalized kernel suffix, and the
additional 16-byte user RSP/SS tail only for a privilege transition. The proof
establishes RDI/frame identity, DF clear, an RSP congruent to eight modulo 16,
the exact common continuation, call/frame non-overlap, and returning
frame/RBX-preserving scalar behavior through final IRETQ state.
Three model, consumer, and two-section link products reproduce byte-for-byte; both accepted instruction images post-link-match independently, and eleven artifact/proof negatives fail. See M1 exception entry/dispatcher join.
The standalone join ends at the scalar body. Its obligations are consumed by the later scalar entry and per-CPU wrapper without broadening the two accepted instruction images.
The concrete scalar-core ABI is a fixed 640-byte, 80-u64 block owned
exclusively by the current CPU during dispatch. Slots 14 through 23 hold the
independently read saved frame, slots 24 through 29 hold the six transported
register arguments, slots 30 through 47 hold the context snapshot, and slots
48 through 79 receive policy, machine, and control outcomes. The verified Rust
adapter takes one thin pointer to this named-field block; its accepted compiled
symbol is 1,885 bytes at 0xffffffff80012000.
The exact wrapper obtains the block and active-frame pointers from the registered GS header. It requires a 16-byte-aligned exclusive block with at least 640 writable bytes and the exact field layout. It copies the registered frame and transported registers through distinct paths, never reads an absent same-ring RSP/SS tail, then invokes only the receipt-bound adapter. The adapter validates the 21/23-word logical shape, rechecks frame versus transport, checks the unique-state token, lock/current-thread and backend snapshot, invokes the accepted Thermite policy, and applies its transactional action model. The return value is restricted to return, schedule, or fail-stop.
Return resumes the common exception continuation with the frame/RBX contract
preserved. Fail-stop reaches a registered cli; hlt loop. Until a verified
scheduler entry is available, schedule reaches a registered nonreturning stub
that branches to the same fail-stop loop; therefore this checkpoint does not
claim that a scheduling action actually mutates run queues. Hosted execution
of the real adapter covers user page-fault scheduling, frame/register mismatch,
and invalid-snapshot failure, including the fixed block size and offsets.
The acceptance gate reproduces three proofs, consumers, adapter executions,
and fixed-address links; audits the adapter, compiler runtime, and verified M0
memcpy; and rejects seven proof, byte, size, and address mutations. See
M1 per-CPU scalar-core wrapper.
Current-thread identity and backend readiness are still snapshot facts supplied under the block's unique-token contract, not live scheduler/object lookups. Real fault-token allocation, ready-queue mutation, IRQ/LAPIC and TLB effects, crash recording, whole-entry linkage, and hardware delivery remain subsequent verified transitions.
Every syscall follows:
- copy and normalize untrusted inputs;
- resolve capabilities without mutation;
- validate all preconditions and reserve bounded resources;
- compute the Thermite transition;
- execute proved machine actions;
- commit the abstract state; and
- copy bounded outputs.
No fallible user copy occurs after authority commit unless the result semantics explicitly allow “operation completed, output unavailable.” Where POSIX requires partial progress, that behavior belongs to the user-space server protocol, not an accidental kernel-copy fault.
The action vector has a fixed maximum of 16 actions per transition. Longer work uses explicit continuation objects.
Actions used in a committing transition are proved total on the supported platform when their preconditions hold. A recoverable hardware observation is collected before commit or becomes a new normalized event for a second transition. If hardware violates an action assumption after a concrete mutation, the kernel fail-stops before user re-entry; it does not roll forward an unproved partially committed abstract state.
The core proof includes:
- object-generation safety;
- capability derivation and rights monotonicity;
- queue membership uniqueness;
- reply linearity;
- endpoint transfer atomicity;
- absence of unauthorized frame/device/IRQ access;
- bounded resource use per transition;
- preservation of VSpace and IOMMU correspondence;
- scheduler state well-formedness; and
- failure-state noninterference for authority-bearing fields.