Micro-Kernel

This project boots freestanding C directly on QEMU's ARM64 virt machine. The emulated computer has no hosted operating system or C library.

The current microkernel milestone implements static thread-control blocks, separate task stacks, cooperative scheduling, an AArch64 context switch, and generation-checked kernel-object identity. Every TCB owns a flat CSpace with a self-TCB bootstrap capability, and protected TCB reads resolve CPtrs relative to the running thread. TCB-owned programs execute at EL0, enter EL1 through svc, and cooperatively switch through complete integer exception-return contexts. The AArch64 MMU now protects kernel memory and gives each user TCB a private stack mapping. Static frame objects can now be mapped and unmapped from EL0 through caller-relative frame capabilities. There is not yet IPC, untyped memory, frame destruction, general-purpose allocation, or timer preemption.

Book

• Chapter 1 — From Reset to the First Interrupt
• Chapter 2 — Machine State: Registers, Memory, and Instructions
• Chapter 3 — How a Function Call Exists
• Chapter 4 — How a Decision Exists

Design

• Capability System Design
• Kernel Source Layout

Build and run

make
make run

qemu_virt is the default compile-time platform. The equivalent explicit commands are make PLATFORM=qemu_virt and make PLATFORM=qemu_virt run. Platform-specific objects are written under build/qemu_virt/.

QEMU prints through its emulated serial port. Press Control-C to stop it.

To inspect the ELF layout and generated ARM64 instructions:

make inspect

Boot path

1. QEMU loads build/qemu_virt/kernel.elf into virtual RAM and jumps to _start.
2. arch/aarch64/boot.S creates a stack and clears the .bss section.
3. _start calls kernel_main in kernel/kernel.c.
4. The QEMU platform binds the console and interrupt-controller ports to PL011 and GICv2 drivers.
5. The kernel builds identity-mapped translation tables and enables the MMU.
6. Bootstrap creates four EL0 TCBs, private stack mappings, CSpaces, two frame objects, and initial capabilities.
7. eret starts the first context; SYS_YIELD alternates runnable EL0 TCBs.
8. A probe's forbidden kernel-data read raises a data abort and halts only it.
9. A frame probe resolves CPtrs in its own CSpace, maps a frame at 0x50000000, writes through the alias, yields, and verifies the value is preserved.
10. Failed rights, address, collision, and wrong-frame-unmap checks leave the live mapping unchanged; a load after successful unmap raises a data abort.
11. SYS_EXIT halts the remaining callers and returns control to EL1.
12. A separate EL1 demo validates typed references and distinct CNode roots.
13. Bootstrap installs self-TCB caps and one read-only cross-CSpace TCB cap.
14. Two EL1 tasks exercise caller-relative lookup while cooperatively switching.
15. The boot context resumes after both tasks halt.
16. The kernel configures the GICv2 interrupt controller and ARM generic timer.
17. The CPU waits with wfi, handles one timer interrupt per second, and resumes.

Components

arch/aarch64/
boot.S reset entry, stack, .bss, VBAR_EL1
vectors.S exception table and complete integer trap frame
context_switch.S cooperative x19-x30 and sp context switch
el0.S load first TCB user context and restore EL1 afterward
exception.c AArch64 syndrome decoding and exception return policy
mmu.c 4 KiB translation tables, permissions, and TTBR0 switch
cpu.c CurrentEL, IRQ mask, and WFI
drivers/
pl011_uart.c PL011 implementation of the console port
gicv2.c GICv2 implementation of the interrupt port
arm_generic_timer.c one-second architectural timer
kernel/
kernel.c top-level initialization and main wait loop
demo/
el0_demo.c construction and validation of EL0 boot probes
el0_demo.h demo-private composition interface
interrupt/interrupt.c IRQ initialization, dispatch, and completion
exception/unexpected.c fatal unexpected-exception diagnostics
memory/
address_space.c generation-checked address-space handles
frame_object.c frame identity, allocation, and zeroing
frame_invoke.c capability-authorized current-TCB map/unmap
syscall/syscall.c architecture-neutral syscall dispatch
thread/
tcb.c TCB storage, lifecycle, and object queries
tcb_capability.c TCB bootstrap and protected capability operations
context.c saved-context initialization and copying
scheduler.c runnable selection, traps, faults, and switching
tcb_internal.h thread-subsystem-private representation
object/object.c object lifetime and generation validation
capability/capability.c caller-relative lookup and rights validation
capability/cnode.c static CNodes and CSpace-root validation
include/
kernel/ kernel/architecture cross-subsystem contracts
microkernel/ architecture-independent object interfaces
ports/ hardware-facing interfaces used by the kernel
drivers/ configuration interfaces used by platforms
platform.h board operations visible to the kernel
*.h architecture and kernel subsystem interfaces
platform/qemu_virt/
platform.c QEMU addresses, interrupt wiring, driver binding
physical_memory.c linker-backed physical-frame pool adapter
platform.mk selected drivers and QEMU command-line settings
linker.ld QEMU virt RAM layout and kernel load address
user/
demo.c yielding, isolation, and frame-map EL0 probes
aarch64/syscall.S x8/x0-x2 plus svc #0 userspace ABI
aarch64/probe.S labeled deliberate post-unmap fault instruction

