Milestone 6.5 Complete: Linux Internal Contract Validation

M6.5 is a validation milestone. Instead of adding new features, we systematically verified that Kevlar implements the undocumented behavioral guarantees that real Linux software depends on — the contracts between kernel and userspace that aren't in any man page but that glibc, systemd, and GPU drivers all assume.

The core idea: compile a C test, run it on Linux and Kevlar, compare output. If they disagree, the kernel has a bug.


What we built

19 contract tests across five categories, validated on both Linux (host) and Kevlar (QEMU). Each test exercises a specific kernel contract and prints CONTRACT_PASS or CONTRACT_FAIL with a diagnostic.

tools/compare-contracts.py — test harness that compiles tests with gcc (host) and musl-gcc (Kevlar), runs both, compares output, and reports PASS/DIVERGE/FAIL with timing.

tools/diff-syscall-traces.py — when a test fails, this tool runs it under strace (Linux) and debug=syscall (Kevlar), aligns the two syscall sequences, and pinpoints the first divergence. Short-circuits the "read kernel source for an hour" debugging cycle.

Runtime debug=syscall — kernel cmdline parameter that enables full JSONL syscall tracing without recompilation. Previously required KEVLAR_DEBUG=syscall at build time.

Results: 18/19 PASS

CategoryTestsPassNotes
VM88/8brk, mmap, mprotect, fork CoW, demand paging, file mmap, TLB flush
Scheduling44/4getpriority, nice values, sched_yield, fork scheduling
Signals43/4delivery order, handler context, mask semantics
Subsystems22/2/dev/null+zero, /proc/self/stat+exe
Programs11/1fork/exec/wait lifecycle
Total1918/19

The single failure (sa_restart) requires alarm()/setitimer() to deliver SIGALRM during a blocking syscall — tracked for M7.

Kernel bugs found and fixed

1. brk() returned negative errno — Linux's brk() never returns an error. On failure it returns the unchanged program break; the caller detects failure by comparing. Our implementation used ? to propagate -ENOMEM, which confused musl's sbrk.

2. musl 1.2.x deprecated sbrk() — The musl binary's sbrk(N) was a stub that always returned -ENOMEM without making a syscall. The contract test was rewritten to use syscall(SYS_brk, addr) directly.

3. mprotect(PROT_NONE) killed instead of delivering SIGSEGV — The page fault handler called Process::exit_by_signal(SIGSEGV), killing the process immediately. The correct behavior is current.send_signal(SIGSEGV) and return — the interrupt return path redirects RIP to the user's signal handler trampoline.

4. sched_getaffinity returned 0 — Should return the number of bytes written to the mask buffer. musl uses this to determine how many bits to scan; returning 0 made CPU_COUNT() always report 0 CPUs.

5. Missing /dev/zero — Added kernel/fs/devfs/zero.rs, a character device that returns infinite zeros on read.

6. Missing getpriority/setpriority — Added syscall implementations with per-process nice value tracking.

7. Dockerfile COPY bugADD testing/etc/passwd /etc silently failed in FROM scratch images. Switched to COPY with explicit full destination paths.

Phase breakdown

  • Phase 1: Test harness infrastructure
  • Phase 1.5: Syscall trace diffing + runtime debug cmdline + brk/mprotect/getpriority fixes
  • Phase 2: VM contract tests (demand paging, file mmap, TLB shootdown)
  • Phase 3: Scheduling contracts + sched_getaffinity fix
  • Phase 4: Signal contracts (delivery order, handler context)
  • Phase 5: Subsystem contracts + /dev/zero
  • Phase 6: Program compatibility (fork/exec lifecycle)

What M6.5 enables

Every contract test is a regression gate. When M7 adds /proc files or M8 adds namespaces, make test-contracts catches any breakage in existing behavior. The trace diff tool makes diagnosis fast: instead of printf-debugging, make trace-contract TEST=brk_basic shows exactly which syscall returned the wrong value.

The known gaps (MAP_SHARED+fork, CFS weights, alarm delivery) are documented and tracked. M7-M10 authors won't discover them the hard way.