[Japabu]

Problem

A change to a user space's leaves (arch::tlb::user_change) reached the CPUs running the space through the machine-wide shootdown generation. On the T14 the 2026-11-11 stage probes put about 900 of the 3,341 ns of mem.munmap_touched_remote.4k in the shootdown (evidence):

• The initiator flushed every user translation of its own, 200 ns, in its wait. Its own wait served the generation it had issued, though it had already flushed its pages one by one (92 ns) before sending.
• The reached CPU flushed every user translation, 254 ns, for a one-page change.
• Read in the code, not seen in those rows: because the generation is machine-wide, every CPU the change did not target also owed it. Each paid a full user flush at its next lock spin or its own next shootdown's wait.

Change

The design approved in design-shootdown.md, with one change of mechanism, explained below.

• Each CPU has a mailbox (shootdown::Asks). user_change writes its range there, sets its bit in each target's asking set, sends the IPIs, and then flushes its own pages while they fly.
• A target takes every bit asking it.
  • Asked by one CPU, for at most 64 pages, it flushes that range by page: INVPCID by address with PCID, INVLPG without.
  • Asked by more than one CPU at once, or for a longer range, it flushes every user translation.
  • It then sets its bit in each asker's answered set.
• The initiator waits for its own answers only. So a CPU it does not ask owes it nothing, and it never asks itself.
• Only a flush of every user translation stamps tlb_tags, as before; a range flush does not.
• Machine-wide rounds keep the generation, unchanged: kernel-half changes (wide), PCID reclaim, MMIO, the bench, counters, SMI_CMD and the clock handover. The IPI handler, every lock spin and every initiator's wait answer both kinds, and only what they owe. So a CPU no longer flushes on an IPI that only asked it for a range.
• The 256-CPU fallback is kept. A CPU numbered past what a set holds (256) reaches every CPU by a machine-wide shootdown, as before.

The mechanism differs from the design. The design kept the global generation and put it in a per-CPU One/Many mark. With a range flush that is unsound. A target that served one initiator's range publishes a generation. That number also counts as an answer to an earlier generation of a second initiator that had not yet marked the target, whose range it never flushed.

So answers here are per pair. Each asking bit is consumed exactly once. An initiator clears its answers before it asks, and asks again only once every target has answered. So no answer stands for a later ask, and no target reads a mailbox while its owner rewrites it: the design's invariant that the outbox is not reused until the wait ends.

The approved outcomes all hold:

• per-CPU owed state, "Many" being several asking bits;
• the initiator never marks or serves itself;
• one ask flushes its range, at most 64 pages;
• the IPI is sent before the initiator's own flush;
• kernel-half shootdowns reach every CPU, wide;
• only full flushes stamp tlb_tags.

With #1251 (switch-drops-unneeded-work, in review; read at a99cd8c):

• A switch loads only what the incoming thread does not already have #1251 lets a change that frees no table skip a CPU idle on the space (Tags::changed(tag, tables, ..)). That composes as is: the ask goes only to the CPUs changed names.
• A switch loads only what the incoming thread does not already have #1251's answer loads the kernel's root on an idle CPU after its flush (leave_idle_space). This PR's ask answer (answer_ask) must do the same. Whichever of A switch loads only what the incoming thread does not already have #1251 and A user change asks each CPU running the space for its range, and owes itself nothing #1267 lands second puts leave_idle_space into answer_ask. Forgetting it fails loudly: retire's assert!(!held(tag)) fires at the first exit that has an idle holder.
• A switch loads only what the incoming thread does not already have #1251's retire asks for [0, u64::MAX), which is past 64 pages, so it is answered with a flush of every user translation, as it is today.
• With The machine's stop keeps its gate and waits for no thread #1241: this does not touch invalidation.rs.

INVLPGB stays out of scope. It is already recorded in issues/features-no-proving-machine-is-known-to-offer.md.

Checks

