Ailura

Ailura is a capability-based microkernel for 64-bit ARM, targeting the Raspberry Pi 3, 4, and 5. Its long-term userland model is WebAssembly-first: application, service, and driver code runs as validated WASM modules inside small native runtime containers, while the kernel remains limited to address spaces, capabilities, IPC, scheduling, memory, and mediated device/interrupt authority.

The microkernel-boot and microkernel-core slices are implemented. The kernel boots under QEMU raspi3b/raspi4b, discovers its platform from the firmware device tree, allocates frames, builds per-task address spaces, enters EL0 with two native user images, and completes a capability-transfer IPC exchange, a contained fault, and an orderly shutdown. The WASM, async, preemption, device, and driver changes remain proposals. The specifications live in openspec/changes/ and are the source of truth for what comes next. Boot details are in docs/boot.md; the core architecture, memory/object/scheduling/IPC/ABI model, and limitations are in docs/core.md.

Goals

• Build a small, understandable AArch64 microkernel that boots on Raspberry Pi 3, 4, and 5.
• Isolate components through hardware address spaces and unforgeable capabilities.
• Use synchronous IPC for simple calls and optional nonblocking operations for asynchronous userland work.
• Run all application, service, and driver code as validated WASM modules using the pinned wasmi interpreter.
• Run drivers in userland with capability-mediated device mappings and interrupt delivery; the kernel keeps the interrupt controller, timer, and console it needs for its own operation.
• Keep the kernel free of a WASM interpreter, async runtime, and application policy.
• Prefer correctness, deterministic behavior, and a small trusted computing base over performance.
• Bound user-thread CPU time with finite quanta and scheduling classes (interactive, service, background), preempting only at the EL0/EL1 boundary while keeping kernel execution non-preemptible. Explicit yields and finite deadlines remain the preferred fast path.
• Test on QEMU raspi3b and raspi4b, with physical Raspberry Pi 3B as the minimum hardware gate and Pi 5B hardware iteration later.

Non-Goals

• Networking, sockets, or a network stack. Networking is out of scope for now.
• POSIX compatibility, a shell, a filesystem, or a general driver framework in the foundation.
• SMP, CPU hotplug, or per-CPU run queues in the initial implementation.
• Preempting kernel-mode execution, fair-share/CFS scheduling, deadline scheduling, or priority inheritance.
• DMA/IOMMU mediation, device hot-plug, or device power management.
• JIT/AOT compilation of WASM, or writable executable memory.
• WASI, WASM threads, shared memories, SIMD, GC, or the component model.
• Production hardware support beyond the Raspberry Pi reference boards.

Architecture

+-------------------------------------------------------------+
| WASM module: init.wasm, ping.wasm, services, drivers        |
| - async tasks, futures, executor                            |
| - no direct kernel access, no raw MMIO or physical address  |
+-----------------------------+-------------------------------+
                              | capability-based host imports
+-----------------------------v-------------------------------+
| Native runtime container (per module trust domain)          |
| - pins wasmi, validates and executes the module             |
| - maps guest pointers, checks linear memory                 |
| - performs ordered device accesses for the module           |
| - submits kernel operations, drains completions             |
+-----------------------------+-------------------------------+
                              | syscalls (`svc`)
+-----------------------------v-------------------------------+
| Microkernel                                                 |
| - address spaces, memory objects, capabilities              |
| - device and interrupt capabilities (mediated delegation)   |
| - synchronous IPC, async operations, notifications          |
| - bounded-quantum scheduler with classes, timers, watchdog  |
+-------------------------------------------------------------+

The kernel does not parse or execute WASM. Each module trust domain gets its own native runtime container and kernel address space. Tasks inside one module share that module's linear memory and capability space; separate trust domains require separate modules and containers.

Concurrency

EL0 threads run under finite quanta determined by their scheduling class: interactive for input and UI, service for drivers and servers, background for bulk work. Selection is strict class priority with FIFO within a class, plus a bounded service guarantee so background work cannot be starved. When a quantum expires, the kernel preempts the thread only at the EL0/EL1 boundary, saves its complete context, and resumes another thread; the kernel itself is never preempted mid-syscall or mid-trap. Explicit yield and blocking still hand off the CPU immediately, and all blocking operations require finite deadlines.

