Merge pull request #30 from iritur/iritur/e2-the-store #79

Workflow file for this run

	name: ci

	# Once per change, not twice.
	#
	# `on: [push, pull_request]` ran this entire matrix twice for every commit on a
	# branch with a pull request open — the same seven jobs, both AArch64 runners
	# and the QEMU boot included, against a tree that had not changed between them.
	# It is invisible precisely because both copies pass, and it was half of the
	# gate's time budget: E0-B07 put seventeen checks on one commit, of which seven
	# were a verbatim second copy of the other seven.
	#
	# The pull request is the gate. `main` is checked again after a merge because a
	# merge commit is a tree nobody has tested — it is the join of two trees that
	# each passed separately, which is not the same claim.
	#
	# The deliberate cost: a branch with no pull request open gets no run at all.
	# That is the trade, and it is the right way round — work that has not asked for
	# review has not asked for a runner either, and the moment it asks for one it
	# gets both.
	on:
	push:
	branches: [main]
	pull_request:

	# Every job runs in the development image, which is the same image a laptop
	# runs. `docker/README.md` states the rule: no step may exist that is not in
	# the repository, and a developer's machine is a step. With the image shared,
	# "works on my machine" and "works in CI" become one statement rather than two
	# that happen to agree — and the per-job tool installation disappears, which is
	# where a meaningful part of the ten-minute budget was going.
	#
	# The gate builds that image itself, and the first version of this did not.
	# It named a tag a separate `image.yml` published on pushes to `main`, so the
	# gate had a prerequisite that no run of the gate produced: on a tree where
	# that workflow had never fired, all ten jobs failed at "Initialize containers"
	# with `manifest unknown`, before a single step ran. That is the same rule this
	# file is quoting one paragraph up — no step exists that is not in the tree —
	# broken by the change that was citing it. A workflow somebody has to remember
	# to dispatch is institutional knowledge with a YAML file in front of it.
	#
	# So the image is a job here, and every other job waits for it.
	#
	# The tag is derived from the files that define the environment rather than
	# from the commit: `env-<hash of Dockerfile, entrypoint, toolchain pin>`. Two
	# consequences, both wanted. A commit that does not touch the environment
	# reuses the image bit for bit, so the build is a cache hit and the job is
	# short. And CI is pinned to an immutable tag rather than to `:latest`, which
	# closes the gap the previous version of this comment admitted to and deferred.
	env:
	REGISTRY: ghcr.io
	IMAGE: ${{ github.repository_owner }}/f-dev

	jobs:
	# What the environment is, as one string. Computed before anything needs it,
	# because a job's `container:` is resolved before its steps run and therefore
	# cannot depend on anything that job does.
	environment:
	name: environment tag
	runs-on: ubuntu-latest
	outputs:
	tag: ${{ steps.tag.outputs.tag }}
	image: ${{ steps.tag.outputs.image }}
	image_full: ${{ steps.tag.outputs.image_full }}
	steps:
	- uses: actions/checkout@v7
	- id: tag
	run: \|
	# Exactly the inputs the image is built from — the two files the
	# build context contains (see .dockerignore) plus the Dockerfile
	# itself. Anything else changing must not invalidate the image, or
	# every commit rebuilds it and the cache is decorative.
	hash=$(echo "${{ hashFiles('docker/Dockerfile', 'docker/entrypoint.sh', 'rust-toolchain.toml') }}" \| cut -c1-16)
	echo "tag=env-$hash" >> "$GITHUB_OUTPUT"
	echo "image=${REGISTRY}/${IMAGE}:env-$hash" >> "$GITHUB_OUTPUT"
	# Both names are computed here rather than assembled at each use.
	# `env` is not a context a job's `container:` key can read — only
	# github, needs, strategy, matrix, vars and inputs are — so anything a
	# container is named by has to arrive through `needs`.
	echo "image_full=${REGISTRY}/${IMAGE}:full-env-$hash" >> "$GITHUB_OUTPUT"
	echo "environment tag: env-$hash"

	# Two native builds rather than one emulated multi-platform build. Installing
	# a Rust nightly and a QEMU under binfmt emulation takes tens of minutes and
	# fails in ways that have nothing to do with this tree; each architecture
	# builds on its own metal and the manifest is assembled afterwards.
	#
	# On a commit that does not touch the environment this is a full cache hit and
	# costs about a minute. That minute is the price of the gate having no
	# prerequisite outside itself, and it is the right way round: a gate that is
	# a little slower is better than a gate that cannot start.
	image:
	name: environment image (${{ matrix.suffix }})
	needs: environment
	runs-on: ${{ matrix.runner }}
	permissions:
	contents: read
	packages: write
	strategy:
	fail-fast: false
	matrix:
	include:
	- runner: ubuntu-latest
	platform: linux/amd64
	suffix: amd64
	- runner: ubuntu-24.04-arm
	platform: linux/arm64
	suffix: arm64
	steps:
	- uses: actions/checkout@v7
	- uses: docker/setup-buildx-action@v3
	- uses: docker/login-action@v3
	with:
	registry: ${{ env.REGISTRY }}
	username: ${{ github.actor }}
	password: ${{ secrets.GITHUB_TOKEN }}
	- uses: docker/build-push-action@v6
	with:
	context: .
	file: docker/Dockerfile
	target: dev
	platforms: ${{ matrix.platform }}
	push: true
	tags: ${{ env.REGISTRY }}/${{ env.IMAGE }}:${{ needs.environment.outputs.tag }}-${{ matrix.suffix }}
	cache-from: type=gha,scope=dev-${{ matrix.suffix }}
	cache-to: type=gha,mode=max,scope=dev-${{ matrix.suffix }}
	# `full` adds cargo-deny, which the dependency-policy job needs at the
	# version docker/Dockerfile pins rather than the version an action chose.
	- uses: docker/build-push-action@v6
	with:
	context: .
	file: docker/Dockerfile
	target: full
	platforms: ${{ matrix.platform }}
	push: true
	tags: ${{ env.REGISTRY }}/${{ env.IMAGE }}:full-${{ needs.environment.outputs.tag }}-${{ matrix.suffix }}
	cache-from: type=gha,scope=full-${{ matrix.suffix }}
	cache-to: type=gha,mode=max,scope=full-${{ matrix.suffix }}

	# One name per image, pointing at both architectures. The AArch64 jobs and the
	# x86-64 ones then name the same tag, which is what stops the two from quietly
	# becoming two environments with one name — the worst possible state for a
	# pair of jobs whose whole purpose is to disagree with each other.
	manifest:
	name: environment manifest
	needs: [environment, image]
	runs-on: ubuntu-latest
	permissions:
	packages: write
	steps:
	- uses: docker/login-action@v3
	with:
	registry: ${{ env.REGISTRY }}
	username: ${{ github.actor }}
	password: ${{ secrets.GITHUB_TOKEN }}
	- name: assemble
	run: \|
	base="${REGISTRY}/${IMAGE}"
	tag="${{ needs.environment.outputs.tag }}"
	docker buildx imagetools create --tag "$base:$tag" \
	"$base:$tag-amd64" "$base:$tag-arm64"
	docker buildx imagetools create --tag "$base:full-$tag" \
	"$base:full-$tag-amd64" "$base:full-$tag-arm64"
	echo "environment published as $base:$tag"
	policy:
	name: policy checks
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	# Each of these encodes an architectural decision. A failure names the
	# RFC it comes from.
	- run: cargo xtask lint-determinism
	- run: cargo xtask lint-licensing
	- run: cargo xtask lint-unsafe
	- run: cargo xtask lint-percpu
	- run: cargo xtask lint-mutations
	# The three rules from docs/what-must-be-stated.html section 15 that
	# could be made executable. CONTRIBUTING.md carries all twelve and says
	# which is which: a rule listed as mechanised that is not is worse than
	# one honestly listed as review, because it is a check somebody believes
	# is happening.
	- run: cargo xtask lint-claims
	- run: cargo xtask lint-units
	- run: cargo xtask lint-callbacks
	- run: cargo xtask lint-claim-owners
	# Formatting and clippy, by calling the definition rather than restating
	# it. This was `cargo fmt --all -- --check` and
	# `cargo clippy --workspace --all-targets` written out here, which is one
	# invocation over one graph — so `f-kernel` was checked for the host, in a
	# feature unification that turned on `image` for three driver crates
	# declared `default-features = false` to keep it off, and the gate went red
	# on a duplicate `panic_impl` while the local loop stayed green. `lint_all`
	# had the two-world split all along; this copy of it did not.
	- run: cargo xtask lint-style
	# The hooks in .claude/ are policy too, and they are the only policy that
	# applies without being read. A hook that has stopped firing is
	# indistinguishable from a hook with nothing to complain about, so it is
	# checked here rather than noticed later.
	- run: bash .claude/hooks/selftest.sh
	# E1-P11. Every crate that reaches the machine, compiled for
	# `aarch64-unknown-none`, with the crate list derived from the workspace
	# rather than written beside it — and every exclusion printed with the
	# reason and the reversal it carries. It is here rather than only in
	# `cargo xtask verify` because `docs/test-taxonomy.md`'s
	# `aarch64-compile` row claims the `every PR` cadence, and until this
	# step existed nothing on a pull request ran it: the arm job built four
	# crates and `f-store` and `f-virtio-blk` were compiled for AArch64 by
	# nothing at all. A cadence claimed by a row and kept by nobody is worse
	# than a row that admits it runs on no cadence. RFC 0045.
	- run: cargo xtask cross
	# E1-P11's second half, and the one `cross` above cannot answer. That step
	# says every crate is compiled for AArch64; this says no test inside one
	# of them is compiled on only one architecture. The two are different
	# questions and the second is the quieter one: a crate on both runners
	# with a `#[cfg(target_arch)]` test inside it leaves `test-host` green on
	# both while the arm runner collects fewer tests, and a smaller test count
	# is not a failure anybody reads. The allow-list is empty today, which is
	# the finding rather than the default.
	#
	# Three gate shapes are refused: an item `cfg`, a block `cfg`, and a
	# file-scope `#![cfg(target_arch = ...)]`. The third is the one this step
	# was green over in review, and it is the one that matters most rather
	# than least — an integration test under `tests/` is named by no `mod`
	# declaration anywhere, so a file-scope attribute is the only gate it can
	# carry, and `ring/tests/litmus.rs` is one of those files. RFC 0045.
	- run: cargo xtask lint-arch-tests
	# E1-P07. `kernel/proofs` compiles `kernel/src/cap.rs` a second time, so
	# that file now has a second set of module dependencies it must keep
	# satisfying — and the crate is outside the workspace, so `cargo xtask
	# test`, the `clippy --workspace` above and the `fmt --all` above all
	# miss it. Without this step the only thing that notices a broken
	# stand-in is the nightly `prove` job, twenty minutes long and hours
	# after the person who wrote the line has gone. It needs no Kani: the
	# harnesses are behind `cfg(kani)`, so this is `cap.rs` and three short
	# files under the pinned toolchain, in the three feature configurations
	# `prove` uses. It also re-checks that nightly.yml still says what
	# E1-P07's exit rests on, which is the only half of runs on a schedule
	# a machine in this repository can decide. RFC 0053.
	- run: cargo xtask lint-proofs

	# The same suite on both architectures, and the same command on both, which
	# is the part that was missing.
	#
	# These two jobs named four crates each while `cargo xtask test` ran the whole
	# workspace. So `f-store`, `f-virtio-blk`, `f-sim`, `f-bench` and `xtask` had
	# tests that ran on a laptop and on no runner — and two of those crates were
	# never compiled on the arm runner, which is the failure `xtask`'s own
	# comment already records happening once with `f-bench` and `f-init`. One
	# command, derived from `Cargo.toml`'s members, is what stops two lists from
	# drifting: there is one list now, and a crate added to the workspace joins it
	# or fails the build saying why. RFC 0045.
	test-x86:
	name: tests (x86-64, total store order)
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	# The control, and not a redundancy: it is what says a red arm run below
	# is about the architecture rather than about the test.
	- run: cargo xtask test-host

	test-aarch64:
	name: tests (AArch64, weak memory)
	needs: [environment, manifest]
	runs-on: ubuntu-24.04-arm
	# The arm64 half of the same multi-architecture tag. Naming one tag on both
	# runners is what stops the two jobs from drifting into two environments
	# with one name — which would be the worst possible state for the job whose
	# entire purpose is to disagree with the other one.
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	# This job is not a portability nicety. x86-64 total-store-order hides
	# the entire class of ordering bug the ring is exposed to, so this is the
	# only configuration in which the ring tests mean anything.
	#
	# `ubuntu-24.04-arm` is a native AArch64 runner rather than emulation, and
	# that distinction is load-bearing rather than pedantic: a store buffer is
	# what this job exists to observe, and QEMU's TCG serialises rather than
	# reordering, so an emulated run would be green whatever the ordering
	# said. E1-P11's title says "under emulation"; the honest answer is that
	# emulation would be the weaker check and this runner is the stronger one.
	# The development container could not stand in for it even if TCG did
	# reorder. It carries `qemu-system-aarch64`, which is the thing a reader
	# checking this comment will find and wonder about — but a full-system
	# emulator needs a frame to boot and the frame is x86-64. What would be
	# needed is a hosted AArch64 binary, and there is no `qemu-user` in the
	# image, nothing registered in `binfmt_misc`, and no
	# `aarch64-unknown-linux-gnu` in the installed target list to build one
	# for. So the container compiles for this architecture and cannot run for
	# it, and this job — not a local command — is what runs. RFC 0045.
	#
	# E0-P09's seeded fault injection — `cargo test -p f-ring --test faults`
	# — used to be a second step here. It is not weakened by being gone: the
	# workspace run above includes every one of `f-ring`'s test targets, that
	# one included, on this runner as well as x86-64.
	- run: cargo xtask test-host

	# Both architectures, both non-advisory, and that is the whole of E0-P07.
	#
	# The AArch64 half is where the ordering means anything: total store order on
	# x86-64 hides the entire class of bug the ring is exposed to, so a Relaxed
	# store that corrupts data on ARM passes every one of these tests on an x86
	# laptop. Neither job carries `continue-on-error`, and neither may: an
	# advisory job that goes red is a job that gets ignored on the second Tuesday,
	# and this one exists to be believed.
	#
	# The x86-64 half is not redundant. It is the control — it is what says a
	# failure on the arm runner is about the architecture rather than about the
	# test — and it runs `--release` for the reason the arm job does: optimisation
	# changes what a stress test explores, and the ordering these guard is exactly
	# what an optimiser is entitled to move.
	litmus:
	name: memory-ordering litmus (${{ matrix.arch }})
	needs: [environment, manifest]
	runs-on: ${{ matrix.runner }}
	container: ${{ needs.environment.outputs.image }}
	strategy:
	# Both results, always. `fail-fast` would cancel the AArch64 job the
	# moment x86-64 went red, which throws away the one number that
	# distinguishes "the ring is broken" from "the ring is broken on weak
	# memory" — and those are different bugs with different fixes.
	fail-fast: false
	matrix:
	include:
	- arch: x86-64, total store order
	runner: ubuntu-latest
	# Whether this machine actually performs the store-load reordering
	# the doorbell defect below depends on. x86-64 does; AArch64's
	# `stlr`/`ldar` forbid it. See that step.
	store_load: true
	- arch: AArch64, weak memory
	runner: ubuntu-24.04-arm
	store_load: false
	steps:
	- uses: actions/checkout@v7
	# These are stress tests, not a model check. RustMC lands at M5 and is
	# what actually explores what RC11 permits. Until then these two jobs plus
	# the AArch64 unit tests are the coverage, and the gap is real.
	- run: cargo test -p f-ring --test litmus --release

	# `mutate-relaxed-submission` and `mutate-relaxed-completion` are NOT run
	# here, and the reason is a result rather than an omission.
	#
	# They were, for one run. The step required the suite to fail with the
	# publishing store weakened from `Release` to `Relaxed`, on the arm runner
	# where that weakening is a real defect — the both-halves standard
	# `mutate` and E0-P02 already meet. The suite passed. Not once by
	# chance: the whole point of putting it on the weak-memory runner was that
	# this is the machine where it should be caught, and it was not.
	#
	# That is this file's own stated limit, arriving as evidence. `litmus.rs`
	# says it in its first paragraph — these are stress tests, they sample
	# what one machine happened to do, and they will not reliably catch a rare
	# interleaving. A gate asserting that a probabilistic test catches a
	# specific reordering is a gate that goes red on a Tuesday for reasons
	# nobody can reproduce, which is exactly the shape of check this repository
	# refuses to ship.
	#
	# The features stay. `lint-mutations` keeps them off by default, they run
	# by hand, and they are the fixture `E0-P16` needs: that task's exit names
	# this exact weakening as what a model checker must catch, and the
	# honest reading of this run is that nothing short of one will.
	#
	# The doorbell fence below is different and is still a gate — but on the
	# other runner, which is the part nobody would have guessed.

	# The doorbell fence, on x86-64 only, and the asymmetry is the whole
	# lesson of this job.
	#
	# Every other defect in this file needs the arm runner because total store
	# order hides it. This one is the exact inverse: it needs the x86 runner,
	# because store-load is the one reordering total store order performs, and
	# it is the one AArch64 forbids. `Release` and `Acquire` compile to plain
	# `mov` on x86-64 — nothing stops the producer's load of `flags` being
	# satisfied out of the store buffer ahead of its store to `head` — and to
	# `stlr` and `ldar` on AArch64, which are RCsc: a Store-Release followed by
	# a Load-Acquire is ordered by the architecture, so the fence RFC 0020 adds
	# is redundant there and removing it changes nothing observable.
	#
	# That is not reasoning applied after the fact. It ran on both: 58 971 lost
	# wakeups in 500 000 rounds on x86-64, and a clean pass on the arm runner
	# with the fence removed. The architecture manual is why the result
	# generalises; the run is the evidence.
	#
	# So which runner catches which defect is a property of the reordering,
	# not of the defect's severity — and a gate placed on the wrong runner goes
	# red for a reason that has nothing to do with the code.
	- if: matrix.store_load
	run: \|
	if cargo test -p f-ring --test litmus --release --features f-ring/mutate-no-doorbell-fence; then
	echo "The litmus suite passed on x86-64 with the StoreLoad fence removed"
	echo "from ring::Producer::doorbell_wanted. This is the one machine that"
	echo "performs the reordering, so the harness is the first suspect: a"
	echo "std::sync::Barrier in place of the spin barrier lines the two threads"
	echo "up microseconds apart, and the window is one store buffer deep."
	echo "Failing that, suppression no longer runs Dekker's algorithm. RFC 0020."
	exit 1
	fi

	coverage:
	name: coverage instrumentation
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	# Prints a line per crate and a total, and writes summary.json beside the
	# profiles. Nothing here gates: a coverage threshold rewards tests written
	# to touch lines rather than to catch anything, so the number is published
	# and watched instead. What gates is in claims/.
	- run: cargo xtask coverage
	# Kept with the run rather than only printed into a log that ages out, so
	# that "coverage fell" is a question anyone can answer from two artifacts
	# rather than from memory. E0-P11 is what turns this into a history.
	- uses: actions/upload-artifact@v4
	if: always()
	with:
	name: coverage-summary
	path: target/coverage/summary.json
	if-no-files-found: error

	# E0-P11. Only on main, and only after a merge — never on a branch.
	#
	# A history every branch appends to conflicts on every rebase (both sides
	# added a line at the end of one file) and, worse, a rebase rewrites the
	# commits those lines name, so the surviving history refers to objects
	# nobody has. Appending only from a commit that is already permanent is
	# what makes the file survive a rebase: a branch never had a line in it to
	# conflict over.
	#
	# The record is uploaded rather than pushed back. Committing to the
	# repository from CI is a decision about who may write to main, and it is
	# not one a workflow file should make on the project's behalf — see
	# TODO.md E0-P11.
	- if: github.ref == 'refs/heads/main' && github.event_name == 'push'
	run: cargo xtask history append
	- uses: actions/upload-artifact@v4
	if: github.ref == 'refs/heads/main' && github.event_name == 'push'
	with:
	name: measurement-history
	path: claims/history.jsonl
	if-no-files-found: error

	kernel:
	name: kernel boots
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	# QEMU arrives with the image. This job used to install it per run, which
	# is the per-job tool installation E0-P14 exists to delete: an emulator
	# whose version nobody chose, resolved fresh on every boot of the gate.
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	- run: cargo xtask run
	# The same image on a machine with a gibibyte in it. The boot above is
	# pinned at 128 MiB because its log is the artefact the determinism job
	# hashes, and 128 MiB cannot hold the largest block the allocator admits
	# — so the top of the buddy structure is reachable by no other check
	# here, and would regress with every one of them still green.
	- run: cargo xtask orders
	# The negative half, and the reason it is in the gate rather than in
	# somebody's habits: seven boots, each one a process deliberately doing
	# something it is not permitted to do. A protection nothing tries to
	# violate is a protection nobody has checked, and these are the only
	# checks in the suite that fail if isolation quietly stops holding.
	- run: cargo xtask user
	# The same argument one milestone up. Seven more boots, each one a
	# process trying to hold authority it was not granted: naming a slot it
	# was never given, forging a handle, using a revoked one, exceeding the
	# rights it has, and filling the table to see what happens at the bound.
	# This is the M4 negative suite — E0-P08 — and it belongs in the gate for
	# the reason `docs/the-long-plan.html` gives when it says authority
	# escapes are caught every build. Eight since E0-B10, the eighth being the
	# one the frame does not refuse at all: the process revokes a capability
	# it is entitled to revoke and then reads the page that revoke unmapped.
	- run: cargo xtask cap
	# The same argument for the bus, which is the one place the two above
	# cannot reach: every protection they check is a protection against the
	# processor addressing memory it should not, and a device is not the
	# processor. Two boots — a real virtio block device performing a real
	# transfer into a buffer its IOMMU domain translates, which must land, and
	# then into one it does not, which must be refused and recorded in the
	# remapping unit's fault registers. E1-B01. Neither half means anything
	# alone: the first is the control that says the device was started at all.
	- run: cargo xtask iommu
	# The same outcomes one layer up, with the descriptor written by a driver
	# component rather than by the frame's own adversary: `user/virtio-blk`
	# builds it out of a `Reach` the frame answered its client's registration
	# with. Three more boots. One carries a sector out and back through a ring
	# byte for byte with nothing copied. One withdraws the client's page from
	# the driver's domain between the write and the read, which is RFC 0024's
	# reclaim and is the frame's property. One takes nothing away and has
	# the driver add to the address it was answered before writing it into a
	# descriptor, which is the component's own arithmetic and is the only one
	# of the three that is `a driver reaching outside its grant`; the unit must
	# fault it at the address the driver invented. E1-B02, and it is here
	# rather than in somebody's habits for the reason `docs/test-taxonomy.md`
	# gives: the `iommu-escape` row claims the `every PR` cadence for all four
	# halves, and a cadence claimed by a row and kept by nobody is worse than
	# a row that admits it runs on no cadence at all.
	- run: cargo xtask blk
	# The second driver, which is what says the first one's shape is a
	# shape rather than a coincidence. Three more boots of a network datapath:
	# `inside` posts a receive buffer, transmits a hand-formed
	# address-resolution request and requires the reply to land in the
	# registered buffer carrying the hardware address this boot invented, which
	# the host's backend could not have produced without the request. `silent`
	# is the identical client with the transmit removed and requires nothing to
	# arrive — without it, a frame arrived is satisfied by any link with
	# traffic on it. `escape` applies the displacement to the receive
	# descriptor, so what the remapping unit must refuse is a device writing
	# into memory the component never held, at a moment nothing chose. E1-B03,
	# RFC 0051, which also records what the frame turned out to owe a second
	# driver.
	- run: cargo xtask net
	# The third driver, and the first device that is not a pipe. Three
	# boots of a display datapath: `inside` fills one buffer of a registered
	# set with a pattern, submits one entry, and the driver turns it into six
	# display commands that put the client's pixels on scanout zero — and this
	# job then captures the emulator's own framebuffer over the monitor socket
	# and requires it to hold those pixels. That capture is the reason this
	# line is not like the two above it: a scanout has no read-back command in
	# the 2D protocol, so nothing inside the machine can observe what is on the
	# screen, and the kernel's own verdict stops at the commands the display
	# accepted. `blank` is the identical client with the submission removed —
	# the pixels are in guest memory for the whole boot and must not reach the
	# display — and `escape` points the device one page past what the
	# registration answered at the memory a display reads, which the
	# remapping unit must fault on a read while the screen shows none of the
	# client's bytes.
	#
	# It needs nothing this job does not already have: the emulator's monitor
	# is a loopback socket this harness opens itself, and the machine is the
	# same one every other boot here runs on with `-vga none` so that there is
	# exactly one display in it. E1-B04, RFC 0054, which records what the frame
	# turned out to owe a third driver and why the harness is part of the check.
	- run: cargo xtask gpu
	# The same datapath, asked an ordering rather than an isolation question.
	# Three more boots of one client script: six batch reads are queued, a
	# hard-class read carrying a deadline arrives last, and the driver hands
	# the device what `f_abi::deadline::inherit` ranked first. `ordered`
	# requires the read back at position zero, having overtaken six;
	# `arrival` is the control and requires it back last, because an overtake
	# with nothing beside it is an array that came out conveniently; and
	# `unadmitted` requires a client that does not hold the hard class to be
	# refused it rather than served at it. The overtake is counted on both
	# sides of the privilege boundary and the two must agree. E1-B06, RFC
	# 0049, and `claims/0012` gates on the count.
	- run: cargo xtask deadline
	# What it costs to undo the isolation the two jobs above prove. One boot
	# retires forty registered buffer sets — thirty-two register-and-retire
	# cycles, then a driver restart's whole grant in one pass — under each of
	# the two invalidation policies, and the host workload beside it drives
	# the identical registry churn while `f_bench::Environment` declines to
	# publish a time. The counts are what gate: one global invalidation per
	# unmap request rather than one per page, and zero shootdowns and zero
	# interrupts from the churn against a boot whose running total is one —
	# which is what makes the zero a property of the datapath rather than of
	# a counter nobody wired up. The boot also reads the unit's own tables
	# back after every retirement — nothing may still be translated, and
	# everything must have been while it was registered — walks the free
	# count either side of the whole thing, and makes the one request shape
	# no client can produce: a set with a page taken out from under it, which
	# one batched request must clear either side of. And it times a thousand
	# and twenty-four unmap requests through the shipped path, which on this
	# runner is recorded and refused rather than published: `F_ENVIRONMENT`
	# is not a measurement class here, so `cargo xtask churn` requires the
	# refusal to appear. E1-B14, RFC 0052, and `claims/0014` gates on the
	# counts while `claims/0015` waits on a machine.
	- run: cargo xtask churn
	# The scheduler, and the one exit on this list that is an absence. Four
	# boots. A component holds a core, adopts its control ring and its own
	# work ring in safe code — `f_ring::adopt`, RFC 0037 — and puts sixteen
	# thousand work items through its own executor; the frame counts every
	# crossing into itself and requires the hot-path count to be zero. The
	# second boot makes one crossing on purpose and requires the count to move
	# by exactly as many, so a build that had stopped counting fails rather
	# than looks clean. The third posts a reclaim from the timer handler once
	# a quarter of the load is done and requires the runtime to park within
	# one quantum with its own queue empty — an interrupt happened and a
	# preemption did not. The fourth scribbles the control ring's header
	# before entry and requires the adoption to refuse rather than believe it.
	# E1-B08, RFC 0038.
	- run: cargo xtask runtime
	# The other half of E0-P08, and the half that says the suite can fail. A
	# kernel built with one deliberate defect, booted into the forging sweep,
	# required to go red with a panic in the log — and then the same boot
	# without the defect, required to go green. Four of the five properties
	# have a fixture that breaks them and runs at every boot; the fifth cannot
	# have one, because a fixture that panics takes the machine down rather
	# than being caught. RFC 0017 argues it.
	- run: cargo xtask mutate
	# The reporting channel itself, which every job above depends on and none
	# of them checks. Three endings have to reach CI as three different
	# things: a clean boot (33), a panic (37), and a boot that never finishes
	# — which the kernel cannot report on its own behalf, so the harness has
	# to be the one that notices. Before this, a hung kernel presented as a
	# job that timed out somewhere during "build", with no log and no clue.
	- run: cargo xtask panic

	# E0-P02. Two runs of the same (seed, commit) on two different runners must
	# produce one trace hash.
	#
	# Two jobs and not a loop in one job, because the claim is about two machines.
	# A pair of boots on one runner is the weaker half and `cargo xtask trace`
	# already does it locally; what a second runner adds is everything a machine
	# can differ in — core count, host load, kernel version, CPU model — and those
	# are exactly the things a boot must not be reading.
	#
	# This job only became possible when every job started running in the same
	# image (E0-P14). Before that the two runners could have had different QEMU
	# versions, and QEMU's version is in the boot log: the check would have failed
	# for a reason that has nothing to do with the kernel, which is the way a
	# gate gets disabled.
	trace:
	name: execution trace (runner ${{ matrix.runner_id }})
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	strategy:
	fail-fast: false
	matrix:
	runner_id: [a, b]
	steps:
	- uses: actions/checkout@v7
	- run: cargo xtask trace --hash \| tee trace-${{ matrix.runner_id }}.txt
	- uses: actions/upload-artifact@v4
	with:
	name: trace-${{ matrix.runner_id }}
	path: trace-${{ matrix.runner_id }}.txt
	if-no-files-found: error

	reproduction:
	name: the reproduction check
	needs: [manifest, environment, trace]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	- uses: actions/download-artifact@v4
	with:
	pattern: trace-*
	merge-multiple: true
	- name: the two runners must agree
	run: \|
	a=$(cat trace-a.txt)
	b=$(cat trace-b.txt)
	echo "runner a $a"
	echo "runner b $b"
	if [ "$a" != "$b" ]; then
	echo
	echo "Two runners produced different traces for one commit."
	echo
	echo "This is the determinism contract failing, and it is the failure"
	echo "every other layer of the test apparatus rests on: a seed stops"
	echo "being a bug report, the simulator stops reproducing, and a claim"
	echo "stops being re-derivable. Something on the boot path is reading a"
	echo "clock, a counter or an address the seeded Env does not own."
	echo "RFC 0004."
	exit 1
	fi
	echo "agreed: $a"
	# The other half of the exit, and the half that says this job can fail:
	# the same command with one unseeded read of time on the boot path, which
	# must make two runs disagree. Without it, a trace hashed over something
	# that never varies would agree with itself forever and this gate would
	# be green for the wrong reason.
	- run: cargo xtask trace

	# The workload's half of the same question the `trace` job asks about a boot,
	# and the same shape of answer: one command, one hash, two runners, a third
	# job comparing the lines. RFC 0032 argues why there are two checks rather
	# than one — the frame's instructions run in QEMU and the components run in
	# the simulator — and RFC 0035 is what makes the pair a claim about one
	# component set rather than two commands in one paragraph.
	#
	# `deployment` and not `contention`, because `deployment` is the scenario
	# whose component set is read from the compiled manifest records this commit
	# builds. It is therefore the one scenario whose hash moves when a manifest or
	# a driver image moves, which is what makes the `commit` half of
	# `(seed, commit)` mechanical rather than a promise.
	#
	# What this job compares is the digest, not the bytes. Two runners cannot
	# hand each other an artefact as cheaply as they can hand each other a line,
	# and `sim/src/trace.rs` is honest that its 64-bit FNV-1a is not a
	# collision-resistant hash. So the exit criterion's word byte-identically is
	# answered elsewhere and deliberately: `cargo xtask sim`, below, compares the
	# whole `deployment` artefact between two processes, and `f-sim`'s own tests
	# compare it in process. Nobody should quote this job as the byte-level
	# evidence; it is the cross-machine one.
	simulation:
	name: simulated workload (runner ${{ matrix.runner_id }})
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	strategy:
	fail-fast: false
	matrix:
	runner_id: [a, b]
	steps:
	- uses: actions/checkout@v7
	- run: cargo xtask sim --hash deployment \| tee sim-${{ matrix.runner_id }}.txt
	- uses: actions/upload-artifact@v4
	with:
	name: sim-${{ matrix.runner_id }}
	path: sim-${{ matrix.runner_id }}.txt
	if-no-files-found: error

	workload:
	name: the workload reproduction check
	needs: [manifest, environment, simulation]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	- uses: actions/download-artifact@v4
	with:
	pattern: sim-*
	merge-multiple: true
	- name: the two runners must agree
	run: \|
	a=$(cat sim-a.txt)
	b=$(cat sim-b.txt)
	echo "runner a $a"
	echo "runner b $b"
	if [ "$a" != "$b" ]; then
	echo
	echo "Two runners produced different simulated runs for one commit."
	echo
	echo "This is the determinism contract failing above the frame, and"
	echo "every layer that reads a simulated run rests on it: a seed stops"
	echo "being a bug report, a sweep stops shrinking, and a snapshot stops"
	echo "re-entering. Something in the model is reading a clock, an address"
	echo "or an iteration order the seed does not own — or the two runners"
	echo "built different component files, which is the same failure one"
	echo "layer down. RFC 0004, RFC 0032."
	exit 1
	fi
	echo "agreed: $a"
	# The half that says this job can fail. A digest taken over something that
	# does not vary agrees with itself forever, so every scenario is also run
	# at a second seed and required to disagree. The boot's equivalent needs a
	# deliberately broken build because a boot takes no seed on its command
	# line; a simulated run does, which is the one place this half of the
	# apparatus has the better of the other.
	- run: cargo xtask sim
	# And the seam. The boot spawns components from compiled manifest records
	# and prints each one's content hash; this requires the set the simulator
	# ran and the set the boot spawned to differ by exactly the gap `xtask`
	# declares — in both directions, because a one-directional check passes
	# while the simulator drives components the kernel never instantiated.
	# Without it `boot-to-workload` is two commands that share a directory
	# name, and a shared directory name is not evidence. RFC 0035, RFC 0036.
	- run: cargo xtask sim --join
	# And the seed corpus: every trial a sweep has ever found something with,
	# required to be clean now. Seconds, because the corpus is minimised
	# trials rather than whole scenarios — the million-trial sweep is
	# nightly.yml's, and this is the part of it that belongs on every change.
	# RFC 0040.
	- run: cargo xtask sweep --corpus
	# Gate G1's first sentence, and the one claim in this epoch that gates on
	# the machine that produces it: every metric it takes is a count from a
	# virtual clock, so a container is as good as bare metal for it and there
	# is nothing to wait for. `claims/0005` says `status = "gating"`, and a
	# gating claim no job runs gates nothing. The latency half is
	# `claims/0006` and is `pending` on E0-D10's machine — split rather than
	# weakened. RFC 0041.
	- run: cargo xtask chaos
	# E1-P08. A run that goes wrong in simulated minute forty, re-entered at
	# minute thirty-nine from a snapshot written while the run passed it, with
	# both wall-clock numbers printed and the ratio gated against a floor. It
	# is here rather than only in `verify` because `claims/0007` records that
	# ratio, and a claim whose reproduction no job runs is a claim that
	# reproduces on one person's afternoon. Twelve seconds warm, most of it two
	# release builds of `f-sim` — one with the deliberate defect that gives the
	# run something to fail at and one without, because the pair is also what
	# shows a snapshot from another build being refused. RFC 0043.
	- run: cargo xtask snapshot

	# E1-P04. Its own job rather than a step in `workload`, because the two halves
	# of it differ by six orders of magnitude and putting them in one job would
	# make a forty-five-second Miri run wait behind a forty-five-second fuzzing
	# run for no reason.
	#
	# Three commands, three properties, three counts — and the counts are in
	# `claims/0008-hostile-peer-operations.toml` rather than here, because a
	# number in a workflow file is a second copy of a number in a claim and the
	# two drift. `--exit` is the exit criterion's own billion by name; the local
	# `verify` runs a hundred million, which is stated there too. RFC 0046.
	hostile:
	name: the hostile peer
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	# First, and the sweep's `harness` job is the precedent: a night where the
	# fuzzer has broken should report the fuzzer is broken rather than
	# report a clean billion nobody should believe. Two defects, one per
	# property this half can see, each required to be found by the property it
	# breaks — and the third required to be invisible here, which is the whole
	# argument for the Miri step below.
	- run: cargo xtask hostile --mutate
	# E1-P04's own number: one billion hostile operations, no panic, no hang.
	# It is `exit_operations` in the claim, and this run refuses to call itself
	# the exit if it performed fewer — so the registry carries the number this
	# step reaches rather than mentioning it.
	# 44 to 60 s on the four-core development container and of the order of twice that on
	# a two-core runner, which is why it is a job of its own and not a step in
	# `verify`.
	- run: cargo xtask hostile --exit
	# And the corpus: every run that has ever found something, required to be
	# clean now. Seconds, because a corpus entry is one episode.
	- run: cargo xtask hostile --corpus

	# E1-P05, and a job of its own for the reason the one above is: the fuzzing
	# half is seconds and the coverage half rebuilds three crates with
	# instrumentation and with link-time optimisation off, which is a second
	# compile of the whole dependency chain. Putting them together would make a
	# two-and-a-half-second gate wait behind a forty-second build.
	#
	# The counts and the floor are in `claims/0009-entry-validation-coverage.toml`
	# rather than here, for the reason the hostile job gives: a number in a
	# workflow file is a second copy of a number in a claim, and the two drift.
	# RFC 0048.
	entries:
	name: the entry fuzzer and its coverage
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	# First, and the hostile job's reason: a run where the oracles have
	# broken should report that rather than report a clean quarter of a million
	# cases nobody should believe. Three defects, one per oracle, each required
	# to be found by the oracle it breaks and by no other.
	- run: cargo xtask entries --mutate
	# The gate: 262 144 generated cases, every family drawn, every refusal
	# earned, and the thirty-seven reach minimums the claim names.
	- run: cargo xtask entries
	# The corpus, replayed: every entry required to be clean now.
	- run: cargo xtask entries --corpus
	# And the number E1-P05's exit is about, measured from that corpus alone.
	# It is `path_line_coverage` in the claim and this step refuses a figure
	# below it, naming the members that fell short.
	- run: cargo xtask entries --coverage
	# Kept with the run for the same reason the coverage job keeps its summary:
	# the number fell is a question anyone can answer from two artifacts and
	# nobody can answer from one.
	- uses: actions/upload-artifact@v4
	if: always()
	with:
	name: entry-corpus
	path: ring/entries-corpus.txt

	# The third property, and the only one no assertion inside the program can
	# make. Its own job because Miri costs about six orders of magnitude: four
	# thousand operations here against a billion above, and reporting both numbers
	# rather than one is the first thing RFC 0046 decides.
	#
	# `MIRI_GAP` is declared there and not here: `f_ring::adopt` carries a channel
	# base as a `u64` — RFC 0037's design — so Miri's aliasing discipline on that
	# one path is weakened to permissive provenance while the `Mapping::adopt`
	# path, which is where the reads a hostile peer aims at actually happen, is
	# checked in full.
	miri:
	name: the ring under Miri
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	# The harness first, for the job above's reason. It arms the one defect
	# that is invisible to everything except this tool and requires Miri to
	# report undefined behaviour by name, then disarms it and requires quiet.
	- run: cargo xtask hostile --miri --mutate
	- run: cargo xtask hostile --miri

	# The fourth thing the gate was always supposed to run, and the one that was
	# missing: lint, test, run — and claims.
	#
	# What this job can assert today is everything about the registry except a
	# number. Every claim names an owner that exists (R09), every document
	# citation matches the value the claim holds, the snapshot regenerates without
	# a diff, and the release manifest still resolves. What it cannot assert is
	# that a gating claim holds, because no claim gates yet: 0001 and 0002 are
	# `pending` on a measurement environment that does not exist, and 0003 is
	# `tracked` on purpose. That is E0-P05 and E0-P06, and it is the reason
	# E0-P01's exit is only half met.
	claims:
	name: claims registry
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/checkout@v7
	# First, and before anything regenerates it. The committed snapshot is a
	# claim about the registry, and `xtask claims` below rewrites the file by
	# design — so a freshness check placed after it grades its own homework.
	#
	# This was a `git diff --quiet` here in the YAML, which is how it came to
	# fail on a byte-identical file: git refuses a working tree owned by
	# another uid, and `git diff` renders that refusal as "Not a git
	# repository" rather than as a refusal. The comparison now happens in
	# xtask, where it needs no repository and where a developer can run it.
	- run: cargo xtask lint-snapshot
	- run: cargo xtask claims
	- run: cargo xtask lint-claim-owners
	- run: cargo xtask lint-claims
	- run: cargo xtask release --dry-run
	# The package, built twice on this runner. It is the weaker half of
	# E0-R01's exit and the comment in `--twice` says so: directory order,
	# uid, path and clock are all constant within one machine, so agreeing
	# here says little about two machines agreeing. What it does catch is the
	# one same-machine difference — a `read_dir` order that reached the
	# archive — and it costs one kernel build.
	#
	# The two-machine half is the `package` job below. This step stays,
	# because when that one goes red this is what says which kind of red:
	# agreeing here and disagreeing there is a difference between machines,
	# and disagreeing in both places is one this machine can reproduce. Same
	# argument as the x86-64 litmus job being the control for the arm one.
	- run: cargo xtask release --twice

	# E0-R01's other half: two runners at one commit must produce one content
	# address. `release --twice` above is the same-machine half and says in its
	# own output why that is the weaker question.
	#
	# Two jobs and not two builds in one, for the reason the trace pair is two
	# jobs: the claim is about two machines, and the things a machine can differ
	# in — core count, host load, filesystem, `read_dir` order — are exactly the
	# things a content address must not be reading.
	#
	# This needs both runners to check out at the same absolute path, and that is
	# measured rather than assumed. The same tree at `/work` and at `/elsewhere`,
	# same image, same commit, packages to two different addresses:
	#
	# /work e544abc2009007758433d33c51e00650190b045d060f09677be29c4be76cbc13
	# /elsewhere 91189800d63270033f6160ab4b0c0b2290a4ea67149edec9399e17f3c98b611a
	#
	# Both are from one tree state and neither can be re-derived later, because
	# this comment is inside the source archive the address is taken over: writing
	# the number changed it. That is a property of recording an address in the
	# tree it addresses, and it is why these two are evidence of a difference
	# rather than constants to check against.
	#
	# The kernel image is a debug build, so its DWARF carries the path it was
	# built at and cargo's -Cmetadata derives from a package id containing it.
	# A container job's workspace is `/__w/<repo>/<repo>`, fixed by the runner
	# rather than chosen here, so the precondition holds by construction — and the
	# comparison below checks it anyway, because a precondition that holds by
	# construction is one nobody notices stopping.
	#
	# `CARGO_TARGET_DIR` is not one of the paths that matters, and that was
	# measured too: the same source path with the target directory moved to
	# `/tmp/t` gives the same address. Worth knowing before someone relocates the
	# target directory for caching and expects this job to care.
	package:
	name: package address (runner ${{ matrix.runner_id }})
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	strategy:
	fail-fast: false
	matrix:
	runner_id: [a, b]
	steps:
	- uses: actions/checkout@v7
	# Two lines: the address, then where it was built. The path is the one
	# known confounder, so the comparison needs it to tell "the package is not
	# hermetic" from "these two ran in different places" — different findings,
	# different fixes, and only one of them is about this repository.
	- name: package this commit, and record where it was built
	run: \|
	cargo xtask release --address > package-${{ matrix.runner_id }}.txt
	pwd >> package-${{ matrix.runner_id }}.txt
	cat package-${{ matrix.runner_id }}.txt
	- uses: actions/upload-artifact@v4
	with:
	name: package-${{ matrix.runner_id }}
	path: package-${{ matrix.runner_id }}.txt
	if-no-files-found: error

	# No checkout: this job compares two text files and needs nothing from the
	# tree. A checkout that nothing reads is a step whose failure would be a
	# mystery.
	address:
	name: the content address check
	needs: [manifest, environment, package]
	runs-on: ubuntu-latest
	container: ${{ needs.environment.outputs.image }}
	steps:
	- uses: actions/download-artifact@v4
	with:
	pattern: package-*
	merge-multiple: true
	- name: the two runners must agree
	run: \|
	a=$(sed -n 1p package-a.txt); pa=$(sed -n 2p package-a.txt)
	b=$(sed -n 1p package-b.txt); pb=$(sed -n 2p package-b.txt)
	echo "runner a $a at $pa"
	echo "runner b $b at $pb"
	if [ "$pa" != "$pb" ]; then
	echo
	echo "The two runners built at different paths, so this comparison"
	echo "cannot say anything about the package. A container job's"
	echo "workspace is /__w/<repo>/<repo> and both of these should be it."
	echo "Fix the workflow; the address difference below, if any, is a"
	echo "consequence and not a finding."
	exit 1
	fi
	if [ "$a" != "$b" ]; then
	echo
	echo "Two machines packaged one commit and got two addresses."
	echo
	echo "The archive has no clock, no uid, no user name, no directory"
	echo "order and no compressor in it — pack::Tar is written that way"
	echo "and tested for it — so the difference came from something put"
	echo "into it. The kernel image is the likeliest: it is the only"
	echo "content that is built rather than read, and a debug build"
	echo "carries its build path in DWARF. Both runners built at $pa,"
	echo "so the path is not it."
	echo
	echo "A release whose address depends on which machine built it is"
	echo "not content addressed, and every claim that cites a release by"
	echo "address is citing something two people cannot both obtain."
	echo "RELEASING.md, E0-R01."
	exit 1
	fi
	echo "agreed: $a"

	deps:
	name: dependency policy
	needs: [environment, manifest]
	runs-on: ubuntu-latest
	# The `full` image, which carries cargo-deny at the version docker/Dockerfile
	# pins. The action installed its own copy, so the version this job enforced
	# policy with was chosen by neither this repository nor its container —
	# which is the ambient dependency the image exists to remove, in the one job
	# whose whole subject is dependencies.
	container: ${{ needs.environment.outputs.image_full }}
	steps:
	- uses: actions/checkout@v7
	- run: cargo deny check

Navigation Menu

Uh oh!

Merge pull request #30 from iritur/iritur/e2-the-store #79

Workflow file

Merge pull request #30 from iritur/iritur/e2-the-store #79

Uh oh!

Workflow file for this run