Skip to content

The interrupt census keeps one word per delivery, so it always adds up - #734

Merged
Japabu merged 3 commits into
mainfrom
wt/toyos-irqcensus
Oct 4, 2026
Merged

Japabu merged 3 commits into
mainfrom
wt/toyos-irqcensus

Conversation

@Japabu

@Japabu Japabu commented Oct 4, 2026 •

Copy link
Copy Markdown
Collaborator

The interrupt census keeps one word per delivery: a CPU's total is the sum of its sources, so a census read from another CPU always adds up.

The defect

irq_census_conservation went red once on the T14, in #728's full Drive-mode suite at 78c21c575: cpu1 counted 24211 interrupt(s) and attributed 24210 to sources. The readback's testcases/kernel.log, line 12102, shows when: cpu7 printed the census at test_rs_counters_metal's exit, and cpu1 was in a kick storm at the time (kick=22906 on cpu1, against 1683–5188 on the other APs).

Every delivery was two adds to the CPU's own block, the total first and then the source: irq_took!, the Ring 0 timer stub's inline pair, and AArch64's irq_took. irq_census::read loaded the slots one at a time with Relaxed loads, from whichever CPU prints. A reader that loads cpu1's total after cpu1's first add and the kick slot before its second sees a total one past the sources. Those are the numbers the T14 printed. No source was uncounted: every writer always did both adds, so the judge's message, "a source is not being counted", named the wrong thing. #728's 20 ms wake of every CPU before its idle second does not cause this. It raises the kick rate on the APs around a process exit, so a read is more likely to land in the window. The window was already on main.

The fix, at its owner

  • kernel/src/irq_census.rs: TOTAL and SLOTS are gone, and the block is one u64 per Source. deliveries_total, taken_by and taken_here sum the same snapshot (taken_* leave out the NMI, as before). irq: cpuN no longer prints total=.
  • irq_took! (x86-64), the Ring 0 timer stub and AArch64's irq_took each do one add. That is one fewer read-modify-write on every interrupt.
  • irq_counts_here returns the CPU's whole block, one gs: load per slot on x86-64. It is still lock-free and division-free for the NMI path.
  • Host side: common::irqcensus::Census loses its total field and gains total(), the sum. The parser now refuses any line whose fields are not exactly SOURCES.
  • The judge (tests/toyos.rs, irq_census): the conservation check is deleted. It compared a derived value with itself and can no longer fail. The monotonic check now checks every source, not only the total. That is stronger: with a derived total, one counter going backwards could be hidden by another going up.
  • issues/every-interrupt-lands-on-the-boot-cpu.md: the instrument paragraph now describes the line and the gate as they stand.

Why there is no new test

The brief asked for a test at the cheapest tier that reds first, and a loom model if the defect is an ordering race. It is an ordering race, but a race between two words, and this change deletes one of them. With no total stored apart from the sources, no sequence of writes and reads can make the two disagree. That is the type tier: nothing is left for a loom model to explore. A loom model of the old two-word layout would only test a design the tree no longer has.

The defect's red is the recorded T14 failure above. It is a recorded real failure on the base, and it is the independent oracle. The negative control is the base itself: reverting the whole change gives origin/main at 4d46c8e55, the layout that produced that red. One green T14 run cannot prove a once-in-a-suite race gone, so the T14 run below shows only that the row and its judge still hold on the machine with the new line format.

Filed, off this branch's fence

Review round 1 found two defects next to this change and outside it. Both are filed, not fixed:

  • issues/the-irq-census-judge-reds-on-two-exits-stamped-in-the-other-order.md: the judge's per-source monotonic check and its tlb: shootdowns= checks compare lines from two process exits. The capture is merged by stamp, and a line is stamped after its counters are read, so two exits on two CPUs can be listed in the other order from their reads.
  • issues/the-spurious-and-unclaimed-selftests-took-interrupts-after-check-cannot-fail.md: both selftests read deliveries_total before the probe, and the probe's own delivery raises it, so "took interrupts after it" holds once delivered holds.

Gates