The EL0 watchdog remains a termination mechanism, not the fairness mechanism: a runaway thread that never yields is killed at its watchdog deadline. The scheduler is planned to gain these quantum and class semantics through preemptive-quantum-scheduling; today's implementation is cooperative.

WASM modules can use an asynchronous executor built on Rust futures. IO is submitted as kernel operations and completed through completion queues, allowing other module tasks to make progress while a request is pending. A module invocation runs under a finite wasmi fuel budget, but fuel is a step budget and a runaway-step tripwire, not a scheduling quantum: compute-bound containers are preempted and resumed by the kernel, not terminated for using CPU.

Specification Roadmap

Work should proceed in this order. Steps 1 and 2 are implemented; everything after them is a proposal.

1. microkernel-boot — implemented

Location: openspec/changes/microkernel-boot/

The first bootable AArch64 system:

• Raspberry Pi firmware boot and device-tree discovery.
• One boot image per board for Pi 3B, Pi 4B, and Pi 5B.
• RAM-variant support through device-tree memory discovery.
• AArch64 exception state, early memory map, GIC, generic timer, and serial output.
• Machine-readable boot report and fatal diagnostics.
• QEMU Pi 3/4 coverage and physical Pi 3B as the minimum hardware gate.
• A parked kernel state; no tasks, user mode, or kernel services yet.

2. microkernel-core — implemented

Location: openspec/changes/microkernel-core/

The core microkernel mechanisms:

• Physical memory, kernel heap, per-task address spaces, W^X, and checked user copies.
• Capability-addressed kernel objects.
• Cooperative scheduling with finite blocking deadlines and a configurable watchdog (default: 1 second).
• Synchronous endpoint IPC and notifications.
• AArch64 svc system-call ABI.
• Embedded fixed-layout native init/ping bring-up clients; no general ELF loader.
• QEMU Pi 3/4 and physical Pi 3B acceptance.

3. memory-map-accounting — proposed hardening

Location: openspec/changes/memory-map-accounting/

Fix a state-corruption bug found in review: MemoryMap currently commits page-table mappings before charging the task's bounded mapping budget, so an over-budget request can leave pages mapped with no accounting. The change reserves the budget before touching page tables, releases it when the architecture map fails, and adds host tests for the failure and boundary cases. Requires no ABI change.

4. page-table-pruning — proposed hardening

Location: openspec/changes/page-table-pruning/

Reclaim intermediate page-table frames during unmap instead of retaining them until task destruction. Without it, a task that churns disjoint regions retains up to roughly 32 MiB of dead tables at the current mapping budget, which can cause premature out-of-memory failures for unrelated work. Includes a QEMU acceptance check for frame-count restoration.

5. wasm-user-runtime

Location: openspec/changes/wasm-user-runtime/

Replace native application logic with WASM. The next major implementation target.

• Pin wasmi 2.0 as the only interpreter.
• Validate modules before execution.
• Run one runtime container per module trust domain.
• Expose only capability-based host imports.
• Enforce fuel, memory, table, call-depth, and deadline limits.
• Port init and ping to init.wasm and ping.wasm.
• Preserve the core acceptance markers.
• Keep networking out of the import ABI.

Depends on the kernel ABI and runtime contracts from microkernel-core.

6. preemptive-quantum-scheduling

Location: openspec/changes/preemptive-quantum-scheduling/

Make the system usable for interactive work alongside CPU-bound background tasks:

• Quantum preemption at the EL0/EL1 boundary only; kernel code stays non-preemptible.
• Interactive/service/background classes with per-class quanta and an anti-starvation guarantee.
• Scheduling class selected through the thread-creation request without changing the ABI layout.
• Watchdog remains a termination tripwire, independent of quantum preemption.
• QEMU latency acceptance under a CPU-bound background thread.

Depends only on the scheduler and trap machinery from microkernel-core; it can be developed in parallel with the WASM work.

7. kernel-device-capabilities

