[Japabu]

Problem

Every unmap that freed a touched private page took each of the 64 futex bucket locks, to end waits on its frames, whether or not anything waited on them. Stage probes measured this on both benches, one boot each (evidence): 1,159 ns on the T14 and 1,146 ns on the AMD bench per unmap of one touched page. That is about a third of mem.munmap_touched_remote.4k (T14 3,341 ns against Linux's 2,279 in the 2026-11-11 scoreboard).

Change

Each address space counts its own threads' futex waits (sched::futex::Waits, held by the Space and its AddressSpace).

• The count's window, stated once, in FutexWait's doc. The futex-wait syscall begins a mm::space::FutexWait, which raises the space's count when made and lowers it when dropped. The word's only translation is FutexWait::translate's, and that Translation<'_> borrows the guard. So the count comes before the translation's hold of the space's lock, and it falls only once the wait, which checks the translation until it has unregistered, is done with it. That hold's release carries the count to any unmap that takes the lock after it, and the gate reads the count under that lock.
• The gate. A clear or a discard ends waits on the space's own private frames only while its count is not zero (revoke_frames(&self.futex, ..)).
• Why it is exact, with A futex wait translates its word once and checks it with one load #1253's single translation, where the later checks read the space's count of leaf changes without the lock (Translation::holds):
  • A private frame is mapped in exactly one space, so only that space's waits can be keyed on it, and only on a frame the syscall's translation found.
  • A wait whose translation came before the clear is counted by then. The space's lock orders that count before the gate's load, so the buckets are walked. From there A futex wait translates its word once and checks it with one load #1253's argument holds: the walk's bucket locks order the shootdown's count of the change before any later check of the wait, which takes the lock and finds the frame gone.
  • A wait whose translation came after the clear finds the frame gone and waits on no frame of these.
  • The lock orders both cases, so Relaxed is enough.
• Shared memory takes no gate. A shared object's frames can be keyed by waits in any space that mapped it. Its drop (SharedMemObject::drop) holds no space lock and keeps walking every bucket, as on main. Unmapping a shared page in one space ends no wait, because its frame is not freed then, as on main.

Rebased onto main after #1253, which moved the count

#1253 made a wait translate its word once, in the syscall. Its checks became a load through the direct map plus Translation::holds, which takes the space's lock only when the space's count of leaf changes has moved.

Round 2's argument rested on every check taking the space's lock after the count, and that no longer holds. With the count where round 2 put it, inside scheduler::futex_wait after the syscall's translation, the gate would be unsound under #1253:

1. A wait translates its word before an unmap's clear, then counts itself.
2. The unmap reads zero, because nothing orders that count before the read, and skips the walk.
3. With no bucket lock taken, nothing orders the unmap's count of the change before the wait's lockless holds.
4. The wait can then park keyed on a freed, possibly reissued frame.

So the count now precedes the translation, which decides the frame. That restores the lock ordering, and #1253's bucket-lock argument covers the checks after it.

Rounds 4 and 5 make that order the type's. FutexWait owns the space it counts, and Translation<'w> borrows it (&'w Space). FutexWait::translate is the only maker of a Translation, and Space::translate is folded into it. The wake translates to a bare frame (translate_user -> Option<u64>), which scheduler::futex_wait does not accept. The three broken forms are compile errors, each shown on a scratch patch (evidence): the guard dropped before the wait (E0505), the guard made as a temporary in the translating closure (E0515), and a wait handed the wake's translation (E0308). Round 4's code commit (440d4bf, head f110f44) claimed this while two of those forms still compiled; its message is replaced. The head is rebased onto main 36ed75b, after #1267, as 14291a2. git range-diff shows the code commit unchanged (=, now a891051). The records commit keeps both records' text in a-tlb-shootdown…md, with the diagnosis put in the past tense where #1267 changed what it describes.

Round 1 made the count machine-wide, so it never reached zero on a booted system. The supervisor's files worker and logkeeper's carrier-stall thread wait on futexes for the whole boot.

The records commit holds the 2026-11-11 diagnosis:

• the frees bullet names the space;
• the shootdown attribution says "most of the rest";
• the T14 large-copy sentence in the small-memcpy record separates 4 MiB (1.0% under Linux over 4 KiB pages, 10.0% under over huge ones) from mem.bw.copy, 16 MiB and 64 MiB (3.7 to 4.9% under both);
• the huge-pages paragraph says that page size explains at most about 1% of the gap;
• the owed metal checks;
• the mem.map_unmap_4k paragraph has moved to The inventory keeps its gaps once, by length, and inserts and removes in place #1256.

Checks

• Host at 697e3bb, whose code commit the head carries unchanged (logs and commands), each exit 0:
  • cargo test -p kernel --lib --features sched-check: 463 passed. That builds kernel/pure; the clippy runs are the host compile of the changed files.
  • cargo run -- --ci host models: 83 steps green, every kernel model with its negative controls.
  • Every kernel shape of build/clippy.rs, with the adopted lints and -D warnings: the two host shapes (sched-check; sched-check,protocol-port with the kernel controls), six on x86_64-unknown-none and four on aarch64-unknown-none-softfloat.
  • The three broken forms fail to compile, as above.
• The full cargo run -- --ci host was not run, under the owner's testing policy.
• No loom model. The gate is ordered by the space's lock, and what follows it by the bucket locks that A futex wait translates its word once and checks it with one load #1253's argument already rests on. Loom cannot run kernel/src, so a model would only restate those edges.
• Guest run 43119229089, green, at 697e3bb, x86-64 and AArch64 together: virt_smp, std_threads_count_the_cpus_and_give_back_ended_threads and a_user_copy_faults_in_mid_copy_or_ends_as_bad_address. The head 14291a2 carries the same code commit (range-diff =). What main gained since, A pass skips the timer write and the ask swaps it does not owe #1263 and A user change asks each CPU running the space for its range, and owes itself nothing #1267, touches no file of the futex path but space.rs's map, which validates an object's range.
  • 43116554248, at round 4's head, is cancelled. 43110908829 was green at a5c75b8, and 43082005007 at the pre-A futex wait translates its word once and checks it with one load #1253 code.
  • The one test of the revoke path itself, test_rs_futex_wake_counts's orphaned_by_unmap, runs only in the metal testcases boot.
• Owed on metal, in issues/user-memory-hot-paths-are-slower-than-2-mib-pages.md. The benches are down, so neither is a landing condition:
  • The T14's testcases boot. Main must pass test_rs_futex_wake_counts: its orphaned_by_unmap waiter shares the unmapping space, so the walk runs. The queued session's mutation boot (the walk skipped while a thread waits) would show the test reds without it.
  • An A/B on both benches of osbench_system, osbench_mem and osbench_sched, main from before and after. Main after must read mem.munmap_touched_remote.4k and the other unmaps of touched pages faster by up to the walk's cost, and pingpong.futex.* and the wake storm no slower.
• The speed-up this PR exists for is not yet measured on metal. The 1,159/1,146 ns per unmap is the walk's cost from the diagnosis's probes, not a measured gain. The staged A/B branches (memperf-futex-ab-base 942c3c3, memperf-futex-ab-head 03c896c) were superseded, predating A futex wait translates its word once and checks it with one load #1253 and the moved count, and are deleted; they never booted. The owed A/B is of main from before and after.

🤖 Generated with Claude Code

[Japabu]

Review of 6b3f796

What I read: both commits and the full diff. In full: kernel/src/sched/futex.rs, scheduler::futex_wait, kernel/src/watch.rs, kernel/src/mm/space.rs (clear, discard, get, Drop), SharedMemObject::drop, process::futex_word, thread spawn, and the loader's space assignment. Also the three changed records, the evidence at 903881ff and the diagnosis at cf6a882c, the branches memperf-ab-base, memperf-ab-head and memperf-futex-mut, and the pre-registered rule.

Architecture

sched::futex is the right owner and the change is small: 39 production lines plus records. But the gate counts every thread in the machine. On a booted ToyOS some thread is always in a futex wait (B1). So every futex wait now pays for the counter, and no unmap is any faster. The gate has to be scoped to the waits that can be keyed on the freed frames.

The race argument: it holds

• A wait arming as an unmap passes the check. Waiting::begin comes before both of the waiter's translation reads, and each read is under the space's lock. The revoke's load runs inside the critical section that cleared the leaf (clear, discard). Suppose the load misses the increment. If the waiter had taken the lock before the clear, the lock's release→acquire would order the increment before the load, and coherence would force the load to see it. So the waiter took the lock after the clear. Its first ready() then finds the leaf gone, or Held, which get answers as None, and it never registers. If the load sees the count, the walk happens as on main. A waiter that registered earlier was counted earlier.
• Shared objects. The order runs: the waiter's read → (space lock) → the mapper's clear → (Arc's release decrement and the last drop's acquire fence) → the load in SharedMemObject::drop.
• Fork or spawn. ToyOS has no fork. A spawned process gets its own space (loader/mod.rs:230), and copied ranges draw fresh frames. Threads share one Arc<Space> and so one lock (process.rs:638), which the argument covers. Drop for AddressSpace still relies on no thread running in a dropping space; that is unchanged.
• AArch64. The argument needs only the lock's release→acquire and Arc's release/acquire. Nothing depends on store→load (Dekker-style) ordering between two locations. So it holds on the Armv8 model as Rust maps acquire and release. SeqCst is stronger than the argument needs, because the ordering comes from the lock.
• Model. None is owed for a gate ordered by the space lock and Arc. Loom cannot run kernel/src, and a model would only restate these two edges. One is owed if the rework moves the gate into kernel::sched::watch, which kernel/loom/tests/loom_watch.rs models.

futex.rs:64-68 states the argument for the clear only. For SharedMemObject::drop (shm.rs:298,303) no space lock is held, and the order comes from the Arc. The comment's replacement must cover that path, or the rework must leave that path ungated.

Findings

BLOCKER

1. kernel/src/sched/futex.rs:18-37,69 — the gate never opens on a booted ToyOS. WAITING counts every thread in the machine, and two services that run on every boot wait on futexes for its whole length:

   • The supervisor starts its files worker at system/supervisor/src/main.rs:679. The worker parks in std's mpsc receive at :747 (for job in queue).
   • logkeeper's log-carrier-stall thread (system/logkeeper/src/carrier.rs:281) waits in self.moved.wait(state) at :335, or in wait_timeout while a channel is owed something.

   At the pinned std fork (a189b3a6b), ToyOS's thread parking and Condvar are the futex implementations (library/std/src/sys/sync/thread_parking/mod.rs:14, condvar/mod.rs:14), and mpmc parks at sync/mpmc/context.rs:143. Both services run in the bench image (tests/images/benchcase.toml boots logkeeper, and the supervisor is init) and in testcases.

   So each unmap that frees touched pages still walks the 64 buckets, as on main, and every futex wait now pays for two SeqCst RMWs on one line shared by the whole machine. By inspection, the expected ~1.1 µs on mem.munmap_touched_remote.4k will not appear. The queued F arm will test that.

   The records describe a saving that does not happen, and must follow the rework:

   • issues/user-memory-hot-paths-are-slower-than-2-mib-pages.md:45-48
   • issues/a-tlb-shootdown-reaches-only-the-cpus-that-ran-the-space.md:47
   • space.rs:722-725, whose cost statement now leaves out the walk

   One direction (the choice is the implementer's): a private frame is mapped in exactly one space, which space.rs:862-866 already relies on. A count on the Space, raised before the waiter's first locked read, therefore gates clear's and discard's revokes exactly, by the same lock argument. The shared-object drop keeps its walk. Another direction is to read each bucket's occupancy, which registration already updates under the bucket lock; that needs the watch model extended. Either way, the A/B has to show the gain on a booted system.

2. The A/B does not measure where the new cost lands. Every futex wait gains work, but the memab row (osbench_system, osbench_mem) measures no futex wait. osbench_sched carries pingpong.futex on one CPU and across cores, and the wake storm (tests/guest/osbench/src/main.rs:100-119). The reworked PR's A/B must include that group. Without it, "no other row moves" is unsupported for the rows the change affects.

3. issues/a-small-memcpy-on-the-amd-bench-runs-at-as-little-as-six-tenths-of-linuxs.md:75-76 — false record. "The T14's large copies trail Linux over 4 KiB pages as much as over huge ones" does not hold for one of the large rows the same record names at :64. In the cited diagnosis, at 4 MiB Linux read 22,197 MB/s over 4 KiB pages and 24,411 over huge pages. ToyOS read 21,967: 1.0% under the first and 10.0% under the second. Either restrict the sentence to mem.bw.copy, 16 MiB and 64 MiB (3.7–4.9% under both), or state the 4 MiB reading.

SUGGESTION

• Land the records commit without this PR. The shootdown attribution and the huge-pages correction do not depend on the futex change. The mem.map_unmap_4k paragraph (user-memory-hot-paths…md:135) belongs with The inventory keeps its gaps once, by length, and inserts and removes in place #1256, which changes that cost and owes the same record its A/B. The candidates paragraph (a-small-memcpy…md:66-76) belongs with libc: a short copy is one rep movsb only where the CPU declares it fast #1257, which must edit that record anyway. Nothing would then wait on this PR, and no edit would be left to whichever PR lands second.
• user-memory-hot-paths…md:91,94 — I checked the figures against the evidence: 6,792/6,865, 9,662/9,690, 6,539 and 9,241 all match. Two wordings are looser than the data:
  • "4 to 5%" is 3.7% to 4.7%.
  • For one Linux run, "page size explains at most about 1% of it" says what was measured more exactly than "Page size is not the cause".
• a-tlb-shootdown…md:45 — "The rest was" the removal and the walk: 900 + 1,004 + 1,159 = 3,063 of 3,341 ns, so "most of the rest".

Evidence

• Host checks. The log at 6b3f796 shows 454 passed and the three clippy runs, each exit 0.
• Branches. memperf-ab-head is the head plus the row, and memperf-ab-base is 34cb4c9 plus the same hunk. memperf-futex-mut is the head plus the one-line mutation.
• testcases at the head. On any boot WAITING ≥ 1, so the boot runs only the walk path. It shows the change did not break a revoke when a thread waits. It cannot show the skip is safe, because no booted state reaches the skip. The mutation boot keeps its value: it shows orphaned_by_unmap detects a missing revoke, which does not depend on the gate's design.
• Queued session. If it has not started, the F arms (two T14 boots, two AMD) and the head testcases boot would measure a revision that goes back. Dropping them leaves the inventory (I) arms balanced: T14 base I I base, AMD I base base I. If they have run, the F arm checks B1: mem.munmap_touched_remote.4k should read unchanged.
• Rule. Points on the rule as a whole are on libc: a short copy is one rep movsb only where the CPU declares it fast #1257. For this PR, its expectation for the F arm is the claim B1 refutes.

Guest rows

None. The declared test runs only in the metal testcases boot. The argument does not depend on the architecture, and no QEMU row exercises the race.

What metal must show for the reworked head

• T14 testcases: green at the head, and red at a mutation that skips the walk while a thread waits.
• A/B on both benches, with osbench_sched added:
  • mem.munmap_touched_remote.4k and the other unmaps of touched pages are MOVED faster, by about the walk's cost.
  • No REGRESSION in pingpong.futex.* or the wake storm.

SEND BACK

[Japabu]

Re-review of bc11e5e

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

What I read:

• bc11e5e's diff.
• In full: sched/futex.rs and scheduler::futex_wait.
• In space.rs: Space::new_user, discard, clear, get and Drop.
• SharedMemObject::drop; process::futex_wait and futex_word; user_ptr::translate_user; watch::wait_until; spawn_thread.
• Every call that frees an owned frame.
• osbench's unmap_touched_remote and ToyOS std's thread join.
• memperf-futex-ab-{base,head}, the r1 host-check evidence (fe5f302a) and rule-futex.txt.

Architecture

Counting per space gives the gate the right scope. The Space owns the count. One Arc<Waits> is raised without the lock (Space::futex_waits) and read under it (AddressSpace::futex). The shared-object drop stays ungated, so round 1's open obligation, an ordering through the Arc for that path, is gone.

Round 1

• B1, resolved. A wait closes only its own process's gate, so the services' permanent waits no longer close everyone's.
  • I checked the bench row against this. During mem.munmap_touched_remote.4k's timed unmaps, the process's threads are:
    • the initiator, which unmaps;
    • the sibling, which spins;
    • the main thread in JoinHandle::join, which on ToyOS is the thread_join syscall (sdk/std/sys/thread.rs:48), not a futex.
  • So the count is 0 and the row measures the skip.
  • The records follow: the hot-paths "Frees" bullet, the shootdown record's attribution, and clear's cost doc.
• B2, resolved. 942c3c3 and 03c896c carry the identical row hunk on 34cb4c9 and on bc11e5e, and the groups include osbench_sched.
• B3, resolved. ToyOS read 21,967 MB/s against Linux's 22,197 and 24,411: 1.0% and 10.0% under. The wording suggestions were taken, and the mem.map_unmap_4k paragraph moved to The inventory keeps its gaps once, by length, and inserts and removes in place #1256.

Soundness, traced

• Private frame, gate closed (the load reads 0).
  • The waiter W counts itself before every re-check read makes under the space's lock. wait_until calls ready() before arm and on each turn after it.
  • Suppose one of W's re-checks preceded the clear in the lock's order. Then unlock→lock orders W's increment before the revoke's load. Each thread's decrement follows its increment in the counter's modification order, so the load would read at least 1.
  • So when the load reads 0, every re-check of W's follows the clear. get then finds the leaf Empty or Held and answers None, and W returns before arm.
  • Suppose instead the frame was reissued and faulted in again at W's address in W's space. Then W waits on the page's current frame, which is correct and is also what main does.
• Gate open (the load reads at least 1): the walk runs as on main.
• The decrement comes after unregistration. Armed drops inside wait_until, and _waiting drops when futex_wait returns, after its final read().
  • Suppose a load reads that decrement, and a later post on a reissued frame still finds W registered.
  • That post would happen after the load, yet sit before W's unregistration in the bucket lock's order, and that unregistration is sequenced before the decrement. The load would then happen before the very decrement it reads, which read-write coherence forbids.
• A shared page mapped in several spaces.
  • SharedMemObject::drop still walks every bucket (shm.rs:298,303).
  • A clear of an object page revokes nothing, because take_owned yields owned frames only, as on main.
  • A waiter on a shared frame raises only its own space's count. That can cost its own space a walk it did not need, but it never causes a skipped revoke.
  • So no lost wake and no stale key arise that main does not already have.
• Threads of one process share one count.
  • spawn_thread passes the spawner's Arc<Space> (process.rs:602,638).
  • A Space holds its one AddressSpace inside its lock, so the count raised without the lock and the count read under it are the same allocation.
  • A loaded process gets a new Space, and with it a new count.
  • There is one futex-wait site, and it translates in the caller's own space.
• A process exits with waiters parked.
  • A kill makes wait_inner return Cancelled after block_on. futex_wait then returns normally, so the count drops.
  • Each waiter holds its space Arc, so Drop for AddressSpace, which frees without revoking, runs only after every waiter has left.
  • A teardown clear made while a waiter is still counted walks, as on main.
  • A leaked count could only keep the gate closed: slower, never unsound.
• Every owned frame freed under a space goes through clear or discard, which are gated and run under the lock, or through Drop, when no thread remains. The paged.rs frees are of frames no leaf maps.
• Relaxed is enough on both architectures, because the space's lock alone orders the count against the clear. No model is owed.

Findings

BLOCKER

1. kernel/src/sched/futex.rs:18-20,50-56, kernel/src/scheduler.rs:265-267 — the window the soundness rests on is stated wrongly.
   • The comments say a wait is counted "from before it first reads its word's translation". That is false. process::futex_wait first translates the word, under the same lock, in futex_word (process.rs:965 → user_ptr.rs:52, space.lock().reach), before scheduler::futex_wait counts.
   • revoke_frames' argument inherits the error. Take a wait whose futex_word ran before the clear and whose count the load misses. It did take the space's lock before the clear, contrary to "so it took the space's lock after the clear".
   • The code is sound, because only read's re-checks decide registration, and they all follow the count. The comments must say that, for example:
     • "counted from before it first re-checks its word's translation under the space's lock";
     • in revoke_frames, "every re-check it makes comes after the clear".
   • As written, a maintainer could move the count below the first read, or treat futex_word's translation as covered by the count.
   • The fix is comment-only, so no check, guest run or boot needs repeating.

For the orchestrator (description and title):

• The body repeats the claim: "A wait counts itself before it first reads its word's translation", and "It takes the lock after the clear".
• The title, "…while no thread is in a futex wait", is round 1's claim, and it becomes main's commit subject. It should read "…while no thread of its space is in a futex wait".
• "Guest rows: none" omits run 43082005007, which the boot-before-flash rule requires.

SUGGESTION

• futex.rs:63-65 — revoke_sorted's doc now says "of a shared object", but revoke_frames also calls it, for private frames. Say what it does, walking every bucket for these frames, rather than naming one caller.

Evidence

• Host checks at bc11e5e: kernel-lib and four clippy shapes, each exit 0. The kernel library does not compile kernel/src, but the clippy targets do.
• Guest run 43082005007 is queued at 03c896c, which is bc11e5e plus the metal row only. Its rows are virt_smp, std_threads_count_the_cpus_and_give_back_ended_threads and a_user_copy_faults_in_mid_copy_or_ends_as_bad_address.
  • The std-threads row parks futex waiters and unmaps thread stacks, so it reaches both states of the gate.
  • The comment fix does not invalidate it.
• testcases: orphaned_by_unmap's waiters live in the unmapping process, so the boot runs the walk. It is what shows that the count is the unmapping space's own: a count raised in another space would skip the walk, and the sweeper would red. Round 1's mutation boot (08-tcmut) remains the control for the test itself.

Rule

rule-futex.txt is sound, and its expectation for the remote row holds, as traced above. Two points on wording:

• "Gate open" for testcases means that the walk runs, the reverse of how round 1 used the phrase.
• Its time label, "~20:50", is later than the file's own write time (20:44 +0200).

Landing conditions

1. The comment fix above.
2. Guest run 43082005007 green before any flash.
3. T14 testcases at the head: test_rs_futex_wake_counts passes.
4. The A/B by rule-futex.txt on both benches:
   • mem.munmap_touched_remote.4k MOVED faster; an INCONCLUSIVE result means more blocks are run.
   • No REGRESSION in pingpong.futex.* or the wake-storm rows.
   • Every head boot passed, or its failure was investigated and shown to have a cause outside the change.
5. The result goes into issues/user-memory-hot-paths-are-slower-than-2-mib-pages.md, whose exit asks for each change measured against its base.

SEND BACK

[Japabu]

Review r3 of a5c75b8

Scope: the moved count, with the code at the head, which is rebased onto 06fcb81 and includes #1253.

What I read:

• Both commits and the full diff.
• In full: sched/futex.rs, process::futex_wait, futex_word, user_ptr::translate_user, Space::translate and Translation::holds, scheduler::futex_wait, watch::wait_until and wait_inner, and the sync::Lock acquire and release.
• In space.rs: put, release, protect, discard, decommit, remap, move_leaves, shoot_down, clear, populate, get and Drop.
• Also SharedMemObject::drop, leave_user_if_due, every caller of free_drawn, revoke_* and watch_of, the three records, the PR thread, the r3 evidence at fe7f5d5e, and guest run 43110908829.

I ran no builds or tests. My role is limited to reading code and evidence, and that limit overrides the brief's request to run them. The host evidence is the author's logs at this exact head.

Architecture

The design is unchanged from round 2:

• the Space owns a count of its threads' futex waits;
• revoke_frames reads that count under the space's lock;
• shared objects stay ungated.

This round moves one line, the count, from after the syscall's translation to before it. Production code in the kernel is +74/−14, about half of it comments. The records are +59/−5. No test was added.

The premise round 2 lost, confirmed

Round 2 argued that every check deciding registration takes the space's lock after the count. #1253 broke that: holds now reads shot_down without the lock. With round 2's placement, the race has a store-buffering shape:

• the unmap stores shot_down, then loads the count;
• the wait stores the count, then loads shot_down;
• both are Relaxed.

The C11 model and AArch64 allow both loads to read the old value. On x86, the locked RMWs would in practice have hidden it. So the author's counterexample is real.

The new order, traced at the head

Take a wait W and an unmap U, with L the space's lock and B the word's bucket lock.

• W's steps:
  • begin(), a Relaxed RMW (process.rs:971);
  • futex_word, which runs Space::translate: lock L, reach, read at, unlock L with Release;
  • the pre-arm ready();
  • arm, under B;
  • ready(), which is the direct-map load and holds;
  • park, or end;
  • Armed drops inside wait_until, under B;
  • the final changed();
  • _waiting drops.
• U's steps, all under L: the leaf leaves the frame, shot_down's increment, the shootdown, take_owned/discard_owned, the gate's load, the walk if the load is not zero, then the free.
• W's translation precedes U's in L's order. The count is sequenced before W's release of L, which synchronizes with U's acquire. Coherence then makes the gate read W's increment or a later value. Every Waiting's decrement follows its own increment in the count's modification order, so that value is at least 1 unless W has already decremented. The walk then runs, and A futex wait translates its word once and checks it with one load #1253's argument through B covers every later check.
• W's translation follows U's. reach finds the leaf Empty or Held, or a different frame. If the allocator handed the same frame back to the same address, W waits on the page's current frame, which is correct.
• The gate reads W's decrement. W's unregistration is sequenced before that decrement. A later post on a reissued frame that still found W registered would have to come before the unregistration in B's order. The load would then happen before the decrement it reads, which coherence forbids. W's last read through the direct map is A futex wait translates its word once and checks it with one load #1253's spurious-wake case, the same as on main.
• The count and the translation are in the same space. A thread's address_space is set only when it is spawned (driver.rs:432). So the two current_address_space() calls (process.rs:970, user_ptr.rs:57) return the same Arc, and AddressSpace::futex is the same allocation as Space::futex.
• Relaxed is enough. The ticket lock acquires with Acquire and releases with Release (sync.rs:141,211). Every edge the gate relies on is message passing through L or B, and none has the store-buffering shape.

Every path

• Gated: clear, reached from release, put, decommit and remap's shrink, and discard, including its kept frames. All of them take &mut AddressSpace, which only Lock hands out.
• protect and remap's move free no frame and walk nothing, the same as on main. A waiter keyed on a frame that protect(None) made Held is caught by the later gated clear, because its translation preceded both under L.
• Shared memory:
  • an object leaf is owned: false, so take_owned never yields its frame;
  • SharedMemObject::drop walks every bucket (shm.rs:298,303);
  • a waiter on a shared frame raises only its own space's count, which can only cause a walk that was not needed.
• Process exit and kill:
  • a kill returns Cancelled out of wait_inner, and process::futex_wait returns normally, so the guard drops;
  • a thread leaves only on its way back to Ring 3 (leave_user_if_due);
  • each Translation holds the Arc<Space>, so Drop for AddressSpace, which frees frames without revoking waits, runs only after every waiter has left.
• The paged.rs frees are of pager frames, which revoke_frames never covered.

The code is correct.

A model

None exists. kernel/loom models the ticket lock and the watch's revoke, but not Translation::holds or this gate. A model is not warranted as a landing condition, for two reasons:

• The final design's edges are lock release→acquire and RMW coherence. Inspection settles those, and the lock itself is modeled.
• The failure found here was a premise that moved under a rebase. A model written in round 2 would have encoded the locked re-checks and kept passing, so it would not have caught this.

If one is written, it should cover #1253's holds and the gate together:

• W: count, lock L, read at, unlock, lock B, register, unlock B, fence(Acquire), load shot_down, and on a moved count lock L and re-check.
• U: lock L, clear the leaf, shot_down += 1, load the gate, walk under B if the load is not zero, free, unlock.
• Assertion: no execution ends with W parked on the frame, unrevoked, after U freed it.
• Negative control: the count after W's unlock of L, round 2's placement. It must go red through the stale shot_down read, which loom explores for Relaxed.

Round 2's placement in comments and records

None remains. scheduler.rs at the head is main's, with no count. No comment in kernel/src and no record under issues/ says that the wait counts itself after the translation or before its re-checks. The comments, the records' "Frees" bullet and the owed checks all describe the new placement.

Findings

BLOCKER

1. kernel/src/process.rs:966-969, kernel/src/sched/futex.rs:17-19 and kernel/src/process.rs:948: the count's relation to the space's lock is stated ambiguously, and stated three times.
   • The call site says "Counted before the word is translated, under the space's lock, and until the wait has unregistered". It lists "under the space's lock" alongside "and until", so it most naturally reads as the count being taken under the lock.
   • Waits' doc uses the same phrase, while Space::futex_waits correctly says "counted without its lock".
   • What the gate needs is narrower: the count must come before futex_word's hold of the lock, so that hold's release carries the count to the unmap. That is the edge this round restored, and a reader who believes the count sits under the lock no longer sees why its place matters.
   • The window also has three homes besides the argument in revoke_frames (futex.rs:49-57), which is needed: Waits' doc, the call-site comment and the clause added to futex_word's doc. Round 2's error was exactly such a window going stale in several comments at once.
   • Fix: state the window once, at the call site, correctly. For example: "Counted before futex_word takes the space's lock, until after the wait unregisters; an unmap reads the count under that lock (sched::futex::revoke_frames)." Then cut Waits' doc to what it counts, and drop the futex_word clause.
   • The fix is comment-only, so no check needs repeating.

SUGGESTION

• Make the order a property of the API. For example, the guard could own the space it counts and hand out the translation: Waiting::translate(addr). Then the translated space is the counted one by construction, and statement order can no longer separate the count from the translation. The current code is correct without this.
• Evidence form.
  • The r3 directory records exits and logs but not the command lines.
  • The clippy runs cover 5 of build/clippy.rs's 10 kernel target shapes. No feature arm changed, and the merge queue's host job runs all of them, so nothing is missing for this change.
  • kernel-lib compiles kernel/pure, not kernel/src. The clippy runs are therefore the only host compile of the changed files.

For the orchestrator (description and commit message):

• "counts itself before it translates its word, under the space's lock" has the same ambiguity, in both the body and the message of cde9573.
• The staged A/B branches (942c3c3, 03c896c) predate A futex wait translates its word once and checks it with one load #1253 and the moved count, so they cannot serve as the owed A/B. The record already asks for main before and after, so only the body should say they are superseded.

Evidence

• Host at a5c75b8. exits.txt records dirty=0.
  • kernel-lib: 461 passed.
  • models: 83 steps green, each negative control red as intended.
  • Six clippy runs.
  • Each exited 0.
• Guest run 43110908829 at a5c75b8: green, 3 of 3 rows.
  • virt_smp ran on emulated AArch64; std_threads_count_the_cpus_and_give_back_ended_threads and a_user_copy_faults_in_mid_copy_or_ends_as_bad_address ran on x86-64.
  • The std-threads row parks futex waiters and unmaps thread stacks, so it reaches both states of the gate.
  • It shows no functional regression. Neither instrument can show the ordering.
• The skip racing a wait is exercised by no test. The claim rests on inspection, which I re-derived independently above and which is enough for edges that are only lock message passing.
• Metal stays owed, as user-memory-hot-paths-are-slower-than-2-mib-pages.md records: one bench's testcases boot, and the A/B on both benches including osbench_sched. The pre-A futex wait translates its word once and checks it with one load #1253 run 43082005007 does not stand for this head, as the body says.

SEND BACK: the comment fix only.

[Japabu]

Review r4 of f110f44

Scope: the FutexWait restructuring and the rebase onto 8188095. I did not reopen settled points.

What I read:

• git range-diff of 06fcb81..a5c75b8 against 8188095..f110f44.
• The full kernel diff.
• Space::translate, FutexWait, Translation and holds.
• user_ptr::translate_user, futex_wait and unlocked_space.
• process::futex_word, futex_wait and futex_wake.
• scheduler::futex_wait.
• watch::wait_until, wait_inner, arm and Drop for Armed.
• leave_user_if_due.
• Every caller of revoke_frames and free_drawn.
• The inventory keeps its gaps once, by length, and inserts and removes in place #1256's kernel/src diff, and the r4 evidence at 1f8ec6c4.

I ran no builds.

Architecture

A guard that owns the counted space and hands out the translation is the right shape. It settles one of round 3's premises by construction: the counted space and the translated space are now one Arc. Round 3 had to show that two current_address_space() calls agreed.

The type closes only one end of the window, though, and only for a caller that chooses to use it. Kernel production code is +96/−22, against +74/−14 at r3. No test was added.

The questions asked

1. Is the order unrepresentable to break? No. Two forms compile:

   • The guard can end before the wait. Translation holds its own Arc<Space> (space.rs:244, cloned at :232) and does not borrow the guard. So either of these compiles:

     • drop(wait) before scheduler::futex_wait;
     • inlining the guard into the closure at process.rs:969: .and_then(|a| crate::user_ptr::futex_wait().translate(..)).

     Either one lowers the count before the wait arms. That is round 3's store-buffering race: the unmap reads 0 and skips the walk, and nothing orders shot_down before the lockless holds.

   • A wait can bypass the guard. scheduler::futex_wait takes any &Translation (scheduler.rs:259). Two functions still make an uncounted one: user_ptr::translate_user (user_ptr.rs:50, pub(crate)) and Space::translate (space.rs:206, pub). futex_wake, at process.rs:982, is exactly that form, and copying it into the wait compiles.

2. Does the drop follow unregistration on every path? Yes, at this head, because the local wait is declared before word and lives to the function's end:

   • A translation error returns before anything is armed.
   • Every other path returns from wait_until, whose Armed unregisters when it drops. These are a satisfied predicate, a refused or notified park, a revoke, the deadline, a cancel, and arm answering None.
   • A kill leaves only in leave_user_if_due, on the way back to user mode, after the syscall has returned.

   This order comes from statement placement, not from the type.

3. Is futex_wake right to count nothing? Yes. It registers no key, so a walk has nothing of its to end. A post on a frame that was freed and reissued after the wake's translation is a spurious wake. The ABI allows it, because the waiter re-checks its word. Main has the same race, since the walk ends registered waits, not posts in flight.

4. Does round 3's argument still hold verbatim? Yes. Its steps map one to one:

   • begin() is now FutexWait::begin (user_ptr.rs:57).
   • futex_word's hold of L is now FutexWait::translate.
   • _waiting's drop is now wait's.

   gate() still runs before the raise, and no lock is taken between them.

5. Did the rebase change anything else? No. The records commit is identical (=). The code commit differs only by r4's intended changes. The inventory keeps its gaps once, by length, and inserts and removes in place #1256's one kernel/src hunk is range_heap's accounting. Every owned frame is still freed through the gated clear or discard, or through Drop.

Findings

BLOCKER

1. kernel/src/mm/space.rs:218-249, kernel/src/scheduler.rs:259, kernel/src/user_ptr.rs:48-52: the order is not the type's. Point 1 above shows both forms. Three statements are therefore false at this head:

   • "by construction" (space.rs:220);
   • the commit message of 440d4bf: "The order is the type's, not the statements'";
   • the requirement that the ordering be structural, which is not met.

   Fix (the spelling is the implementer's): make the translation borrow its guard, and make the guard its only maker.

   • FutexWait::translate(&self, ..) -> Option<Translation<'_>>, with Translation<'w> holding &'w Space.
   • Fold Space::translate into it.
   • The wake takes only the frame (translate_user -> Option<u64>).

   Both forms then fail to compile (E0505 and E0515), and each wait clones one fewer Arc. translate_user's "pub(crate) because the futex word outlives its syscall" (user_ptr.rs:49) is already stale, because its only caller is the wake. It goes too.

2. Comments.

   • kernel/src/process.rs:948: futex_word's second sentence describes "the frame, translated ...", but futex_word no longer translates anything. Move the not-a-lease contract to Translation, or delete it, since holds already states what matters.

   • The window is stated three times besides revoke_frames' argument:

     • FutexWait's doc (space.rs:218-221);
     • user_ptr::futex_wait's doc (user_ptr.rs:54-55);
     • the call site (process.rs:963-965).

     Round 3 asked for one home. Once finding 1 is fixed, the type's doc is that home. Drop the call-site comment, and cut user_ptr::futex_wait's doc to what it returns.

SUGGESTION

• user_ptr::futex_wait() waits on nothing, yet it sits between process::futex_wait and scheduler::futex_wait in one call chain. A name such as begin_futex_wait would say what it does.
• FutexWait::translate's access has one value, so the call site reaches past user_ptr's Access to kernel::vm::Access (process.rs:969). The wake, two lines down, uses user_ptr::Access. Taking a UserAddr and fixing Read inside would remove both points.

For the orchestrator (PR body):

• "so no statement order can separate the two again" is false at this head (finding 1).
• The window is not stated once, at the call site (finding 2).

Evidence

• Host at f110f44:

  • commands.sh is recorded now, which fixes round 3's gap, and the tree was clean (dirty=0).
  • kernel-lib: 463 passed.
  • models: 83 steps green.
  • Six clippy shapes.
  • Each exited 0.

  This is valid for this head. The fix changes the types, so it needs the clippy shapes again. They are the only host compile of kernel/src.

• Guest run 43116554248 at f110f44 was still queued at this review, with no conclusion. Its rows are owed at the fixed head instead.

• Metal stays owed, as the record states, and is not a landing condition while the benches are down.

SEND BACK

[Japabu]

Review r5 of 697e3bb

Scope: whether round 4's blocker is resolved, read against the five questions in the brief. I did not reopen settled points.

What I read:

• git range-diff 818809583..f110f445e 3b93f3770..697e3bbb7. The records commit is unchanged (=). Main's 8188095..3b93f37 touches nothing under kernel/src.
• In full: the changes to space.rs (Space, FutexWait, Translation, clear, discard), sched/futex.rs, user_ptr.rs, and process::futex_word, futex_wait and futex_wake.
• scheduler::futex_wait, plus watch::wait_until, arm, wait_inner and Drop for Armed.
• Repo-wide greps for Translation, FutexWait, Waits, translate_user, Space::translate and watch_of, both at the head and on main.
• The r5 evidence at ea45a55d, and the state of guest run 43119229089.

I ran no builds.

Architecture

This is the shape round 4 asked for. The guard owns the counted space, and the translation borrows the guard. The same type now enforces both ends of the window. Each wait clones one Arc<Space> instead of two, and the wake no longer builds a translation it never checked. Against main, the kernel changes are +106/−38 lines, much of that comments. No test was added. None is owed, because the compiler enforces the property.

The questions

1. Nothing makes a Translation without a live FutexWait.
   • Translation's fields are private, and mm::space has no child modules. Its one struct literal is in FutexWait::translate (space.rs:231).
   • FutexWait's field is private, and its only constructor is begin, which raises the count (:214).
   • Waits is reachable only through the private Space::futex and AddressSpace::futex fields. So nothing outside space.rs can lower() a space's count.
   • The pub items are FutexWait::{begin, translate}, Translation::{phys, holds}, Waits::{raise, lower}, revoke_frames, and the pub(crate) functions translate_user and begin_futex_wait. None of them yields a Translation without a guard.
   • translate_user now answers Option<u64> (user_ptr.rs:49). scheduler::futex_wait accepts only &Translation<'_>.
   • mem::forget or a leak can only keep the count raised, which leaves the gate open, the safe direction.
2. The count falls only after the wait unregisters, on every path. scheduler::futex_wait borrows the translation for the whole call. Its changed closure captures word and stays live across wait_until and the final check. So the borrow checker keeps wait alive until scheduler::futex_wait returns. wait_until always drops Armed before returning: on a satisfied predicate, the deadline, a cancel, a revoke, or arm answering None. The two refusals, an unaligned word or a failed translation, return before anything is armed. This order now comes from the types, not from where the statements sit.
3. No capability was lost. On main, Space::translate's only caller was translate_user, whose only caller was futex_word. That served the wait, and the wake, which used only phys(), always with Read. Nothing stored a 'static translation.
4. Round 3's argument still holds. Its steps map one to one:
   • begin is a Relaxed RMW sequenced before translate's lock.
   • translate holds L for the reach and the read of at.
   • The checks run as before.
   • The decrement comes when process::futex_wait returns.
   • The Arc that keeps Drop for AddressSpace away from parked waiters now sits in FutexWait rather than in Translation.
5. The docs are accurate.
   • The window has one home, FutexWait's doc (space.rs:204-210), and what it says is true.
   • revoke_frames' argument (futex.rs:42-51) refers to that doc rather than restating the window.
   • Translation keeps the not-a-lease contract.
   • The stale pub(crate) rationale and the call-site comment are gone.
   • Both commit messages are truthful.

Round 4's findings:

• B1 is resolved. The three forms fail with E0505, E0515 and E0308. Each patch applies at the head's line numbers (process.rs:962-969), and restored.log checks clean.
• B2 is resolved, as point 5 shows.
• Both suggestions were taken.

Findings

BLOCKER: none.

SUGGESTION

• kernel/src/mm/space.rs:222 spells crate::UserAddr, which :38 already imports.

For the orchestrator (PR body):

• "Round 4's head (440d4bf)" is wrong. 440d4bf was round 4's code commit, and its head was f110f44.

Evidence

• Host at 697e3bb: the tree was clean (dirty=0) and every command is recorded.
  • kernel-lib: 463 passed.
  • models: 83 steps green.
  • All 12 kernel shapes in build/clippy.rs ran: 2 host, 6 x86-64, 4 aarch64.
  • Each exited 0.
• The three broken forms: each was checked against kernel/src identical to the head's, and each fails with the claimed error.
• Guest run 43119229089 at 697e3bb was still queued at this review, behind five other dispatches. By inspection, runtime behavior is unchanged from a5c75b8, where run 43110908829 was green: this round changed types and where the Arc sits, not the order or the operations. The orchestrator should still read the run before landing, as round 4 asked.
• Metal stays owed, as the hot-paths record says, and is not a landing condition while the benches are down.

LAND, once guest run 43119229089 is green.

[Japabu]

Orchestrator: landing under the benches-down rule. Review r5 LAND. Head 14291a2 is the same code commit (range-diff =) rebased onto 36ed75b, with the records conflict against #1267 resolved by keeping both. Guest run 43119229089 at 697e3bb: success (virt_smp, std_threads, user-copy faults). Owed on metal recorded; the speed-up is not yet measured on metal.