Logs are in the orchestrator's job scratchpad, under orch/. The code gates ran at 27fc30994, the change's commit, with the worktree clean. After them, origin/main (0613f93f7: #729, #732) was merged cleanly and the two issue files were committed. The merge touched no file this change touches except tests/toyos.rs, where it auto-merged hunks outside irq_census. cargo test --lib sourcegate ran at the pushed head.

command at exit log
cargo run -- --build-only 27fc30994 0 orch/irqcensus/build.log
cargo run -- --build-only --arch aarch64 27fc30994 0 orch/irqcensus/build-a64.log
cargo run -- --ci host (Host: 75 step(s), all green) 27fc30994 0 orch/irqcensus/host.log
cargo test (whole guest suite: 28 passed, 28 total; the census summary parsed 17 guests' lines in the new format) 27fc30994 0 orch/irqcensus/guest.log
cargo test --test toyos-build -- --metal --metal-readback <scratch>/metal irq_census_conservation (staging only, exit 2 by design: Verdict::Staged) 27fc30994 2 orch/irqcensus/metal-stage.log
T14 run of the staged testcases image, judge irq_census ([metal] 1 passed, 0 failed, 1 boot(s); none of its 72 irq: cpu lines carries total=) 27fc30994 0 orch/irqcensus/metal/judge-irq_census.log
cargo test --lib sourcegate (10 passed) pushed head 0 orch/irqcensus-r2/sourcegate.log

What I am unsure of

  • Whether a reader of irq: cpuN lines elsewhere in the tree still wants total= printed. Old quotations in issues/ keep the old format because they are recordings. Every parser in the tree (tests/common/irqcensus.rs, and the tests/checks.rs fixture) now reads the new one.

Net against main: 10 files, the change's 8 at +78 −111 and the two filed issues.

🤖 Generated with Claude Code

https://claude.ai/code/session_01WcU2Dsw6mDYtwYfzVHPzM8

Each delivery was two `add`s to the CPU's own block, the machine's total
first and the source second, and `irq_census::read` loaded the slots one
at a time from whatever CPU prints the census. A reader landing between
a CPU's two `add`s saw the total move and the source not, and printed a
census whose total was one past its sources. The T14 recorded exactly
that: in #728's full Drive-mode suite at 78c21c5, cpu7's process-exit
census read cpu1 mid-kick-storm (22906 kicks) as total=24211 against
sources summing to 24210, and `irq_census_conservation` named it "a
source is not being counted". No source was uncounted: every writer,
`irq_took!`, the Ring 0 timer stub and AArch64's `irq_took`, always did
both adds. #728's 20 ms wake of every CPU raises the kick rate on the
APs around a process exit and so the odds of the read landing in the
window; the window is main's.

The total is now the sum of the sources, read off the same snapshot, so
there is no second word to disagree with and nothing for a torn read to
tear. Every delivery costs one `add` instead of two. `taken_here` and
`taken_by` sum every source but the NMI; `irq: cpuN` drops its `total=`
field and the host's `Census::total` sums the sources. The judge's
conservation check, which can no longer fail, goes; its monotonic check
now asks every source rather than the total.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WcU2Dsw6mDYtwYfzVHPzM8
@Japabu

Japabu commented Oct 4, 2026

Copy link
Copy Markdown
Collaborator Author

T14 result at 27fc30994 (orchestrator's run; worktree clean at head, image sha256 49435fd64c625388d9693d97d7a3230716f52cadca0e98954f3b220de840c489 hashed by the orchestrator and checked before the flash): boot testcases rc=0; judge irq_census EXIT=0, [metal] 1 passed, 0 failed, 1 boot(s). Log: orch/irqcensus/metal/judge-irq_census.log in the orchestrator's job directory.

@Japabu

Japabu commented Oct 4, 2026

Copy link
Copy Markdown
Collaborator Author

Review of 27fc30994 against origin/main (9cba42fe2). This is round 1, at the high-risk bar, under the owner's 2026-10-04 ruling: there are no prose or cosmetic findings.

Net: +78 −111 across 8 files. Production (kernel) is +49 −64, tests +26 −44, and issues/ +3 −3.

Diagnosis holds. I checked it against the recorded readback, countersquiet-r5/metal/drive/728r5-full-readback/testcases/kernel.log. At 36.226, cpu7 printed cpu1 total=24211 timer=1141 kick=22906 … tlb=142 nmi=21. The sources sum to 24210. The kick count is the one that moved since cpu4's line 1 ms earlier, where total=24205 equals its sum. On main, read loads slot 0 (the total) before the source slots, and every writer added the total before the source. A total that is one ahead with kick in flight is exactly that window. No source went uncounted: every writer did both adds in one macro or one function. So the deleted check could only ever red on a torn read.

Deleting the total and the conservation check loses nothing a reader needed. Each writer is now one add to a single-writer word, so there is no second word left to disagree with. taken_here and taken_by subtract nmi from a sum over the same snapshot. They can no longer underflow, so the old saturating_sub that hid a tear is gone with it. For any one reader the sum is monotonic, because each slot's loads are coherent in order. The hard-lockup sample therefore compares like with like. The kernel's other census readers are counters.rs (Kick) and the spurious and unclaimed selftests (deliveries and deliveries_total). Each reads one slot or a per-reader sum, and none of them pairs two words.

Merge. git merge-tree --write-tree origin/main 27fc30994 exits 0 and produces tree a546ccbfb. None of main's four new commits names irq_census::TOTAL, SLOTS, sum_of_sources or the old irq_counts_here(first, second). Nothing in the tree outside issues/ parses total= on an irq: line.

Measurements. I read the orchestrator's logs in orch/irqcensus/, at HEAD, with the worktree clean:

  • build.exit and build-a64.exit: EXIT=0.
  • host.exit: EXIT=0, and the log ends Host: 75 step(s), all green.
  • guest.exit: EXIT=0, with 28 passed, 28 total and irq census: 17 guest(s) reported.
  • T14 metal/judge-irq_census.log: PASS irq_census_conservation and [metal] 1 passed, 0 failed, 1 boot(s). Of its 72 irq: cpu lines, none carries total=.

The negative control is the recorded T14 red, and the independent oracle is the real hardware. For the claim "the census cannot tear between total and sources", no test is possible: there is no total left to tear.

BLOCKER

None.

NOTE

  • tests/toyos.rs:2690 and :2770. The irq_census judge's other two cross-line checks can still red with no defect, and both should go to an issue before landing (off this task's fence). The cause is the same in each: log! "formats, then stamps" (kernel/src/log/mod.rs:179), and the capture is merged by stamp, so lines from two CPUs printing at once can appear in a different order from the order of their reads. Process exits do not serialise irq_census::log_census or tlb::log_census (kernel/src/process.rs:1067).
    • (a) The per-source monotonic check. Suppose exit X reads cpu1 before exit Y does, but X is stamped after Y. Then the capture shows a count going backwards. The check this branch rewrote has the same exposure as the total-based one it replaced.
    • (b) tlb::log_census (kernel/src/arch/x86_64/tlb.rs:34). Y loads ISSUED=T1, then X loads T2 > T1, swaps REPORTED and logs. Y's swap then returns T2 ≠ T1, so Y also logs, after X. The capture shows shootdowns=T2 then T1, which reds "the issuer census went backwards". The newest census can also exceed the last tlb line.
  • kernel/src/arch/x86_64/idt/spurious.rs:112 and idt/unclaimed.rs:164. The "took interrupts after it" check cannot fail once delivered has held. taken_before is read before send_self, and the spurious or unclaimed delivery itself raises deliveries_total past it. This predates the branch, which keeps the semantics unchanged. It should go to an issue, not be fixed here.
  • The pull request body. The gates table gives commands and exit codes but no logs. The logs exist (orch/irqcensus/{build,build-a64,host,guest}.log); the body should name where each one is.

REMOVE

None.

LAND AFTER NAMED CHANGES

Japabu and others added 2 commits October 4, 2026 22:19
…t cannot fail

Review round 1 of #734 found both off this branch's fence: the irq_census
judge's per-source monotonic and tlb issuer checks compare lines from two
exits that the stamp-merged capture can list in the other order from their
reads, and the spurious and unclaimed selftests read their total before the
probe that itself raises it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WcU2Dsw6mDYtwYfzVHPzM8
@Japabu
Japabu marked this pull request as ready for review October 4, 2026 20:24
@Japabu
Japabu enabled auto-merge October 4, 2026 20:24
@Japabu
Japabu added this pull request to the merge queue Oct 4, 2026
Merged via the queue into main with commit b75ca2b Oct 4, 2026
6 checks passed
@Japabu
Japabu deleted the wt/toyos-irqcensus branch October 4, 2026 21:03
Japabu added a commit that referenced this pull request Oct 4, 2026
…os-acpi1

tests/toyos.rs conflicted in `counters_on_metal`, in its doc and in its SMI
summary line. Both sides are kept: #728's refusal of any line stamped in the
idle second, and this branch's ACPI mode with the SMI count flat from `idle0`
to `spin`, which replaced main's legacy-mode rise.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01WcU2Dsw6mDYtwYfzVHPzM8
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