At a5ca5fa (review r1; the head e11ea5e only deletes one comment and adds the record's owed list), each exit 0 unless the note says red (logs). The checks at cf96bb9 are here.

• kernel-loom tlb_shootdown, 11 models. Four are new, on the ask:

  • an answered ask flushed its range after the write;
  • two asks of one CPU at once, coalescing One and Many: each initiator finds its own page gone;
  • a mailbox reused waits for its new answer;
  • each asker is answered once, with its own range.
  • counters_round and tlb_tags also pass.

• Not modelled: the order in which a waiting CPU answers before it reads its own answer lives in arch::tlb::wait_for, which loom does not compile. Its doc states it, and inspection holds it. Round 1 had two models that claimed it and could not red for it: an_initiator_answers_while_it_waits is deleted, and its ask counterpart is renamed to what it asserts.

• Negative controls, each red with its listed verdicts. Five are new and are in build/ci.rs's CONTROLS:

  • shootdown-take-relaxed: the target takes its asks Relaxed.
  • shootdown-answer-relaxed: the target answers Relaxed. This is the answer edge, the counterpart of shootdown-served-relaxed.
  • shootdown-ask-range-late: the range is written after asking.
  • shootdown-ask-stale-answers: answers are left standing across asks. This is the mailbox reuse.
  • shootdown-ask-many-as-one: two asks are answered with one range.
  • The existing shootdown-serve-relaxed and shootdown-served-relaxed still red.

• Kernel library: cargo test -p kernel --lib --features sched-check, 459 passed. It compiles neither shootdown.rs nor tlb.rs.

• Clippy in the kernel's CI shapes, with the adopted lints and -D warnings:

  • the host library with tests;
  • x86_64-unknown-none plain, with the actuators, and with every instrument;
  • aarch64-unknown-none-softfloat;
  • kernel-loom, all targets, with and without the shootdown controls.

• toyos-build's every_model_control_is_run.

• The full cargo run -- --ci host was not run, under the owner's testing policy.

• Guest run 43092270183 at the head e11ea5e, x86-64 and AArch64 together. It is queued. It shows the kernel boots and that shootdowns complete, under KVM with -cpu host:

  • virt_smp;
  • std_threads_count_the_cpus_and_give_back_ended_threads: thread stacks are unmapped while a sibling runs;
  • affinity_pins_hold_on_every_cpu;
  • a_user_copy_faults_in_mid_copy_or_ends_as_bad_address;
  • desktop_without_x2apic: four CPUs in xAPIC mode, the only row whose IPIs use the two-half ICR.

  The runs at the measurement branches (43081320048, cancelled; 43082013102, green) were for flashing and are not code-identical.

• Owed on metal, in issues/a-tlb-shootdown-reaches-only-the-cpus-that-ran-the-space.md. The benches are down, so none of it is a landing condition:

  • The T14's shared-debug boot. Main must pass test_rs_tlb_shootdown_waits: a change still waits for every CPU running the space.
  • An A/B on both benches of osbench_system and osbench_mem, main from before and after. Main after must read mem.munmap_touched_remote.4k faster, and mem.munmap_part.4k, mem.mprotect.4k and the multi-thread mem.malloc_churn.* rows no slower.
  • Each bench's cost of a flush by page (INVPCID on the T14, INVLPG on the AMD bench) against a full user flush, which decides whether BY_PAGE (64) is lowered. The branches memperf-sd-ab-base and memperf-sd-ab-head carry a probe that logs both.

• The speed-up this PR exists for is not yet measured on metal. The 900 ns of shootdown it addresses is the diagnosis probes' attribution, not a measured gain.

• Not taken, unmeasured: aligning each Mailbox to 128 bytes, so that a spinning initiator's lines are not a neighbour's. It is the first thing to try if the A/B shows the remote row gaining less than expected.

Risks

• A CPU reached for a range keeps its other translations. If it leaves the space and later re-enters it, tlb_tags still sees a change since its last full flush and flushes everything at that entry, as before. Whether that moves cost rather than removing it is for the A/B and later rows to say.
• On the AMD bench every targeted flush is INVLPG on the current space. It is correct because, without PCID, a CR3 load drops the previous space's translations (SDM Vol. 3A §4.10.4.1, APM Vol. 2 §5.5).

🤖 Generated with Claude Code

[Japabu]

Review of #1267 at cf96bb9 (base main 45935f4)

Architecture. The split is right. shootdown.rs gains a second hardware-free protocol, Asks, beside Shootdown, and kernel-loom compiles it. arch/x86_64/tlb.rs owns targeting, the IPIs, the kind of flush and the wait.

The change of mechanism is a real soundness fix. Suppose a One/Many mark carries the machine-wide generation. B marks the target first, and the target flushes only B's range and publishes generation 6. A's wait for generation 5 is then satisfied before A's mark even lands, and A's range was never flushed. Per-pair asking and answered bits remove this:

• each bit is taken by exactly one swap;
• the initiator clears its answers before asking;
• it asks again only after every target has answered.

So no answer outlives its ask, and no mailbox is rewritten while a target reads it.

All six approved outcomes hold in the code (user_change, flush_asked, answer_owed; shootdown is unchanged). Two protocols now share vector 0xFE and every spin. That is the approved shape, since machine-wide rounds keep the generation.

Size: net production is +175 lines (shootdown.rs +148, tlb.rs +25, paging.rs +2). Tests add 165 loom lines and 4 controls (+12 in ci.rs, +32 manifest lines). wait_turn goes with no caller left.

Ask/answer correctness, traced.

• No missed flush found.
  • The range and the cleared answers are stored before the Release fetch_or that sets the asking bit.
  • The target's Acquire swap takes the bit. It then reads the range, flushes, and sets its answer with a Release OR.
  • The initiator's Acquire load of that answer comes before the free.
• A target that changed spaces after it was targeted is still covered. With PCID the flush names the tag. Without PCID, the CR3 load already dropped the old space's non-global entries (SDM Vol. 3A §4.10.4.1, APM Vol. 2 §5.5). INVLPG in the new space only over-flushes.
• Freed tables: UserTables::shoot_down already widens any change that unlinked a table to [0, u64::MAX) (paging.rs:1083). That is past BY_PAGE, so a full flush drops the paging-structure caches. A by-page ask never covers a freed table.
• Nesting: an IPI inside the Asks::serve of poll or wait_for takes only bits the outer swap left. Each bit is answered by whichever serve took it.
• Deadlock: wait_for answers both protocols before it reads its own answer (tlb.rs:231-234). Every spin with IF clear (the lock, SMI_CMD, the clock handover) goes through poll, then answer_owed. The counters read sleeps in watch::wait_until, not a spin.
• One ask in flight per CPU holds. user_change runs under the space's sync::Lock with preemption off, and no interrupt handler takes a space's lock.

Memory ordering.

• x86-64. The asking fetch_or is a LOCK OR. The x2APIC send fences before its non-serializing WRMSR (apic.rs:187-195; SDM §13.12.3, APM §16.11.2). So the handler's Relaxed gate loads (owes, asking.load) read what was asked.
  • The IPI path now depends on that: before this change it called serve unconditionally (B2).
• AArch64. Nothing changes:
  • It never calls user_change; it invalidates by broadcast TLBI.
  • Asks compiles there unused; the target carries -Adead_code.
  • The counters round's Shootdown loses only wait_turn, which AArch64 never called.
  • Loom's C11 model is weaker than TSO, so the models would also hold on a weakly ordered CPU.
  • Under root's AArch64 rule, no aarch64 guest row is owed.

#1251. The composition is sound as stated, with one obligation.

• changed(tag, tables, ..) skips an idle holder only when no table goes. A change that frees tables asks [0, u64::MAX), and so does retire; flush_asked answers both with a full flush.
• leave_idle_space must go into answer_ask as well as answer. If it is forgotten, the failure is loud: retire's assert!(!held(tag)) and UserTables::drop's assert fire at the first exit that has an idle holder.
• An idle CPU reached by a by-page ask, because its idle mark raced changed, is still correct: its range is flushed, and leaving the space is extra.

Kernel half (#1211). Stack and Guard still call shootdown(origin, Half::Kernel). That issues a wide generation to every CPU, which the initiator answers wide itself and the IPI handler answers wide through serve_if_owed. Unchanged.

BY_PAGE = 64. The constant and its approved scope are unchanged, but it now carries weight on the target. A 64-page ask runs 64 INVPCID/INVLPG instructions in the target's handler, with IF clear, before it answers; before this change the target ran one full flush. Nothing measures ranges of 2 to 64 pages, because the A/B rows ask for one page. Not blocking; see S3.

Loom. The models are adequate for the protocol's safety. Each of these reds for its stated reason in the logs:

• the take's ordering (take-relaxed);
• the range written before the bit (ask-range-late);
• two asks answered with a full flush (ask-many-as-one);
• answers that do not outlive their ask (ask-stale-answers).

Gaps:

• No control covers the answer edge (S1).
• Asks to several targets, and a serve nested inside a serve, are held by inspection, which is enough.
• Two tests misstate what they check (B1).

Required

B1. kernel/loom/tests/tlb_shootdown.rs:225-268 and :574-596. an_initiator_answers_while_it_waits and the new two_cpus_asking_each_other_answer_from_their_waits claim to check that the wait answers before it asks. With wait_turn gone, that order exists only in arch::tlb::wait_for, which loom does not compile. Each test now runs the serve itself, so neither can red for the 2026-08-07 deadlock its doc cites. The commit message and the PR body also list the second as a model of the ask.

• Fix: rename and re-document each test to what it asserts. The first checks that a serve answers a generation issued while its own is outstanding. The second checks that each asker is answered once, with its own range. Alternatively, delete the first as covered elsewhere.
• Inspection of wait_for, whose doc states it, then holds the wait's order.

B2. kernel/src/shootdown.rs:121. The comment "A hint: serve carries the real ordering, so a stale false costs nothing" is now false, because serve_ipi gates on owes (tlb.rs:300-302).

• A stale false there loses the IPI, and on a halted target that ends in the DEAF_CPU panic.
• What keeps the load fresh is apic::send's ordering, as tlb.rs:297-299 says, so the two comments contradict each other.
• State both cases: a poll that reads a stale value retries, and the interrupt handler relies on the send's ordering.

B3. kernel/src/arch/x86_64/paging.rs:1076-1078. "every CPU's user translations go, paging-structure caches with them" was true while every reached CPU flushed everything. Now a range of up to 64 pages without unlinked tables is flushed page by page. Limit the clause to the case where tables went.

B4. For the orchestrator, in the PR description. The reason given for running no guest rows is false:

• The description says "TCG's x86-64 CPU has no PCID", but x86-64 guest rows do not run under TCG.
• The guest runner is x86-64 Linux with /dev/kvm (guest-rows.yml:20). There Arch::accel selects KVM and Arch::cpu boots -cpu host (build/arch.rs:142-168; tests/toyos.rs:814, "the KVM runner's CPU"). So PCID and INVPCID are live in those guests wherever the runner's CPU has them.

My judgment is that no guest row is owed. The queued metal boots exercise the ask on a PCID x2APIC machine and on a no-PCID machine, with all CPUs churning. That is stronger liveness evidence than a two-CPU q35 guest, and the description should give that reason instead. S10 names a cheap optional dispatch.

Suggestions

• S1. Add a control on the answer edge: make serve's Release OR on answered, or answered()'s Acquire, Relaxed. It is the edge the initiator's free rests on, and TSO hides it from every guest and metal test. The generation path already has its counterpart, shootdown-served-relaxed.
• S2. tlb.rs:114: Flush::All is a flush of every user translation. In the same call graph, paging::flush_tlb_all also drops global translations. A name like Flush::User removes the ambiguity.
• S3. For each bench, work out from the probe how many pages flushed one by one cost as much as one full flush (target_full cycles divided by target_range cycles per page). Record that number in the issue with the A/B results. If it is well below 64 on either bench, lower BY_PAGE or record why not.
• S4. Mailbox is 88 bytes, packed in one CpuSlice. So the lines a spinning initiator polls (asking and answered) are shared with a neighbour's mailbox, which other CPUs' asks and answers write. If the remote row gains less than expected, try #[repr(align(128))] first, as A switch loads only what the incoming thread does not already have #1251's Idle does. This is unmeasured.
• S5. paging.rs:355-358: the no-PCID claim runs on AMD, and the AMD bench takes exactly that path. Cite APM Vol. 2 §5.5 beside the SDM, here and in the PR's Risks.
• S6. shootdown.rs:209-211: "Its previous ask is answered" reads as something ask ensures. It is the caller's precondition, and the protocol's key invariant. Phrase it as one.
• S7. sync.rs:147-148 names only Shootdown::serve as surviving a nested IPI. poll now also runs Asks::serve, which survives for the reason given above.
• S8. For the orchestrator: note the leave_idle_space-in-answer_ask obligation on A switch loads only what the incoming thread does not already have #1251 too. Its description does not mention A user change asks each CPU running the space for its range, and owes itself nothing #1267.
• S10. An optional x86 dispatch, for liveness only (neither row asserts a stale translation):
  • desktop_without_x2apic: 4 CPUs in xAPIC mode. It is the only row whose IPIs use the two-half ICR, and no bench runs that mode.
  • std_threads_count_the_cpus_and_give_back_ended_threads: thread stacks unmapped while a sibling runs, under KVM.

Evidence and the A/B rule

Checks at cf96bb9. The local logs match the published evidence; exits.txt records the revision and a clean tree.

• 12 models green.
• All six controls red with their listed verdicts.
• Clippy clean in every kernel shape.
• every_model_control_is_run passes.
• The kernel library run (pure/lib.rs) compiles neither shootdown.rs nor tlb.rs, so it says nothing about this change; harmless.

The fixes asked above touch only comments and test names, so the queued metal at cf96bb9 and 1466c03 stays valid. Re-run tlb_shootdown and clippy-loom after the renames.

rule-sd.txt works as a screening rule, with gaps:

• A failed head boot is not noise. A head boot that does not pass may be this PR's defect: a tlb: cpu N has not flushed panic or a lock DEADLOCK. Investigate it before landing; do not exclude it.
• The probe costs the two arms differently. Each probe add is two RDTSCs and three LOCK XADDs on four adjacent globals, which initiator and target both write.
  • Base: the initiator's probed by-page flush runs before the IPI, and its probed self-flush runs in the wait.
  • Head: its own flush overlaps the IPI's flight.
  • Base therefore pays more probe cost per remote shootdown, and more probes overall in the multi-thread churn rows. The bias favours head, so a head regression of that size would read as no change.
  • Read the remote and churn ratios with that caveat stated. A probe-free pair would settle a marginal result.

What metal must show for LAND:

1. tlb_shootdown_waits passes on the T14's shared-debug boot.
2. Every one of the four head boots in the A/B (two per bench) passes, or each failure is shown to be independent of the ask protocol.
3. Neither bench shows an unexplained REGRESSION, by the rule, in mem.munmap_touched_remote.4k, mem.munmap_part.4k, mem.mprotect.4k or the multi-thread mem.malloc_churn.* rows; the churn rows are where concurrent asks and the full flush for several askers run. A missing gain on the remote row does not block.
4. The A/B numbers, and the probe's per-page and full-flush costs on each bench, go into the issue record.

SEND BACK. B1-B3 are small fixes to comments and test names; B4 is the orchestrator's correction to the description. With those done, LAND pending the metal results above.

[Japabu]

Re-review of a5ca5fa

Scope: whether round 1's findings are resolved, and whether the changed code is correct.

What I read:

• The diff from cf96bb9.
• In full: Asks, Shootdown::owes, arch::tlb's user_change, flush_asked, wait_for, answer_owed and serve_ipi.
• The loom file's Asked machine and the changed tests.
• build/ci.rs's control judging.
• The r1 evidence (ac9ba8114).
• The diff from a5ca5fa to the staged image 1466c03.
• Guest runs 43081320048 and 43082013102.

Round 1

• B1, resolved.
  • an_initiator_answers_while_it_waits is deleted.
  • The other test is now each_asker_is_answered_once_with_its_own_range, and its doc says what it asserts.
  • wait_for's doc (tlb.rs:220-223) states that the wait answers before it checks.
• B2, resolved. owes (shootdown.rs:121-124) separates a poll, which retries, from the handler, which relies on the send's ordering. Asks::serve's gate (:256-257) says the same, and both agree with serve_ipi's doc.
• B3, resolved. paging.rs:1076-1079 keeps the full flush for the case where tables went.
• B4, resolved. The description now says KVM with -cpu host, and gives the metal reason.
• Suggestions taken:
  • S1, the control;
  • S2, the rename;
  • S5, the APM citation;
  • S6, the precondition;
  • S7, the sync.rs note.

Changed code

• The rename changes no behaviour. All three uses changed (tlb.rs:114, shootdown.rs:271, the loom test at :423), none of Flush::All is left, and every arm flushes as before.
• ANSWER is Release unless shootdown-answer-relaxed, which only kernel-loom selects. The kernel's Cargo.toml declares the feature only for cfg checking. So a kernel build is identical to the literal it replaces.
• The control reds for its stated reason.
  • Under it, an_answered_ask_flushed_its_range_after_the_write ... FAILED with "cpu 1 answered the ask while still holding the page asked". The asker's Acquire load reads a Relaxed answer without synchronizing, so the target's re-walk need not be visible to it.
  • two_asks_of_one_cpu_are_each_answered_for_their_own_page reds on the same edge.
  • CI runs only the test the verdict names.
• The rest of the r1 evidence, at a clean tree at a5ca5fa:
  • 11 models green;
  • all seven controls exit 101;
  • every clippy shape, kernel-loom with the controls included;
  • every_model_control_is_run (build-tests, exit 0).
• The staged images stay valid.
  • In kernel/src, a5ca5fa differs from cf96bb9 only by comments, the rename and ANSWER.
  • The diff from a5ca5fa to 1466c03 shows exactly those, plus the probe and the row.
  • So the head image and the shared-debug image at cf96bb9 stand for this head. Only line numbers in panic locations differ. The base, b48f19f, is untouched.

Findings

BLOCKER

1. kernel/src/shootdown.rs:273 — redundant comment. "Release: an asking CPU that reads its answer follows the flush." repeats ANSWER's own comment (:151). The ordering at that call is now the constant's, as at TAKE's call (:258), which has no comment. Delete the line. It can ride in the record commit that LAND already requires, and nothing needs to run again.

SUGGESTION

• kernel/loom/tests/tlb_shootdown.rs:551 — the name says each asker gets its own range, but only cpu 1's is asserted. Use asks.serve(1, |what| assert_eq!(what, Flush::Range { tag: 0, start: 0, end: 1 })).
• tlb_shootdown.rs:534-537 — the doc's last sentence describes another function's order, which this test does not check. That rule's home is wait_for's doc, so the sentence can go.
• tlb.rs:222-223 — in "Answer first, then ask", ask is now the protocol's word for requesting a flush, so it reads as sending one. "Then check" says what is meant.

Guest runs

Both are queued:

• 43081320048 at the head image 1466c03: virt_smp, std_threads…, affinity_pins_hold_on_every_cpu and a_user_copy_faults…;
• 43082013102 at the base image b48f19f.

Rule

Amendment 2 of rule-sd.txt covers every point from round 1. The published copy (evidence ac9ba8114) is the same file.

For the orchestrator: its label "AMENDMENT 2, … ~21:20" is later than the commit that published it, at 21:01:48 +0200. The file was last written at 20:58. rule.txt's "~21:00" and rule-futex.txt's "~20:50" are also later than their files' write times (20:42 and 20:44). A pre-registration should carry its actual time. The rules stay valid only if every boot started after those write times.

Landing conditions

1. The one-line deletion.
2. Both guest runs green before any flash.
3. tlb_shootdown_waits passes on the T14's shared-debug boot at cf96bb9.
4. All four head boots pass, or each failure is shown independent of the ask protocol.
5. No unexplained REGRESSION in these rows:
   • mem.munmap_touched_remote.4k, mem.munmap_part.4k and mem.mprotect.4k;
   • the multi-thread mem.malloc_churn.* rows, read with the probe caveat. A marginal result is settled by a probe-free pair.
6. Into the record go:
   • the A/B;
   • each bench's probe costs per page and per full flush;
   • the BY_PAGE decision.
7. Whichever of A switch loads only what the incoming thread does not already have #1251 and A user change asks each CPU running the space for its range, and owes itself nothing #1267 lands second puts leave_idle_space into answer_ask.

SEND BACK, for the one line.

[Japabu]

Orchestrator: landing under the benches-down rule. Review r2 SEND BACK was one comment deletion, verified at e11ea5e. Guest run 43092270183 at e11ea5e (incl. affinity_pins_hold_on_every_cpu and desktop_without_x2apic, the xAPIC two-write send): success. Owed on metal recorded (tlb_shootdown_waits, A/B, the BY_PAGE probe); the speed-up is not yet measured on metal. #1267 lands before #1251, so #1251 adds leave_idle_space to answer_ask.