Location: openspec/changes/kernel-device-capabilities/

Prepare the kernel for userland drivers:

• Device and Irq typed objects with capability-gated authority.
• MMIO mappings into EL0 using device memory attributes, excluded from checked user copies.
• Mask-on-delivery interrupt delegation to notifications, with mediated mask/ack and kernel-owned EOI.
• Device-tree enumeration and deliberate bootstrap delegation; the kernel retains the GIC, timer, and console.
• Resource limits raised together for a driver-bearing workload, with a written static-memory budget.
• No DMA, hot-plug, or device power management.

Depends on microkernel-core and can proceed in parallel with the WASM work.

8. async-ipc

Location: openspec/changes/async-ipc/

Add nonblocking kernel operations:

• Operation and CompletionQueue kernel objects.
• Nonblocking IPC send/receive, notification waits, and timers.
• Exactly-once completion delivery and reserved queue capacity.
• Finite deadlines, cancellation, revocation, and peer/task teardown.
• Transactional capability transfer and memory-lifetime rules.
• No kernel futures or async runtime; the kernel remains internally synchronous.

Depends on the object, capability, IPC, timer, and scheduler mechanisms from microkernel-core. It is technically independent of wasm-user-runtime and can be developed in parallel after the core, but the recommended sequence keeps the WASM userland stable before adding the async kernel ABI.

9. wasm-async-executor

Location: openspec/changes/wasm-async-executor/

Make the WASM userland truly asynchronous:

• Add a module-local no_std async executor.
• Use Rust futures, wakers, a ready queue, and a bounded step loop.
• Map future-based host imports onto async-ipc operations.
• Deliver completions through a bounded module inbox.
• Define cancellation on future drop and late-completion handling.
• Treat fuel as a bounded step budget; kernel quantum scheduling provides CPU share and latency.
• Port init.wasm and ping.wasm to async service loops.
• Prove concurrent progress while IO is pending.

Depends on wasm-user-runtime, async-ipc, and the quantum scheduler contract from preemptive-quantum-scheduling.

10. wasm-driver-architecture

Location: openspec/changes/wasm-driver-architecture/

Run drivers as WASM services in userland:

• One driver module per native runtime container with only its device, IRQ, endpoint, and console capabilities.
• Offset-validated, ordered device register imports; no raw MMIO or physical addresses.
• Interrupt waits through the async completion model with mediated acknowledgement.
• Driver lifecycle, idle parking, and orderly shutdown.
• init as the name/registry service; the kernel performs no name resolution.
• Supervisor-owned restart with bounded retries; clients handle peer termination and re-resolve.
• Programmed I/O only: DMA is explicitly excluded from the first slice.
• Hardware acceptance with a real device plus QEMU lifecycle and security coverage.

Depends on kernel-device-capabilities, wasm-user-runtime, and the quantum scheduling guarantees; it is the last step in the current roadmap.

Dependency Graph

microkernel-boot (done)
└── microkernel-core (done)
    ├── memory-map-accounting
    ├── page-table-pruning
    ├── wasm-user-runtime
    ├── preemptive-quantum-scheduling
    └── kernel-device-capabilities

async-ipc                 <- depends on microkernel-core
wasm-async-executor       <- depends on wasm-user-runtime + async-ipc
wasm-driver-architecture  <- depends on wasm-user-runtime,
                             kernel-device-capabilities, and
                             preemptive-quantum-scheduling

Recommended implementation sequence:

microkernel-boot -> microkernel-core
  -> memory-map-accounting -> page-table-pruning
  -> wasm-user-runtime -> async-ipc -> wasm-async-executor
  -> preemptive-quantum-scheduling -> wasm-driver-architecture

kernel-device-capabilities and preemptive-quantum-scheduling are independent of the WASM sequence and may be developed in parallel once the core is stable. wasm-driver-architecture should land after both.

Development Workflow

The project uses OpenSpec. Before implementing a change:

openspec list
openspec show microkernel-boot
openspec status --change microkernel-boot
openspec instructions <artifact> --change microkernel-boot --json

Validate all planning artifacts:

openspec validate --changes --strict

When a change is ready to implement, use the OpenSpec apply workflow. Do not assume a crate, module, syscall, or feature exists because a proposal mentions it.

The planned Rust toolchain is stable Rust 2024 for aarch64-unknown-none, with wasmi modules built for wasm32-unknown-unknown. Host tooling may use std; kernel and runtime code are no_std.

Project conventions, dependency policy, and verification requirements are in AGENTS.md.

Repository Layout

.
├── AGENTS.md              # Engineering and dependency conventions
├── Cargo.toml             # Workspace and lint policy
├── clippy.toml            # Test lint exceptions
├── docs/
│   ├── boot.md            # Boot architecture, images, and hardware procedure
│   └── core.md            # Memory, objects, scheduling, IPC, ABI, userland
├── crates/
│   ├── kernel/            # Portable core library and final no_std binary
│   ├── kernel-abi/        # ABI version, syscalls, handles, errors, markers
│   ├── kernel-aarch64/    # Boot stub, vectors, page tables, user copies
│   └── kernel-raspi/      # Device-tree discovery, UART, GIC, timer, report
├── user-runtime/          # Native EL0 startup, svc wrappers, panic handler
├── userland/
│   ├── init/              # Native root-server conformance image
│   └── ping/              # Native acceptance client image
├── xtask/                 # Build, userland images, QEMU acceptance
├── openspec/
│   ├── config.yaml
│   ├── specs/             # Archived/main capabilities (currently empty)
│   └── changes/           # Active proposed changes
│       ├── microkernel-boot/
│       ├── microkernel-core/
│       ├── memory-map-accounting/
│       ├── page-table-pruning/
│       ├── wasm-user-runtime/
│       ├── preemptive-quantum-scheduling/
│       ├── kernel-device-capabilities/
│       ├── async-ipc/
│       ├── wasm-async-executor/
│       └── wasm-driver-architecture/
├── rustfmt.toml
├── rust-toolchain.toml
└── LICENSE.md             # GPL-3.0-or-later

Quick Start

cargo xtask host-check
cargo xtask images
cargo xtask qemu --board pi3b
cargo xtask qemu --board pi4b
cargo xtask qemu --board pi3b --watchdog-selftest
cargo xtask acceptance

cargo xtask fetch-firmware downloads the pinned Raspberry Pi firmware into target/firmware/ and verifies its SHA-256 hashes. QEMU acceptance supplies the image device tree explicitly because the raspi3b/raspi4b machines do not generate one. For a serial-less hardware check, build the image with cargo xtask image --board pi3b --led-status and use the ACT LED patterns documented in docs/boot.md.

Current Status

microkernel-boot and microkernel-core are implemented and pass the QEMU raspi3b and raspi4b gates, including the boot report, frame/heap self-tests, native user-space exchange, capability transfer, contained guard-page fault, watchdog termination, unsupported-board and panic failure paths. The physical Raspberry Pi 3B hardware gate is the minimum acceptance target and remains to be recorded with the procedure in docs/boot.md. Raspberry Pi 5B hardware bring-up remains a later iteration and does not gate this slice.

Eight further changes are fully specified and awaiting implementation:

Change	Purpose
memory-map-accounting	Fix MemoryMap committing mappings before budget accounting
page-table-pruning	Reclaim empty page-table frames during unmap
wasm-user-runtime	Replace native userland with validated WASM modules
preemptive-quantum-scheduling	Bound interactive latency with quanta and scheduling classes
kernel-device-capabilities	Device/IRQ objects and mediated MMIO for EL0
async-ipc	Kernel operations and completion queues
wasm-async-executor	In-module futures executor and async host ABI
wasm-driver-architecture	Drivers as WASM services with mediated hardware access

The next implementation targets are the two hardening fixes, then wasm-user-runtime; kernel-device-capabilities and preemptive-quantum-scheduling can proceed in parallel once the core is stable. No code exists for any of these proposals yet. openspec/specs/ remains empty until the implemented changes are archived.

License

Ailura is licensed under GPL-3.0-or-later. See LICENSE.md.