Each .c and .S file compiles independently into an object file. The linker still combines all objects into one freestanding build/qemu_virt/kernel.elf; source modules do not become processes or dynamically loaded libraries.

Hardware adapter boundary

The kernel depends on small hardware ports, not on a board model:

kernel code ──uses──> ports (console, IRQ controller, timer, translation)
^
| implements
drivers + architecture adapters
^
| selected/configured by
platform + build

platform/qemu_virt/platform.c is the only C file that knows the QEMU device addresses and timer interrupt wiring. It passes those values into the PL011 and GICv2 drivers during platform_initialize(). The drivers know their device protocols but not which board supplied the addresses. The kernel knows the operations it needs but not which concrete devices implement them.

Address translation follows the same boundary in the architecture direction: kernel/memory/address_space.c manages generic handles while arch/aarch64/mmu.c implements the translation-table format and system-register operations behind ports/address_translation.h. Frame storage follows a second adapter: kernel/memory/frame_object.c uses ports/physical_memory.h, implemented for QEMU by linker-reserved pages in platform/qemu_virt/physical_memory.c.

Binding happens at build time through platform/qemu_virt/platform.mk. There is deliberately no runtime function-pointer table yet: one kernel image targets one platform, so direct calls are smaller and easier to trace in disassembly.

All three drivers remain linked into the EL1 image for now. The interrupt controller and scheduler timer are kernel mechanisms. PL011 can later become an EL0 UART service, but only after IPC, capabilities for device frames, and user-level interrupt delivery exist. The port boundary lets that move happen without teaching the rest of the kernel about PL011 registers.

To add another AArch64 board, create platform/<board>/platform.c, platform.mk, and linker.ld; select or add drivers that implement the same ports; then build with make PLATFORM=<board>. A same-architecture board port should not require changes to kernel/thread/ or kernel/interrupt/.

Cooperative task experiment

Each task has a 16 KiB static stack and a TCB containing its execution state. At the thread_yield() ABI boundary, context_switch.S saves the outgoing task's x19 through x30 registers and sp, then restores those values for the next runnable task. Caller-saved registers do not belong in this minimal context because the switch occurs through an ordinary function call. The build uses -mgeneral-regs-only; enabling FP/SIMD would expand the context contract.

The kernel creates two finite tasks. Their output alternates while independent local counters survive every switch. After both entry functions return, their TCBs become HALTED and the scheduler restores the original boot context.

This scheduler remains deliberately cooperative and its TCB tasks still run at EL1. Exception entry now preserves the full integer register set plus ELR_EL1 and SPSR_EL1. The EL0 scheduler below attaches that state and SP_EL0 to user TCBs, while timer-driven preemption remains future work.

EL0 TCB and syscall scheduler experiment

Each user TCB owns x0–x30, SP_EL0, ELR_EL1, and SPSR_EL1, plus a separate 16 KiB user stack and CSpace root. cpu_run_user_context() preserves the kernel's EL1 callee-saved registers, loads the first complete user context, and executes eret into AArch64 EL0t.

The user demo cannot call the console port directly in its source. Its assembly wrappers place a syscall number in x8, up to three arguments in x0-x2, and execute svc #0. The lower-EL synchronous vector builds a 272-byte exception frame containing x0–x30, ELR_EL1, and SPSR_EL1; AArch64-specific code validates the syndrome, and architecture-neutral dispatch writes the byte. Restoring the frame and executing eret resumes the instruction after svc at EL0.

For SYS_YIELD, the exception adapter copies that frame plus SP_EL0 into the outgoing TCB. The scheduler derives the caller from current_tcb, chooses the next runnable user TCB, and copies its saved state into the exception frame. The vector's ordinary restore plus eret therefore resumes a different owner of the CPU. The alternating local values demonstrate that both contexts survive.

SYS_EXIT records the caller's exit value and marks that TCB halted. When no user TCB remains runnable, exception return deliberately targets the suspended EL1 scheduler frame. This is TCB-owned EL0 scheduling across separate translation-table roots. The debug-output syscall remains temporary and is not capability-authorized.

Address spaces and MMU experiment

The bootstrap address-space model deliberately keeps its code, data, and stack virtual addresses equal to physical addresses so page permissions are visible without also relocating the image. Dynamic frame mappings are the first intentional aliases. AArch64 uses 4 KiB pages and a 32-bit lower virtual-address range. The low device region is EL1-only Device memory, RAM is Normal cacheable memory, kernel text is privileged read/execute, and kernel data is privileged read/write and execute-never.

