Skip to content

fix(786): install an aarch64 process TTBR0 through one discipline that settles both shadows (slice 1) - #795

Merged
ryanbreen merged 15 commits into
mainfrom
fix/ttbr0-shadow-reconciliation
Sep 5, 2026
Merged

fix(786): install an aarch64 process TTBR0 through one discipline that settles both shadows (slice 1)#795
ryanbreen merged 15 commits into
mainfrom
fix/ttbr0-shadow-reconciliation

Conversation

@ryanbreen

Copy link
Copy Markdown
Owner

What and why

Ports the #786 TTBR0 shadow-reconciliation repair from the parked branch
fix/562-761-aarch64-testing-profile onto main, and only that repair.

On main, every one of the 10 aarch64 process-root install decision sites
wrote TTBR0_EL1 directly without keeping the two per-CPU shadow words
(next_cr3, saved_process_cr3) that the syscall-return corridor in
syscall_entry.S reads in sync with the register. When they disagree, a
return to EL0 can install a root the CPU has already left; on the parked
branch that showed up as init's first svc returning onto the kernel root
and taking an instruction abort at its own return address.

This slice adds one discipline, adopt_process_ttbr0, that runs the full
dsb ishst / msr ttbr0_el1 / isb / tlbi vmalle1is / dsb ish / isb
sequence and then settles both shadow words, and routes it through 9 of the
10 process-root install decision sites main had:

  • main_aarch64.rs::launch_init_from_elf
  • arch_impl/aarch64/syscall_entry.rs::sys_exec_aarch64
  • arch_impl/aarch64/syscall_entry.rs::check_and_deliver_signals_aarch64
  • arch_impl/aarch64/context_switch.rs::check_and_deliver_signals_for_current_thread_arm64
  • syscall/wait.rs::ensure_current_address_space
  • syscall/futex.rs::ensure_current_address_space
  • syscall/graphics.rs::ensure_current_address_space
  • syscall/handlers.rs::poll_ensure_address_space
  • memory/process_memory.rs::switch_to_process_page_table (aarch64 arm)

Two of those are behaviour changes on main in their own right, independent
of whether the shadow-word trigger below is reachable: graphics.rs's site
was doing dsb ishst / msr / isb with no TLB invalidation at all, and
process_memory.rs::switch_to_process_page_table left both shadows naming a
different root than the one its Cr3::write had just installed.

The tenth site, kernel/src/syscall/time.rs::ensure_current_address_space,
carries the identical defect shape but is on CLAUDE.md's Tier-1 prohibited
list (syscall hot path) and is not touched here.

It is disclosed rather than hidden: every_ttbr0_install_settles_the_per_cpu_shadows
prints it each time tests/ttbr0_shadow_reconciliation_structure.rs runs.
Repairing it is authorized as slice 1b, the next PR after this one.

Is the trigger reachable on main today? No, measured.

main's boot CPU is preemption-pinned through the whole boot sequence, so it
does not take an idle dispatch before launch_init_from_elf.

Measured, not argued: a scratch kernel with the next_cr3 clear removed from
adopt_process_ttbr0 (restoring main's pre-port disposition of that word)
read next_cr3=0x0 (the word the return corridor reads first) and
post_next_cr3=0x0, with 0 INSTRUCTION_ABORTs, in 5 of 5 strict-gate boots.
This slice is therefore defensive on that arm today, on main, plus the two
graphics.rs / process_memory.rs repairs above (which are not conditional
on it) and the ratchets that keep the shape from regressing.

The proof of consequence is the parked branch's own committed A/B/A mutation
battery -- cited here by commit and path, not re-run against main because
main cannot reproduce it (previous paragraph). At branch commit 1245c64b
(docs/planning/green-program/aarch64-testing/serials/r7/aba/): baseline
(no mutation) hit INSTRUCTION_ABORT in 13 of 26 boots; with both shadow
stores added, 0 of 24; reverted again, 4 of 8.

Review: round 1 (Sol) findings closed in rounds 2-3

Round 1's review (Sol) raised twelve findings on the initial port. Round 2
(ruling R154) closed five of them on this branch:

  • F-001 -- adopt_process_ttbr0's asm block declared
    options(nomem, nostack), a compiler licence to reorder the shadow stores
    and the caller's page-table stores across the install. Dropped across 4 of 4 install blocks that carried the same shape (the
    discipline helper plus three call sites), leaving the two mechanism
    primitives (neither of which carried it) untouched and the Tier-1 site
    disclosed rather than changed.
  • F-002 -- new ratchets pin the six-step install sequence in order and
    that no non-Tier-1 install is declared nomem, read off the extracted
    asm! block rather than prose.
  • F-003 -- the raw-install ratchet had cleared a site as soon as its body
    named set_saved_process_cr3, without requiring set_next_cr3(0) -- the
    weaker half, since the corridor reads next_cr3 FIRST. Replaced with one
    shape predicate, settles_both_shadows, requiring both words agree with
    the register.
  • F-009 -- corrected a false "one hunk" claim; the launch_init_from_elf
    diff is two hunks (the install, and the now-dead use core::arch::asm;
    import it leaves behind).
  • F-012 -- stripped a single trailing-whitespace byte from a committed
    evidence diff so git diff --check is clean.

