Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Build, Boot, and Test

The commands below are the current local workflow for the x86_64 QEMU target. The root Cargo configuration defaults to x86_64-unknown-none, so host tests must use the repo aliases instead of bare cargo test.

Prerequisites

Expected host tools:

  • Rust nightly from rust-toolchain.toml
  • make
  • qemu-system-x86_64
  • xorriso
  • curl, sha256sum, and standard build tools for pinned tool downloads
  • Go, used by the Makefile to install the pinned CUE compiler when needed
  • Optional policy and proof tools for extended checks: cargo-deny, cargo-audit, cargo-fuzz, cargo-miri, and cargo-kani

The Makefile pins and verifies:

  • Limine at the commit recorded in Makefile
  • Cap’n Proto compiler version 1.2.0
  • CUE version 0.16.0

Pinned tools are installed under the clone-shared .capos-tools directory next to the git common directory.

Build the ISO

make

This builds:

  • the kernel with the default bare-metal target;
  • init as a standalone release userspace binary;
  • release-built demo service binaries under demos/;
  • the capos-rt-smoke binary;
  • manifest.bin from system.cue;
  • capos.iso with Limine boot files.

Relevant files: Makefile, limine.conf, system.cue, tools/mkmanifest/.

Boot QEMU

make run

This builds the ISO with the qemu feature, boots QEMU with serial on stdio, and uses the isa-debug-exit device so a clean kernel halt exits QEMU with the expected status.

The default smoke path should print kernel startup diagnostics, manifest service creation, demo output, and final halt. Current default smokes include CapSet bootstrap, capos-rt-smoke, Console paths, ring corruption recovery, reserved opcode handling, NOP, ring fairness, TLS, VirtualMemory, FrameAllocator cleanup, Endpoint cleanup, and cross-process IPC.

Spawn Smoke

make run-spawn

This boots with system-spawn.cue. Only init is boot-launched by the manifest; init uses ProcessSpawner to launch endpoint, IPC, VirtualMemory, and FrameAllocator cleanup demo children, wait for ProcessHandles, and exercise hostile spawn inputs.

This is the current validation path for init-driven process creation. It is not yet the default manifest executor.

Networking and Measurement Targets

make run-net
make qemu-net-harness
make run-measure
  • make run-net attaches a QEMU virtio-net PCI device and exercises current PCI enumeration diagnostics.
  • make qemu-net-harness runs the scripted net smoke path.
  • make run-measure enables the separate measure feature for benchmark-only counters and cycle measurements. Do not treat it as the normal dispatch build.

Formatting and Generated Code

make fmt
make fmt-check
make generated-code-check
  • make fmt formats the kernel workspace plus standalone init, demos, and capos-rt crates.
  • make fmt-check verifies formatting without modifying files.
  • make generated-code-check verifies checked-in Cap’n Proto generated code against the repo-pinned compiler path.

Host Tests

cargo test-config
cargo test-ring-loom
cargo test-lib
cargo test-mkmanifest
make capos-rt-check
  • cargo test-config runs shared config, manifest, ring, and CapSet tests on the host target.
  • cargo test-ring-loom runs the bounded Loom model for SQ/CQ protocol invariants.
  • cargo test-lib runs host tests for pure shared logic such as ELF parsing, capability tables, frame allocation, and related property tests.
  • cargo test-mkmanifest runs host tests for manifest generation.
  • make capos-rt-check builds the standalone runtime smoke binary with the userspace relocation flags used by the boot image.

Extended Verification

make dependency-policy-check
make fuzz-build
make fuzz-smoke
make kani-lib
cargo miri-lib

These require optional tools. Use them when changing dependency policy, manifest parsing, ELF parsing, capability-table/frame logic, or proof-covered shared code. See the Security and Verification Proposal for the rationale behind the extended verification tiers.

Validation Rule

For behavior changes, a clean build is not enough. The relevant QEMU process must exercise the behavior and print observable output that proves the path works. make run is the default end-to-end gate; make run-spawn, make run-net, or make run-measure are additional gates for their specific features.