The linker gives .user.text and .user.rodata their own page-aligned ranges. Every user address space maps those shared pages read-only, but maps only its own 16 KiB stack as EL0 read/write. Other user stacks, the TCB pool, CNodes, and the rest of kernel data remain EL1-only. The scheduler activates the incoming TCB's root through TTBR0_EL1 before exception return.

A third EL0 TCB deliberately loads from __kernel_data_start. Hardware raises a lower-EL data abort instead of completing the load. The exception adapter records the syndrome, fault address, and instruction address in that TCB, marks only it halted, and schedules the next user context. Successful alpha and beta output after the probe proves that the kernel contained the fault.

The new frame window occupies 0x50000000-0x501fffff in every user address space. Its L3 entries start invalid. SYS_FRAME_MAP resolves a frame CPtr in the current TCB, requires CONTROL | READ and additionally WRITE for a writable mapping, obtains the physical page inside EL1, and installs a non-global, execute-never user descriptor. SYS_FRAME_UNMAP requires CONTROL and clears only a descriptor whose physical address matches the selected frame. A failed request changes no PTE.

This remains a small static memory model rather than general virtual-memory management. Page-table roots, stacks, frame metadata, and four backing pages come from fixed pools; user code is shared; frames live for the boot because safe destruction needs reverse-map tracking; and TLB invalidation is intentionally broad.

Kernel objects and flat CSpaces

Each allocated TCB now has an object header containing its type, allocation state, and generation. Trusted kernel bootstrap code receives an object_ref_t containing the TCB type, static-pool index, and matching generation. State lookup rejects references with the wrong type, a stale generation, or an out-of-range index before touching the TCB.

An object reference is identity, not authority. It is not given directly to task code and it does not carry rights. A capability combines that internal identity with rights inside a kernel-owned CNode slot.

Each created TCB also receives a kernel-held root capability to a distinct, generation-checked CNode. The first CNode shape is deliberately flat: it has 16 slots addressed directly by cptr_t. CPtr zero stays empty, while CPtr 1 holds the thread's READ | CONTROL self-TCB cap. In the demo, alpha also has a read-only beta TCB cap at CPtr 2; beta's CPtr 2 remains empty.

cap_lookup_current() starts from the running TCB, validates its CSpace root, resolves the CPtr, checks the target's type and generation, and then checks the requested rights. The demo proves self reads succeed, beta's empty slot fails, and alpha cannot request CONTROL through its read-only beta cap.

The CNode and TCB pools are in EL1-only pages, so EL0 cannot directly read or overwrite capability state. Frame map/unmap are the first EL0 operations that accept a CPtr and enforce that authority end to end. The debug-output syscall remains temporary ambient debug authority; it is not a frame capability and must eventually move to a user-level service through IPC.

Memory experiment

The kernel prints one representative from each writable storage area:

• boot_count starts at 42 and lives in .data.
• zero_initialized_value starts at 0 and lives in .bss.
• local_value starts at 7 and lives in a function's stack frame.

The addresses make two behaviors visible: linked sections grow upward through RAM, while the stack begins near __stack_top and grows downward. Run make inspect to compare the printed addresses with the ELF sections and ARM64 instructions.

Timer interrupt experiment

The timer experiment begins after both EL0 TCBs have exited and the kernel is again idling at EL1. Its interrupt path is:

1. arch/aarch64/boot.S installs the vector table into VBAR_EL1.
2. kernel/interrupt/interrupt.c asks the selected interrupt-controller port to enable the platform's physical timer interrupt.
3. The kernel loads one second into CNTP_TVAL_EL0 and enables the timer.
4. Clearing the IRQ mask in DAIF allows the CPU to receive IRQs.
5. wfi waits without repeatedly polling a device register.
6. At zero, hardware transfers control to arch/aarch64/vectors.S.
7. irq_entry saves all general registers and calls irq_handler in C.
8. The C handler acknowledges PPI 30, reloads the timer, and signals completion.
9. Assembly restores the registers and eret resumes the interrupted loop.

The QEMU adapter owns this fixed hardware map:

0x08000000 GICv2 distributor
0x08010000 GICv2 CPU interface
0x09000000 PL011 UART
PPI 30 non-secure physical timer interrupt

The QEMU runner explicitly disables EL2 virtualization and selects GICv2 so the teaching platform remains deterministic and the kernel starts at EL1.

Why a little assembly is necessary

C assumes that a stack and initialized memory already exist. A userspace C runtime normally prepares those before calling main. Bare metal has no such runtime, so arch/aarch64/boot.S performs the minimum setup and then enters C.