Round 3 (ruling R158) closed the three ratchet gaps round 2 left open, each
proven with a mutation that fails red before the file is restored from its
byte copy:

  • N-003 -- the six-step sequence check covered only
    arch_impl/aarch64/ttbr0.rs; the installs in context_switch.rs and
    syscall_entry.rs could lose their barriers with the suite still green.
    every_non_primitive_ttbr0_install_performs_the_install_sequence (new)
    extends the check to 5 of 5 non-primitive installs at this head. Mutation: deleted the tlbi / dsb ish / trailing isb from
    switch_ttbr0_if_needed's install block -- suite failed, exit 101,
    restored, green again.
  • N-004 -- settles_both_shadows scored the FIRST write to each shadow
    word, so a body that cleared next_cr3 and then re-armed it with a root
    passed, while the corridor reads whatever the LAST store left there. Both shadow predicates now score the last write. Mutation: appended a
    set_next_cr3(next_ttbr0) right after the existing set_next_cr3(0) in
    switch_ttbr0_if_needed -- suite failed, exit 101 (invisible to round 2's
    first-write reader), restored, green again.
  • N-005 -- switch_ttbr0_to_kernel settles neither shadow by design (the
    kernel root is not a value either corridor arm should install on return to
    EL0), so the obligation falls to its callers, and no round-2 check scored
    them. every_caller_of_the_kernel_root_install_settles_the_shadows (new)
    censuses all 3: sys_exit_aarch64, sys_exec_aarch64 and
    quiesce_ttbr0_for_exit, requiring each to settle both words itself or
    (the exec shape) route both exits of its kernel-root window through a
    helper that does.
    Mutation: deleted set_saved_process_cr3(0) / set_next_cr3(0) from
    quiesce_ttbr0_for_exit -- suite failed, exit 101, restored, green again.

Round 3 also corrected five documentation claims (N-001, N-006 through
N-009) that had drifted from the tree after round 2 changed kernel source;
see the slice document's section 12 for each.

Round 3 boot and build results (this head)

Each boot below was run alone on this Mac with
pgrep -fl qemu-system-aarch64 | wc -l recorded immediately before launch,
gated to <=2 (host-load rule).

It read 0 before each of the 6.

profile pgrep-at-launch boots result
strict (run-aarch64-boot-test-strict.sh) 0 3 3 PASS, 0 FAIL
production (run-aarch64-prod-profile-boot-test.sh) 0 3 2 PASS, 1 FAIL

The one production red is a stall, not a fault: clonevm_exec_test prints
second stage and does not reach the post-exec rendezvous, so init stays
blocked in waitpid and bsshd does not spawn.

The guest stays alive the whole time (heartbeats reach 119415 ms, the gate
counted 0 crash markers). This is open issue #690's exact signature, is not
one of the 5 signatures pre-adjudicated for this round, and was recorded as
UNATTRIBUTED -- see the #690 A/B below for how that was resolved.

