The test bench
The bench is how every claim in this book is tested. It builds the real kernel, loader and
programs, packs and signs a boot bundle, boots it under QEMU, and judges what appears on the
console, over SSH and on the network, from outside the guest. It also runs host tests and source
checks. It is part of the system under tenet 6 (the tenets),
held to the same standard of simplicity as the kernel: one tool, tools/testbench, and one file per
case in tests/.
How to use it
cargo testbench # every case but those run only by name
cargo testbench timer # cases whose name contains "timer"
cargo testbench --arch rv64 # one target
cargo testbench --list # names and descriptions, those run only by name marked
cargo testbench sched-latency --sweep 1..20 --jobs 4 # one case, a seed sweep, 4 boots at a time
cargo testbench --exact sched-latency # that case alone, not sched-latency-tcg too
cargo testbench --prebuild target/prebuilt # build every case's pieces once, both widths
target/prebuilt/testbench --prebuilt target/prebuilt --exact --arch rv64 timer # run from them
./test # the same, from the repository root
The exit status is non-zero if anything fails. Each run keeps its boots’ console logs, SSH
transcripts, disk images and captures in a directory of its own,
target/testbench/run-<pid>-<time>/, and target/testbench/last names the latest. Only the
newest few run directories are kept, so --keep-failed DIR copies a failing boot’s console log,
its second boot’s and its sessions’ into DIR as <arch>-<case>.smp<N>…, where they outlive
the run (host:testbench::a_failing_boots_logs_are_kept_under_its_jobs_name). Runs may
overlap in one worktree: each packs the kernel cargo reports for its own features, never the
shared target/ path another run may have rebuilt. A case the host cannot run (no RustSBI
firmware, no OpenSSH) fails and says what is missing; --allow-skip reports it as skipped
instead. Every run boots the vendored RustSBI prototyper: scripts/build-bios.sh builds it for
both widths, or RUSTSBI_PROTOTYPER and RUSTSBI_PROTOTYPER_RV32 name the images. There is no
fallback to QEMU’s own firmware.
| Path | What |
|---|---|
tools/testbench/ | the bench: builds, injects programs, boots QEMU, judges the console, sessions and network |
tests/*.toml | the cases, one per file (tests/data/: files they read; tests/keys/: SSH test keys) |
tests/programs/ | no_std programs that run inside Redoubt: the log server, victims, attackers, checkers |
tests/net/ | the network clients and the judge that the net cases start under init, and the host test that checks each net case’s manifest against its case file |
A filter takes every case whose name contains it, so cargo testbench timeouts runs
timeouts-tcg too; --exact takes the one case it names, run only by name or not, and refuses a
name no case has. A run stages each userland disk it boots in a directory named for the recipe’s
whole path, as two recipes may share a file name.
Building once
Status: built · tested: host:testbench::an_index_survives_its_rename_and_names_its_tree, host:testbench::the_fingerprint_follows_the_trees_changes, host:testbench::an_exact_filter_runs_one_case, host:testbench::userland_recipes_of_one_name_stage_apart, host:testbench::a_build_asked_for_again_in_a_run_is_not_run_again
A run builds what it boots: cargo run of the bench, then a cargo build of the kernel, the loader
and each program, a check that costs about 30 ms when nothing changed and waits on the build
directory’s lock while another run compiles, then the bundle and any userland disk. Alone that is
a quarter of a second before QEMU starts; beside a train of other runs, each waiting on the
others’ compiles, it was most of a case’s time. A run makes each distinct build once, and a case
asking for one already made takes its binary without running cargo, since a run takes the tree
as it was when it began: the kernel and the loader are built once per profile and target, not
once per case. --prebuild DIR does it once for every case:
DIR/testbench the bench, copied from the --prebuild that made the directory
DIR/redoubt-sshd-host Redoubt's sshd on its host platform, for the loopback cases against it
DIR/<arch>/index.json the tree's fingerprint; each case's pieces, or its build's results
DIR/<arch>/... cargo's copies, the bundles, the userland disks
Every boot and build case is built for each of its targets (--arch for one; a filter for
some), the widths one after the other in one process: two userland stages at once would compile
the same Mix project in its one build directory. A build that fails is kept as the case’s
result, printed by the prebuild and again by each run of the case, as is a build case’s
verdict. Each width is built in a directory of its own and renamed into place when done, so a
run reading the old pieces never sees a half-written one.
DIR/testbench --prebuilt DIR then runs cases as cargo testbench does, but takes each boot
case’s bundle, loader and userland disk from DIR and runs no cargo and packs nothing; what
stays per boot is what each boot must have afresh: the QEMU probe, its disk (a disk recipe is
still packed for every boot) and its devices. A case starts in about the time QEMU takes to
start. The index names the workspace that made it and the tree’s fingerprint: its commit, its
uncommitted changes and its untracked files that git does not ignore, taken when the prebuild
starts and again before each width is put in place, which a change in between refuses. A run
from a directory another workspace made is refused naming it, and so is one from this tree
before a change, never a silent test of old code, so the directory is made again after any
change. What git ignores is not in the fingerprint: the pinned toolchains (toolchains/, or
where BEAMLET_TOOLCHAINS points) and a Mix project’s _build (userland/shell/_build/); a
change to those needs a prebuild by hand. The other kinds run as
always, with their own cargo where they have one (host-tests). scripts/jobs.mk makes the
directory (prebuilt) and runs every case target from it when it is there (“On a shared host”
under the case file).
Verdicts
What a case passes on
Status: built · tested (9)
- bench:bench-console-after-expect
- bench:bench-poweroff-missing
- bench:bench-qemu-early-exit
- bench:rustsbi-boot
- host:testbench::a_killed_bench_leaves_no_qemu
- host:testbench::a_line_is_shown_without_its_control_sequences
- host:testbench::a_qemu_lacking_an_option_is_named
- host:testbench::a_shown_line_keeps_its_own_prefix_first
- host:testbench::forbid_matches_the_line_as_it_came_or_as_shown
A boot case passes when every expect pattern matches a console line, in order, no forbid
pattern ever matches, and the boot ends as the case says. Four patterns are always forbidden:
PANIC, TEST FAILED, WARNING: INSECURE, and ipd: an invariant broke, the line ipd says
if a socket’s buffers ever fail to fit its heap, reachable only at a residual of its sizing that no
case reaches (ipd). After the last expect, and any sessions, the bench
keeps reading for 50 ms (1 s in a checked build), so a forbidden line right after the last expected
one still fails the case. With poweroff = true it reads instead until QEMU exits, and requires the
exit status the case names (0 by default; 255 for an SBI system failure). A boot that ends, or
times out, while an expect is still waited for fails with the first failure a program printed
([name] FAIL) ahead of the line it waited for, since that is the cause. The bench starts QEMU
with Linux’s parent-death signal asked for between fork and exec, so a bench killed at its
timeout, even outright, takes its QEMU with it and leaves no guest running to skew the next run.
A console line is matched as a terminal shows its text: with its control sequences removed. A CSI
sequence goes whole, any other escape with the character after it, and every other ASCII control
character but tab, DEL among them, and trailing space after them. Nothing is drawn, so a carriage
return does not take the line back to its start, and the prefix the log server or consoled gave
the line stays first: no program’s text can be shown in front of it. expect, expect_after,
[[input]] and the poke’s after, and distinct_across_boots match the shown line. forbid, the
four always forbidden, and the checks on the reporter’s PASSED and DONE lines see both the
line as it came and as it is shown, so a forbidden word split by a sequence is caught, and so is a
raw sequence a case forbids ('\x1b'). The console log keeps every line as it came, and distinct
and a post_check read that log.
Before a width’s first boot the bench runs that width’s QEMU with -version, and a QEMU that
cannot run fails every boot case at once with its complaint (skips them, with --allow-skip, as a
missing firmware does). A guest that ends before it prints a line, or whose QEMU exits with a
failing status, fails with QEMU’s exit status and the last lines of its stderr,
which go to the console log too; one that printed and then died fails as it did, with QEMU’s exit
status.
In-guest programs print through the log server and finish with <NAME> TEST PASSED or
<NAME> TEST FAILED; attack programs end with attempts done instead. The log server starts every
line it prints for a client with the sender’s badge, as the kernel reports it, on every path that
takes client text: [pid N] for a badge below 0x100, and [badge N] for any other. The
tester numbers a case’s programs by their place, 2 on (it is 2), at most 16, and gives each its
place as its badge, and every badge a test program mints is 0x100 or more, so a minted badge can
never print as a place and forge a case program’s line (tests/programs/src/logsrv.rs). Lines
without a prefix come from the kernel, the loader, the log server’s own fixed templates, or a
program that owns the UART.
Rule F (trusted verdicts)
Status: built · tested: bench:bench-attack-forgery, bench:bench-reporter-mismatch, bench:logsrv-badge-forgery, bench:bench-init-reporter-forged, bench:init-console-forgery
A verdict comes only from a party the attacker cannot impersonate. The console does not say who
wrote a line, and an attacker can print anything, including another program’s PASSED, so an
attack case passes only on a line the attacker cannot write:
- The kernel or the loader, refusing: a line with no
[pidprefix, withKMAINor a later stage forbidden so that no program ever ran (loader-rejects-*), or an anchored line the kernel prints at boot before any program starts, which a relayed line cannot match (kernel-wx). - A victim that owns what is attacked and still has it afterwards: the log server still hears
UART input after every attempt (
irq-attack); a victim inspects its pages (mem-attack,uaf-lent-page). - The log server’s
DONE. The program ininit’s place owns the console: it holds the console’s device handles, and every other program’s text reaches the UART only through it, prefixed with the sender’s[pid N]or[badge N]. A victim, or with no victim the attacker once it is done, calls the checker’sdone(); the log server prints one[server] done:line naming the caller by the badge the kernel delivers with the call, which the tester chose, and powers off. A case that names areporterpasses only if exactly one line starts[server] done:and it names the reporter’s place; any other such line fails it, as does one in a case with noreporter. consoled‘s prefix, underinit. In a servers’ case the realinitholds the UART untilconsoledstarts, andconsoledstarts every line written through a child’s connection with that connection’s[con N], so onlyinit’s lines are bare. The bench learns the reporter’s N frominit’s bare announcement and takes aTEST PASSEDonly under it (the servers’ cases underinit).- A sole first program judging the kernel. In
map-fixed-attack,write-only-attackandprocess-attackone program runs, alone: it holds the console and the reset, makes every refused call itself, and prints its own unprefixedok:lines. It is trusted because nothing else runs that could impersonate it, and because what it attacks is the kernel, not another party in the case: eachok:line reports a kernel result it read back (the error, the budget’s usage, the mapping left in place), and the case also needs a clean power-off, which a fault in the program prevents. The residual: a kernel bug that corrupted this program’s own memory could make it misreport, and no second party would see it.
Program order. A program that attacks another program, or the fixture, is never the first. In a case with several programs, the
first is the trusted tester (the log server, unless the case is one of the sole-program cases
above), and the case’s programs list fixes the order of the rest, so which place and which
handles each program gets is the case’s choice, never a race.
Every verdict pattern is anchored with ^ and pinned to its writer, with a comment beside it saying
why it cannot be forged. The attacker’s own lines may be required as progress (so a refusal for the
wrong reason fails) and forbidden as evidence of a breach, but are never the verdict. Where the
attacker itself reports to the checker, the case shows only that the system survived, and its
description says so (“verdict: survival only”).
Cases
The case file
Status: built · partly tested: that an unknown field or table is refused is read from the code, not attacked by a case · tested: bench:bench-console-after-expect, bench:bench-poweroff-missing, host:testbench::a_case_out_of_the_whole_run_runs_only_by_name, host:testbench::host_tests_route_only_to_a_requested_workspace_and_forward_features, host:testbench::an_oracles_tools_must_be_on_the_path, host:testbench::sweep_seeds_are_ranges_or_lists, host:testbench::a_sweep_is_refused_before_anything_builds, host:testbench::sweep_boots_have_their_own_files, host:testbench::the_join_prints_in_seed_order_and_counts_failures, host:testbench::a_sweeps_boots_hold_disjoint_slices_of_the_lease, host:testbench::two_boots_at_once_run_in_different_slots, host:testbench::smp_is_one_list_or_a_list_per_width, host:testbench::a_boot_runs_its_widths_own_hart_counts, host:testbench::a_fanout_is_of_values_files_or_tests, host:testbench::a_job_passes_fails_or_runs_past_its_deadline, host:testbench::a_cpu_list_counts_its_ranges, host:testbench::a_failing_boots_logs_are_kept_under_its_jobs_name, bench:rt-miri, bench:model-mutations
A case is one TOML file. Paths in it are relative to the workspace root, and an unknown field or
table is an error, so a misspelling cannot silently drop a check. The one exception is a programs
entry (and a bundle file’s from): its forms are told apart by their keys, so an extra key in one
is ignored rather than refused (tools/testbench/src/case.rs).
description = "What this proves"
arch = ["rv64", "rv32"] # targets to run on
whole_run = true # false: run only when the filter is the case's name
kind = "boot"
programs = [ # the first in init's place, the rest started by it
"log-server", # a binary of the test programs
{ package = "my-crate", bin = "my-server" }, # any workspace binary, built for the target
{ package = "my-crate", bin = "my-probe", features = ["probe"] }, # built with these features, in a target directory of its own
{ package = "beamlet-redoubt", bin = "beamlet", workspace = "userland/otp" }, # a binary of a workspace of its own, built there
{ path = "prebuilt/thing.elf" }, # or a prebuilt ELF
{ erlang = "path/to/module.erl" }, # an Erlang module, compiled by the pinned erlc (a bundle file's)
{ otp = "io" }, # an OTP module's .beam from the pinned toolchain (a bundle file's)
{ zeros = 6291456 }, # that many zero bytes, an entry only its length matters for (a bundle file's)
]
smp = [1, 4] # one boot per hart count (default [1]), or per width (below)
keep_smp = true # the counts stand under `--smp N` (a comment says why)
timeout_secs_smp = 90 # the bound under `--smp N` instead (a comment says why)
memory_mib = 32 # guest RAM (default 256)
memory = false # true: stop an init guest and measure its servers' painted stacks
timeout_secs = 60 # default 60; fractions allowed
icount = "shift=3,sleep=off" # virtual time: 2^3 ns per guest instruction, the RTC on it too
qemu_seed = 1 # pin the guest's randomness (QEMU -seed)
kernel_features = [] # extra kernel features
debug_assertions = false # true: a checked build of the kernel and the loader
expect = ['regex 1', 'regex 2'] # each must match a console line, in this order
forbid = ['regex'] # must never match
poweroff = false # true: the guest must power off after the last expect
reporter = "checker" # the program whose done() is the verdict (rule F)
launch = false # true: boot `./launch --system`'s own QEMU command line (launch-*)
post_check = "sched_oracle" # a host-side check of the console after a passing boot
[[input]] # typed on the console once a line matches `after`
after = "claimed irq 10"
send = "xyz"
A boot case also takes allow_panic, tamper_bundle, sign_bare_archive, short_initrd,
device_tree, distinct_across_boots and distinct (hostile inputs), [[file]]
(bundle files), [disk] and [net] (devices),
[[session]] (SSH sessions), must_fail (self-checks), and
poweroff_status: the QEMU exit status a poweroff case requires (0 by default; 255 for an SBI
system failure, which a rejection case asks for).
smp is one list for every width the case runs on, or a list per width:
smp = { rv64 = [1, 2], rv32 = [1] } boots rv64 at one and two harts and rv32 at one, for a case
whose count on one width is a finding of its own, so that the other width’s run does not go into
a copy of the case. A width the map leaves out runs the default, [1]; a key that is not one of
the case’s arch, and an empty list in either form, are refused before anything builds (a case
leaves a width out of arch, never boots it zero times). jobs.mk leases the width’s own
largest count, and --smp N replaces a map as it does a list.
With icount, QEMU runs the guest at a fixed instruction rate, skips idle time to the next timer
deadline and puts the RTC on the same clock (-rtc clock=vm). A time a case asserts is then a
count of guest instructions (at shift=3, 1 ms is 125,000), the same on any host however loaded.
It does not make a run repeat on its own: QEMU fills the guest’s boot RNG seed from host entropy on
every boot, the kernel draws PIDs from it, and that moves every later event. qemu_seed = N pins
it (QEMU -seed N, which fills the device tree’s /chosen/rng-seed), and with icount a run then
repeats exactly. The bench prints the seed before the result, and TESTBENCH_QEMU_SEED=M replaces
the pinned seed of every case that has one, to replay a run or to sweep. An idle guest’s clock
skips to its next armed timer deadline, sleep on or off: with sleep=off at once, so while
blkd waits for the host’s virtio completion the next deadline is its own 10 s request timeout,
the read fails and the volume is poisoned, which is why a case with a disk keeps sleep on
(icount = "shift=3"); with sleep on the skip was measured too, once the guest idled with no
timer armed nearer than a lease’s deadline 1,337 s ahead, which it reached inside a 295 s boot,
the lease destroyed at it as its rule says. So a case under the virtual clock whose guest can
idle while a lease it means to outlive the case is live either runs on the host’s clock or
expects the lease’s end; with sleep on such a run repeats closely, not exactly, and a time a
case is held to comes with a sweep’s spread.
--sweep SEEDS runs one case once per seed (1..20, or 3,5,9), from one build, and prints each
seed’s result in seed order and a summary line; each boot keeps its files in seed-<N>-<arch>/
inside the run’s directory. --jobs J boots up to J seeds at once. Under scripts/q the sweep
cuts the job’s port lease (q run --ports N, REDOUBT_PORTS=lo-hi) into J disjoint slices from
its start, one per concurrent boot, and each boot forwards on its slice alone, so no two meet on
a port; a lease shorter than J times the case’s forwards (its forward ports and its poke) is
refused before anything builds, naming the --ports to ask for, and no boot is ever handed a
slice another holds. One boot at a time takes the range’s start, as a single run does; outside
q each boot asks the OS for its ports, with that path’s race. --jobs is never the default; what a
result under it is worth is the shared-host rule below. A timing gate runs one pinned seed and
states its target from a sweep of seeds (responsiveness).
Which cases run in guest time. A boot case runs under icount = "shift=3,sleep=off" unless
something in it waits on the host, and 145 of the 226 do. What keeps a case on the host’s clock:
a disk or a userland disk (38 cases; the rule for a disk is above); host sockets, a forward, a
poke, a peer or a dial (8); input the host types on the console, [[input]] (4; under icount
the rv32 UART lost a burst of it); and a run whose purpose is the host’s
time (asid-cost-host, sched-latency-tcg, timeouts-tcg, and smp-evict-mttcg,
smp-shootdown-mttcg, console-one-writer, sched-lock-contention-4-mttcg and
beamlet-schedulers-mttcg, which need QEMU’s multi-threaded TCG; its one-hart twin
beamlet-schedulers-one-hart runs in guest time, since on one hart what it measures is the
instructions two schedulers’ switching costs). Several harts do not keep a case
on the host’s clock: under icount QEMU runs the harts in turn on one host thread, and a hart
waiting for the kernel lock halts rather than spending its turn
(R78 (fair kernel entry)). One case reads no host clock and stays on it for now: redoubt-ipc
fails under icount on both widths (189 calls abandoned of the 256 it wants), until that is
understood. A timeout_secs is the bench’s bound, never a measurement: a case in guest time
is given at least four times its slowest pass alone on either width, rounded up to 10 s, and
more than any wait of its own program, so that a stuck check reports itself; it is never raised
without a measurement. bench-poweroff-missing keeps its 3 s: there the deadline is the oracle,
the timeout its must_fail waits for.
On a shared host. cargo testbench runs its cases one after another; what may run beside
the invocation, another invocation in its own run directory, a seed under --jobs, a build, is
decided by the clock each case measures with. A boot case with icount measures in guest time:
the host’s load does not move a guest time, so its pass, and a failure the guest itself
reports, are verdicts whatever ran beside it (a pinned seed adds only that the run repeats
exactly). Its one exposure to the host’s clock is timeout_secs, the bench’s deadline for the
boot: a case that only ran out of that deadline beside other work has no verdict, and is rerun
alone. A boot case without icount (68 of them) keeps the host’s clock in the guest, so load
lengthens every wait it makes: its pass is a verdict unless what it expects is a timeout or a
bound on a time, and a failure beside other work has no verdict until it fails alone. Every
bound a case states on a time, a step’s, a probe’s or a notice’s, is the box’s under one
condition, one whole bench at a time with QEMU its alone for the run and any other work on the
machine host-only and off the bench’s cores: measured under it, held to under it, and a bound
missed beside another boot is no verdict until the case misses it under it. A [net]
table by itself changes neither class: an empty one gives the guest a card that reaches
nothing, and binds no host port. A table with a forward, a poke, a peer or a dial puts host
sockets beside the boot, in wall time: its dials retry until the case’s deadline, so a pass
stands and a failure is rerun alone, as for any host-clock wait. Its host ports come from the
job’s lease under scripts/q (q run --ports N, the forwards and the poke; the job sees
REDOUBT_PORTS=lo-hi, a range no other lease holds, and the bench takes the forwards’ ports from
its start), so two such boots run side by side without meeting on a port; a sweep’s --jobs J
boots are J such boots inside one lease, each on its own slice of it (the sweep paragraph
above: the lease must hold J times the case’s forwards, or the sweep is refused); what remains under q
is a stranger to q taking a pooled port between the daemon’s probe and QEMU’s bind, which fails
that boot loudly, as before. Outside q the bench
picks a forwarded host port by binding and releasing it before QEMU takes it, so two such boots
at once may race for one port, and there the rule asks that two such boots not run at once; a
lost race fails the boot rather than hiding (QEMU cannot bind). An ssh-loopback
case is the same kind of case: its sshd runs in inetd mode through ssh‘s ProxyCommand
and binds no port, its guest’s stdio is a virtio-serial port, and the kind’s probe (one
loopback session with a 30 s connect timeout) runs once before any case and decides whether the
host can serve the kind, never a case’s verdict. So a loopback case that asserts no time (13 of
the 14) passes as a verdict, and a failure that is only its deadline is rerun alone. A case
that measures with the host’s clock is a verdict only alone: the rule asks that no other
invocation and no build run beside it, and for a whole bench scripts/jobs.mk holds that rather
than asks it, through the scheduler’s qemu lock (the scripts/q paragraph below). Those are a host-tests case whose crates’ tests assert
a wall-clock bound (redoubt-rt, redoubt-client, redoubt-keyd and redoubt-consoled do;
redoubt-ipd, redoubt-model and testbench only read the clock), which no tolerance would
make load-proof; a boot case whose bound is a ratio of two host times (sched-lock-contention-4-mttcg:
a stalled vCPU thread lengthens a wake but not the search it is counted in; beamlet-schedulers-mttcg:
a stalled vCPU thread lengthens one of the two runs it compares, and on the quiet set’s four cores
alone its one-hart twin read 81 to 95 for a ratio that is 94 in guest time, which is why that twin
runs under icount); a case whose expectation is a timeout (bench-ssh-guest, and
bench-ssh-loopback-deadlock, whose must_fail is the mark it never gets); and a host-clock
case with a VM session whose console goes through the hub’s hold and which must still be alive
after a hold boundary (the steward’s SSH session cases): a stall of the guest of a second or
more at the boundary reads, inside the guest, as the server’s silence past its promise, so the
session’s completion call times out and the session ends as at Ctrl-D. A host-tests case whose crates assert no bound measures nothing with the host’s clock; it may
run beside other work, and the rule asks that its test threads be bounded then
(RUST_TEST_THREADS), so that it cannot oversubscribe the host by itself. A bound the platform
under test keeps on the kernel’s clock is such a bound too when the kernel is the fake’s and its
clock the host’s: beamlet-lookup-host’s system tests once let a bind’s ATTACH_US and a call’s
timeout run against a fixture server under a whole bench’s load, and about one train in two the
host’s second ran out first; they hold the fake’s clock now (Fake::hold_clock), so each such
bound, a retry’s RETRY_US and a file operation’s FILE_WAIT_US included, is a step the test
takes once the state it waits on is reached, and the ten-second waits are gone with the race. Its
console.rs tests held the host’s clock the same way — one, input_nobody_reads_holds_no_idle…,
read the idle’s 200 ms deadline against the host and under load a read’s submit timeout ran out,
queued the read, and woke the idle early — and hold the fake’s clock too now, each deadline a step,
the console server’s session bound crossed by the ticks that cross it. A tick is taken only once
every other thread of the fake is in a wait, and a thread a change has woken counts as waiting
only when it waits again: before that, a tick could fall between a server’s answer and the
waiter’s hand-over of it whenever the host had not yet run the waiter, and on a loaded host the
busy-retry test’s retry fell past its last tick and the platform’s end waited for it on a clock
nobody moved, about one ./test-shell run in ten. The kinds that boot
nothing (build, fmt, no-cruft, the size and unsafe budgets, the docs checker, the Elixir
oracles) have no clock, and are verdicts anywhere, but for a timeout_secs: as for a boot, a
host-tests job or an Elixir case that only ran out of its deadline beside other work is rerun
alone.
scripts/q applies that rule for a whole machine. It is one scheduler process that leases real
cores: q run --cores N -- <command> waits for N free cores, runs the command pinned to them
(taskset; cargo’s jobs and RUST_TEST_THREADS follow the lease) and returns its exit code;
--quiet runs a host-clock case on a reserved core set (the daemon’s --quiet, by default its
last four cores, "" for none), one such case at a time, while the rest
of the machine keeps working; --ports N leases N host ports from the daemon’s pool (23000-23999,
below the ephemeral range; a port a stranger holds is skipped) and hands them to the job as
REDOUBT_PORTS=lo-hi, so a [net] case’s forwards never meet another’s, where before one
machine-wide --lock net ran every such case in turn (train 40: 30 cases, 12,360 s of summed
waiting, 1,353 s once for a 0.5 s case); a lease ends with the
client process, so a killed job frees its cores and ports, and a restarted daemon adopts the
jobs still running, their pins and their ranges, until they end (scripts/q-test checks the
lease on a daemon of its own). --lock NAME takes a named lock exclusively and --share NAME
the same lock shared: sharers run beside each other, an exclusive taker runs alone among the
jobs naming the lock, and from the moment it waits no new sharer starts ahead of it, so a
stream of sharers cannot hold it off. The lock qemu is how the condition every bound on a time
holds under, one whole bench at a time with QEMU its alone, is held rather than asked: a whole
bench (jobs.mk’s cases-*, quiet-* and all-* targets, and a set holding every case of
the boot, quiet or net class) takes it exclusively as a lock-only lease (q run --cores 0 --lock qemu, the qemu-held target) before its first case and keeps it to the make invocation’s own
exit, the lease’s command ending when make’s pid is gone, so the hold ends with the lease by any
exit path, a killed make or a dead train included, never by a trap or a file; a second whole
bench waits for the first. Every single boot case, a case with an arch run by name or in a
smaller set, a sweep by hand (q run --share qemu --cores M -- cargo testbench --smp N) and
launch‘s boot take it shared: single boots run beside each other as before, and one started
while a whole bench holds the lock waits, printing one line naming the holder (its tenant, its
name and its checkout) and since when, then runs when the hold ends; it never fails for the
wait. Under the whole bench’s own make its cases take no lock, since the make holds it, and a
case that boots nothing (no arch: the host-tests, Elixir, build, formatting and docs cases)
takes none: what it measures the lock does not protect, and the quiet set keeps the host-clock
host tests off the bench’s cores. A restarted daemon adopts a running hold as it adopts cores
and ports (Q_LOCK and Q_SHARE in the job’s environment), q ls names the holder and since
when, and a daemon from before the shared take runs a --share job unlocked and says so, as it
does for ports (restart it). scripts/q-test checks the lock as it checks the lease: the
sharers beside each other, the waits, the line, the hold’s end with its client and its
adoption. A job’s scratch goes to $REDOUBT_TMP, by
default .tmp at the checkout’s root, which git ignores, so removing the checkout removes it;
the job gets it as TMPDIR too, since a host’s /tmp may be a RAM filesystem a sweep would
fill. scripts/jobs.mk names every case as a make
target (rv64/<case>, cases-rv64, quiet-rv64, build-rv64, prebuilt, docs) and picks
the class for it: a boot takes one core per guest hart, a host-tests case or an Elixir case four
(an Elixir case is mostly the build of beamlet and the model’s trace writer, under that lease
but outside its deadline, so it stays in this class: Elixir oracles), a case
with a fanout two for its build while each of its jobs asks q for its own, and the host-clock cases
go quiet. A case target runs that case alone (--exact), from target/prebuilt when its width
is there (building once), else through cargo testbench; its output is
target/jobs/<arch>-<case>.log, and a failing boot’s console and session logs are kept beside
it (--keep-failed), so a transcript is never lost to the run directories’ pruning; the
scheduler oracle judges a kept console log again by hand, through its ignored host test
(SCHED_ORACLE_LOG=<log> SCHED_ORACLE_ARGS='<the case's post_check arguments>' cargo test -p testbench a_kept_log_judged_again -- --ignored --nocapture). A failing
host-tests case’s log holds the test harness’s failures block, from its failures: line: each
failed test’s panic and name and the test result line (a block past 400 lines keeps its first
panics and the names list), then Cargo’s line naming the test file that failed and how its binary
ended, never the warnings Cargo printed last (train 49 kept twelve of those and no test name). A case
with no arch boots nothing, so it runs under rv64/<case> alone, and rv32/<case> does
nothing. Case targets may run at once (set CASES="..." runs a set on both widths) only while
each still takes its own lease, the quiet ones run alone on the quiet set and the [net] ones hold
their port leases, as every case target does: the leases, not make, keep the host from being
oversubscribed. q ls shows
the core map and the queue; q log the recent jobs with the time each waited and ran.
cargo testbench --smp N boots every boot case once at N harts instead of its own counts, but
a case that keeps them (keep_smp), and bounds it by timeout_secs_smp where a case gives one;
since jobs.mk leases a case’s cores from its own counts,
such a sweep runs as q run --share qemu --cores M -- cargo testbench --smp N, M at least N.
The heavy host cases. What each costs on the 24-core build host, and the deadline it has (each a measured run and a third, unless its row says otherwise):
| Case | Its cost | timeout_secs |
|---|---|---|
model-mutations | 175 jobs, one per mutation, in release, one core each; a mutation’s steward families stop at 500 seeds, and the three they catch only after many seeds are caught first by directed scenarios (mutations). About two and a half minutes of wall, the build included; the longest job R2NoWaitCap’s, 18.7 s | per job, 25 |
model-host-tests | one cargo test on four cores, every model test but the mutations, the steward families and their coverage check: under two minutes, the build included | none |
steward-model-host-tests | the two steward families at their counts and the check that their coverage table is reproduced (property families), each a job on four cores and threads: under two minutes of wall, the build included; the longest job steward_policy’s, 26 s | per job, 35 |
rt-miri | 12 jobs, one per file, about 100 s of wall: heap’s 60 to 96 s; connection 25 s; the rest under 10 s | per job, 128 |
elixir-oracles, bench-elixir-oracles-broken-guard | a cold build of beamlet and the model’s trace writer, 29 s alone on four cores and up to 46 s beside a bench, outside the deadline (Elixir oracles); then the scripts, 2.5 and 1.3 s alone, 3.2 and 1.7 s beside two prebuilds | the scripts’, 10: four times elixir-oracles’ alone |
A case with whole_run = false is left out of a run with no filter and out of one whose filter
is only part of its name; it runs when the filter is its whole name, and --list marks it “by
name only”; jobs.mk’s cases-* and quiet-* leave it out too, and its own target runs it. It has
one reason: a measurement too long to repeat at every train.
The kinds, and the fields each takes besides description, arch and whole_run:
| Kind | What it does | Its fields |
|---|---|---|
boot | boots the kernel with programs as its first processes and judges the run | those above |
build | only checks that a package compiles for each target: coverage for what the bench does not boot; with forbid_in_binary, that the binary holds none of the byte strings named (self-checks) | package, features, debug_assertions (the checked profile instead of the release), forbid_in_binary, must_fail (the build’s error, or the scan’s finding) |
host-tests | runs cargo test on the host for the named workspace packages, for what no boot can reach (a constant the loader and the bench share is right in the machine’s eyes even when it is wrong); with miri, under nightly Miri. These cases are the bench’s only host tests; cargo test --workspace is not run, though it compiles. The kernel and the test programs have no host tests (test = false on their targets) | packages, tests (the test files to run; default all), miri, workspace, features, tools, filter (only the tests whose names contain one of these), skip (tests left out, by part of their name), profile (Cargo’s, such as release), fanout (each, env, values, cores, vars, late, late_cores), timeout_secs (each fanned job’s deadline) |
ssh-loopback | runs [[session]]s against a host OpenSSH server with no guest, to check the session runner on its own | authorized (the test keys the server accepts), [[session]], timeout_secs, host_key (default: the server’s own), server_log (patterns each of which must match a line of the server’s own log), must_fail |
unsafe-budget | the ratchet on unsafe (below) | [[budget]]: name, paths, max_unsafe, max_undocumented; [[uncounted]]: path, reason |
size-budget | the ceiling on each trusted crate’s size (below) | [[crate]]: name, paths, max_lines |
no-cruft | the source gate (below) | paths, [[forbidden]] (pattern, unless, within), no_allow_dead, one_definition, definition_paths, [[allow]] (path, rule, reason) |
fmt | the formatting gate (below) | roots, [[skip]] (path, reason) |
elixir | runs scripts that check an Elixir oracle on beamlet against the Rust it shadows, each of which must exit 0, on the pinned toolchain (below) | otp, elixir, build (commands run first, outside the deadline), scripts (each a path and its arguments), must_fail, timeout_secs (the scripts’ together) |
For host-tests, workspace defaults to the repository root and otherwise names a relative
directory below it with a Cargo.toml; an absolute path, a path outside the repository or a
missing workspace fails before Cargo runs. features defaults to none and passes the named
features to Cargo. For example, beamlet-lookup-host runs the VM and Redoubt tests from
userland/otp with beamlet-redoubt/fake; beamlet-lookup-cli-host runs separately without that
feature, so the two cases do not combine their Cargo features. tools names host programs the
tests run as an oracle (erofs-oracle’s mkfs.erofs, fsck.erofs and dump.erofs): each must be
an executable on the path, or the case fails naming the first missing, and skips it with
--allow-skip, as for any other host lack.
A fanout runs a long case as many jobs instead of one cargo test, one per each:
"value", one per line the shell command values prints, each running the case’s one test file
with that line in the variable env (model-mutations, one job per mutation, the names
cargo run --example mutations prints, in REDOUBT_MODEL_MUTATIONS); "file", one per entry of
tests (rt-miri); "test", one per test of every test binary the case builds, by libtest’s own
list, each run alone, those filter takes and skip does not (steward-model-host-tests). The
bench builds the tests once, first, with no deadline; then each job runs its test binary as
cargo test would, from its package’s directory (under Miri, which runs no binary by itself,
cargo miri test of the one file), through scripts/q on cores cores of its own (default one), as many at once as the
machine has room for. vars are set for every job: a test that spawns its own threads is told how
many it has (the model’s MODEL_THREADS), since under q its RUST_TEST_THREADS is the lease’s.
Where q does not answer, the jobs run one after another. Each job’s output is a file in
<case>/ of the run’s directory, and <case>.log lists every value with the time its tests
took; the case passes when every job does, and its failure names each value whose job failed. A
job that runs past timeout_secs fails, saying so: a deadline on the cores the job asks for,
stretched in proportion when q, once the job has waited, grants it fewer. late names values known to pass only past
a bound their test keeps, each with the follow-up that removes it: their jobs run with
TESTBENCH_LATE=1, the test’s leave to go past it, and a pass is reported as “caught late,
known” in the result and as LATE in the log, never hidden; any other value past the bound, an
entry that names no job, and one whose test now passes within the bound fail the case.
late_cores gives a late value’s job, the long search, its own count of cores; a {cores} in a
vars value becomes the count each job is granted, which q may lower from its ask once it has
waited, so a test that spawns its threads runs one per core it holds (the model’s
MODEL_THREADS, in model-mutations and steward-model-host-tests). No case names a late value
now.
A post_check judges the console after the boot has passed. sched_oracle rebuilds the
scheduler’s order from the raw events a tracing kernel prints and checks every pick against its own
reading of the rules (scheduling); a limit such as r10_p99_us=30000
bounds a measured cost. Two arguments judge a sibling’s first run: round, that it comes before
any other budget is picked twice, and lift-delay, that it comes within a round of what the lift
on its parent predicts. A walk-trace kernel’s walks are bounded by their longest, net of the
audits inside them (pump_max_us, expiry_max_us, reconcile_max_us), judged before
r10_p99_us, so a run whose destruction is over its bound still has its walks judged.
gate_harts=2 judges the latency targets on a trace of at most two harts (its F record) and
only reports them on more, marked recorded at N harts, not gated: the targets are gated at one
hart and two and recorded at four (responsiveness).
smp_fence reads only the same trace’s shootdown records: a page made executable was shot down
on another hart running its process, which acknowledged (memory).
smp_inflight reads only an inflight-trace kernel’s records of each RAM frame’s way through
R81 (frames in flight): retired (i, the frame and the process whose entry
for it was cleared), each shootdown (s), pending (d), given back to the bitmap (b) and taken
from it (o). Each frame is pending only on the hart that retired it and, if it was mapped, only
after that hart shot its process down; given back only once pending, so its hart has zeroed it;
and never taken in between. A run where no frame from a live space was retired, given back and
taken again fails as racing nothing.
Starting a case’s programs
Status: built · tested (7)
- bench:rng
- bench:budget
- bench:budget-carve-attack
- bench:budget-destroy-kills
- bench:programs-unknown-budget-attack
- bench:programs-unknown-program-attack
- bench:bundle-mapped
The loader loads only the kernel and init
(boot), so a kernel case’s first
program is packed as the bundle’s second entry and runs in init’s place. It gets init’s
handoff: the three budgets, the Reset right, every device and the bundle. It is the trusted
tester. When it is the log server, it starts the case’s other programs itself, through the
loader stub and from the bundle’s pages, each in a budget of its own carved from system. Each
program gets the same slots:
- slot 1, the boot endpoint: its receive right for the first program started, a send badged with its place for each later one;
- slot 2, the log endpoint, badged with its place;
- slot 3, its own budget;
- slot 4 on, the budgets the case names for it (
budgets = ["system"]), in the line’s order.
Its own budget’s handle gives a program nothing it lacks: the pages are already its own to
spend, a carve from it comes out of its own share (R7 (carving)),
and destroying it ends only the program and what it started
(R10 (destruction)), which the tester sees as a killed
notice. It lets a program read its own charges and run measured work in a budget it carves. The
budget is system-class, as its parent is, so a program may add labels below it; a kernel case
has no server those labels could reach.
The builder tells the tester which programs to start, and with which budgets, in one more data
entry, programs. It has one ASCII line per program after the first, in the case’s order: the
program’s entry name, then the names of the budgets it gets (root, system, users),
separated by spaces. The tester reads it from the bundle’s pages, which the loader verified with
the rest, and reads every line before it starts anything. It refuses the boot, and powers off,
on a line that is not printable ASCII, names an entry the bundle lacks or a budget other than the
three, or names a budget twice, and on more programs than system has processes. Each
program’s own budget gets an equal share of what system has free (pages and processes) and
weight 1,000, a driver’s, so no program’s limits depend on another’s name or order. A case that
needs other sizes builds its own tree from the budgets it is given.
The log server badges each program’s handles with the program’s place in the case, 2 on, and names programs by that place, because the kernel draws every PID but the first. A case matches a PID in a kernel line with a pattern. Each program gets an exit endpoint of its own, so the tester tells their notices apart (processes) and prints each under the program’s name and place, with the kernel’s PID beside it.
A program the tester starts holds no device, and every page it has is backed, its stack
included: only the process the loader starts has a stack reservation
(memory). So a case that needs a device, or a page never
touched, runs its program alone in init’s place, where its own budget is root.
init itself never takes a case’s place and has no mode for the bench. The kernel’s cases need
root and system, which no program under init may hold
(R33 (no server holds a system budget)),
so they run a tester in init’s place instead.
The servers’ cases under init
Status: built · tested (5)
- bench:init-servers
- bench:init-console-forgery
- bench:bench-init-reporter-forged
- bench:init-boot
- bench:littlefsd-reboot
A servers’ case boots the real init with a manifest of its own, packed as the manifest
entry, and its test programs are servers entries in that manifest. They get no budget handle,
their own included, as no server does
(R33 (no server holds a system budget)).
init prints its own lines bare, and consoled starts every other program’s line with its
connection id, [con N] with N in 16 lowercase hex digits
(consoled). A case’s reporter names a manifest entry, and
the bench reads that entry’s connection id only from init’s bare line announcing it,
init: started NAME, console N; a second such line in one boot fails the case. A restarted
server is announced as init: restarted NAME, console N, and the bench never reads a reporter’s
id from that line, so a reporter that restarts cannot pass its case. A case that judges a reboot
expects init’s reboot line and then the next boot’s first line, the loader’s. The machine
resets in the same QEMU run, with the same disk, and from that line on the bench reads the
reporter’s id afresh from the next boot’s announcement, so a case may go on to its verdict in the
next boot; still only one TEST PASSED line, in the whole run, may pass it. The case passes only if
exactly one line says TEST PASSED and it starts with that [con N] ; any other such line fails
it, wherever it came from. Such a case ends at its last expect, which waits for the verdict,
since no test program holds the Reset right. The test programs are redoubt-init-programs
(tests/init-programs): boot-reader reads a public entry through the root badge at bootfsd
its entry is handed, con-forger prints its arguments as lines, and the rest are the servers,
clients and drivers of init’s restart cases. Since init restarts a program that exits, each
parks when it is done, unless its exit is the point of its case.
The scheduler oracle
Status: built · tested (38)
- bench:sched-ties
- bench:sched-capped
- bench:sched-lock-contention
- bench:sched-lock-contention-4
- bench:sched-lock-contention-4-mttcg
- bench:sched-timer-entry
- host:testbench::kernel_sections_say_what_the_lock_waits_waited_behind
- host:testbench::the_driver_wake_is_judged_in_searches_of_its_own_run
- host:testbench::a_pick_passes_over_only_a_budget_that_other_harts_run
- host:testbench::the_oracle_decides_whether_a_timer_interrupt_ended_the_slice
- bench:sched-wake-no-preempt-harts-mttcg
- host:testbench::a_pick_in_place_is_a_slice_end_that_requeued_its_runner
- host:testbench::lock_waits_are_reported_per_mille_of_the_harts_time
- host:testbench::lock_waits_take_the_lock_in_ticket_order
- host:testbench::a_shootdown_record_is_passed_over
- host:testbench::a_trace_that_keeps_every_clause_passes
- host:testbench::each_broken_clause_is_caught
- host:testbench::a_broken_trace_is_rejected
- host:testbench::the_models_own_ranks_pass
- host:testbench::the_models_broken_ties_are_caught
- host:testbench::lifts_are_recomputed
- host:testbench::weight_changes_are_recomputed
- host:testbench::the_floor_and_the_passes_are_checked_on_their_own
- host:testbench::destructions_are_timed_and_bounded
- host:testbench::audits_are_subtracted_inside_each_window
- host:testbench::water_filling_caps_a_budget_at_its_threads
- host:testbench::a_charged_share_across_harts_is_judged_by_water_filling_net_of_lock_waits
- host:testbench::a_hart_share_is_judged_of_every_charge_against_water_filling
- host:testbench::timer_work_billed_elsewhere_in_a_budgets_time_is_bounded_inside_its_share
- host:testbench::idle_sections_that_found_nothing_are_bounded
- host:testbench::an_unmatched_audit_fails
- bench:sched-irq-wake
- bench:sched-deadline-preempt
- bench:call-bounds
- host:testbench::a_device_wake_that_preempts_is_caught
- host:testbench::a_device_interrupt_bills_its_devices_owner
- host:testbench::a_deadline_that_does_not_preempt_is_caught
- host:testbench::call_bounds_hold_each_call_to_its_empty_system_section
The oracle is independent of the kernel’s code: it reads what the queue did (woke, requeued, left,
pass changed, picked), never why, and rebuilds the order from the events alone: the lowest pass
first; at an equal pass a budget that woke ahead of one requeued; of two that woke, the later
kernel entry’s first, and within one entry the lower id; requeued ones in the order they were
requeued. On several harts it also reads which budget each hart runs (H) and how many of each
budget’s threads wait for a hart (J, those no hart runs): a pick takes the first budget in that
order with a thread waiting, and passes over one ranked ahead only if another hart runs it and
none of its threads waits, never one it runs itself. A slice’s end that picks where it is
(preemption points) records the requeue and the pick of
the hart’s own runner, with no H and no J: the oracle counts the preempted thread as waiting,
as the round trip’s J counted it, only at a timer interrupt on that hart that requeued the
budget, began no destruction and decided the slice over (=), and only for a budget with no other
thread waiting; anything else is refused, and the rank clauses judge the pick as any other. One
that picks another budget’s thread records that pick inside the interrupt and the hart’s new
runner at its return (H), and is judged as any pick. It
recomputes each lift and each weight
change from the rule, and lets a pass fall only at a weight change. A kernel built with
lock-trace, a test feature that implies the trace, also records each wait for the kernel lock’s
ticket after the wait (k: the ticket and the sections ahead of it when drawn); a release build
carries neither the feature nor the record. The records are written holding the lock, so the waits
appear in the order they took it, and the oracle requires that order to be the tickets’, each
drawn behind fewer sections than the harts: no wait outlasts the sections queued ahead of it
(R78 (fair kernel entry); sched-lock-contention at
two harts, sched-lock-contention-4 at four). A kernel built with hold-trace, which implies
lock-trace, also records each section of the lock as it is released (h: its first and last
tick; then j: its cause, a system call’s number, an interrupt’s or an exception’s code, and the
ticks of audits inside it). The oracle reports the sections’ lengths net of their audits, the
longest by cause, and splits the lock waits into the part another hart’s section covered (its
audits pro rata) and the part with the lock free, the hand-off to the halted waiter. The
contention cases carry it and judge nothing by it. fault_section_max_ticks=N bounds the
longest section a page fault began, net of its audits (fault-report-bound), and
timer_section_max_ticks=N the longest a timer interrupt began and timer_section_p99_ticks=N
their p99, the steady entry’s cost, which the few cold sections (a program’s first preemptions)
cannot hide a regression of; both are gated up to gate_harts as the latency targets are,
since under icount a section on several harts counts the others’ instructions too
(sched-timer-entry, at one hart; recorded at two). With the trace beside it,
idle_sections_max=<mark>:<N> bounds the kernel sections a hart entered from the idle and left
with no record of its own but an audit’s, a lock take that found nothing due and nothing runnable,
from the first run of the budget the program marks (the mark’s weight, as a share’s):
timer-flood-at-rest‘s two sleepers each sleep a thousand short timeouts on two harts, and a
kernel that arms every hart’s timer for a timeout whose payer runs nowhere wakes each hart for
the other’s naps too (the hart timer). Where the clock is the host’s,
driver_wake_p50_searches=K and driver_wake_p99_searches=K judge the driver wake’s net p50 and
p99 against K searches of the same run alone, from the program’s one search alone line, at any
hart count (sched-lock-contention-4-mttcg). Three checks read the interrupts’ brackets
(preemption points, charging):
irq_wake_no_preempt=N needs N device interrupts from user mode that claimed a source, woke one
budget and returned to the runner with no pick inside, whose hart’s next pick or interrupt was the
runner’s slice’s end (sched-irq-wake), and refuses any device interrupt that began no destruction
yet did not return to user mode; irq_billed_to=<mark> needs every device interrupt that claimed a
source to charge the budget the program marks after the claim, and lets
it charge only that budget and, for its return, the one it interrupted: the owner is the program’s
to name, and sched-irq-wake names the boot’s, system; deadline_preempts=N needs
every timer interrupt from user mode that destroyed another budget by its deadline to leave for
kmain with its runner requeued and the hart’s next event a pick, and N of them
(sched-deadline-preempt). With hold-trace, a CALL-BOUNDS line names two windows in the
kernel’s ticks, a factor and a floor: for every system call made in the first, its longest
section in the second, net of audits, is held to factor times its longest in the first or the
floor; a call made in the second alone is reported; at least eight must be judged (call-bounds,
R12 (scheduling)). sched-capped runs the model’s capped scenarios
(model) on the machine at two, three and four harts, each
budget’s share judged as below; hart_shares_from=4 records the shares on a trace of fewer harts,
since under icount QEMU’s turns move them, and sched-capped-mttcg judges the two- and
three-hart shares where the harts run at once (QEMU’s turns). It is itself checked against the model’s ranks and against traces broken one clause at a
time. The tracing kernel is a test build only
(R23 (no test channels)).
Elixir oracles
Status: built · tested (5)
- bench:elixir-oracles
- bench:bench-elixir-oracles-broken-guard
- host:testbench::another_version_is_refused
- host:testbench::the_scripts_share_the_case_deadline
- host:testbench::the_deadline_starts_after_the_build
An elixir case runs its scripts in order from the workspace root, each judged by its exit
status: elixir-oracles runs the steward core’s reference over its traces
(the trace encoding) and the wire codec’s vectors. The
scripts source userland/otp/tools/oracle.sh, which puts the pinned toolchain on the path and
runs a module on beamlet. Before any script the case checks the toolchain: the erl that
userland/otp/tools/env.sh puts on the path must be of the OTP release otp (its
releases/<major>/OTP_VERSION), and elixir --version must say elixir. A missing or other
toolchain fails the case even with --allow-skip, and no must_fail waits for it: an oracle that
does not run catches nothing; the dev image carries both, and scripts/setup.sh --with-beam
builds both on your own machine. Then the case runs its build commands, each of which must
exit 0, together within 600 s, a bound only a hung build reaches (a cold build’s times are
below). A failed or late build fails the case as a build, never as the oracle’s timeout, and is
never what a must_fail waits for. Both cases name userland/otp/tools/build-oracles, which
builds beamlet, the model’s trace writer and the trace checker as the scripts build them, so the
scripts’ own builds find nothing to do. With timeout_secs, the scripts together have that deadline, counted
from the end of the build, each run under timeout with what the ones before it left; one past
it fails the case, saying so, and is never what a must_fail waits for. The build is most of a
cold run (29 s alone on four cores), and its time is the host’s load: beside a whole bench, the
two cases building the same targets at once on loaded cores, it has taken 46 s. Built, the
scripts take 1.3 s (the self-check) and 2.5 s (elixir-oracles), so the deadline measures the
oracles alone. The case’s log says what the build and the scripts each took.
Checked builds
Status: built · tested (20)
- bench:bench-debug-assertions
- bench:bench-debug-assertions-off
- bench:boot-profile
- bench:boot-profile-unverified
- bench:sched-latency
- bench:sched-budget-churn
- bench:sched-exit-churn
- bench:timer-flood-at-rest
- bench:sched-exit-churn-mttcg
- bench:sched-timer-flood
- bench:sched-carve-return
- bench:deadline-flood-billed-traced
- bench:deadline-flood-billed-traced-mttcg
- bench:deadline-placement
- host:testbench::audits_are_subtracted_inside_each_window
- host:testbench::a_hart_share_is_judged_of_every_charge_against_water_filling
- host:testbench::an_unmatched_audit_fails
- host:testbench::cluster_credit_is_the_certified_interior_only
- host:testbench::cluster_lower_witness_counts_the_union_of_outer_bins
- host:testbench::a_device_interrupt_that_claims_nothing_bills_nobody
debug_assertions = true builds the kernel and the loader (the trusted base, not the programs) with
the workspace’s checked profile: release with debug assertions and overflow checks on. It is the
same kernel checked harder, not a special build. Three things that are silent in a release build
then panic, and every case forbids PANIC:
core’s preconditions on raw-pointer calls (slice::from_raw_parts,ptr::read,copy_nonoverlapping): a misaligned or null pointer, which is undefined behaviour and silent in a release build;- the kernel’s own
debug_assert!s: every error a call returns must be in that call’s row of the error table (the ABI), whichbudget-syscall-attackexercises over every call and thousands of hostile values; - arithmetic overflow, wherever the kernel or the loader does not use a checked or wrapping operation on purpose.
A checked build also runs the kernel’s audits, full scans that check the indexes, frame owners and
handle chains after a destruction and when a process object is freed, and the live PIDs, the
frame owners and the IRQ index when one of them changes outside a destruction (a process’s end
scans all of RAM, about 7 ms under icount). Every scan of a whole table is an audit; the checks a
return to user mode or a shootdown makes, a few entries each, are not. They hold the hart while
they run, and a release build has none of them. So a latency target or a share, which is measured
in a checked build because the scheduler trace needs one, excludes them: an audit neither fills a
window nor moves the schedule. The scheduler charges an audit’s time to no budget and moves the
running slice’s end past it, so the thread that ran it is picked and preempted as in a release
build; a kernel built with audit-billed, which keeps the old charge, misses the containment
gate’s deadline notice, in a recorded negative run. On several harts an audit also holds every
hart that waits for the kernel lock behind it, and that wait is the audit’s too: each hart marks
when it came from user mode, each audit’s end gives every marked hart the part of the audit it
waited through, and the waiter, once it holds the lock having waited, bills its runner none of it
and moves its slice’s end by it, as the auditor does. The trace records it after the wait (y:
the ticks), never more than the wait by the waiter’s own clock (harts’ clocks differ by a few
ticks under icount), and the oracle takes out of a share only the part of a wait that was
billed. A hart’s zeroing, idle, of the frames it freed
(frames in flight) is billed when it takes the lock back, to
the budgets that freed them; the trace records it (0: the ticks, the frames), and the oracle
reports the total. A destruction gives any hart’s zeroing still to bill to a budget it ends to
its own payer, lifted with the rest of that budget’s debt (p: the payer, the entries), which
the oracle counts and refuses outside a destruction; the checked kernel stops if a bill names a
budget that is gone. A kernel built with audit-wait-billed bills the whole wait as before:
sched-budget-churn-shell at two harts reads 329 and 339 of 1000 on rv64 and rv32 against 404
and 509, in a recorded negative run. The traced kernel stamps each audit’s start
and end (records U and V: which audit, and the time). The program prints each latency
sample’s window, its end on time_now and its length (LATENCY-SAMPLE <group> <measure> <end> <gross>) and how many it took of each, so a window lost on the way fails the check, and it
judges none of them. A program whose run goes on past its measurement marks the window’s end,
LATENCY-END <time> on the kernel’s clock: sched_oracle then judges no sample printed after it
and no destruction ending after it, reporting their count (the real steward’s steward-latency,
whose marker-file exits reap every lease). sched_oracle subtracts the audit time inside each window,
counting only the part of an audit that falls in it, and then applies the case’s bounds
(deadline_notice_p99_us=40000). It reports the gross, the net and the audit time beside each
target (responsiveness). A share is the kernel’s
charges, never a count: under icount a count is the machine’s instructions, not a hart’s time
(R12 (scheduling)). The program prints its window, marks the budget it
judges (an empty child of the mark’s weight, carved and destroyed, so the trace’s lift names the
parent), and names by weight and runnable threads each budget it runs against it (HART-SHARE <name> <start> <end> <tolerance>[+|-][@<harts>] <mark>:<threads> <weight>:<threads>...; + for
at least, - for at most, @ judged only at that many harts and reported at any other).
sched_oracle sums what the kernel charged each budget in the window, its pass’s rises times its
weight as the trace states it (each hart’s runner, H, carries its weight), less the part of each
hart’s waits for the kernel lock billed to the waiting hart’s runner though no thread of it ran
(a Q less its y); a lift
out of the cap set (u, followed by z with the floor then, which the lift may not pass) is no
charge. The part is the marked budget’s and what was lifted into
it, the whole every budget’s, and what the budget is owed is its water-filling share of the
trace’s harts (F) among the budgets the program names, which on one hart is its weight’s share;
every want is stated in the result. An audit is charged to no budget, so the share is net of the
audits; on several harts they fall mostly on the hart that switches budgets each slice, so
sched-large-weight keeps one hart. Each program notes its counts beside with no verdict, and
sched-share reports what the three counted of the calibrated rate (counted <n> of the calibrated 1000), the efficiency the slice ends leave. The release twins (sched-share-release,
sched-large-weight-release, deadline-flood-billed) have no trace and judge their counts at one
hart, in their expect lines; deadline-flood-billed-traced judges the same run’s share across
harts. Where the budgets a share is judged among are hostile agents the program cannot name one
by one, the share is of the charges under marks (CHARGED-SHARE <name> <start> <end> <tolerance> <mark>[:<threads>]..., the containment gate’s bystander against the leases under users). The
program prints its window and marks the budgets it means, each by carving an empty child of
the mark’s weight and destroying it, so the trace’s lift names the parent; sched_oracle sums
each budget’s pass rises in the window times its weight as the trace states it, for the first
mark’s budget against every marked budget and those lifted into them. What the budget is owed is
its weight over the weights of those the kernel charged in the window, its competitors, at one
hart, and on several its water-filling share of the harts among them, net of their harts’ lock
waits as above, a mark naming its runnable threads; the share must lie within the tolerance of it; a window in which a budget under the marks is
reweighed or ended is refused, since its competitors changed. The audits are charged to no
budget, so the share is net of them by construction; what a budget is charged out of the queue
shows only under its next wake’s floor lift and is not counted, so the wakes in the window are
reported beside, with every budget charged in it that no lift places under a mark. The residual:
it judges what the kernel charged, so a kernel that under-bills every budget under the marks
alike (idle or switch time charged to no one) passes it; the gate’s own expect lines and its
latency clauses bound that, not this one. An audit
that never ends, ends without beginning or runs inside a destruction fails the check. The oracle subtracts only what the trace shows it: a
kernel built with audit-unstamped, which leaves the audit after a destruction unstamped, misses
the containment gate’s deadline notice, in a recorded negative run. The audits themselves stay
full. The cluster’s envelopes (responsiveness) are credited
more strictly: a stamp is a floored microsecond, so an audit stamped u and v ran from somewhere in
[u, u + 1) to somewhere in [v, v + 1), and only its certified interior [u + 1, v) (empty
unless v > u + 1) is subtracted, where it meets the envelope. The uncertain edge bins stay counted
as elapsed time, so the credit is never more than the audit time inside, and an audit outside an
envelope lowers nothing. The credit is summed with checked arithmetic and may not exceed the
envelope. The other cases keep the whole-stamp subtraction above. The same trace records each
timer interrupt from user mode with every charge inside it, and sched_oracle checks that the
budget it interrupted pays only for its own items or its slice’s end
(charging); a kernel built with timer-tail-billed, which keeps
the old billing, fails that check in a recorded negative run. It records each device interrupt
from user mode the same way (x), with its claim (c: the source, or 0 when another hart claimed
it first), and checks that one that claims nothing is billed as a timer interrupt that ends no
slice: after its expiry, to the budget the expiry billed last or to nobody, never to the budget it
interrupted; one a deadline answered at its entry preempted before its claim (a destruction
inside it, O 2 and no c) the same way, and any other missing claim fails. It reports the
timer interrupts that charged a budget other than the one they interrupted and those ticks:
another budget’s timer work in the interrupted budget’s time on its
hart (timer); with foreign_timer_in=<share>:<N>
it bounds them inside that share’s window, the ticks of timer interrupts from user mode that
interrupted the judged budget (or one lifted into it) and charged a budget outside its marks, at
N of 1000 of what the judged budget was charged there, on a trace of two harts or more (at one
every interrupt is on the victim’s hart: recorded). Only timer interrupts count against the
bound: an item that has passed when a call’s entry or kmain’s comes is served there, so the
kernel records an expiry’s charges outside an interrupt too ($: the payer, the ticks and the
time in µs, which wraps after 2^32 µs, 71 minutes, longer than any case), and the check reports
beside each share the ticks they charged others at the judged budget’s own entries and in kmain
on a hart it had just left, judging nothing by them, and in its summary how many such charges the
trace holds, at a call’s entry and in kmain, and their ticks. The bound is judged where the
harts run at once (deadline-placement, deadline-flood-billed-traced-mttcg,
sched-exit-churn-mttcg, host-clock cases on the quiet core set): under icount which hart’s
entry first reaches an item that has passed is the order of QEMU’s turns, and a run locks into
one phase (timer). An
interrupt’s return (O) says where it goes: 1 to user mode with the interrupted runner’s slice
running, 0 the slice ended at this entry (to kmain, or in place to user mode, where the return
is recorded as the entry’s handling ends), 2 to kmain without, a preemption. Whether the slice
is over the oracle decides itself: the kernel records its decision’s inputs after the entry’s
expiry (=: the slice’s end and now, µs), the slice is over if its end is not after now, and a
return that says otherwise fails, as does a decision outside a timer interrupt on its hart or a
second one. With
wake_no_preempt=N the oracle proves a timeout only wakes: at one hart N naps each against the
slice that follows it; on several, each wake of the one budget that woke N times or more at the
entry that made it, a return to user mode or a call its runner goes on from counting as a witness
and a preemption (O 2, or the runner requeued outside an interrupt, with no destruction) failing
it, with at least wake_witnesses=K witnesses and at least wake_mid_slice=M of them mid-slice. A
kernel built with wake-preempts, whose timeout wake preempts as a deadline does, fails
sched-wake-no-preempt-harts and sched-wake-no-preempt-harts-mttcg on both widths in recorded
negative runs. The trace ends with one record of
the kernel’s time (C): every hart’s ticks in the kernel, from a trap’s entry or kmain‘s loop
to the return to user mode or the idle, in its id; the ticks charged to budgets in its pass; and
in its entry field, which it alone uses so, the ticks the checked build’s audits took.
sched_oracle reports nobody N of 1000 (kernel K ticks, audits A, charged C), the share of
the kernel’s time net of audits that no budget was charged, and judges nothing by it
(residual risks). Ahead of it, one record (F) holds the
ticks since boot and the harts started, and each wait for the kernel lock from user mode, the lock
held by another hart, is a record (Q: its start and end in ticks); sched_oracle reports
lock waits N of 1000, the waits as a share of the harts’ time, judging nothing by it either. The counters read the billing’s clock
and move no schedule, and a kernel without sched-trace compiles none of them. A kernel built with
alloc-first-fit, which takes each frame by the first-fit scan of RAM the bitmap replaced,
fails scan-bounds on both widths in a recorded negative run
(R12 (scheduling)).
Many cases use the profile: every case file with debug_assertions = true, most of them over
both widths (budget, budget-syscall-attack, lend-untouched-page, ipc and smp-boot among
them), and some, such as all-together, on rv64 only. The kernel
prints one line under cfg!(debug_assertions): bench-debug-assertions expects it, and
bench-debug-assertions-off forbids it in an ordinary boot. To check the whole suite:
CARGO_PROFILE_RELEASE_DEBUG_ASSERTIONS=true CARGO_PROFILE_RELEASE_OVERFLOW_CHECKS=true cargo testbench
That run fails bench-debug-assertions-off, as it should; everything else must pass.
sched-trace keeps the trace in a 64 MiB ring, and a trace that drops a record fails its case;
sched-trace-large is the same ring at 256 MiB, and two cases build it. The containment gate
does, at 576 MiB of RAM, since at the 1 ms slice its run of nine leases a slot writes about ten
records a slice, and at two harts each hart’s picks, waiting counts and lock waits besides, some
7.1 million, past 192 MiB’s 6.3 million. The ring’s frames are kept as 32-bit page numbers, so its
table fits the kernel’s RAM region. So does worst-walk, whose run at full occupancy
writes about 2.6 million records on rv64 and 2.9 million on rv32, past the 64 MiB ring’s 2.1
million.
boot-stats is a diagnostic feature like sched-trace and walk-trace, but of programs, not the
kernel: a Cargo feature of init, blkd, verityd, littlefsd, erofsd and beamlet-redoubt, off by
default and never in the image’s build. Without it the release binaries of init, blkd,
verityd, littlefsd, erofsd and beamlet have the section sizes they had before it, on rv64 and rv32
(measured with llvm-size against the commit before it, both built from the same path: beamlet’s
sizes move with its build path). With it, init’s lines and beamlet’s line for its first object
carry [t=N], time_now in µs; blkd, littlefsd and erofsd say their counts at each power
of two of their requests from 2^12 and verityd from 2^7, and littlefsd and erofsd once more, exactly, on a
walk of
Elixir.BootStats.beam, a name no volume holds; at the VM’s first console read beamlet says
beamlet: first console read [t=N] and what its lookups cost: their count and the guest time spent
in them; and when the shell’s driver has drawn its first prompt, beamlet: first prompt drawn [t=N], the end of the boot’s span (beamlet on Redoubt). The feature needs no
checked build. boot-profile and boot-profile-unverified boot the image’s programs with it under icount and a pinned seed: measurements, which bound only the boot’s time
to its prompt (the boot-time target).
Hostile inputs
Status: built · tested (17)
- bench:loader-rejects-kernel-address
- bench:loader-rejects-kernel-entry
- bench:loader-rejects-truncated-elf
- bench:loader-rejects-segment-data-cut
- bench:loader-rejects-wx-segment
- bench:verified-boot-rejects-tamper
- bench:verified-boot-rejects-bare-archive
- bench:verified-boot-rejects-short-initrd
- bench:boot-rejects-no-seed
- bench:boot-rejects-short-seed
- bench:boot-rejects-no-timebase
- bench:boot-rejects-irq-past-plic
- bench:rng
- host:testbench::a_dropped_property_is_gone_and_the_rest_still_reads
- host:testbench::a_shortened_property_keeps_its_first_bytes
- host:testbench::an_overwritten_property_has_the_words_and_its_length
- host:testbench::a_property_the_tree_lacks_is_an_error_not_a_quiet_boot
A program entry can be a good binary the bench corrupts before injecting it:
programs = ["log-server", { corrupt = "rng-test", with = { segment-vaddr = "0xffffffffffd00000" } }]
with is segment-vaddr, entry, truncate (a byte count smaller than the file),
segment-flags (letters of rwx for the first loadable segment: "rwx" asks for a page no
loader may map) or truncate-segment-data (the section table dropped and the file cut this many
bytes before the end of the last loadable segment’s data, so the headers parse and the data runs
past the end). tamper_bundle = true flips one bundle byte after signing, sign_bare_archive = true
signs the archive without its domain and length, and short_initrd = 63 hands the loader only that
many bytes of the signed bundle; the loader must refuse all three
(R15 (verified boot), R17 (fail closed)).
device_tree changes the device tree QEMU built for the case’s own command line: the bench dumps
it (-machine dumpdtb=), edits it in place and boots it with -dtb, so the firmware, the loader
and the kernel see the one machine with that one difference. Each edit names a property by path
and must find it:
device_tree = [{ drop = "/chosen/rng-seed" }] # removed
device_tree = [{ shrink = "/chosen/rng-seed", to = 8 }] # its first 8 bytes
device_tree = [{ set = "/cpus/timebase-frequency", words = [0] }] # its cells, as many as it has
A dropped or shortened property leaves FDT_NOP tokens behind, so no byte moves and the header
stays true (tools/testbench/src/fdt.rs). A case that expects a deliberate panic
sets allow_panic = true, which drops only PANIC from the always-forbidden list, and forbids what
must not happen instead. distinct_across_boots = ['id: (.*)'] boots twice and requires the captured
text to differ; distinct = ['console (.*)'] requires, within one boot, two or more lines it
matches and no capture twice, such as a restarted program’s new console. A hostile program is an
ordinary programs entry; hostile data for a program to use, such as a malformed ELF for a parent
to launch, is a bundle file.
The file systems’ parsers are also fuzzed, by hand with cargo fuzz and outside the bench, each
from its crate’s own fuzz/ workspace: littlefs’s image and mutate
(littlefsd), and beside them walfs’s image, arbitrary
bytes mounted, walked and written, and mutate, a valid volume with bytes changed and its hashes
forged or not (walfsd).
Files in the bundle
Bundle files
Status: built · tested: bench:bench-bundle-file, bench:programs-unknown-budget-attack, bench:littlefsd-reboot, host:testbench::a_file_s_servers_merge_into_its_manifest_by_name
[[file]] # a data entry, after the programs
name = "trace"
from = { path = "tests/data/bundle-file.txt" } # or any `programs` form, corrupted ones included
[[file]] # a manifest, with entries merged into its `servers`
name = "manifest"
from = { path = "tests/data/littlefsd/boot.json" }
servers = [{ name = "client", args = ["reboot", "littlefsd:data"] }]
[[file]] # a manifest pinning the userland disk's root, from the run's pack
name = "manifest"
from = { path = "image/manifest.json" }
verity = "image/userland.toml"
A file read from a path may be a manifest with servers entries merged in by name: each replaces
the members it gives in the entry of its name, or is added after the rest if none has it, so cases
that differ in one entry share one manifest, and a case can boot the image’s own manifest with a
client added.
Entry names must differ from each other and from kernel. A file named programs replaces the
listing the builder writes, so an attack case can hand the tester a hostile one. The bench
refuses a [[grant]] table: a program reaches a device only through the handles it is given
(R18 (device authority)). The loader starts only the
kernel and the program in init’s place, so a data entry reaches the guest signed and is never
run. bench-bundle-file reads its entry back: the program in init’s place finds it in the
bundle’s pages and compares it, byte for byte, with the file it was built with.
Data entries for init
Status: built · partly tested: no model trace is replayed under `init` yet · tested (1)
- bench:init-servers
init receives the verified bundle and hands the public entries to bootfsd, and a data entry
is how a model trace reaches an in-guest replayer, which compares results itself and prints its
verdict (boot). The program in init’s place
already reads a data entry from the bundle’s pages (bundle files); under init,
a program reads it again through /boot once the manifest’s public list names the entry.
Devices and the network
Disks and network cards
Status: built · tested (38)
- bench:bench-virtio-devices
- bench:bench-virtio-legacy-off
- bench:erofs-corrupt
- bench:erofs-read-only
- bench:image-disk
- bench:init-boot
- bench:net-tcp
- bench:userland-boot
- bench:userland-read-only
- bench:verity-flipped-tree
- bench:verity-wrong-root
- bench:verity-signed
- bench:verity-bad-signature
- host:testbench::a_recipe_can_generate_a_directory_of_files
- host:testbench::a_recipe_packs_a_table_and_a_volume_per_partition
- host:testbench::a_stage_is_walked_parents_first_in_name_order
- host:testbench::devices_sit_on_fixed_slots
- host:testbench::the_vault_disk_sits_beside_the_data_disk
- host:testbench::each_disk_holds_the_volumes_on_its_device
- bench:walfsd-boot
- host:testbench::every_network_is_restricted
- host:testbench::a_lease_slices_into_disjoint_ranges_or_none
- host:testbench::virtio_devices_are_modern
- host:testbench::the_userland_disk_sits_on_its_slot_read_only
- host:testbench::the_userland_pack_is_deterministic_and_stages_each_object_by_name
- host:testbench::a_verified_partition_is_its_volume_then_its_tree
- host:testbench::an_erofs_partition_is_its_stage_and_each_damage_is_corrupt_where_it_is
- host:testbench::a_walfs_partition_is_its_stage_and_two_packs_are_the_same_bytes
- host:testbench::the_manifest_pins_the_packs_root
- host:testbench::a_signed_partition_ends_in_its_root_block_signed_deterministically
- host:testbench::the_cases_volume_seed_is_the_development_seed
- host:testbench::a_volume_s_bytes_are_held_to_its_partition
- host:testbench::the_image_s_volumes_are_its_disk_s_partitions
- host:testbench::a_case_s_manifest_is_held_to_its_disk
- bench:launch-keep-disk
- host:testbench::a_kept_disk_is_attached_as_it_is
- host:testbench::a_kept_disk_of_another_layout_is_refused
- host:testbench::a_kept_disk_is_held_to_its_recipe_s_manifest
[disk] # a virtio-blk disk, zeroed, created afresh for every boot
size_kib = 4096
partitions = 1 # optional: a GPT of this many equal partitions, by blkd's builder
# or, instead of both: a disk recipe packed for every boot as ./mkimage packs it
# recipe = "image/disk.toml"
# stage = "tests/data/littlefsd/stage" # optional: what every partition holds instead of its stage
# flip_version = true # optional, with a recipe: one bit of each signed volume's version flipped
# keep = true # optional, with two boots: the second boots the disk the first left
[vault] # optional, with [disk]: a second writable disk, disk2, the same keys
size_kib = 2048
partitions = 1
[userland] # the userland disk, attached read-only, packed once per run
recipe = "image/userland.toml"
# flip = "Elixir.Enum.beam" # optional: one bit of this file's data flipped on the disk
# flip_tree = true # optional: one bit flipped in the first level-1 tree block
# wrong_root = true # optional: the manifest pins a root one digit off the pack's
[net] # a virtio-net card on QEMU's user-mode network
forward = [22] # guest TCP ports reachable from the host (default: none)
host_key = "ssh-ed25519 AAAA..." # optional: the only SSH host key sessions accept
[idle] # with launch = true: measure a session's `idle` step (one)
interrupts_per_hart = 9.0 # optional ceilings, each per second of the window
user_ecalls = 18.0
host_cores = 0.01
A disk recipe (image/disk.toml) is packed by the code ./mkimage runs (testbench --pack-disk): a GPT of equal partitions by blkd’s builder, then each partition as its fs
says, holding its stage’s tree: littlefs, a writable volume written through littlefsd’s own
code; erofs, a read-only volume written by libs/erofs’s writer
(erofsd); or walfs, a writable volume written by libs/walfs
itself (walfsd), so a case boots the disk the image ships.
A disk with keep = true is made for the case’s first boot and booted again, as that boot left
it, by the second (distinct_across_boots): launch-keep-disk writes a file at the prompt in one
boot and reads it in the next, as ./launch --system --keep-disk keeps a person’s disk between
launches. A kept disk whose size or partition table is not the one a fresh disk would have is
refused, never reformatted.
A manifest’s volume that gives bytes (init) must be exactly
its partition’s size, which init never reads. A recipe names the manifest its disk serves
(manifest = "image/manifest.json"), and the pack is refused if a volume’s bytes differs from
its partition’s, or the partition at its index has another name; at load the bench refuses a case
whose manifest file gives a volume bytes its disk’s partition does not have, whether the disk
is a recipe or size_kib and partitions. With a [vault], each disk holds the volumes of the
blkd its device goes to: a volume’s disk names its blkd, whose devices entry is disk0 or
disk2.
[vault] is a second writable disk beside [disk], with the same keys and its own recipe or
layout, for a manifest that keeps the unlabelled home volume and the vault on separate devices,
as a confined one must (R34 (confined placement): one blkd serves one label set,
so two label sets need two disks). It is disk2 on its own slot, made and kept as the data disk
is, beside it. walfsd-boot boots both: a blkd on each, a walfsd on each disk’s one volume,
and a client writing and reading back on both. Its slot, bus 4, is the one
tests/data/init/driver.json names slot5: the empty slot dma-driver is given in
init-driver-restart and init-quarantine-reboot, empty only because no disk sits there. A case
carries [vault] or that manifest, never both.
A recipe’s volume may also generate files, for a case that needs many and not their
contents: generated = { files = 600, read = "f000" } makes f000 to f599 in the volume’s root
(as many digits as the last needs), all empty except read, which holds its own name and a
newline. They sit beside the stage’s tree, if there is one, and a name in both is refused.
A volume may be verified, verity = true: it holds the largest volume that
fits beside its hash tree, then the tree (verityd), and the pack says
its root and data blocks. An erofs volume is followed in its range by zeros, which the tree covers
too. A verified partition may be signed, sign = { key = PATH, version = N }: its last whole block
is then a root block holding N, the version and the root, signed with the 32-byte Ed25519 seed in
the file PATH (relative to the workspace root) under the volume domain
(verityd), the volume and tree fit before it,
and the pack says the version too. Signing is on the build host only; a manifest names the key,
never the seed. The cases’ seed, tests/data/verity/dev-seed, is 32 bytes of 0x42 (B): the
bundle builder’s development seed (DEV_SEED in tools/testbench/src/build.rs), so "key": "bundle" verifies it. Ed25519 is deterministic, so two packs are byte-identical. A case’s
flip_version flips one bit of each signed volume’s version after the signing, on the disk and
never in the manifest.
For erofs-corrupt, an erofs partition may be damaged after its pack, through the parser
erofsd uses to find the place: damage = { what = "magic" } flips a bit of the superblock’s
magic; { what = "block-past-count", path = "tail.txt" } starts that file’s blocks at the
volume’s block count; { what = "compressed", path = "motd" } lays that file out compressed;
{ what = "name-offset", path = "lib" } starts the last name of that directory’s first block past
the block’s end.
The userland disk (image/userland.toml) is packed by the same code: first its objects are
staged, each module of the applications the recipe names, compiled by the pinned toolchain and
stripped, as a plain file under its own name, then its one partition is packed as a verified
volume of those files. The bench stages and packs it once per run: a bundle file read from a path
with verity = "image/userland.toml" is a manifest, and the builder writes the pack’s root and
data blocks into the verity of the volumes entry of the partition’s name, so the signed
manifest pins the disk; [userland] attaches the same pack. A case’s damage goes on its own copy
of the disk after the pack, never on the root: flip flips one bit of a file’s data where the
volume holds it, and flip_tree one bit of the first level-1 tree block. wrong_root changes the
manifest’s root by one digit instead, never the disk
(R76 (verified volumes)). Nothing is generated beside the objects.
Devices use virtio-mmio’s modern transport, which blkd and netd require. Each sits on a fixed
virtio-mmio slot, whether or not the case has the others, so a case’s manifest names its devices
as the image’s does (image/manifest.json names the first three):
| device | [table] | QEMU bus | base | irq | manifest line |
|---|---|---|---|---|---|
| data disk | [disk] | virtio-mmio-bus.7 | 0x10008000 | 8 | { "name": "disk0", "base": "268468224", "irq": 8, "dma": true } |
| network card | [net] | virtio-mmio-bus.6 | 0x10007000 | 7 | { "name": "net0", "base": "268464128", "irq": 7, "dma": true } |
| userland disk | [userland] | virtio-mmio-bus.5 | 0x10006000 | 6 | { "name": "disk1", "base": "268460032", "irq": 6, "dma": true } |
| vault disk | [vault] | virtio-mmio-bus.4 | 0x10005000 | 5 | { "name": "disk2", "base": "268455936", "irq": 5, "dma": true } |
The userland disk is attached read-only (readonly=on): QEMU refuses every write
to it, so nothing on the box can change it. The guest reaches nothing outside QEMU
(restrict=on, checked for every [net] case): there is no outside peer, only forwarded
connections coming in, unless a case adds one deliberately. Nor is it offered IPv6 (ipv6=off),
which it does not speak: slirp would otherwise send it router advertisements. Each boot gets its
own host ports, from the job’s lease under scripts/q (a sweep’s concurrent boots each from
their own slice of it) and chosen by the operating system otherwise, so benches running side by
side do not collide.
Peers, dials and the capture
Status: built · tested (16)
- bench:bench-net-peer
- bench:bench-net-peer-twice
- bench:bench-net-peer-count
- bench:bench-net-peer-pcap-empty
- bench:netd-restart
- bench:sshd-login-bound
- host:testbench::a_dial_with_a_line_waits_for_it
- host:testbench::a_held_dial_ends_when_the_far_side_closes
- host:testbench::a_poke_gets_a_udp_forward
- host:testbench::peers_are_judged_on_records_and_capture
- host:testbench::a_capture_is_read_fail_closed
- host:testbench::what_the_guest_sends_is_checked
- host:testbench::records_are_counted_per_peer
- host:testbench::a_dial_needs_its_echo
- host:testbench::prefixes_and_peers_are_checked
- host:testbench::peers_get_the_wider_network_and_a_capture
A network case can give the guest hosts to reach, and judge what it sent, all from outside the guest, after the boot has passed:
[net]
forward = [8000]
self_forbidden = ["10.0.2.0/24", "127.0.0.0/8"] # the guest must never send a SYN to these
[[net.peer]] # a host the guest may connect to, and exactly how often
addr = "10.0.9.100:7"
connections = 1
[[net.dial]] # the bench connects in through a forwarded port and needs the echo
port = 8000
send = "hello\n"
expect = "hello\n"
after = '^\[con [0-9a-f]{16}\] judge is up$' # optional: dial only once a console line matches
until_closed = true # optional: then hold the connection until the guest closes it
[net.poke] # one UDP datagram into the guest, sent when a console line matches
port = 47000
payload = "redoubt netd restart probe"
after = '^\[con [0-9a-f]{16}\] judge knows netd.s instance: poke it$'
- Peers are QEMU
guestfwds to a program: for each connection the guest makes, the bench’s own binary starts as a helper on it, records the connection as a file before it echoes a byte, and then echoes. After the boot each peer’s count must equal itsconnections. There is no host listener another process could take. - The poke is one UDP datagram, sent once, through a host port QEMU forwards to its guest port,
when a console line first matches its
after: a trigger from outside that nothing resends, as TCP would.netd-restartfaultsnetdwith it, through a test-only feature. - A dial is a TCP connection the bench makes into the guest through a forwarded port, retried
every 100 ms until one connection echoes
expectforsend, from the boot’s start or, withafter, from the console line that matches it; one never echoed by the deadline fails the case, with what came. Withuntil_closedthe bench then keeps the connection, typing nothing, until the guest closes it, and notes under the case’s result how long it was held; one still open at the deadline fails. That is a client that connects and never goes on, which the guest must end itself:sshd-login-boundholds everysshdslot that way and the verdict is the login the box then serves, never the dials, which write nothing on the console. - The network. A case with peers widens slirp’s network to a /16 in which its host, resolver
and the guest’s address stay where they were; the peers sit outside the /24 the guest is
configured for, reached through its gateway.
restrict=onstill holds. - The capture. A case with peers records every frame on the guest’s card, before slirp, and
reads it fail closed: missing, empty, cut or malformed fails the case (
net.truncate_capturecuts it on purpose, for the self-checks). The guest may send only ARP requests for the gateway, ARP replies (to any address) and IPv4 TCP, never a fragment and never a SYN to aself_forbiddenprefix. Each peer’s count must also match the distinct SYNs to it in the capture, and a case with peers needs one that expects a connection, whose SYN shows the capture was live.
The guest’s own claims about the network are never trusted.
SSH sessions
Sessions and the loopback server
Status: built · tested (20)
- bench:bench-ssh-loopback
- bench:bench-ssh-loopback-openssh
- bench:bench-ssh-loopback-deadlock
- bench:bench-ssh-loopback-forbid
- bench:bench-ssh-loopback-exit
- bench:bench-ssh-loopback-host-key
- bench:bench-ssh-loopback-aborted-text
- bench:bench-ssh-guest
- bench:steward-ssh-two-principals
- host:testbench::expect_after_matches_in_order_and_names_the_first_miss
- host:testbench::the_reference_proxy_quotes_only_what_the_bench_chose
- host:testbench::the_cpio_writer_writes_newc
- host:testbench::the_guest_recipe_parses_and_hashes
- host:testbench::a_bad_package_is_broken_and_no_network_is_the_hosts
- host:testbench::the_keeper_finds_what_names_the_case
- host:testbench::the_keeper_waits_to_the_deadline
- host:testbench::resize_needs_a_pty
- host:testbench::only_marks_follow_exit
- host:testbench::ended_keeps_the_input_open_until_sshs_own_exit
- host:testbench::no_other_child_inherits_a_sessions_terminal
Sessions need net.forward = [22]. They start once every expect has matched and run concurrently
while the bench keeps watching the console; a session whose first steps are waits starts its
ssh only once those marks are set, so its login follows what they mark. Each drives the host’s
OpenSSH ssh, an implementation independent of the box’s, to the guest’s port 22 with a test key.
What the box says about them, a login it refused or a session’s budget given back, is asked for
with the case’s expect_after: console patterns matched in order from the sessions’ start to the
case’s deadline, a miss failing the case with the first pattern unmatched. expect cannot ask for
those lines, since the sessions start only once it has all matched.
[[session]]
user = "alice+secrets" # the login name
name = "vault" # optional; unique in the case, names its log; defaults to `user`
key = "alice" # optional; defaults to `user` up to any '+' or '.'
pty = false # true asks for a terminal
forbid = ['bob-secret'] # never in this session's output, until ssh exits
steps = [
{ expect = '\(1\)> ' }, # wait for the prompt
{ send = "File.read(\"/work/x\")\n" },
{ expect = 'id ([0-9a-f]+)' }, # a pattern with groups keeps its captures...
{ send = "approve $1\n" }, # ...for a send to type back ($1 to $9; $$ is a $)
{ mark = "alice-ready" }, # tell other sessions this one got here
{ wait = "bob-ready" }, # wait for another session's mark
{ resize = [132, 43] }, # with `pty = true`: resize ssh's terminal
{ idle = 60 }, # with [idle]: type nothing for 60 s while the bench measures
{ within = 30 }, # the next step must finish within 30 s, before the case's deadline
{ exit = 0 }, # close input, read until ssh exits, require this status
{ ended = 0 }, # or: input open, read until ssh exits on its own, require this status
{ mark = "alice-gone" }, # only marks follow `exit` or `ended`: this session's ssh is gone
]
ssh_args = ["-W", "host:9"] # optional: more ssh arguments, before the host
command = "echo hi" # optional: a command (with `-s`, a subsystem) in place of a shell
A session the box ends, after a line it must act on (a call that ends the session, say), follows
that line with ended, not exit: exit closes the input first, and with pty = true that
close hangs up the terminal ssh reads and discards what it has not read yet, so the line may
never leave the host; the box’s end of a channel whose input is still open has nothing to race.
exit stays for the sessions the bench itself closes. The log notes when the end came, as it
does an expect’s match. Every session’s exit status is checked and all of its output passes
forbid; a session that fails stops the others. Its log notes each expect that matched and when, in seconds after its ssh
started, and the bench prints under the case’s result those matched before the session first
typed: a login’s latency to its first prompt, re-measured by every run
(sshd). A pty = true session’s ssh reads its input from a pseudo-terminal the bench
opens at 80x24, so that ssh reports a size change as OpenSSH does for a user; its output stays on
pipes. resize sets that terminal’s size and signals ssh (SIGWINCH), which then sends a
window-change if the size changed. The terminal is the client’s input and never a verdict. With net.host_key set, ssh refuses any other host key. Test keys live in
tests/keys/; they are public and marked not for production, and a boot manifest that lists one
must never ship. A launch = true case (launch-system) boots the command line ./launch --system builds, unchanged, and its sessions log in with a key made beside the bundle when it is
packed, which alice alone holds in that bundle’s manifest, as launch gives her the checkout’s key
(try the system). The ssh-loopback kind runs sessions against a server that ssh starts itself
for each session as its ProxyCommand, so nothing listens on a port: Redoubt’s sshd on its host
platform (against Redoubt’s sshd), or with server = "openssh"
OpenSSH’s server in inetd mode, in a QEMU guest. Its log goes to a file beside the transcripts,
never to ssh’s output; the standard error ssh would otherwise share with it goes to that log
for Redoubt’s sshd and is discarded for QEMU’s. So a late line of the server’s, such as the
broken pipe it may meet writing to an ssh that has refused its host key and hung up, cannot
stand in for the session’s last output, which is ssh’s own. The bench creates the log, empty,
before the first session, so a case whose sessions time out before ssh starts the server reads
it empty. A case’s server_log asks what the server saw (a refused key, say), not only what the
client printed, and its server_log_forbid what the server must not have done (a console
started, say).
OpenSSH’s server runs in a QEMU guest. On a host that enforces SELinux, sshd moves every
login shell into the user’s default context, and a bench running in a service’s context may not
enter it, so the host’s own sshd cannot serve the reference case. A container needs a runtime
and user namespaces that the bench’s host may refuse. A guest under the bench’s own
qemu-system-riscv64 needs neither; the client, the session runner and the case are unchanged,
so the case is still a witness independent of Redoubt’s server. The guest is not Redoubt, and it
boots QEMU’s own OpenSBI: the rule that only RustSBI boots is Redoubt’s.
- The image is a Linux kernel and an initramfs built from
tests/ssh-reference/guest.toml: Debian’s riscv64 kernel,openssh-server, the libraries it links andbusybox-static, each pinned by version and sha256 in one timestamp ofsnapshot.debian.org, which keeps every version it has published; with them the guest’s/init, its logins (root andsshd’s privilege-separation user), the kernel module it loads (virtio_mmio) and what it leaves out, each with its reason. The bench fetches each package withcurl, checks its sha256, unpacks it withdpkg-deb, and writes the initramfs’snewcarchive itself. It keeps the image intarget/ssh-reference/under the first 16 hex digits of the recipe’s sha256, and builds it only when that is missing, so only the first run after a change to the recipe needs the network. - Each session boots its own guest:
ssh‘sProxyCommandis QEMU with no network and no host filesystem. The case’s configuration and keys reach the guest in its initramfs: the bench writes, for each case, the image’s archive followed by an archive of the case’s files. The session’s stdio is a virtio-serial port; the guest’s/initrunssshd -ion it, reading and writing one open of the port, and powers off whensshdis done. Everysshdprocess opens its log anew and a port takes one open at a time, so they share a FIFO that one reader carries, a line per write, to a second port, which QEMU appends to the case’s log: a line of up to 4 KiB, the most a FIFO takes in one write, reaches the log whole among other sessions’ lines. The guest’s console goes toguest.logbeside it, for people reading a failed run, and is never a verdict; a failed boot powers off rather than reboots. The server logs in only root, inside the guest, runs/bin/shfor every login and allows nothing else. - ssh ends each guest. Once the session ends,
sshexits without waiting for the server and hangs up on its proxy. Whatsshdlogs after that is lost; the lines the cases ask for come earlier.sshhas no parent-death signal, so a bench killed outright leaves it running until its session ends, and its guest with it. The keeper: once a case’s sessions have all exited, anyqemu-system-riscv64whose command line names the case’s directory (the run’s own) has until the case’s deadline, and at least five seconds, to go, as a loaded host may slow a guest’s shutdown with nothing wrong; one still running then is killed, and the case fails, naming it, unless a session has already failed it. - Before the first OpenSSH loopback case the bench logs in once and runs
exit 0, and the server’s log must name OpenSSH’s version, so that no other server can pass for it. Itssshwaits at most 30 seconds for the server’s banner, so a guest that never boots fails the probe rather than hanging the bench. Without aqemu-system-riscv64the bench can use, withoutcurl,dpkg-deborxzto build the image, or with no image andsnapshot.debian.orgnot answering, every OpenSSH loopback case fails with that reason, as on a host without OpenSSH, and--allow-skipskips them. A package whose sha256 is not the recipe’s, a fetch that fails while the snapshot answers, a build that fails and a probe that fails all fail every OpenSSH loopback case. The check connects directly: on a host whose only way out is an HTTP(S) proxy thatcurluses, a fetch that fails there finds the snapshot silent, and is a host lack that--allow-skipskips.
The machine at rest
Status: built · tested (11)
- bench:launch-idle
- host:testbench::the_log_is_counted_by_hart_and_name
- host:testbench::a_rate_over_its_ceiling_fails
- host:testbench::a_window_that_measured_nothing_fails
- host:testbench::the_monitor_is_reached_and_left_by_the_mux_escape
- host:testbench::an_idle_step_needs_idle_and_launch
- host:testbench::the_window_opens_once_the_frames_in_flight_are_back
- host:testbench::the_window_opens_after_the_lines_already_queued
- host:testbench::a_drain_that_never_ends_fails_at_the_bound
- host:testbench::no_drain_seen_fails_at_the_bound
- host:testbench::only_the_kernel_s_lines_open_a_drain_and_one_inside_is_named
What an idle Redoubt costs its host is measured from outside the guest. A launch = true case
with an [idle] table and one session step { idle = N } boots ./launch --system’s command
line; when the session reaches the step, it types nothing for N seconds, still reading its output,
and the bench measures that window:
- Traps, from QEMU’s own log.
-nographicmultiplexes QEMU’s monitor on the console, so the bench types Ctrl-A c,logfile <case>.int.logandlog int, and Ctrl-A c back, when the window starts, andlog nonewhen it ends: QEMU logs each trap a hart takes (riscv_cpu_do_interrupt: hart:H, async:A, … desc=NAME) for the window alone, and the command line stays launch’s. The session’s quiet starts once the bench has typedlog int, and its next step waits until the bench has typedlog none, so no other step’s work falls in the window. Logged from the boot on, every system call would be a line. The bench counts each hart’s interrupts per second by name (timers, software interrupts the firmware and the kernel send between harts, devices) and the exceptions per second by name, every hart’s (user_ecall, the system calls;supervisor_ecall, the kernel’s calls to the firmware). - QEMU’s host CPU time, its user and system time from
/proc/<pid>/statat both ends, per second of the window: the host cores the idle machine takes. The kernel counts that time in clock ticks (getconf CLK_TCK, 100 a second here), so a 60 s window reads it to 1/6000 of a core: 0.002 cores is about 12 ticks, and a 0.01 ceiling is 60.
The case log gets one [idle] line with every rate, and a rate over its ceiling fails the case;
a ceiling left out is measured and printed only. A window that measured nothing fails too, never
passing under its ceilings for want of data: no log, no timer interrupt on any hart (an idle hart
may take none in a whole window, since a timeout whose payer runs nowhere is armed on one hart:
the hart timer), no system call from user mode, or no host CPU
time. launch-idle’s ceilings are twice the most that ten 60 s windows measured, five a width
(the case’s comment gives each), so a ceiling catches a cost that doubles, not the
window-to-window spread: 3.8 interrupts a second on the busiest hart (1.6 to 1.9 measured), 12.2
system calls from user mode (6.0 to 6.1), and 0.01 host cores, the measure’s own resolution
(0.001 to 0.002). Before the one-hart rule the busiest hart took 3.4 to 3.5 a second, three
quarters of them the kernel lock’s hand-off interrupts, each timeout waking every hart
(the hart timer).
The window never holds the zeroing of the frames in flight
(frames in flight): about 35,000, which the boot and the
login leave in flight and one hart zeroes once every hart first idles after the login, about half
of a window’s host time when the window held them. The kernel says on the console when a drain of
1,024 frames or more begins (mem: 1024 frames in flight) and when the frames in flight are back
to 0 (mem: frames in flight 0, at most N). When the session reaches its idle step, the bench
reads the console lines already queued, until it falls silent for 50 ms (a host-clock settle, for
those lines only), and holds the session and
the window until a drain has ended since the sessions began, none being open. Six runs a width
alone, at four harts, saw them back 0.32 to 0.39 s after the step began on rv64, at about 0.6 host
cores, and 5.8 to 6.2 s on rv32, at about 0.15; why rv32’s every hart idles that much later
after the prompt is not yet measured. The bench waits at most 30 s from the step’s start, about five times
rv32’s most, the margin for a loaded host; a drain still open then, none ended, or a console never
silent fails the case, and the failure names which; the drain’s end is the kernel’s line, never a
settle time. The case log’s [idle] drain: line, before the window’s own, says what
the wait came to: the drain’s most frames, the wall time from the step’s start to its end and
QEMU’s host CPU meanwhile, or that none ended in the wait. A drain that opens inside the window
is named on the window’s own [idle] line, written once it has ended: the window’s work,
measured. Before R81 the busiest hart took 3.1 interrupts a
second on rv64 and 2.8 on rv32, at 0.002 cores; with the wait, those twelve windows read 2.9 to
3.5 at 0.001 to 0.003 cores. The measures are the hardware’s view: they say how often the guest wakes, not which budget woke it;
that would take the kernel’s own trace, which prints only at a reset. launch-idle is a
host-clock case, run in the quiet class.
Against Redoubt’s sshd
Status: built · partly tested: agent forwarding is refused inside `sunset`, which no case sees, since `ssh` asks for it without a reply ([residual risks](servers/sshd.md#residual-risks)) · tested (13)
- bench:sshd-loopback-logins
- bench:sshd-loopback-r67
- bench:sshd-loopback-interrupt
- bench:sshd-loopback-independent
- bench:sshd-loopback-window-change
- bench:sshd-loopback-window-change-zero
- bench:sshd-loopback-env-refused
- bench:bench-ssh-loopback
- bench:bench-ssh-loopback-host-key
- bench:sshd-host-tests
- host:testbench::an_ssh_lacking_an_option_is_named
- host:testbench::the_redoubt_proxy_keeps_its_errors_off_ssh
- host:testbench::the_redoubt_servers_log_exists_before_any_session
ssh-loopback cases run the host’s OpenSSH ssh against Redoubt’s own sshd on its host
platform, redoubt-sshd-host (the core and its platforms),
which the bench builds and ssh starts as its ProxyCommand. Its host key is loopback-host,
and each of the case’s authorized keys is a principal of the same name. Nothing there needs a
shell, a login context or a guest. The box’s platform, on the guest’s port 22 with the steward’s
logins and real sessions, is the steward-* boot cases’ (steward-ssh-two-principals and the
rest, sshd).
- The self-checks run on it, their steps written for its scripted console, and their
server_logpatterns for its log. - Cases, verdicts from
ssh’s exit status and the server’s log: a login key the server’skeydholds is refused and never reaches the login table, and so is an unknown principal;alice+secretsgets the labels{alice-secrets}; on a labelled channel a shell without a pty,exec, a subsystem, and remote and local port forwarding are refused, and no console starts (R67 (a channel keeps its labels)), and the log names each refusal, the shell’s asshell-without-pty; a break reaches the console as its interrupt; one connection’s end leaves another’s session running; a host key other than the case’s is refused. A resized terminal’s window change reaches the console as its new size, and one to no size (0x0) is refused and never reaches it.envis refused, and the log names only the request’s kind, never the client’s name or value.sshwants no reply to either refusal, so the server’s log is the whole evidence: each case requires the refusal’s line and forbids its opposite. - One reference case stays on OpenSSH’s own
sshd, withserver = "openssh": concurrent sessions, marks, exit statuses, a pty and a refused key. It is the session runner’s independent witness, so a bug the runner shares with Redoubt’s server cannot pass every self-check (bench-ssh-loopback-openssh). Its server runs in a QEMU guest (sessions and the loopback server). sshgetsWarnWeakCrypto=no-pq-kexagainst Redoubt’s server, whose exchange is not post-quantum: OpenSSH’s warning would otherwise be session output. OpenSSH 10.1 introduced the warning and the option together, so the bench hasssh -Gparse the option once per run, with no configuration file as the sessions run it, and passes it only to ansshthat takes it: an older one has no warning to quiet, and none to filter from its output (OpenSSH 9.6 prints nothing over such an exchange). When it drops the option, the run’s output says why.
Self-checks
Status: built · tested (17)
- bench:bench-attack-forgery
- bench:bench-console-after-expect
- bench:bench-poweroff-missing
- bench:bench-reporter-mismatch
- bench:bench-init-reporter-forged
- bench:bench-debug-assertions
- bench:bench-debug-assertions-off
- bench:bench-net-peer-twice
- bench:bench-net-peer-count
- bench:bench-net-peer-pcap-empty
- bench:bench-net-self-unrefused
- bench:bench-cbo-self-unrefused
- bench:bench-qemu-early-exit
- bench:bench-elixir-oracles-broken-guard
- bench:bench-no-trace
- bench:bench-trace-scan-catches
- bench:bench-test-only-refused
The harness can fail, and each feature shows it. Cases named bench-* check the bench itself:
each feature has a case that passes only if the feature works and, where the bench can be
misconfigured on purpose, a case that must fail:
must_fail = '^regex$' # passes only if the run fails with a matching reason
must_fail is judged against the run’s verdict only (console, sessions, devices); a build error or
the bench’s own trouble is a failure regardless, and so is an elixir case’s toolchain. A build
case’s must_fail alone matches its build’s error, or its binary scan’s finding (below). Each case
writes its pattern anchored and quoting the evidence, so it cannot pass by failing for some other
reason; the bench does not enforce the anchoring, so a reviewer checks it. An attack case can have
a self-check of its own: bench-net-self-unrefused runs net-attacks’s boot with ipd not told
one of the box’s addresses, and must fail on the SYN the capture then shows.
bench-cbo-self-unrefused runs cbo-user-fault’s boot with a kernel that leaves senvcfg
permissive: all four cache-block operations must be seen running, and the run must fail on the
verdict line that never comes.
bench-elixir-oracles-broken-guard runs the steward core’s reference with its not_locked guard
held always, and must fail on the first event where its output leaves the core’s
(the trace encoding).
A build case with forbid_in_binary reads the binary it built and fails on the first byte string
named that it holds anywhere, quoting the offset and what is around it: bench-no-trace builds the
production kernel, the release profile with the board feature alone as ./build makes it, and
forbids the scheduling trace’s console-line prefix and its module’s mangled path: the scan proves
this trace absent, not every channel
(R23 (no test channels)); bench-trace-scan-catches
builds a checked kernel with sched-trace (debug_assertions = true: a test-only feature
compiles into no other) under the same scan and must fail on the trace’s console line; and
bench-test-only-refused asks the release profile for sched-trace and must fail on the kernel’s
own refusal, a test-only feature needing a checked build, in the compiler’s words.
The unsafe budget
Status: built · tested (13)
- bench:unsafe-budget
- host:testbench::actual_source_counts_still_enforce_the_budget
- host:testbench::empty_configuration_is_not_coverage
- host:testbench::every_configured_root_must_contain_rust_source
- host:testbench::missing_paths_fail_regardless_of_extension
- host:testbench::unreadable_source_reports_its_path
- host:testbench::broken_nested_symlink_is_not_silently_skipped
- host:testbench::zero_unsafe_source_is_valid_as_a_file_or_nested_directory
- host:testbench::every_on_target_source_is_in_a_budget
- host:testbench::a_long_safety_block_directly_above_justifies
- host:testbench::a_raise_needs_its_unsafe_budget_line
- bench:rt-miri
- host:testbench::a_miri_case_runs_its_files_under_miri
unsafe-budget.toml lists every source directory of the trusted computing base that runs on the
target, each with the most uses of unsafe it may hold and the most that may lack a justification
(zero everywhere): a // SAFETY: comment above an unsafe block, and a # Safety section in the
doc comment of an unsafe fn or unsafe impl, in the comment block directly above or within a
few lines. The case counts both and fails if either is over.
Budgets only go down. Raising either limit, dropping a budget or narrowing its paths needs a line
Unsafe budget: <name>: <reason> in the commit that does it, which the case reads the way the
size budget reads its own (below), with the same history check. A page that
quotes the ceilings, in a `unsafe` (pinned) column like the
kernel’s TCB table, is held to them by the docs checker
(below), so a ceiling cannot move without the page.
A configured path with no Rust source in it fails. So does coverage left out: every workspace
member that can be built for the target (its crate root is no_std) must have each of its Rust
sources in some budget, unless the file lists it under [[uncounted]] with a reason (the test
programs, the model, host tools, vendored code), and an uncounted entry that names no such
member fails too. Vendored third-party crates are outside the ratchet
(below). So are crates outside the workspace: the gate reads only the
workspace’s members, and userland/otp is its own workspace whose no_std crates (re, crypto,
vm) no budget counts. They are not in the trusted computing base; if one ever joins it, it joins
the workspace and the gate sees it.
The ratchet counts unsafe; it does not check it. rt-miri runs the native runtime’s host tests
under Miri (Stacked Borrows, isolation off), which checks the heap’s free lists, page buffers,
lends and device registers that a native run only executes. It runs the files that finish in
seconds, among them registers over the fake kernel’s real device memory, and the heap’s own,
heap, in a minute or two (fewer random rounds under Miri), each file a job of its own
(fanout); ipc and echo take minutes under Miri and are run by hand. Its
files assert no wall-clock bound, only hang guards, so it is not a host-clock case. Without
nightly Miri the case is missing, not passed.
With the runtime’s page-buffer aliasing fix reverted, mapping_views fails it with the Stacked
Borrows error not granting access to tag <wildcard> because that would remove [Unique for <…>] which is strongly protected.
The size budget
Status: built · tested (12)
- bench:size-budget
- host:testbench::only_code_lines_count
- host:testbench::a_test_module_does_not_count
- host:testbench::a_test_module_file_does_not_count
- host:testbench::a_shipped_file_always_counts
- host:testbench::a_form_the_case_cannot_follow_fails
- host:testbench::a_raise_needs_its_reason
- host:testbench::the_ratchet_reads_the_commit_that_raised
- host:testbench::a_merge_is_judged_against_its_first_parent
- host:testbench::merged_history_is_not_read_again
- host:testbench::a_new_budget_file_needs_every_reason
- host:testbench::a_deleted_budget_file_fails
The size of the trusted computing base is budgeted, not observed
(the tenets). size-budget.toml lists each trusted crate (the kernel, the loader,
the stub, the libraries they and the servers link, the model and the servers) with a ceiling in
lines of code: every line of every .rs file under its paths that is not blank, a // comment
(doc comments included) or inside a /* */ comment. Tests are left out, so writing them costs a
crate nothing: a #[cfg(test)] item counts for nothing, and neither does a file only test modules
reach (mod tests;, the modules it declares in turn, and those declared inside an inline test
module). A file any other module declaration reaches counts, whatever else names it; a module is
found by its name, its enclosing inline modules and its #[path] or cfg_attr path, and one whose
file is not under the crate’s paths fails the case. So does a form the case does not follow, which
could reach a file past a test’s #[path] to it: a mod whose name is not a plain identifier
(r#name, a macro’s $name) and the word include, however it is invoked. The case fails when
a crate is over its ceiling. The ceilings started at each crate’s size when the case landed and only
fall: the case reads the commits that changed its file on the branch it runs on, merges included,
and where one raised a ceiling over the file in its first parent, dropped a crate (a rename drops
the old name) or narrowed a crate’s paths (fewer lines counted under the same ceiling), requires a
line Size budget: <crate>: <reason> for each such crate, in its message or, for a merge, in a
commit it brings in. A commit whose parent lacks the file is judged against the last version
before it; where there is none, as for a file the main branch lacks (new or renamed), every entry
in it needs its line. A commit that deletes the file fails the case, so deleting it and adding it
back raised cannot escape. A raise not yet committed fails, and so does a path with no Rust source in
it; uncommitted changes do not stop the committed ones being judged.
A branch is judged on its own commits: those since its merge-base with the main branch
(redoubt, or origin/HEAD in a clone that has no such branch), so a package is judged before it
merges and merged history is never read again. On the main branch itself only a raise not yet
committed is judged. With neither branch to measure from, as in a shallow clone that lacks the
merge-base, the case fails rather than passing unchecked.
The residual: a macro defined outside the budgeted paths, a dependency’s macro_rules! or a
proc macro, can emit mod x; or include! at a call site, and the case reads only the call. No
trusted crate’s dependencies are known to, and adding one is a Cargo.toml change reviewed as
part of the trusted computing base
(tenet 5).
The memory budget
Status: built · tested: bench:init-boot, bench:userland-boot, bench:userland-read-only, bench:beamlet-footprint, bench:beamlet-compile-footprint, bench:steward-session-ends, bench:steward-ssh-two-principals, bench:init-refuses-stack, bench:memory-host-tests, host:testbench::a_qmp_socket_is_private_and_binds, host:testbench::heap_fits_holds_an_eighth_of_the_cap_over_the_peak
A boot case under init can set memory = true. After its console verdict the bench stops
QEMU over QMP and dumps the guest’s physical RAM beside the case’s log, as
<case>-<arch>-smp<N>.ram. The runtime writes each server’s heap record before main, so the
record is the witness that a server has started: a dump missing a declared server’s record lets
the guest run on and is taken again, until every record is present or the case’s deadline
passes, when the case fails. A server’s peak is therefore the most pages its heap had held when
the last declared server had started, or later, never earlier than the stop line. A wait is
printed first, as memory: dumped twice, waited S s for NAMES. The launcher has painted each
server’s first-thread stack with a tag for that server and an index for every eight-byte unit.
The bench scans the RAM for those tags at their encoded offsets within physical pages. That
ignores paint words copied into ordinary stack slots, while refusing a missing server, a
duplicate unit or an out-of-range index at an encoded offset. A stack page’s units are counted
from the one physical page that holds the most of them, so a stack word copied into a buffer or a
message is not a duplicate. The lowest missing unit marks the stack’s deepest touched point; two
pages holding equally many of a stack page’s units are refused for that unit’s stack page or one
below it, and ignored above it, where either leaves the peak where it is. The bench prints
stack NAME PEAK of PAGES pages for each server and fails when the declared pages are less than
twice the measured peak rounded up to a page. The runtime paints each stack it spawns a thread on
the same way, with the server’s tag, the spawn’s number from 1 and each unit’s index from the
top, since the stack’s size is the program’s, not the manifest’s
(redoubt-rt); the bench prints stack NAME thread N PEAK for
each it finds, the peak the deepest unit overwritten under the deepest one found, which is the
stack’s bottom short of an overflow (which ends the process at the guard page), and checks no
margin: the program’s constant (beamlet’s SCHEDULER_STACK_PAGES) is sized from the largest by
hand. The dump, the size of the guest’s RAM, is deleted
once scanned; a scan that fails on a duplicate or out-of-range unit, or cannot read the dump,
keeps it as the evidence. The QMP socket is in a directory of the run’s own under the temporary
directory, made 0700 under a name drawn at random, so whatever the bench’s umask only its user
can reach the socket and no other user can leave a file where it will be; the directory and the
socket go when the run ends, passed, failed or in error. A bench killed outright leaves the
directory, empty of any listener since QEMU dies with the bench, under $REDOUBT_TMP, the
job’s scratch. A temporary directory so deep that the socket’s path would reach a Unix socket’s
108 bytes is refused before QEMU starts, naming the limit. The manifest’s
stack_pages defaults to 16 and cannot exceed 128
(the boot manifest).
Each server’s runtime also keeps a heap record, 32 bytes in its data: a magic word, the server’s
launch tag, its heap cap and the most pages its heap has held at once
(the native runtime). The runtime writes the
magic word and the tag before main, so the program’s file and the launcher’s copies of it hold
none. The same scan finds each server’s record by its magic word and tag and prints
heap NAME PEAK of CAP pages, or heap NAME PEAK pages uncapped. It fails a missing or
duplicated record, a record whose cap is not the manifest’s heap_pages, and a capped server
whose cap is less than twice its peak; an uncapped server is reported only. A case that drives a
workload within a server another case sizes from its idle peak sets heap_fits = true, and its
capped servers pass instead when the peak leaves at least an eighth of the cap unused: the
question there is whether the work fits, not what the server’s size should be
(beamlet-compile-footprint).
The standard image is scanned after init-boot, userland-boot and userland-read-only on both
widths, and after steward-session-ends and steward-ssh-two-principals, whose SSH logins are the
most its servers do. Its declarations are twice the largest peak across those runs: each stack
rounded up to pages, each heap cap in pages. sshd is sized for its four slots (its entry’s
buckets=4, sshd) busy at once: its
heap held 8 pages at boot, 54 with one login (rv32, before the boot pack) and 56 with two at once,
so at most 46 a connection, and its cap is twice 8 pages and four connections, 384. Its declared
stack is a page over twice its peak. ipd’s cap is not twice its peak either: it holds a base of
twice its peak apart from its socket tables, 2 × 37 = 74 pages, and every socket its buckets may
charge, its buffers, its slot and its table entries, 108 × 4.25 = 459 pages, since a socket the
heap could not hold would fail an allocation in a shared server (ipd).
Its peak of 61 pages holds those tables, sized at start for its 108 sockets, 24 pages beside the 37
of everything else. consoled’s row is from the runs once it serves each
session’s console as a multiplexed session. The two walfsd rows are one server’s, from six runs of
walfsd-quota, three on each width, which writes through it, as the image’s memory cases do not
(their boots peak at 16,040 bytes of stack and 9 heap pages); its heap cap is also above what a
transaction of the format’s 32 blocks adds to that case’s peak, 32 pages, since no case writes
that many at once (walfsd). The read-only case also scans its
additional client from the merged manifest.
| Image server | Largest stack peak (bytes) | Declared stack (pages) | Largest heap peak (pages) | Heap cap (pages) |
|---|---|---|---|---|
keyd | 7,368 | 4 | 4 | 8 |
consoled | 10,384 | 6 | 11 | 22 |
bootfsd | 7,320 | 4 | 1,089 | 2,304 (the image publishes beamlet, piped, consrelay and crossing, and the cap follows each manifest’s own published total) |
blkd | 4,520 | 3 | 19 | 38 |
netd | 4,296 | 3 | 2 | 4 |
ipd | 13,768 | 7 | 61 | 533 (twice its peak apart from its socket tables, 74, and its buckets’ 108 sockets’ buffers, which the cap must hold, ipd) |
walfsd:data | 28,616 | 14 | 15 | 64 |
walfsd:alice-secrets | 28,616 | 14 | 15 | 64 |
blkd:system | 4,520 | 3 | 17 | 34 |
verity:system | 8,264 | 5 | 59 | 118 |
erofsd:system | 9,704 | 5 | 13 | 26 |
steward | 16,392 | 9 | 15 | 30 |
sshd | 5,256 | 4 | 56 | 384 |
The read-only client’s largest stack peak is 6,616 bytes and its heap’s 31 pages; its case uses
the 16-page stack default and no cap. A session’s beamlet is no manifest server: the steward
launches it with an 18-page stack, twice beamlet’s stack peak of 36,136 bytes (beamlet-footprint
on rv64, with the boot pack read before its VM starts and its console on the hub; a compile at the
prompt peaks at 34,280 on rv64 and 25,832 on rv32 in beamlet-compile-footprint, whose heap is
judged under heap_fits: 9,135 and 8,798 pages of the 11,220 cap), its second
scheduler’s thread with a stack of the same size (its peak at the prompt between 21,496 and
25,200 bytes on rv64 over three runs, 21,752 on rv32, stack beamlet thread 3; the platform’s
three other threads stay under 1,600, beamlet-footprint), and a heap cap of what its share holds beside
its two schedulers’ stacks and thread pages, its locks’ endpoints and its process’s page, 11,220
pages of the 11,264 the steward gives it of the 11,392 sizes gives a session, the rest its
console relay’s (budgets, the steward): 108 pages over twice its heap’s
largest peak across the memory cases on each width, 5,556 pages (rv64 at 1 hart),
above what its prompt holds (beamlet). beamlet-footprint scans
the VM alone, under its own copy of the single-VM manifest. Its cap leaves its process heap,
ETS and persistent_term limits, a sixteenth of its budget each (696 pages), reachable: a flooding process, about
four times its limit, still fits under the cap (beamlet).
A context’s console relay is no manifest server either: consrelay-footprint has init start it
under a manifest of its own, beside a stand-in that takes its hello, and scans it once it says it
serves, since it reserves every buffer before then. Its first thread’s stack peaked at 8,360 bytes
on rv64 and 7,392 on rv32, its heap at 22 pages on both; the steward launches it with a 5-page
stack and a 44-page heap cap (consrelay). The steward’s own
cleanup thread and launch thread are the two threads it spawns painted (stack steward thread 1
and thread 2): in steward-session-ends the cleanup thread’s stack peaked at 1,432 bytes on
rv64 and 1,168 on rv32, and the steward gives it one page, twice 1,432 being 2,864; the launch
thread’s at 4,840 and 3,808, and it gets three pages, twice 4,840 being 9,680
(the steward).
This is a measurement of the paths the case drove. Other requests or deeper call paths may need more stack or heap, and any guest, including another server, can forge the public paint pattern and the heap record. The result is evidence for the image’s declarations, not a proof against hostile guest code.
Vendored dependencies
Crates as published
Status: built · partly tested: provenance against crates.io needs the network, so no bench case runs it; it is run by hand in the review of any change to `vendor/` · tested (11)
- bench:vendor-check
- bench:vendor-build
- host:redoubt-vendor-check::the_real_structure_passes
- host:redoubt-vendor-check::a_renamed_header_fails_before_any_download
- host:redoubt-vendor-check::a_missing_row_fails
- host:redoubt-vendor-check::a_row_without_its_directory_and_a_stray_directory_fail
- host:redoubt-vendor-check::vendored_files_are_the_published_bytes
- host:redoubt-vendor-check::the_vendored_copies_are_the_ones_that_build
- host:redoubt-vendor-check::the_patches_point_at_vendor
- host:redoubt-vendor-check::the_readme_records_each_crate
- host:redoubt-vendor-check::every_vendored_file_is_tracked
vendor/ holds third-party crates exactly as crates.io published them, each used through a
[patch.crates-io] path, and vendor/README.md records each one’s version, license and published
checksum. Git must track every vendored file: a crate’s own .gitignore applies inside vendor/,
and many name Cargo.lock. Two checks guard them, and they prove different things:
- Integrity since vendoring (
vendor-check, every bench run): every file is byte for byte whatvendor/SHA256SUMSrecords, nothing is added or removed, and the build takes the crates fromvendor/, never from a registry copy. The checksums were taken from the tree itself, so this proves the crates have not changed since they were vendored, not that they are what crates.io published.vendor-buildchecks they buildno_stdfor both widths. - Provenance (
tools/vendor-check/provenance.sh, in review): downloads each published crate, checks its SHA-256 against the live crates.io index and againstvendor/README.md, and compares it with the vendored copy. It fails closed: before any download it checks that the README’s table andvendor/name the same crates, in the same number, and it exits 0 only if every crate it checked matches on all three counts and it checked as many crates asvendor/holds.
The residuals: provenance is only as current as the last review that ran it, and the vendored
crates’ unsafe is checked by recorded Miri runs, not by a bench case
(ipd under Miri, sshd under Miri).
Patched crates
Status: built · tested (4)
- bench:vendor-check
- host:redoubt-vendor-check::vendored_files_are_the_published_bytes
- host:redoubt-vendor-check::a_patched_crate_differs_only_by_its_patch
- host:redoubt-vendor-check::every_patch_is_a_vendored_crates_and_recorded
A crate we must change is still vendored from its published bytes, with exactly one patch file,
vendor/patches/<crate>.patch, holding every change. vendor/<crate>/ is the published crate
with that patch applied, since that is what Cargo builds, and nothing else differs.
- Integrity:
vendor/SHA256SUMSrecords the published bytes.vendor-checkcopies the crate, reverses the patch on the copy, and requires the result to match the sums byte for byte, so the patch file is the whole difference. - Provenance:
provenance.shdownloads the published crate, applies the patch, and compares the result withvendor/<crate>/. - The README records each patched crate’s patch: what it changes and why, as its own section.
- A new release of the crate means taking the published bytes again and redoing the patch on them; a patch the crate’s author has taken goes away with the release that carries it.
sunset is patched (sshd), and what its patch does
is tested through its public API (tools/vendor-check/tests/sunset_patch.rs). ascii is patched
too: rustc 1.98 refuses to build it from a path as published, since Cargo caps a registry crate’s
lints, not a vendored one’s. miniz_oxide is patched to box the deflater’s 64 KiB code buffer
under with-alloc, as it is on wasm32, so its state is never a 65 KiB stack local on a scheduler
thread (beamlet; tests/zlib_codec.rs measures the
inline and the boxed parts).
The no-cruft gate
Status: built · tested: bench:no-cruft, host:testbench::a_rule_scoped_where_nothing_is_searched_fails
no-cruft.toml reads the sources and boots nothing. It fails on:
- a name of an interface the tree has dropped (its
forbiddenpatterns); - the native runtime handing out the raw call:
libs/rt/srcre-exportingredoubt-syswhole (alias, glob,selforextern crate), or apubitem or one-line re-export there namingsyscall(forbiddenpatterns heldwithinthat path; awithinthat is missing or outside the case’spathsfails the case); allow(dead_code)orallow(unused...)in the kernel, the loader, the layout and paging crates or the test programs;- a Cargo feature that no
cfg(feature)reads; - a second literal definition of
PAGE_SIZEorUSER_AREA_END, or anyconst PAGEalias; the model is searched too, and its ownPAGE_SIZEinmodel/src/spec.rsis an[[allow]], because the model is the independent oracle and depends on no implementation crate.
Its [[allow]] entries (path, rule, reason) are the only exemptions, and an entry that no longer
covers anything fails the case too.
The formatting gate
Status: built · partly tested: that a skip with no reason, or one that names no workspace, fails is read from the code, not run by a self-check · tested: bench:formatting, host:testbench::only_tracked_workspaces_are_reported, host:testbench::diff_headers_of_both_rustfmt_forms_name_the_file, host:testbench::every_elixir_file_is_walked_from_its_deepest_root
formatting.toml holds the tree to the formatting rule: in each
cargo workspace root it names (the main workspace, each host-only fuzz or oracle crate that is its
own workspace, and userland/otp), it runs cargo +nightly fmt --all --check and fails on every
file that is not formatted with the repository’s rustfmt.toml. It also fails on a tracked Cargo.toml
with a [workspace] table that is neither a root nor a [[skip]], so a new crate outside the main
workspace cannot drift unchecked, and on a skip with no reason or no workspace. Two are skipped:
bios/, the upstream RustSBI firmware with its own configuration, and the docs checker’s fixture
crate, whose layout is the checker’s input. The generated wire codecs (libs/wire/src/proto/) are
in rustfmt.toml’s ignore: the generator is their one definition, and its own test holds them to
its output. Without nightly rustfmt the case fails, unless
--allow-skip. The case file is not called rustfmt.toml: rustfmt would read it as the
configuration for everything under tests/.
The Elixir is held the same way, and by the file rather than by the project: the case lists every
.ex and .exs git tracks or has not ignored (so a file about to be added counts, wherever it
is put) and runs mix format --check-formatted on them, under the pinned toolchain, from the
deepest of the [elixir] roots above each, which is where its .formatter.exs is: the
repository root, whose .formatter.exs (110 columns, as rustfmt.toml sets) covers the
steward’s and the wire’s Elixir, the OTP test programs, the bench’s script and the docs
checker’s fixtures; and userland/shell, the shell’s own. Each root must hold a
.formatter.exs, and one anywhere else is a finding, as a configuration the walk would not use;
a file under no root is one too. Three directories are skipped with their reason, as the Rust
codecs are: libs/wire/elixir/proto and client, redoubt-wire-gen’s output, and
libs/steward/elixir/gen, redoubt-steward-gen’s; each generator’s test holds its files to its
output. A skip over no Elixir, or without a reason, fails. Before this walk only the shell’s
./test-shell ran mix format, over the shell’s own inputs, and the bench ran none: the
steward’s reference, the wire’s hand-written Elixir and the OTP test programs went unformatted
for as long as they existed. Without the pinned mix the case fails, unless --allow-skip.
The docs checker
What it checks
Status: built · tested (9)
- host:redoubt-doccheck::good_tree_is_clean
- host:redoubt-doccheck::narrow_cases_fire
- host:redoubt-doccheck::c1_reports_each_failure
- host:redoubt-doccheck::c13_reports_each_failure
- host:redoubt-doccheck::index_over_its_ceiling_names_the_largest_pages
- host:redoubt-doccheck::pages_scope_keeps_only_the_listed_pages
- host:redoubt-doccheck::pages_scope_keeps_a_directory
- host:redoubt-doccheck::untracked_code_is_not_checked
- host:redoubt-doccheck::a_copy_under_an_ignored_directory_is_checked_whole
redoubt-doccheck (tools/doccheck) holds this book to its own rules:
cargo run -q -p redoubt-doccheck prints each finding as path:line: C<n>: message;
--pages <path>... keeps only the findings on those pages, and --code adds C11, the check of
code comments and case descriptions for the documentation switch-over. It checks that
every section has one well-formed status line and every test it names exists; that milestones carry
their names; that no page carries process references; that every rule ID is defined once and cited
by its short name; that every relative link resolves; that the security register
agrees with the pages; that no binary sits under docs/; that pages keep their templates; that
every wire table is included once; that every page is in the table of contents; and that every
count in a `unsafe` (pinned) column equals the ceilings in unsafe-budget.toml
(the unsafe budget), summed over the budgets under a row’s Where paths or
read by the name in its Ratchet budget cell. Each rule has a small bad tree it must fire on and a
good one it must not. mdbook build docs renders the book; its search index is held to the
ceiling the book’s rules state, a failure naming the size and the
three largest pages, and the check has its own small book over the ceiling.
Running its tests. cargo test -p redoubt-doccheck runs them from any directory and any
shell the project supports (through scripts/q too); the bench’s docs case runs the same suite
(below). The fixtures are found by the crate’s own path, not
the working directory. C11 asks git which files under the tree it checks are tracked, so that a
checkout’s untracked files (reference sources, scratch) are not Redoubt’s code; a tree that is no
tracked part of a repository, outside one or under an ignored directory such as .tmp/ or
target/, is checked whole, and the caller’s GIT_DIR does not redirect the question.
The docs checker in the bench
Status: built · tested: bench:docs
A host-tests case runs the checker’s tests, among them one that checks this whole book and one
that builds it with mdbook and fails on any warning, on a search index over its ceiling and on
an indexer older than the book needs; the checker also reads code comments and
case descriptions, so they cite pages and rule IDs that exist.