[Japabu]

Problem

A parked task's record lived in its home CPU's park map, inside a
CpuSched that no other CPU may touch. Whoever won the claim that ends a
park could only post Msg::Wake to the home and wait for the home's pass
to place the task. When the home was busy, a wake behind it cost three
things: an IPI to the home, a pass on the home, and a second hop and IPI to
the idle CPU that the home's place then forwarded it to. osbench's
wake.onto_busy reads 1.74x Linux's on the T14 and 1.80x on the AMD bench
(issues/a-wake-onto-a-busy-cpu-costs-toyos-1-8-times-linuxs.md).

Behaviour

• The record travels with the claim. The parking pass writes it into a
  one-owner slot on the task's TaskShared (ParkedSlot, in the
  scheduler core's one unsafe module). Only then does it move the word
  Committing -> Blocked, with release. The winner of
  Blocked -> WakeQueued takes the record. A claim made between the commit
  and the park took nothing, so the parking pass wakes the record it
  published, and keeps the task for its own pick.
• A task is sent on only once its home has saved it. Each task has an
  on-CPU word (TaskShared::on_cpu):
  • The CPU that dispatches the task sets it.
  • The switch that leaves the task clears it with release, inside
    context_switch on both architectures, once the context is saved and
    the CPU has moved onto the incoming stack. Nothing this CPU does after
    that, an interrupt included, touches the old stack.
  • A claimant reads it with acquire after winning the claim. While it is
    set, the wake goes home as Msg::Wake, which the home's next pass,
    after the switch, places. Nothing spins.
• The home keeps only its deadlines: one entry per task, with the
  park's commit generation. claim_deadline claims only the park of its
  own generation. An entry whose park another claim ended is dropped
  before the timer is armed (Due::prune), or when it falls due.
• A wake behind a busy home goes straight to an idle CPU. Each pass
  publishes which wakes would queue behind its running task
  (CpuHandle::behind), from the predicate its own placement reads
  (CpuSched::behind). A claimant whose wake would queue there takes the
  record and sends the task as an Adopt to an idle CPU in its mask. A
  boosted wake counts as RT, as its wake will lend it. The target CPU must
  be asleep and not yet rung. It is chosen the way the home's own forward
  chooses (CpuHandles::idle_near): nearest the home, a free physical core
  first, then the CPU quickest to wake. Otherwise the claimant hands the
  record back and posts Msg::Wake home, as before.
• Three claims go home whatever the home runs: a task its home still
  stands on, a claim made on the home itself, and a killed task.
• Msg::Wake carries the task's Arc<TaskShared>. handle_wake,
  handle_retire and the deadline take the record from the slot after
  their claim.

Decisions

• As approved: the record in a one-owner slot, read from published words,
  and Msg::Wake kept for the home case. Synchronous wakes are not in
  this PR.
• Amended after review r1 (orchestrator's decision): the on-CPU word
  above. It closes a window in which another CPU could resume a context its
  home had not saved, on a stack the home still stood on. Wakes claimed in
  that window keep today's two hops.
• Review r2: the clear moved after the stack switch. Interrupts can be
  open across a switch in a default build, so the clear must follow the
  stack move rather than rely on masking.
• With x86-64: FSGSBASE is taken, and the switch carries each thread's FS and GS bases #1264 (FSGSBASE). The x86-64 switch now also stores each user
  thread's GS base into its record (user_bases.gs), beside the FS base,
  at the top of Hw::switch. Every write into the outgoing record
  precedes context_switch, whose clear releases them in program order.
  Those writes are the FS and GS bases, the preempt count, the XSAVE area
  and its Left record, the pushed registers and the stack pointer. So
  the GS base is part of the context the clear publishes, and a CPU that
  resumes the task after reading the word clear loads the base its home
  saved. On AArch64, x86-64: FSGSBASE is taken, and the switch carries each thread's FS and GS bases #1264 adds only an empty UserBases.
• Rule 2 is partly implemented. Its clause for a home that has a task
  of the wake's band queued is not implemented. The claimant follows the
  home's own place, which weighs only what runs. The clause is recorded
  in issues/a-claimed-wake-ignores-a-queued-task-of-its-band-at-home.md,
  with its exit tied to the owed A/B.
• Behind is two bits, a fair wake's and an RT wake's, because the home's
  two rules read different facts. A running corpse holds neither.
• Kicker carries the clock and the trace (now, trace), because a
  claimant that hands a task on accounts for it and traces it. Machine
  keeps the rest.
• SchedMsg::send_wake is the hook: park::post_wake by default, and
  CpuHandles::send_claimed_wake for the kernel's Msg<X>.
• The record carries no deadline; the home's due set is its only home.
• TaskShared::peek_parked is an unsafe fn for the simulator alone
  (protocol-port). Only a caller that runs every CPU on one thread can
  promise that nobody takes from the slot meanwhile.
• The simulator's call-site commit shapes and their gates are removed. A
  commit can no longer publish Blocked while the task runs. The
  simulator's switch is now a step of its own, which the window above
  needs.
• The claim-token suggestion is not taken in this PR.
• The manual is unchanged. The scheduling page says nothing about where
  a parked task lives or how a wake is placed.

The simulator's finding

On this policy, before the prune,
the_two_cures_are_priced_against_the_pull_path read one wake of a halted
CPU for nothing in each of wakeup_storm(4,16) seeds 1, 5, 11 and 13
under the shipped balance path, where it requires none.

• The suspicion. I suspected a race between the timer and a kick, and
  seed 1's trace refutes that. cpu1 passed to idle at 19 ms, and its timer
  fired at 55.75 ms with no kick or IPI in between. The pass the timer woke
  found nothing to do.
• The cause. The timer had been armed for the deadline of a park that
  had already ended. The trace does not show which claim ended it. But
  only a claimant that sends a park on leaves its home such a deadline, and
  the first commit, which has no forward, kept the suite green. The waste
  was real and the forward caused it.
• The fix. The policy changed: the home drops an ended park's deadline
  before it plans a timer. All 20 seeds now read zero, and
  a_park_sent_on_leaves_its_home_no_timer reds without the prune.

One window remains, inferred from the orderings and not observed. A
claimant that read the busy word of the home's last pass, and claims after
the pass that takes the home idle has pruned, still leaves that timer
armed. It fires once. The on-CPU word does not close it, since that timer
is armed by a later pass than the switch the word orders. It is recorded,
with a candidate close, in
issues/a-wake-sent-on-as-its-home-goes-idle-can-leave-the-home-a-timer-for-nothing.md.

Checks

Evidence, all masked:

• Round 4
  is at head e1325aab6 on main 29c5f2dfa, rebased and composed with
  x86-64: FSGSBASE is taken, and the switch carries each thread's FS and GS bases #1264. It has the 14 clippy shapes, cargo test -p kernel --lib (516),
  the simulator and its control, and --ci host models (95 steps, all
  green).

• Round 3
  is at head 37b8806cc. It covers the clear moved after the stack switch,
  the clippy shapes on both targets, the kernel library, the simulator and
  its control.

• Round 2
  is at 0ae65b768, on the same main 3c5c55584. Its loom and
  --ci host models results still hold: no model source changed since.

• Round 1.

• Host: 14 clippy shapes, -D warnings with the adopted lints, all
  exit 0:

  • the kernel on x86-64 and AArch64, each with default features,
    actuators, boot actuators and instruments;
  • the kernel library with sched-check, and with controls;
  • kernel-loom and kernel-sim, each alone and with
    forward-ignores-on-cpu.

  cargo test -p kernel --lib: 506 passed. every_model_control_is_run
  passes.

• Models: cargo run -- --ci host models reads 95 steps, all green,
  exit 0. That is kernel-loom, kernel-sim and every control.

• The on-CPU word. The control forward-ignores-on-cpu makes
  on_cpu answer false. It reds three checks:

  • Unit test a_claim_before_the_homes_switch_goes_home notifies between
    cpu0's dispose_block and finish, and cpu1 must not dispatch the
    task. Red: "cpu1 ran a task its home still stands on".
  • Loom a_claim_sends_a_task_on_only_once_its_home_has_saved_it. Its
    context is a cell and its switch saves it, so a resume of an unsaved
    one is a race. cpu1 claims while cpu0 commits, parks and switches, and
    the model reaches a claim before the park, one before the switch and
    one after it. Red: "Causality violation: Concurrent write accesses to
    UnsafeCell".
  • Simulator a_claim_never_sends_on_a_context_its_home_has_not_saved
    sweeps 1,000 seeded schedules of claimed_behind_busy_home; the switch
    is now a step of its own. Red: "I11: resumed TaskKey(1) whose context
    was never saved", in 22 of 1,000 schedules.

• Blockers 2 and 3. a_task_woken_as_it_parks_with_its_mask_moved_away_is_sent_on_by_the_pick
  reds at hand_off's assert without the loaded-task rule.
  a_boosted_wake_behind_a_fair_home_goes_home reds without the boost.

• Round 1's tests and controls, still in force. Without the prune,
  a_park_sent_on_leaves_its_home_no_timer reds. A forward that takes any
  sleeping CPU reds the mask test and the one-sleeper-each test. The loom
  deadline-versus-wake model reaches both winners.

• A control removed. Round 1's parked-publish-relaxed is now green,
  so it is removed. Once a claimant takes the record only after the on-CPU
  word's acquire, commit_park's release is no longer the only edge that
  orders the record's write before the take.

• Simulator schedules moved by the step split. Two old-protocol corpus
  traces were found again and shrunk. The corpse-migration gate now sweeps
  2,000 seeded schedules; its defect is reached about once in 140.

• Guest: run 43173669251
  at e1325aab6, after the rebase onto 29c5f2dfa, is queued. Run
  43154897516
  passed all ten rows at 37b8806cc, before x86-64: FSGSBASE is taken, and the switch carries each thread's FS and GS bases #1264.
  43143253873 and 43152223133 were cancelled.

  • Its x86-64 rows are vector_state_survives_a_switch,
    std_threads_count_the_cpus_and_give_back_ended_threads,
    affinity_pins_hold_on_every_cpu, libc_children, and the two shared
    boots run whole, testcases_members_exit_0 and
    shared_debug_members_exit_0. Every switch changes, so the full shared
    boot is worth its slot.
  • Its AArch64 rows are virt_fp_isolation, virt_smp,
    virt_jobs_at_el2 and virt_mask_windows.
  • Why these rows: the change is to the scheduler core both
    architectures share, and to both architectures' context_switch. The
    rows cover parks and wakes across CPUs, affinity masks, processes
    waiting on children, and a switch's state.
  • virt_mask_windows has a known red on main
    (issues/virt-mask-windows-finds-a-mask-with-no-hook-in-a-lower-el-data-abort.md).
  • QEMU can show a crash from the old window, but it cannot show the
    window's absence; the models do that.
  • The result at e1325aab6 is not in yet.

Owed on metal

The benches are down, so this PR lands on review, host checks and guest
rows. The speed-up is not yet measured on metal. What is owed is
recorded in issues/a-wake-onto-a-busy-cpu-costs-toyos-1-8-times-linuxs.md:

• One A/B of main from before and after this PR, on the T14 and the AMD
  bench. Four boots a side, in the order B,H,H,B,H,B,B,H. The rows are
  osbench's wake.onto_busy, pingpong.*.cross_core, ipc.reqrep.*,
  wake.storm.* and energy.*. Main must read wake.onto_busy faster on
  both benches, with no other of these rows slower beyond its spread.
• A second set of the same rows with every CPU busy, where a claimant's
  scan for an idle CPU finds none and the home's placement scans again. No
  row may read slower there beyond its spread.
• A wake whose home runs a task of another band with one of the wake's
  band queued. No osbench row stages it yet, and its reading decides rule
  2's queued clause.
• The idle-exit latency per sleep depth on both benches, so that each
  bench's wake.onto_busy is split between the removed hop and the idle
  exit.

Risks

• The scan's cost. The scan for an idle CPU moves from the busy home's
  pass into the waker's context: an interrupt handler's, and a watch post's
  under its list lock. Its cost there is unmeasured, and when no CPU is
  idle the scan runs twice.
• Which wakes keep two hops. A wake claimed before its home has
  switched away from the task still takes both hops. How many wakes land
  in that window on metal is unmeasured.
• The stale-timer window above.

🤖 Generated with Claude Code

[Japabu]

Review r1 of #1274 at 15afe7813

I ran no builds or tests. reviewer.md forbids them, and the brief's request to run them does not override it. No worktree or target/ was created. Everything below comes from reading the branch against origin/main and the r1 evidence.

Architecture

The ownership move is the approved one, and it simplifies the code:

• The park map is gone.
• The claim CAS that already admitted one waker now also confers the record.
• The home keeps only (deadline, generation, key).
• The call-site commit gates are rightly deleted, because only dispose_block can construct a ParkedRecord for the kernel's Msg<X>.

The approved mechanism missed one invariant that main depends on: a task leaves its CPU only after that CPU has switched away from it. Publishing the record in the parking pass lets a remote claimant move a task whose context its home still stands on (blocker 1). The defect is in the approved design, not an implementer deviation. The fix needs something the design does not have. The orchestrator decides whether that goes back to the owner.

Size: about +1,370/−830 lines in total.

• Production core: roughly +250 net (Due, ParkedSlot, send_claimed_wake, Band).
• Simulator: roughly −250 net (the call-site gates).
• Loom: roughly +250 net. That is the new model, plus the whole-CpuSched scaffolding moved out of loom_retire.rs.
• About a dozen test kickers each gained a now/trace stub.

BLOCKERS

1. A claimant can migrate a task while its home still stands on its kernel stack.

Locations: kernel/pure/sched/cpu.rs:1325-1364, cpu.rs:1765, kernel/pure/sched/park.rs:296.

What happens:

• dispose_block publishes the record (ticket.park). The pass then carries on: settle, finish (pick, the published words including the band, the timer), charge_cpu_time, the accounting publish, and Hw::switch.
• Hw::switch writes the outgoing context into that task's record: thread_pointer, preempt, the FPU area, then sp in context_switch.
• A remote claim that lands anywhere in that window wins Blocked → WakeQueued and takes the record.
• The home's band word still reads the parking task's own band (published by the pass that dispatched it), or the band of whatever the home picks next. Either way send_claimed_wake forwards the task as an Adopt.
• The target adopts and dispatches it, and reads incoming.sp before the home has saved it.

Consequences: two CPUs run on one kernel stack, and an unsaved context is restored. The home's switch writes into a record another CPU now owns. If the task exits there first, that record may already have been released. execute's SAFETY argument, "freed only by a later pass" (kernel/src/sched/driver.rs:617), no longer holds.

The fastest route needs no IPI. A device interrupt on an idle CPU is a claimant whose own CPU still reads sleeping_unrung. It can choose itself and dispatch on the pass that follows the interrupt.

The code states this window as the invariant:

• cpu.rs:1727-1731 (dispose_block): "Sound only because … a wake for the just-parked task arrives as a message to this same CPU and cannot be processed until the next pass, which necessarily runs after the switch completes."
• cpu.rs:922-944: hand_off's assert, "this is where every migration passes". send_claimed_wake now migrates without passing there.
• kernel/src/arch/x86_64/hw.rs:303-304.
• kernel/sim/src/hw_impl.rs:213-215: "park-before-switch is safe only when nothing touches the task between the park and here."

No check in the PR can see this:

• Loom's Payload has Ctx = () and Silent::switch does nothing.
• loom_claimed_wake.rs:141 asserts the forward as correct, including interleavings in which the home's finish() has not run.
• The simulator runs a pass and its switch in one step (vm.rs:1457). That is the same blind spot the deleted blind_spot_needed_the_step_split documented for the commit.

What is needed: a claimant must not move a record whose home has not yet switched away from it. One direction: hand such a claim home as Msg::Wake, whose next pass runs after the switch. The claimant would know this from a word the home publishes after the switch has saved the context, if that word still names the task. Any other mechanism that keeps claimants out of the window would also do.

Cheapest red test: in cpu.rs's World, call notify_from_afar between cpu0's dispose_block and finish, run cpu1's pass, and assert that cpu1 does not dispatch the task. That is red today. Also make the simulator's switch its own step, so that I11 ("resumed … whose context was never saved") can fire.

2. Parked::WokenFirst can panic the kernel when the task's mask has changed.

Path: cpu.rs:1765 → cpu.rs:1065 → cpu.rs:944.

WokenFirst sends the task its CPU still stands on through place. If the task's mask no longer names this CPU, place_behind relocates it: relocate → hand_off. hand_off's assert task.key() != loaded_key() then fires.

Userland can reach this. A thread blocks; a set-affinity that excludes its CPU races with it, and a wake lands between WaitTicket::commit() and ticket.park().

Main never routed the loaded task through place. AlreadyWoken kept it running, and the pick sends a masked-out loaded task to outbound (cpu.rs:2051).

Fix: put a woken-first task in the run queue, or the dying list if it was killed, and leave it to the pick's existing loaded-task handling. Add a unit test that changes the mask between commit and park.

3. The woken task's band is read before its wake applies the boost. (cpu.rs:1335-1339)

For a boosted cause, BlockedTask::wake lends RT (task.rs:1267), so is_rt() changes after the decision has been made. Two consequences:

• A boosted wake of a fair thread behind a fair home is forwarded to an idle CPU and pays an idle exit. The approved rule 1 says "RT waking behind fair: post Wake to h". Today the home runs such a wake at once by preempting.
• Behind an RT home, the same wake goes home and takes the two hops this PR exists to remove.

This is the audio lend path.

Fix: classify the task as RT if record.task.rt().is_rt() || cause.boost.is_some(). Add a test for a boosted wake behind a fair home.

4. Comments the change made false. Each is a contract a reader relies on:

• cpu.rs:1727-1731: the dispose_block doc (see 1).
• cpu.rs:922-933: says "every migration passes" through hand_off, and its argument names the old parked map.
• kernel/pure/sched/timer.rs:3-12: "A deadline lives in exactly one place: the ParkedEntry … There is no separate index." Due is an ordered index, a deadline is also stored in ParkedRecord::deadline, and entries outlive their parks by design.
• kernel/pure/sched/task.rs:976: BlockedTask "Exists only inside a ParkedEntry in CpuSched.parked".
• task.rs:148: WakeQueued "a Wake message is queued to the home CPU". A claimant may be holding the task mid-forward.
• kernel/pure/sched/hw.rs:73-76: Kicker is "The one effect a wake path needs … the targeted kick IPI".
• kernel/src/trace.rs:12: "is Machine::trace".
• kernel/sim/src/hw_impl.rs:52-53: "the only thing [Machine::now] is read for".
• kernel/sim/src/vm.rs:1370-1380: describes the old residual window (the commit publishing Blocked, Msg::Wake landing behind the drain, RunningTask::park accepting WakeQueued). The injected claim now lands on Committing and ends in WokenFirst.
• kernel/pure/sched/msg.rs:8-9: "single #[allow(unsafe_code)] island stays exactly the intrusive-list code". ParkedSlot now lives there, and there are unsafe blocks at cpu.rs:1136, cpu.rs:1324 and park.rs:295.
• cpu.rs:170-171: prune means "a timer is never armed for one". The new issue file records the case in which one is.

Evidence

• The r1 evidence covers 228b2aa83:
  • Thirteen clippy shapes, cargo test -p kernel --lib and every_model_control_is_run, all rc=0.
  • --ci host models: 93 steps, rc=0.
  • Each control has its diff and log.
• 15afe7813 differs from 228b2aa83 only in issue records and two comments, so the reuse holds.
• What the evidence establishes:
  • The record handover's ordering: loom, with the parked-publish-relaxed control red.
  • The prune: unit test, with its control.
  • The mask and ring choice: unit tests, with their control.
• It cannot establish the absence of blocker 1, and its loom model asserts the defective forward as expected behaviour.
• Guest run 43143253873 is still queued. Its result is owed before landing. Being QEMU, it could at most crash on blocker 1 now and then; it cannot clear it.

On the questions asked

• Ownership transfer. Apart from 1 and 2, it holds:
  • The slot is written before a release CAS and taken after an acquire claim. A hand-back is ordered by the mailbox post.
  • Kill: whichever CPU places the task reads the sticky bit. The home's retire correctly drops while the word names the home.
  • Deadline against wake: the claim checks the generation (loom model 2).
  • The home's own wake: runs_on sends a Wake to itself, which the next pass handles.
• Stranding. None:
  • A target that went busy drains the Adopt, then forwards or queues it.
  • A mask changed after the claimant read it is refreshed by the adopter, which relocates the task.
  • realign kicks whichever CPU the word names.
  • One hazard is not new in kind but now reaches claimant forwards too: a CPU that stopped mid-idle (forward_target's doc).
• Lock and IPI order. Post, then ring, then kick. Under a watch post, Deferred still holds kicks until the list lock is let go. An Adopt to a sleeper is always run, by the doorbell protocol.
• Policy. It follows the home's place (running band only). It does not implement the design's rule 2 clause "or publishes a queued task of that band". Besides 3, a running corpse is published as its own band, while the home's behind_fair excludes it.
• Scan cost. Bounded: O(CPUs × SMT siblings) acquire loads, no waits, no locks taken. But it now runs:
  • inside the watch's list lock, once for every waiter a post wakes;
  • in interrupt context;
  • twice when no CPU is idle: the claimant's scan finds nothing, and the home's place then scans again.
• Stale-timer window. Acceptable to defer on its merits. It costs one spurious timer interrupt, never a missed deadline (invariant T bounds the arming from above), and the record has an exit. The fix to 1 reopens the same orderings, so reassess it there rather than adding SeqCst now.
• Manual. I agree no sentence is needed. The scheduling page says nothing about where a parked task lives or how many hops a wake takes.

SUGGESTIONS

• Claim token. Make the claim CAS return a linear token whose consumption takes the record, with the hand-back carried by the message. The three unsafe call sites and the runtime assert "a park taken without its claim" (cpu.rs:1138) then become types.
• One band predicate. Publish the band with the predicate place_behind uses (a corpse is not fair-band work; behind_rt reads is_rt), as one function both call, so the claimant and the home cannot drift apart.
• Drop ParkedRecord::deadline (msg.rs:36). Its only use is take_parked's is_some() before due.remove(key). Removing by key unconditionally is correct, because any entry left then is this park's or a stale one. The deadline then has one home, the Due.
• Price the doubled scan. Add a row to the owed A/B in which every CPU is busy.

PR description (for the orchestrator)

• "rules 1 to 3 … as approved": rule 2's queued clause is not implemented, and rule 1 is broken for boosted wakes (3).
• "A commit can no longer publish Blocked while the task runs": true, but the record can now be moved while the home still stands on its context (1).

SEND BACK

[Japabu]

Response to review r1 at 0ae65b768

Blocker 1: a claimant moved a task its home still stood on. Fixed, under
the orchestrator's amendment to the design.

• The word. Each task has an on-CPU word, TaskShared::on_cpu. The CPU
  that dispatches the task sets it, in switch_to_current.
• Where it is cleared. Inside context_switch on both architectures,
  right after the outgoing stack pointer is stored and before the stack
  moves:
  • x86-64 uses a plain byte store. x86-64 does not reorder a write with
    older writes (SDM Vol. 3A §11.2.2, 325384-093US), and the FPU save,
    thread pointer and preempt count are ordinary writes made before the
    call. Nothing touches the old stack after the clear: interrupts are
    masked, and NMI, #MC, #DF and #DB run on IST stacks.
  • AArch64 uses STLRB. Its FP state is stored on the outgoing stack
    before the stack pointer, so it is ordered too.
• How the switch knows the word. RunToken::left_ptr carries the
  outgoing task's word, and the CPU keeps the loaded task's word beside
  loaded_ctx.
• The claimant. send_claimed_wake reads the word with acquire after
  winning the claim, before it touches the record. If the word is set, the
  wake goes home as Msg::Wake. If it is clear, the claimant may send the
  task on. Nothing spins.
• The red test. a_claim_before_the_homes_switch_goes_home is the test
  you described: notify between cpu0's dispose_block and finish, and
  cpu1's pass must not dispatch the task. The control forward-ignores-on-cpu
  reds it with "cpu1 ran a task its home still stands on". The test world
  now runs every pass's switch.
• Loom. The model's context is a loom cell. Silent::switch saves it,
  clears the word, and resumes the next context. In
  a_claim_sends_a_task_on_only_once_its_home_has_saved_it, cpu1 claims
  while cpu0 commits, parks and switches, and then dispatches what it was
  sent. The model reaches all three outcomes: a claim before the park, one
  before the switch, and one after it. Under the control it reds with
  "Causality violation: Concurrent write accesses to UnsafeCell".
• Simulator. A pass's switch is its own step, Step::Switch, with
  interrupts masked. The existing scenarios never reach the window. In
  them, either the wake comes from a device interrupt while no time passes,
  or no third CPU sleeps. claimed_behind_busy_home stages the window. Under
  the control it hits I11 ("resumed TaskKey(1) whose context was never
  saved") in 22 of 1,000 seeded schedules. With the rule,
  a_claim_never_sends_on_a_context_its_home_has_not_saved sweeps 1,000
  seeded schedules clean.
• Comments. dispose_block's contract, hand_off's argument, x86's
  Hw::switch note and the design note now state the invariant.

Blocker 2. Fixed in wake_parked, for any woken task its CPU still
stands on. Such a task goes to the run queue, or to the dying list if it was
killed, and the pick sends it on as on main. A woken-first park is the only
case.
a_task_woken_as_it_parks_with_its_mask_moved_away_is_sent_on_by_the_pick
changes the mask between commit and park. With the old path it panics at
hand_off's assert.

Blocker 3. Fixed: the claimant classifies the wake as RT when
rt().is_rt() || cause.boost.is_some(). a_boosted_wake_behind_a_fair_home_goes_home
fails without it.

Blocker 4. Every listed comment is fixed. I also fixed the remaining
mentions of the old park map in finish, a cpu.rs test, two loom_retire
model docs and the sched-check feature note.

Suggestions.

• One band predicate: taken. Behind { fair, rt } is computed by
  CpuSched::behind, which place_behind reads and each pass publishes for
  claimants. It is two bits rather than one band, because the home's two
  rules read different facts (running_is_fair for a fair wake, is_rt for
  an RT one), and the predicate keeps both exactly.
• Drop ParkedRecord::deadline: taken. take_parked removes the
  task's due entry by key.
• Claim token: not taken this round. It would turn the three unsafe
  take and publish sites and take_parked's assert into types, but it
  reshapes notify's return and every SchedMsg. I kept this round to the
  blockers.
• Price the doubled scan: taken. It is a row of the owed A/B with every
  CPU busy.
• Stale-timer window: reassessed, unchanged. The on-CPU word orders a
  claimant after the switch that left the task. The stale timer is armed by
  a later pass, the one that takes the home idle, so the window stands as
  recorded.

One control removed. parked-publish-relaxed no longer reds. A claimant
now takes the record only after the on-CPU word's acquire, whose release
follows the record's write, so commit_park's own release is no longer the
only ordering edge.

PR description. Rule 2's queued clause is now named as not implemented:
the claimant follows the home's place, which weighs only what runs.

Moved by the step split.

• The corpus's two old-protocol traces were found again and shrunk:
  old_steal_port seed 5 for I8, and old_migrate_kept_the_corpse seed 135
  for I14.
• The corpse-migration gate now sweeps 2,000 seeded schedules. Its defect is
  reached about once in 140 seeded schedules and once in 3,000 PCT ones. A
  boosted wake whose claimant may send it on now never reaches hand_off.

Checks and evidence: round 2: 14 clippy shapes, cargo test -p kernel --lib (506) and --ci host models (95 steps, all green, the three new controls among them) at 0ae65b768. Guest run 43152223133 is queued at that head.

[Japabu]

Review r2 of #1274 at 0ae65b7

Scope: round 1's blockers and their fixes. I read the r2 commit, every file it changes, the r2 evidence, and the callers and entry paths named below. I ran no builds or tests.

Assessment

The amended mechanism has the right shape and stays small:

• one word per task, set at dispatch and cleared by the switch;
• one acquire load by a claimant that has already won the claim;
• a Msg::Wake home while the word is set.

Nothing spins. The only new CpuSched state is the loaded task's word pointer. The protocol holds in all three models.

The kernel's placement of the clear does not hold. The clear publishes the context before the CPU has left the outgoing stack. The argument that nothing uses that stack in between assumes interrupts are masked, and in a default build they are not (B1).

Blockers 2 and 3 are fixed correctly, and each test reds under its control. Round 2 is +673/−293 over 27 files. About 110 of cpu.rs's added lines are the three new unit tests and the test world's switch.

BLOCKERS

B1. kernel/src/arch/x86_64/switch.rs:25-30, kernel/src/arch/aarch64/switch.rs:77-81: the on-CPU word is cleared before the stack moves, while a maskable interrupt can still be taken on the outgoing stack.

• The comments are false. x86's says "interrupts are masked" (switch.rs:13-15); AArch64's says "IRQ and FIQ are masked" (switch.rs:34-35). Neither holds in a default build:

  • The IrqGuard::close() in both Hw::switch bodies is #[cfg(feature = "mask-windows")] (x86_64/hw.rs:310-313, aarch64/hw.rs:73-76). 0e148b1 added it for that build alone.
  • block_on → pass_block → execute → HW.switch runs inside a syscall, which opens interrupts before dispatch (x86_64/syscall.rs:116, aarch64/trap.rs:324).
  • exit_to_user opens interrupts before do_preempt (scheduler.rs:193).
  • preempt::disable only raises a count.
  • AArch64's context_switch saves the live DAIF because it can be open.

• Where such an interrupt runs. A timer, device, kick or shootdown interrupt can arrive at the boundary after mov byte ptr [rdx], 0 or stlrb wzr, [x2]. It then runs on the outgoing stack:

  • On x86, only vectors 1, 2, 8 and 18 have an IST (idt/mod.rs:242-259). The Ring 0 path of timer_entry pushes onto the current stack.
  • AArch64 runs at EL1 on SP_EL1 (control_regs.rs:144). Every vector begins sub sp, sp, #frame; stp x0, x1, [sp] (trap.rs:482-488).

• Consequence. A claimant that read the word clear may already have sent the task on, and the target resumes it. The task's frames then grow down from the saved stack pointer into the region where the home's interrupt frame lives. That is the two-CPUs-on-one-stack fault blocker 1 was meant to close. The window is now one instruction boundary plus a handler's run time. Either the home's iretq/eret frame or the task's stack is corrupted.

• What does hold. The IST argument for NMI, #MC, #DF and #DB on x86 is correct, and it stops mattering once the clear moves. No model can see this defect: loom, the simulator and TestHw all clear the word inside an atomic switch.

• Fix. Clear the word after the stack switch, on the incoming stack:

  • x86: move test rdx, rdx / jz 2f / mov byte ptr [rdx], 0 / 2: after mov rsp, rsi, still inside switch_save!, so the witness build's call cannot clobber rdx.
  • AArch64: move cbz x2 / stlrb wzr, [x2] after mov sp, x1.

  Every save still precedes the release in program order. Nothing the home does afterwards can reach the old stack, whatever is masked. Each comment then needs only that one fact; the IST and SError enumerations go. Masking interrupts across every switch would also close the window, but it would change what every saved context carries.

• Evidence owed.

  • The changed assembly compiles on both targets: the existing clippy shapes.
  • The guest rows that already cover a switch's state (vector_state_survives_a_switch, virt_fp_isolation, virt_smp) pass at the new head. Run 43152223133 tests the current assembly.

B2. Comments this round made false or unreadable.

• kernel/pure/sched/cpu.rs:48-50, RunToken: the keys let a driver work "without dereferencing the pointers — which is what keeps the simulator free of unsafe". SimHw::switch now dereferences left (kernel/sim/src/hw_impl.rs:232).

• kernel/sim/src/lib.rs:21-23 says "Three exemptions … Nothing here dereferences a raw pointer." There are now four allow(unsafe_code) sites:

  • vm.rs:561 (peek_parked);
  • vm.rs:1465;
  • hw_impl.rs:210;
  • payload.rs:64.

  The simulator also dereferences a raw pointer now.

• kernel/pure/sched/cpu.rs:181, Due::prune: "A claim that lands after this reads the word arms it all the same." The sentence does not parse, and a claim arms nothing. It should say that a park ended after the prune's read leaves its deadline armed.

• kernel/sim/tests/scenarios.rs:199-202:

  • PCT's rate is an investigation figure for a sampler the gate no longer runs.
  • "a boosted wake whose claimant finds the CPU it may leave" does not parse.

  Keep the seeded rate that sizes CORPSE_SEEDS. The rest is already in the commit message and the evidence.

• The two switch.rs comments are covered by B1.

SUGGESTIONS

• S1. kernel/sim/src/vm.rs:226 and :887 give "interrupts masked" as the model's reason. That restates B1's premise. Say instead that the model takes a switch as one step; after B1's fix that abstraction is sound without the claim.
• S2. kernel/pure/sched/task.rs:390-391: dispatched says the set is ordered before the park "by that CPU's own order". What carries the set to a claimant is the claim's acquire of the word that begin_commit and commit_park release. Naming that edge would state why no claimant reads a previous run's clear.
• S3. The pre-existing "Every context is saved masked" comments (x86_64/hw.rs:310, aarch64/hw.rs:73) read as unconditional but describe only the mask-windows build. They probably misled this fix. Scoping them to that build costs one word each.
• S4. The body discloses rule 2's unimplemented queued clause, but no issue record holds it. If the clause is still wanted it needs a record with an exit. If it is dropped, the body's statement suffices. The orchestrator decides which.

On the questions asked

1. Is the window sound?
   • Is every byte the switch writes stored before the clear becomes visible? Yes, on both architectures.
     • x86-64: thread_pointer, preempt, the XSAVE area (ordinary write-back stores, fpu.rs:26-30), the pushes and mov [rdi], rsp all precede the byte store in program order. TSO keeps stores in that order.
     • AArch64: the frame, the FP/SIMD registers, FPCR/FPSR, DAIF and the sp store all precede STLRB, which orders them.
   • Does anything run on the old stack after the clear? It can, on both architectures (B1). x86's NMI, #MC, #DF and #DB use IST1-4, which idt/mod.rs:286-289 checks at compile time. Maskable interrupts use no IST on x86, and AArch64 has no equivalent.
   • Can a claimant read a stale clear from the task's previous run? No.
     • A previous clear happens-before the next set. On one CPU that is program order. Across CPUs it is a claimant's acquire followed by the Adopt post and drain, or a steal's Adopt.
     • The set is sequenced before begin_commit's AcqRel CAS, and commit_park is AcqRel too. The claim's acquire reads from that release sequence.
     • So the set happens-before the claimant's load, and coherence forbids that load returning the older clear.
   • Is the set at dispatch ordered before any park on that CPU? Yes: by program order, and it reaches other CPUs as above. Action::Resume neither sets nor clears the word, which is correct.
2. Do the models and controls hold?
   • Loom: does Ctx now see an unsaved context, and does the control fail for that reason? Yes.
     • ModelCtx is a loom cell, and both the save and the resume write it.
     • Under the control, the only access left unordered is KEY's context. The slot's take stays ordered by the claim.
     • So the "Concurrent write accesses" red comes from the unsaved context. The log does not name the cell, but the inference holds.
   • Simulator: does the switch step reach the window? Yes.
     • Step::Switch lets cpu2 pass and resume KEY before cpu0 takes its switch step.
     • The control's log reds at seed 36 with I11.
     • The count of 22 in 1,000 appears only in the README, not in a log. The test needs only one red, so the count is informational.
   • Does the unit test exercise notify-from-afar between dispose_block and finish? Yes.
     • notify runs between them, and TestHw::runs_on answers false.
     • cpu0's published word still reads fair, so without the on-CPU word the claim would go to sleeping cpu1.
   • Was removing parked-publish-relaxed right? Yes. A control for the record's own ordering is no longer owed.
     • The record is written before the clear.
     • A claimant touches the slot only after reading the clear with acquire.
     • A claimant that reads the word set never touches the slot.
     • The commit's release is also not the only edge for the set, since begin_commit's release heads the release sequence the claim reads from.
     • The loom model sets the word before the claimant thread exists, so it could not test that edge anyway. S2 covers the comment.
   • Is the corpse-migration gate sound? Yes.
     • Its seeds are fixed, so the gate is deterministic.
     • At about 1 in 140, 2,000 seeds give about 14 catches; the evidence shows 22 in 3,000.
     • If that rate holds, a future renumbering would leave zero catches with probability around e^-14 (an inference).
     • Dropping PCT loses nothing measurable at 1 in 3,000.
3. Are blockers 2 and 3 fixed, with the right tests? Yes.
   • Blocker 2: wake_parked keeps a woken task its CPU still stands on for the pick, or puts it on the dying list if killed. After the switch, the pick's existing loaded-task rule sends a masked-out task on. The test changes the mask between commit and park, and its control reds at hand_off's assert.
   • Blocker 3: rt().is_rt() || cause.boost.is_some() matches what BlockedTask::wake makes is_rt(). wake calls boost (task.rs:1294-1296), which sets inherited. The test reds without the fix.
   • Behind is now one predicate. place_behind reads it, and each pass publishes it for claimants.
4. Are the comments true, and does the body match the change?

   • Comments. Round 1's listed comments are fixed and true, except Due::prune's replacement (B2). New false comments are listed in B1 and B2.

   • Body. It is accurate on:

     • rule 2's unimplemented clause: place passes queued_ahead = false, and only place_settled weighs the queue;
     • the stale-timer record: the window stands, because the timer is armed by a later pass than the switch the word orders;
     • what is owed on metal: it matches the issue file, including the every-CPU-busy set.

     After B1's fix, "once the outgoing stack pointer … is stored" becomes "after the stack has moved". The author's response says "interrupts are masked", which is false in default builds.

   • Evidence reuse. Between the old base d1cefba and 3c5c555, main changed nine files, none under kernel/ or build/. The pre-rebase control runs therefore hold for 0ae65b7.

SEND BACK

[Japabu]

Response to review r2 at 37b8806cc

B1: fixed. You were right. My round-2 response's "interrupts are
masked" holds only in the mask-windows build. On both architectures the
clear now follows the stack move:

• x86-64: mov rsp, rsi, then test rdx / jz / mov byte ptr [rdx], 0.
  It is still inside switch_save!, so the witness build's call cannot
  clobber rdx.
• AArch64: mov sp, x1, then cbz x2 / stlrb wzr, [x2].

Each comment now states only that fact: the context is saved and the stack
left, so nothing this CPU does afterwards touches either. The IST and
SError lists are gone. x86's Hw::switch note now says the claim's word is
cleared only once the CPU has left the stack.

B2: fixed.

• The simulator dereferences no raw pointer again. Its switch step
  clears the word by key once SimHw::switch has run
  (TaskShared::left_cpu, protocol-port). RunToken's note holds as
  written, and now names the on-CPU word among the driver's bookkeeping.
• Crate note. sim/src/lib.rs counts four exemptions, round 1's
  Vm::parked_record among them.
• Due::prune. It now reads: "A park that a claim ends after this read
  leaves its deadline armed."
• The corpse gate's note. It keeps only the seeded rate that sizes
  CORPSE_SEEDS.

Suggestions.

• S1: taken. The step is described as the model taking the switch as
  one step.
• S2: taken. dispatched names the claim's acquire of the word that
  begin_commit and commit_park release after the set.
• S3: taken. Both "every context is saved masked" comments now begin
  "Under mask-windows".
• S4, the orchestrator's decision.
  issues/a-claimed-wake-ignores-a-queued-task-of-its-band-at-home.md
  records the unimplemented queued clause. Its exit is tied to the owed
  A/B: implement the clause if a wake behind a home running another band,
  with its own band queued, waits longer than one sent to an idle CPU. No
  osbench row stages that case yet, so the A/B owes one; the wake-onto-busy
  record and the body say so.

Checks (evidence round 3):

• 14 clippy shapes on both targets, all exit 0.
• cargo test -p kernel --lib: 506 passed.
• cargo test -p kernel-sim: green.
• The simulator's forward-ignores-on-cpu control still reds with I11.
• Loom is unchanged since round 2.

Guest: run 43154897516
at 37b8806cc is queued, with these rows:

• vector_state_survives_a_switch, virt_fp_isolation and virt_smp;
• the earlier five;
• testcases_members_exit_0 and shared_debug_members_exit_0.

43152223133, which tested round 2's assembly, was cancelled.

[Japabu]

Review r3 of #1274 at 37b8806

Scope: review r2's findings only. I read 37b8806's diff, the files it touches, the author's response and the r3 evidence. I ran no builds or tests.

B1: the clear after the stack switch — resolved

• x86-64 (switch.rs:18-30). The sequence is now push … / mov [rdi], rsp / mov rsp, rsi / test rdx, rdx / jz 2f / mov byte ptr [rdx], 0 / 2:.
  • Saves before the release. In program order the caller's saves (thread_pointer, preempt, the XSAVE area), the pushes and the rsp store all come before the byte store. TSO keeps that order.
  • rdx still holds left. It is the third SysV argument, and nothing between entry and the clear writes it.
  • The witness build. mov rdi, rsp / call {verify} follows the macro, so the clear runs before the call can clobber rdx.
  • Nothing reaches the old stack after the clear. An interrupt taken between mov rsp, rsi and the clear lands on the incoming stack below its frame, as it did on main. Any handler taken earlier on the old stack has returned before the next instruction runs.
• AArch64 (switch.rs:76-80). The sequence is now str x9, [x0] / mov sp, x1 / cbz x2, 2f / stlrb wzr, [x2] / 2:.
  • x2 still holds left. The save half uses only x9 and x10.
  • Saves before the release. STLRB orders every earlier load and store, including the frame and the FP/SIMD stores.
  • Nothing reaches the old stack after the clear. Any exception from here on is taken on SP_EL1, which now points at the incoming stack.
• The incoming side does not depend on the word. On both architectures it reloads its own frame from the new stack pointer and never reads the outgoing task's word. Action::Resume excludes outgoing == incoming. The incoming loads may complete before the release becomes visible. That is harmless, because this CPU already owns that frame.
• Comments. Each now states only that the context is saved and the stack left. Both "every context is saved masked" notes are scoped to mask-windows, and the x86 Hw::switch note is true.

B2: the comments — resolved

• RunToken and the simulator's crate note (cpu.rs:48-50, sim/src/lib.rs:21-25) are true again.
  • The simulator clears the word by key in Vm::switch (vm.rs:1467-1479), so SimHw::switch dereferences nothing.
  • There are four allow(unsafe_code) sites, matching the note: hw_impl.rs:207, vm.rs:561, vm.rs:1467 and payload.rs:64.
  • peek_parked is an unsafe fn call, not a raw-pointer dereference in the simulator.
• Due::prune (cpu.rs:181) now says what the issue record says.
• The corpse gate's note (scenarios.rs:199-201) keeps only the seeded rate that sizes CORPSE_SEEDS.
• The r2 suggestions. S1's and S2's wording (vm.rs:226-229, vm.rs:887, task.rs:390-393) is accurate.

left_cpu and the simulator's fidelity

The simulator stays faithful to the protocol:

• Same task. The kernel clears the word of loaded_on_cpu, and RunToken::outgoing comes from the same loaded in switch_to_current/switch_to_idle. Clearing by outgoing() therefore clears the same task's word, null and None included.
• Same order. The clear follows the I11 shadow's save within the one switch step, which is the order the kernel now keeps.
• The lookup cannot miss. Vm::shared is only ever inserted into, so the key is always present.
• What the simulator no longer exercises, and what does. It no longer exercises left_ptr. The unit-test TestHw::switch and loom's Silent::switch still clear through it, and the forward tests would go red if loaded_on_cpu named the wrong word: the outgoing word would stay set, and the wake would go home.
• The control still reds at this head. test-sim-control.log shows rc=101, seed 36, I11.
• The new method is test-only. left_cpu is protocol-port-only, like peek_parked, so no kernel build carries it.

Evidence

• r3's host checks ran at 37b8806 with a clean tree:

  • 14 clippy shapes on both targets;
  • cargo test -p kernel --lib, with 506 passed;
  • every_model_control_is_run;
  • cargo test -p kernel-sim.

  All passed with rc=0. The simulator control exits 101, as required.

• Loom was not rerun. That is sound, with one correction to the evidence README: the loom crate's shared pure/sched sources did change, but only in comments and in left_cpu. Loom does not enable protocol-port, so left_cpu is compiled out there, and clippy-loom compiled the crate at this head.

• No model sees where the clear sits within the switch. Inspection settles the placement. Guest run 43154897516 is the run check; it is pending, and you are judging it.

Body and records

• The body now describes the clear after the move onto the incoming stack, and points to the new record for rule 2's queued clause.
• issues/a-claimed-wake-ignores-a-queued-task-of-its-band-at-home.md (track, open) states the gap correctly: place passes queued_ahead = false. It names an exit and an owner.
• The wake-onto-busy record names the A/B's third case. One of its lines is left unwrapped; I am not asking for a change.

No blockers remain from r2, and no new ones.

LAND

[Japabu]

Rebase onto main 29c5f2dfa: what composed where

e1325aab6 is the r3 LAND head 37b8806cc rebased onto 29c5f2dfa. The
rebase was clean. Main and this PR both changed the x86-64 and AArch64
hw.rs, pure/sched/cpu.rs and sched/driver.rs; main's side is #1264
(FSGSBASE).

The switch, x86-64. #1264 stores each user thread's GS base into its
record ((*save).user_bases.gs) beside the FS base, at the top of
Hw::switch. This PR clears the on-CPU word inside context_switch, after
mov rsp, rsi. These writes into the outgoing record precede that clear in
program order:

• the FS and GS bases;
• the preempt count;
• fpu::leave's XSAVE and its Left record;
• the pushed registers and the stack pointer.

They are all ordinary write-back stores, and x86-64 does not reorder a write
with older writes (SDM Vol. 3A §11.2.2). So the clear publishes the GS base
with the rest of the context. A CPU that resumes the task after reading the
word clear finds the base its home saved: it compares that base with its
own per-CPU cache and writes the MSR if they differ. Nothing writes the
outgoing record after the clear. On the incoming side, #1264 writes CPU
registers and the per-CPU cache, not the outgoing record.

AArch64. #1264 adds only an empty UserBases. The thread pointer, the
frame and the FP state are stored before the STLRB, as before.

driver.rs and cpu.rs. Main's changes are #1264's
UserBases::INITIAL in the idle and spawn contexts, and one comment in
cpu.rs. Neither touches the word.

Checks at e1325aab6 (evidence round 4):

• 14 clippy shapes on both targets, all exit 0.
• cargo test -p kernel --lib: 516 passed.
• cargo test -p kernel-sim: green.
• The simulator's control still reds with I11.
• --ci host models: 95 steps, all green; the three on-CPU controls reach
  their verdicts.

Guest: run 43173669251
at e1325aab6 is queued, with the same ten rows.

[Japabu]

Review r4 of #1274 at e1325aa (composition with #1264)

Scope. This round reviews only how the rebase composes with #1264 (FSGSBASE). git range-diff 3c5c55584..37b8806cc 29c5f2dfa..e1325aab6 shows commits 1–6 unchanged (=). Commit 7 changes only in its context lines: #1264 rewrote the SAFETY comment that sits beside x86_64/hw.rs's edited hunk. #1274's own diff is the r3 diff, so r3's findings and its growth accounting still stand.

Architecture. Nothing moves. #1264 adds two kinds of state to the switch: a per-task record field (KernelCtx.user_bases) and two per-CPU value caches (PerCpu.fs_base, PerCpu.user_gs_base). Each cache describes the register of the CPU it lives on and is not tied to any task. Either kind composes with forwarding on its own terms.

Checked

Every store into the outgoing record comes before the clear.

• x86-64 (kernel/src/arch/x86_64/hw.rs:335-397, switch.rs:16-31). The switch writes these into *save, in order:

  • thread_pointer and user_bases.gs (lines 338 and 341, x86-64: FSGSBASE is taken, and the switch carries each thread's FS and GS bases #1264);
  • preempt (347);
  • fpu through fpu::leave, whose XSAVE writes the area above the stack top (395);
  • the pushed frame, then [rdi] = rsp;
  • after that come mov rsp, rsi and mov byte ptr [rdx], 0.

  percpu::set_fs_base and set_user_gs_base write this CPU's PerCpu, not the record. After the clear, CPU A pops the incoming frame and returns into the incoming task's own continuation. That continuation reads only its own save and area, and the RunToken has no Drop. Under switch-witness, switch_witness_verify runs after the clear. It dereferences only shadow.ctx, which is the incoming record, and prints shadow.save as an integer without dereferencing it. TSO orders all of this before the clear. The XSAVE stores are not an SDM write-ordering exception either; even fast-string stores are ordered before a later discrete store.

• AArch64 (kernel/src/arch/aarch64/hw.rs:79-112, switch.rs:45-80). The switch writes thread_pointer and preempt into the record at the top. The callee-saved registers, DAIF and the q0–q31/FPCR/FPSR state go onto T's stack, then str x9, [x0], mov sp, x1 and stlrb wzr, [x2]. STLRB orders all earlier loads and stores, including the SIMD stps. x86-64: FSGSBASE is taken, and the switch carries each thread's FS and GS bases #1264's UserBases is a ZST here and adds no store.

No reader assumes the task stayed on its CPU.

• The only readers of the per-CPU caches are the incoming comparisons at x86_64/hw.rs:371 and :375. Both compare the cache, which is exact at every switch-in, against the incoming task's saved value. The cache can be exact without belonging to that task: every switch away from Runs::User refreshes it from the register before the comparison, and idle never changes either register. The cache answers "does this CPU's register already hold this value?", which is correct whoever left the value there.
• Other code that touches the bases does not depend on CPU identity:
  • cpu::thread_pointer() (process.rs:1013) and sys_set_thread_pointer act on the live register of the running thread. The next switch-out reads that register back.
  • The nmi_user_gs self-test saves and restores IA32_KERNEL_GS_BASE under IrqGuard::close(), and no switch can happen in that span.
  • The NMI and #DB entries' rdgsbase/wrgsbase move IA32_GS_BASE and leave the user base alone.

A forwarded task gets its own bases. If B's cache differs from T's saved value, B writes the register. If they are equal, B's register already holds T's value. Each PerCpu.user_gs_base starts at NO_GS_BASE (1<<63, not canonical), so a CPU's first switch into any thread always writes it. fs_base: 0 matches the register as load_gdt leaves it. The FPU follows the same per-task-plus-per-CPU pattern: resume restores unless both fpu_holder == ctx and Left == this CPU. A task forwarded A→B→A therefore restores on its return to A (Left = B), even when A's holder is still T.

The INITIAL contexts. The idle context's user_bases is never read: Runs::Idle neither saves nor writes bases, and its left is null (cpu.rs:2303 and :2328). A spawned context's INITIAL (gs 0) is written at the task's first switch-in on whichever CPU, through the comparison above. Neither path touches the on-CPU word.

Evidence (r4/ at evidence 748bfad8). rev.txt and models-rev.txt both record e1325aab6, and rev.txt records a clean tree.

• summary.txt lists 14 clippy shapes on both targets, all rc=0, plus kernel --lib, every_model_control_is_run and kernel-sim, all rc=0.
• The simulator control forward-ignores-on-cpu reds with rc=101.
• --ci host models ends with rc 0.

These match the author's composition note, and the note's three claims hold on inspection. Run 43173669251 was still queued at the head when I checked, so its result is not part of this review.

Findings

None. No blocker and no suggestion. #1264's exit asks for bases to read back unchanged "after its CPU has run another thread". That does not cover a thread moving between CPUs. Since each cache stores a value and the switch compares it against the task's own saved value, inspection settles this; no new test is needed.

LAND