Builds: 3 of 3 aarch64 profiles (no-features/production, boot_tests,
testing) BUILD_EXIT=0 with check-kernel-no-neon.sh PASS; the beast x86
build (--features testing,external_test_bins --bin qemu-uefi) BUILD_EXIT=0
with an empty ^(warning|error) grep; 27 of 27 tests/*_structure.rs suites
green over 528 cases.

The #690 A/B (ruling R160)

The production red above carries #690's exact signature but was left
UNATTRIBUTED with no origin/main control on that profile. Ruling R160
resolved that with a dedicated 20-boot A/B: alternating one boot at a time
between this branch's head and origin/main, on the same production-profile
gate, pgrep-gated the same way.

arm boots PASS #690 occurrences other reds
branch (fix/ttbr0-shadow-reconciliation) 10 10 0 0
origin/main 10 9 0 1 (unattributed TTY-oracle cloexec/EAGAIN, boot 3; not #690)

R160's mechanical rule, verbatim: landable = (branch has no red outside #690) AND (branch #690 count <= main #690 count + 1). Branch produced 0
reds of any kind, so the first conjunct is vacuously true, and 0 <= 0 + 1, so
landable = true. Full table, per-boot transcripts and the Fisher's-exact
calculation (p = 1.0, uninformative at 0/10 vs 0/10) are at
docs/planning/green-program/aarch64-testing/serials/slice1/ab-690/README.md
and section 13 of the slice document. Neither arm reproduced #690 in this
10-boot-per-arm sample, which the same README's Discussion section notes does
not confirm or rule out an elevated branch rate at the previously-reported
1-in-3 figure -- that figure was observed on a different, more expensive gate
(the cortex-a72 service-sequence profile), not the production profile this
A/B ran.

x86

No x86 boot gate was run, and this round did not intend to run one: the x86
boot_tests gate is red on main for the #787 regression, and this slice
touches no x86 code path. The x86 reds tracked at #630, #636, #554, #608 and
#540 are unrelated to it as well. The x86 build itself is clean: on beast,
cargo build --release --features testing,external_test_bins --bin qemu-uefi exits 0 with an empty ^(warning|error) grep at this branch's
head (commit 0f2621b0; the 3 commits after it are documentation only, touching no kernel/ or tests/ source -- git diff --stat 0f2621b0..HEAD -- kernel tests is empty).

Docs

Full detail, evidence paths and the two review rounds' complete records:
docs/planning/green-program/aarch64-testing/TTBR0-SHADOW-SLICE-2026-09-04.md.

ryanbreen and others added 15 commits September 4, 2026 18:50
…t settles both shadows

Ported from the parked branch fix/562-761-aarch64-testing-profile (head
2b3fb18): the kernel halves of 5bd91b8 and 5f0a548.

Two per-CPU words decide which page-table root a return to EL0 runs on, and
both are read by syscall_entry.S: next_cr3 (offset 64) first, and
saved_process_cr3 (offset 80) as the fallback. setup_idle_return_locked
publishes the kernel root into next_cr3 on every idle dispatch and nothing on
the idle return corridor consumes it, so once published it sits armed. A site
that installs a process root with a raw `msr ttbr0_el1` and reconciles neither
word therefore does not merely disagree with the register -- it leaves the next
return to EL0 free to install whatever root the shadows still name.

ttbr0.rs gains adopt_process_ttbr0(): the barrier/msr/TLBI sequence, then
set_saved_process_cr3(value) and set_next_cr3(0). Nine process-root installs
are routed through it -- init's launch, exec, both signal-delivery paths, the
four ensure_current_address_space copies (one of which, graphics.rs, had no TLB
invalidation at all), and process_memory.rs's aarch64 switch, which wrote the
register with Cr3::write and left both shadows naming another root.
Cr3Flags::bits() is added so that last site can hand the complete value (root
plus ASID) to the discipline.

On main the next_cr3 arm is latent: the boot CPU is preemption-pinned for the
whole boot, so it takes no idle dispatch before launch_init_from_elf and the
trigger word is not armed. Measured, not assumed -- a probe build reads
next_cr3=0x0 at init's ERET in 5 of 5 boots. The consequence evidence is the
parked branch's own A/B/A: 13 of 26 baseline boots aborted at init's return
address, 0 of 24 with the two shadow stores added, 4 of 8 on reversion. The
graphics.rs TLB invalidation and the process_memory.rs reconciliation are
repairs on main in their own right, independent of that trigger.

kernel/src/syscall/time.rs::ensure_current_address_space is the tenth site and
the same defect shape. It is NOT fixed: syscall/time.rs is Tier-1 prohibited.
The census ratchet in the next commit prints it on every run rather than hiding
it.

claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
…c-path validator

The ratchet halves of the parked branch's 5f0a548 and 35dc2f1.

tests/ttbr0_shadow_reconciliation_structure.rs walks every Rust function under
kernel/src whose body writes TTBR0_EL1 and sorts the result by shape rather
than by a list of known sites. A censused function must be the discipline
itself, or reconcile inline (it names set_saved_process_cr3), or be a mechanism
primitive -- one whose installed value came in through its own signature, which
fetched nothing of its own and named no per-CPU shadow. Anything left over must
live in a file CLAUDE.md lists as Tier-1 prohibited, and
the_tier_one_exemption_matches_the_project_rule reads that list back out of
CLAUDE.md rather than trusting the test's own copy.

every_aarch64_caller_of_a_mechanism_primitive_settles_the_shadows closes the
exemption's other end: an aarch64-scoped caller of an exempt primitive must
name adopt_process_ttbr0, quiesce_ttbr0_for_exit or set_saved_process_cr3, or
be the MMU bring-up that installs the kernel root before per-CPU state exists.

The census reaches 7 functions at this head, the same 7 the parked branch
reported, and prints the one Tier-1 site it is not allowed to repair:

  TTBR0 installs still unreconciled behind the Tier-1 rule:
  ["kernel/src/syscall/time.rs::ensure_current_address_space"]

Anti-vacuity legs in the same file: an invented site that reads a root out of
the process manager and installs it raw is classified unreconciled; an invented
site whose operand is a masked parameter is still admitted as a primitive; an
invented site that fetches its root is rejected as a primitive; an invented
site that touches one shadow is rejected as a primitive; and an invented
aarch64 wrapper handing a process root straight to a primitive is caught by the
caller census and cleared once routed through the discipline.

The branch carried these tests inside tests/aarch64_testing_profile_structure.rs
alongside #562/#761 checks that pin functions main does not have, so the TTBR0
half was lifted into its own file and the rest left on the branch.

tests/exec_lock_order_structure.rs is re-anchored because it had to be: its T4
validator asserted sys_exec_aarch64 holds exactly one `msr ttbr0_el1` and one
set_saved_process_cr3(, both of which the previous commit removes from that
function. It now requires the call to the discipline and checks the shadow
publication in the helper the exec path calls, and gains two negative tests --
deleting set_next_cr3(0) from the helper reddens it, and putting a raw msr back
into sys_exec_aarch64 reddens it.

All 27 tests/*_structure.rs suites pass at this head.

claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
…t control

Every serial this slice's numbers are counted from, committed.

serials/slice1/mutation-5/ -- 5 strict-gate boots of a scratch kernel with
set_next_cr3(0) deleted from adopt_process_ttbr0 and a probe printing both
shadow words either side of init's install. 5 of 5 SUCCESS, 0 of 5 carrying
INSTRUCTION_ABORT, and the probe line identical in 5 of 5:

  [SLICE1_PRE_ERET] pre_next_cr3=0x0 pre_saved=0x0 post_next_cr3=0x0
  post_saved=0x100004406c000 ttbr0=0x100004406c000

next_cr3 reads 0x0 at init's ERET on main, so the trigger word is not armed and
deleting the clear changes nothing a boot can see. The defect this slice
repairs is latent on main; that is the honest result and the reason the
consequence evidence is the parked branch's A/B/A rather than a red here.

serials/slice1/diffs/mutation-and-probe.diff -- the scratch changes exactly as
they were reverted out of the worktree. Neither is in the shipped tree.

serials/slice1/smoke-strict/ -- 3 strict boots at this head, run one at a time,
3 of 3 PASS.
serials/slice1/smoke-prod/ -- 3 production-profile boots at this head, 3 of 3
PASS with 0 crash markers.
serials/slice1/smoke-testing/ -- 3 boots of the `testing` profile at this head.
It builds and does not boot: 2 of 3 panic at
kernel/src/task/softirq_tests.rs:228:5 ("ksoftirqd should have processed
deferred softirqs"), 1 of 3 makes no progress past "[smp] 4 CPUs online".

serials/slice1/main-control-testing/ -- the same 3 boots with this branch's
work stashed out, at origin/main d6b7a18. Same distribution: 2 of 3 panic at
softirq_tests.rs:228:5, 1 of 3 no-progress. The `testing` profile's red is #562
and is inherited from the base commit, not introduced here.

claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
… what did not, and why it is latent on main

The slice document for the port of #786's TTBR0 discipline from the parked
branch fix/562-761-aarch64-testing-profile onto main, plus the build logs the
last section indexes.

It says, in order: the corridor mechanism and the two per-CPU words; the nine
process-root installs routed through adopt_process_ttbr0 and the three branch
commits they came from; what was deliberately left behind, including the whole
#562/#761 boot-sequence change and the Tier-1 site; the mutation battery that
shows the next_cr3 trigger is NOT observable on main (next_cr3=0x0 at init's
ERET in 5 of 5 probed boots, 5 of 5 boots green with the clear deleted) and the
statement that this slice is therefore defensive on that arm; the parked
branch's A/B/A cited by commit 1245c64 and path rather than restated as if
re-run here; the R13 smoke, with the `testing` profile's 3 of 3 red attributed
to #562 by a 3-boot control at the base commit; the Tier-1 disclosure and the
census line that prints it; the ratchets and their five anti-vacuity legs; and
the builds.

Build logs added under serials/slice1/builds/: the three aarch64 profiles with
their check-kernel-no-neon.sh output, and the beast x86
testing,external_test_bins build (exit 0, 0 of 123 lines matching
^(warning|error)).

claim-lint: scripts/claim-lint.py -> exit 0
claim-lint: scripts/claim-lint.py --files docs/planning/green-program/aarch64-testing/TTBR0-SHADOW-SLICE-2026-09-04.md -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
R13 asks for 3 boots each of strict, prod and testing at the head being
returned. The first battery ran at the code commit 9e9131d; this one runs
after the ratchets, serials and the slice document landed, so the boots are
against the exact head this branch returns. 0 of the 4 commits after 9e9131d
touch kernel/, so the kernel bytes are the same -- this is a re-run, not a
second kernel.

serials/slice1/r13-final/, 9 boots, run one at a time:

  strict      3 of 3 PASS   (run-aarch64-boot-test-strict.sh 1, three times)
  production  3 of 3 PASS   (run-aarch64-prod-profile-boot-test.sh, three times)
  testing     3 of 3 FAIL   (#562)

The `testing` red is the inherited #562 blocker, attributed by the 3-boot
control at origin/main d6b7a18 already committed under
serials/slice1/main-control-testing/. Its two signatures appear in different
proportions between the two batteries and this is stated in the document rather
than smoothed over: battery 1 scored 2 panics at
kernel/src/task/softirq_tests.rs:228:5 and 1 no-progress boot; battery 2 scored
3 panics and 0 no-progress. The base-commit control scored 2 and 1. Both
signatures are #562's; neither is introduced here.

Section 5 of TTBR0-SHADOW-SLICE-2026-09-04.md is rewritten to describe both
batteries and the proportions, and section 8 indexes the new serials.

claim-lint: scripts/claim-lint.py -> exit 0
claim-lint: scripts/claim-lint.py --files docs/planning/green-program/aarch64-testing/TTBR0-SHADOW-SLICE-2026-09-04.md -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
adopt_process_ttbr0 declared its asm options(nomem, nostack). nomem tells the
compiler the block reads and writes no memory, which is a licence to move
memory accesses across it -- and the memory in question is exactly the two
per-CPU shadow stores that follow the install (set_saved_process_cr3 /
set_next_cr3(0)) and the caller's page-table stores that have to be settled
before it. The option is dropped; nostack stays.

What the block now orders relative to the surrounding Rust stores: without
nomem the compiler must assume the asm may read or write the same memory as the
code around it, so it may not move those stores across the block in either
direction. That is a constraint on the compiler alone. No instruction is added,
and no claim is made here about what another CPU observes -- the hardware
ordering is still the dsb ishst before the msr and the dsb ish; isb after,
unchanged.

No miscompilation was observed. This closes a permission, not a measured
reorder, and the doc comments on the helpers say so in those terms.

The finding named the discipline helper. 3 more sites had the identical shape
-- an install block declared nomem with shadow stores beside it -- so 4 of the 4
are fixed together:

  arch_impl/aarch64/ttbr0.rs::adopt_process_ttbr0            (the finding)
  arch_impl/aarch64/ttbr0.rs::switch_ttbr0_to_kernel         (quiesce_ttbr0_for_exit stores after it)
  arch_impl/aarch64/syscall_entry.rs::restore_ttbr0_after_failed_exec
  arch_impl/aarch64/context_switch.rs::switch_ttbr0_if_needed

The 2 mechanism primitives, paging.rs::write_root and
memory/arch_stub.rs::Cr3::write, already carried options(nostack) alone and are
untouched. The 7th censused site,
kernel/src/syscall/time.rs::ensure_current_address_space, is nomem and carries
the same hazard; it is Tier-1 prohibited, so it is disclosed and printed by the
suite on every run rather than changed.

One consequence worth stating: the raw block this slice replaced at
launch_init_from_elf carried options(nostack, preserves_flags), so routing that
site through the discipline helper as round 1 shipped it ADDED nomem where the
code had not had it. This removes it again.

context_switch.rs is Tier-2. The change there is one asm option plus a comment;
it adds no instruction, no logging, no lock and no allocation on that path.

Builds re-run after the change, all exit 0 with only the pinned toolchain's
core v0.0.0 future-incompat warning, and check-kernel-no-neon.sh PASS on each:
docs/planning/green-program/aarch64-testing/serials/slice1/r2/.

claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
…, and no nomem

Two asymmetries in the round-1 ratchet, and one site it never pinned.

F-003, the shadow asymmetry. The raw-install ratchet cleared an inline
installer as soon as its body named set_saved_process_cr3; it did not ask for
set_next_cr3(0). That is the weaker half. The corridor reads next_cr3 FIRST and
installs it whenever it holds a value other than 0, so a site that publishes a
correct saved_process_cr3 and leaves a stale next_cr3 armed has decided which
root the next return to EL0 runs on just as surely as a raw msr would. The
primitive-caller census cleared a caller the same way. Both now go through one
shape predicate, settles_both_shadows: a body qualifies when it publishes a root
other than 0 into saved_process_cr3 AND clears next_cr3 with a literal 0. It is
a shape, not a list of blessed function names.

F-003, the missing pin. context_switch::switch_ttbr0_if_needed was reached only
through the census, though it is the install a userspace thread takes on each
dispatch that changes address space.
the_dispatch_ttbr0_switch_settles_both_shadows pins it directly: the root it
publishes into saved_process_cr3 must be the operand it just installed, it must
clear next_cr3, and its block must not be nomem.

F-002, the asm shape. the_discipline_installs_in_order_and_orders_the_shadow_stores
asserts, for each install helper ttbr0.rs holds (found by shape), that the block
performs dsb ishst -> msr ttbr0_el1 -> isb -> tlbi vmalle1is -> dsb ish -> isb in
order and does not carry nomem. The option is read off the extracted asm! block,
not the function body, so prose naming nomem cannot decide the answer. Coverage
is an equality, not a floor: the install occurrences inside the checked bodies
must equal the occurrences the file holds, so a helper added later cannot slip
past it. no_ttbr0_installer_claims_it_touches_no_memory applies the nomem half
to the censused installers kernel-wide, with the shadow census's Tier-1
disposition -- print, do not pin.

Anti-vacuity, both recorded under serials/slice1/r2/ with the assertion each
printed:

  mutation A, nomem put back in adopt_process_ttbr0 -> exit 101, 14 passed /
  2 failed; the_discipline_installs_in_order_and_orders_the_shadow_stores and
  no_ttbr0_installer_claims_it_touches_no_memory both red.

  mutation B, set_next_cr3(0) deleted from switch_ttbr0_if_needed -> exit 101,
  14 passed / 2 failed; the_dispatch_ttbr0_switch_settles_both_shadows and
  every_ttbr0_install_settles_the_per_cpu_shadows both red.

Each file was restored from a byte copy taken before its edit, and the suite is
green at this tree: 16 of 16 cases.

4 self-contained legs were added beside the mutations so the tightened
predicates cannot quietly go vacuous later: the nomem check is proven to read
the block and not the prose and to clear when the option is dropped; a bare msr
with no barriers fails the sequence check; the 4 one-word-settled shapes are
accepted and rejected as their names say; and a synthetic aarch64 caller that
publishes only saved_process_cr3 is caught by the caller census, clearing only
when set_next_cr3(0) is added beside it.

27 of 27 tests/*_structure.rs suites green, 524 cases, 0 failures:
docs/planning/green-program/aarch64-testing/serials/slice1/r2/structure-suites.txt

claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
…whitespace, record round 2

F-009. Section 2 said "the whole diff to that function is 1 hunk". It is 2:

  $ git diff --unified=0 origin/main..HEAD -- kernel/src/main_aarch64.rs | rg "^@@"
  @@ -90 +89,0 @@ fn launch_init_from_elf(
  @@ -271,12 +270,26 @@ fn launch_init_from_elf(

The first removes `use core::arch::asm;`, which the replaced block was the
file's last user of; the second is the install itself. The sentence now says two
hunks and names both, and the claim-lint annotation cites the command and the
two headers rather than the wrong count.

F-012. serials/slice1/diffs/mutation-and-probe.diff line 13 was a single space
-- the unified-diff context line for a blank source line -- which made
`git diff --check origin/main..HEAD` exit 2. Only that whitespace is removed;
the line is now empty and no other byte of the artifact changed. It was the sole
trailing-whitespace line the file held, and `git diff --check` is clean at this
head.

Section 7 is rewritten to describe the ratchets as they now stand: what
"reconciles inline" means (both corridor words, by shape), the caller census's
matching clearance, the new sequence/nomem pins, the independent dispatch pin,
and the 4 added anti-vacuity legs.

Section 8 is retitled to say the rows are the round-1 head, since round 2
changed kernel source; section 10 indexes the new serials/slice1/r2/ directory.

Section 11 is new: each closed finding, what changed, and the anti-vacuity run
behind it -- command, exit code, and the assertion that printed -- plus the
round's builds and suites with an artifact path per row, and the F-007
disposition recorded verbatim as the arbitration rule this branch is held to.

New artifacts under serials/slice1/r2/: the 3 rebuilt aarch64 profiles with
their check-kernel-no-neon.sh runs (3 of 3 BUILD_EXIT=0, 3 of 3 PASS), the
27-suite run (27 of 27 green, 524 cases), and the 2 anti-vacuity mutation runs
(both exit 101).

claim-lint: scripts/claim-lint.py -> exit 0
claim-lint: scripts/claim-lint.py --files docs/planning/green-program/aarch64-testing/TTBR0-SHADOW-SLICE-2026-09-04.md -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
Section 11 closed with a placeholder for the claim-lint block. It now carries
the invocations that were actually run and what each returned: diff mode over
the branch, and --files over the slice document, the mutation-and-probe
evidence artifact, and the 3 new serials/slice1/r2/ text artifacts -- 5 runs,
all exit 0.

Also stated, rather than left implicit: whole-file --files runs over the 4
kernel and test sources this round edited return exit 1 on prose those files
already carried, outside this round's hunks. Diff mode is what scores the
change, and it is clean.

claim-lint: scripts/claim-lint.py -> exit 0
claim-lint: scripts/claim-lint.py --files docs/planning/green-program/aarch64-testing/TTBR0-SHADOW-SLICE-2026-09-04.md -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
…left open

N-003. The install-sequence check ran over `kernel/src/arch_impl/aarch64/ttbr0.rs`
alone, so the two installs outside that module -- `switch_ttbr0_if_needed` and
`restore_ttbr0_after_failed_exec` -- could lose their barriers without a test
noticing. `every_non_primitive_ttbr0_install_performs_the_install_sequence`
applies `performs_install_sequence` to each censused install that is not a
mechanism primitive: 5 of the 7 censused functions at this head, in 3 files,
with the same print-do-not-pin disposition for the Tier-1 site the other
kernel-wide censuses use. The coverage floor is census-shaped -- at least 4
installs, in at least 2 files -- so it cannot collapse back to the discipline
module and keep passing. The primitive exemption is a real narrowing and the
doc comment says so: 2 of 2 primitives at this head run no `isb` after the
`msr` and no `tlbi vmalle1is`, and this test makes no claim that their callers
compensate.

N-004. `settles_both_shadows` read the FIRST occurrence of each accessor, so a
body that cleared `next_cr3` and armed it again afterwards passed. `call_argument`
becomes `call_arguments` plus `last_call_argument`, and both shadow predicates
now score the LAST write to each word -- which is the write the return corridor
actually reads.

N-005. Callers of `switch_ttbr0_to_kernel` -- the kernel-root install, which
settles neither shadow by design -- were constrained by nothing.
`every_caller_of_the_kernel_root_install_settles_the_shadows` censuses them (3
at this head: `quiesce_ttbr0_for_exit`, `sys_exit_aarch64`, `sys_exec_aarch64`)
and requires each to settle or zero both words itself, or to sit in one
interrupt-masked window whose every exit reinstalls through a helper that
settles both -- the exec shape, whose window is pinned by
`validate_aarch64_failed_exec_ttbr0_rollback` in
tests/context_restore_structure.rs and
`validate_sys_exec_releases_process_manager` in
tests/exec_lock_order_structure.rs, both named in the doc comment.

Also: the module doc now states both accountings that were being conflated (10
process-root DECISION sites, 9 routed and 1 Tier-1, versus 7 raw-`msr`
FUNCTIONS censused -- 2 discipline helpers, 2 reconciling inline, 2 mechanism
primitives, 1 Tier-1); the duplicated claim-lint sentence on
`ttbr0_install_census` is collapsed to one; and the cfg-free
`kernel/src/memory/kernel_page_table.rs::build_master_kernel_pml4` narrowing is
disclosed on `aarch64_scoped_functions`, including why nothing on aarch64
reaches it at this head.

4 new tests, 20 of 20 green.

claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Claude <noreply@anthropic.com>
…het gaps

One recorded mutation per gap, each a scratch kernel edit, one suite run, the
verbatim assertion, a SHA-256-verified byte-copy restore, and a green re-run:

* N-003 strips `tlbi vmalle1is` / `dsb ish` / `isb` from the install block in
  `switch_ttbr0_if_needed` -- exit 101, 1 failure.
* N-004 re-arms `next_cr3` with the installed root after the existing clear in
  the same function -- exit 101, 2 failures.
* N-005 deletes the shadow-zeroing pair from `quiesce_ttbr0_for_exit` -- exit
  101, 1 failure.

Restored tree: exit 0, 20 of 20 passed. The README also records what each new
census reaches -- 5 install sites and 3 kernel-root callers, observed by
raising each coverage floor until the assertion printed its own list -- because
a census that silently shrinks is how a ratchet goes quiet.

claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Claude <noreply@anthropic.com>
… head

Builds, each artifact carrying the full cargo command on its second line and a
`BUILD_EXIT=` line at the end, with `grep -cE '^(warning|error)'` scored over
the build output:

* no features (the production profile) -- `BUILD_EXIT=0`, 1 line, the
  toolchain's `core v0.0.0` future-incompat notice
* `--features boot_tests` -- `BUILD_EXIT=0`, the same 1 line
* `--features testing` -- `BUILD_EXIT=0`, the same 1 line

`scripts/check-kernel-no-neon.sh` after each: 3 of 3 exit 0, PASS, 0 FP/SIMD
load/store in `.text`.

The `boot_tests` profile links userspace ELFs a fresh worktree does not carry.
They were copied from the primary working copy rather than rebuilt here, and
`userspace-elfs.md` records that with the hash comparison that shows the 152 of
152 files match -- this branch changes no userspace source.

27 of 27 `tests/*_structure.rs` suites green, 528 cases, 0 failures.

Boots at this head, one at a time, with `pgrep -fl qemu-system-aarch64 | wc -l`
recorded before each launch (0 before every one of the 6):

* strict `docker/qemu/run-aarch64-boot-test-strict.sh 1`, 3 runs -- 3 of 3 PASS
* production `docker/qemu/run-aarch64-prod-profile-boot-test.sh`, 3 runs --
  2 of 3 PASS, 1 red

The red is preserved whole under `serials/slice1/prove-r3/`. It is a stall, not
a fault: `clonevm_exec_test` prints `CLONEVM_EXEC_TEST: second stage` and never
reaches `post-exec rendezvous complete`, `init` stays blocked in `waitpid` on
it, so `bsshd` is never spawned and the gate times out -- while heartbeats,
`[net-rx-counters]` samples and the strand census keep advancing. 0 crash
markers. That is the exact signature of open issue #690, on a different CPU
profile than the one that issue reports. It is NOT one of this round's
pre-adjudicated signatures, so it is recorded as UNATTRIBUTED and this round
does not call the branch landable. No control at `origin/main` was run, so
nothing here rules the branch out either.

claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Claude <noreply@anthropic.com>
…at this head

Round 2's review found five documentation claims that had stopped matching the
tree. Each is fixed rather than softened, and section 12 records the round.

N-001. Section 5 said round 1's boots were a re-run at the returned head
"because the kernel sources are byte-identical" from `9e9131d0` onward. Round
2's `4770c056` dropped `nomem` from four install blocks, so that stopped being
true the moment it landed. Section 5 is now round 3's boots at this head -- 3
of 3 strict PASS, 2 of 3 production PASS -- with round 1's batteries kept as
labelled history and the false sentence gone. Sections 8 and 10 likewise carry
round 3's builds and artifact paths, with earlier rounds' listed separately.

N-006. The header counted 10 installs / 9 routed / 1 Tier-1 while section 7's
census counted 7 functions, and nothing reconciled them. The header now states
both accountings -- 9 of 10 process-root DECISION sites routed plus 1 Tier-1,
and 7 of 7 raw-`msr` FUNCTIONS censused, of which 2 are discipline helpers, 2
reconcile inline, 2 are mechanism primitives and 1 is the same Tier-1 site.

N-007. Round 2's build table used a code-font `BUILD_EXIT=0` token its
artifacts never recorded. Round 3's do: each carries the full cargo command on
its second line and a `BUILD_EXIT=` line at the end, and `userspace-elfs.md`
records where the userspace ELFs came from with the hash comparison.

N-008. "The tenth site" now says which of the two accountings it belongs to
wherever it appears.

N-009. Section 7 said round 2 added "4 more self-contained legs" and listed 4
items, one of which is an assertion inside another test. It now says 3 tests,
names them, and says which leg lives inside the first.

Section 12 also records the three ratchet gaps this round closed, each with its
mutation and the verbatim assertion, and the production red -- open issue
#690's exact signature, recorded UNATTRIBUTED, with the plain statement that
this round does not call the branch landable and ran no `origin/main` control
that would rule the branch out.

The 5 green boots' gate transcripts are committed beside the red's, so the
pre-launch process count claimed for each of the 6 can be read off the file.

claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Claude <noreply@anthropic.com>
…arms

R160 asked whether fix/ttbr0-shadow-reconciliation (b731e53) raises the
#690 rate on the aarch64 production profile vs origin/main (d6b7a18), 20
boots alternating one at a time via run-aarch64-prod-profile-boot-test.sh.
Result: branch 10/10 PASS, main 9/10 PASS with one unattributed TTY-oracle
red unrelated to #690; neither arm hit the #690 signature. Per the R160
mechanical rule (branch has no red outside #690, and branch #690 count <=
main #690 count + 1) this reads landable, though the run does not reproduce
the 1-in-3 rate reported for this slice elsewhere -- see the Discussion
section in the committed README for the honest caveat and the Fisher
p=1.0 that follows from an all-zero table. Transcripts for all 20 boots
(gate + full guest serial, both arms) are committed alongside the README.

claim-lint: scripts/claim-lint.py --files docs/planning/green-program/aarch64-testing/serials/slice1/ab-690/README.md -> exit 0
claim-lint: scripts/claim-lint.py -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Code <noreply@anthropic.com>
Section 12's "does not call the branch landable" paragraph was written
before ruling R160's dedicated 20-boot A/B discriminator against
origin/main existed. Add section 13 with the two-arm per-boot table,
the counts (branch 10/10 PASS/0x#690, main 9/10 PASS/1 unattributed
red/0x#690), the Fisher's-exact p (informational only, p=1.0 on
[[0,10],[0,10]]), R160's mechanical rule verbatim, and its outcome
(landable=true). Replace section 12's stale sentence with a pointer to
section 13 and the actual conclusion: the branch is landable under
R160, with #690 pre-adjudicated for this slice by that ruling.

claim-lint: scripts/claim-lint.py                                                                                                          -> exit 0
claim-lint: scripts/claim-lint.py --files docs/planning/green-program/aarch64-testing/TTBR0-SHADOW-SLICE-2026-09-04.md                     -> exit 0
@ryanbreen
ryanbreen merged commit bdb5be9 into main Sep 5, 2026
@ryanbreen
ryanbreen deleted the fix/ttbr0-shadow-reconciliation branch September 5, 2026 01:45
ryanbreen added a commit that referenced this pull request Sep 5, 2026
…rtifacts

Everything here ran at cd17ff2, i.e. after `git merge --no-ff origin/main`
(bdb5be9, PR #795) landed on this branch with no conflict.

x86, on beast in /root/breenix-787fix, qemu_before recorded as 0 before each of
the three boots:
- the testing-profile build's `grep -E "^(warning|error)"` wrote a 0-byte file
- run-x86-boot-tests.sh 1, twice: PASS / PASS, rc=0 both, one
  x86_retire_cohort:PASS marker in each user serial
- run-x86-prod-profile-boot-test.sh, once: rc=0
Both boot-tests runs booted kernel ELF sha256 bd255118...; per-run UEFI,
test-binary and ext2 hashes are in round2/x86/boot-{1,2}.hashes.

The allocation guard ran INLINE in both gate runs, after the build, reporting 3
in-scope symbols and 19 resolved call edges with 0 violations. Its four
standalone legs are committed under round2/alloc-guard/ with the mutation diff:
green on both profiles, red on the restored name.clone(), and red on the shipped
b257e69 kernel.

aarch64, on the Mac, qemu_before 0 before each of three launches: the soft-float
boot_tests build completes, check-kernel-no-neon.sh passes with 0 FP/SIMD
load/stores in kernel .text, and run-aarch64-boot-test-strict.sh 1 passes 3 of 3.
Round 1's "80 of 80" had no committed log and is withdrawn above; this is what
round 2 ran and what it claims.

One honesty note the round-2 doc section carries: that aarch64 build is not
silent. It prints one warning line, the future-incompatibility notice for the
toolchain's own vendored core v0.0.0, naming no Breenix crate. Round 1 called
the build "clean" without that qualification.

All 28 tests/*_structure.rs suites run once at this head: 28 green of 28.

claim-lint: python3 scripts/claim-lint.py -> exit 0

Co-Authored-By: Ryan Breen <ryan.breen@gmail.com>
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com>
ryanbreen added a commit that referenced this pull request Sep 5, 2026
Re-runs the zero-warnings build check, docker/qemu/run-x86-boot-tests.sh 1
(twice), and docker/qemu/run-boot-parallel.sh 1 (once) at the head that
merged origin/main (PR #794, #795) into fix/737-df-oracle-ratchet, on
beast -> Incus breenix-x86, clone /root/breenix-737-oracle, every boot
isolated under unshare -m with a per-clone /tmp bind (R18). All three
boots and all three build invocations are green: 0 warnings/errors,
x86_retire_cohort clears at balance=0 on both boot-tests runs (exited=110
expected>=105), and the oracle boot reproduces df_after_cld=0
df_roundtrip=ok with 0 ring-0 page faults. The timer_interrupt_entry cld
is confirmed still present in the merged-head kernel ELF via objdump.
Appends a "Landing re-smoke" section (with hashes) to
docs/planning/green-program/nic-bus/737-FIX-2026-09-04.md and adds the
serial evidence + a matching .gitattributes -text rule.

claim-lint: scripts/claim-lint.py -> exit 0
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant