Evidence
A machine page says what it was checked against. These are those things, unchanged: the programs that ask a real kernel or a real shell what happens, what they wrote down, and the tests that hold each page to it. The hash of every file is in manifest.json, so a copy you hold can be compared with the one a page was checked with.
How the checks are chosen is in the method. The same list is in manifest.json for a program to read.
Goodhart
- goodhart.test.mjs The test. Every score is computed a second way and compared with scipy; the closed forms are held against an independent sweep; each quotation is held to the archived source.
- goodhart.js The model the page runs, which is also the thing under test.
Line Discipline
- line-discipline-pty.py Opens a real pseudo-terminal on Linux, writes the bytes a key sends and records what read() returns. The oracle is the kernel.
- line-discipline-pty.json The recording it wrote: every case, the kernel release, and the terminal's full settings.
- line-discipline.test.mjs The test that compares the page's engine with every recorded case, and with a second route written from POSIX's wording.
- line-discipline.js The engine the page runs.
Shell Expansion
- shell-expansion-oracle.py Runs command lines through real dash and bash and records the argument vector and descriptor table each command received.
- shell-expansion-probe.c The program that stands in for every command and writes down what it was given, including which descriptors share an open file.
- shell-expansion-pipe-atomicity.py The recording of how the shells arrange a pipeline's descriptors.
- shell-expansion-extra-oracle.py A second set of lines, drawn from a fixed seed.
- shell-expansion-oracle.json The recorded corpus, with the exact dash, bash, strace and kernel versions it was made on.
- shell-expansion-extra.json The second corpus.
- shell-expansion-pipe-atomicity.json The pipeline recording.
- shell-expansion.test.mjs The test that compares the page's predictions with every recorded line.
- shell-expansion.js The engine the page runs.
Futex
- futex-measure.c The benchmark: the three mutexes from Drepper's paper, transcribed to C.
- futex-measure.sh Builds and runs it under strace, and records the system calls.
- futex_oracle.py A second model checker, written from the C rather than from the engine, with a different search, so agreement on a state count is evidence.
- kernel.json The kernel, compiler, strace version and date the measurements were taken with.
- futex.test.mjs The test.
- futex.js The model the page runs.
- mutex-contended.json A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex-contended.strace.gz A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex-held.json A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex-held.strace.gz A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex-uncontended.json A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex-uncontended.strace.gz A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex2-contended.json A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex2-contended.strace.gz A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex2-held.json A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex2-held.strace.gz A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex2-uncontended.json A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex2-uncontended.strace.gz A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex3-contended.json A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex3-contended.strace.gz A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex3-held.json A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex3-held.strace.gz A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex3-uncontended.json A recording from the measurement: strace output or timings for one mutex under one condition.
- mutex3-uncontended.strace.gz A recording from the measurement: strace output or timings for one mutex under one condition.
Consensus
- consensus-counterexample.mjs Searches every reachable state with the current-term clause removed and writes the shortest failing run.
- consensus-counterexample.json That run as data: the thirteen steps, the bounds, the state counts under each rule, and the hash of the engine that produced it.
- consensus.test.mjs The test, which carries a second implementation of Raft written from the paper's Figure 2, with messages, and compares every reachable state.
- consensus.js The engine the page runs.
What is not here
The archived texts of the papers and standards the pages quote are not published: they are other people's work, kept here only so each quotation can be checked against what the source says. Each page links the original.
The files are published as they ran, including their paths and comments. A hash that differs from the one listed means the file you have is not the one a page was checked with.