Skip to content

A withdraw names again every waiting read it takes a page from - #1233

Merged
Japabu merged 3 commits into
mainfrom
paged-rereport
Nov 11, 2026
Merged

Japabu merged 3 commits into
mainfrom
paged-rereport

Conversation

@Japabu

@Japabu Japabu commented Nov 11, 2026 •

Copy link
Copy Markdown
Collaborator

Problem

A holder's SYS_PAGED_READ can wait for ever on main. A reader that finds a page absent links one request, and its pager hears of the range in one notice. The reader stays linked across its wait, and asking again for the same range was a no-op. A reader left its wait only when its page was no longer absent. So any route that makes the page absent again after the notice was answered, before the reader looks, strands it: no notice goes out, the pager believes it answered, and the reader waits, reported overdue, until it is killed. Three routes do that:

  • a withdraw (for example the file server making room) of a page supplied for the notice;
  • a shrink and a grow before the woken reader looks (the file server's truncate, "cut or grown");
  • a dirty supply the ceiling refuses over a failed page: the supply removes the failed slot, then answers DirtyFull.

Found reading the paged object for 7b's design review; review r1 found the second and third routes.

Change

  • The wait ends on a version change, and every move of it wakes the object's waiters. A write's end (write_end, end_write) posts the waiters' watch as a supply, failure, resize and release already did. Every write and resize moves the object's version, and a holder's read already answers WouldBlock once it finds the version moved. The wait's ready check is now Pages::wait_over: the page is no longer absent, or the version moved. That covers the shrink-and-grow and the refused-supply routes.
  • A withdraw re-reports. A withdraw is the one removal that leaves a page absent without moving the version. Pages::withdraw now takes the object's waiters (Waiters, which the kernel implements over its request list) and marks every want its removed range meets (Want::withdrawn), in the hold of the pager's lock that removes the pages; the kernel posts the pager's watch when that is news. The kernel cannot withdraw without handing its waiters over, and a slot released and reused between two holds gets no stray notice.
  • kernel::paged::Want (pure) is a waiting reader's range as its pager hears of it: named once while the reader waits, again where it moved, and again where a withdraw takes back a page of it.

Duplicate notices happen, and are accepted. A withdraw marks a request the server has read and not yet answered (the file server's make_room does this whenever it withdraws pages inside a waiting reader's longer range), and a withdraw of a later page of a range whose first page is still awaited names the whole range again. The server answers a request for a present page as a supply, which the kernel answers Present; the file server counts that as held. Each costs one device read. The design (7b rev 5 §3) accepts that cost, and step 2 builds on both mechanisms: its fault waiters record the version when they park and request afresh when their wait ends on a version change.

Kernel only, measured against the merge base b566931: +371 / -44 over two files at 7ce1e83. Production: the pure Want, Waiters, wait_over and the withdraw's marking about +78, the kernel's wiring +64 / -28. Tests, the wait model among them: about +215.

Checks

Targeted under the owner's testing policy: two kernel files, so the kernel's paged tests, the kernel's clippy shapes and the boot that runs the paged rows. The head 7ce1e83 is 43fa982 plus review r2's B3 (two posts of the waiters' watch at a write's end, and a doc line): clippy on the x86-64 kernel shape and the AArch64 kernel check exit 0 there, and by review r2 the host tests, controls and the T14 boot below stand for it, since a post only makes a waiter look again at its pure ready.

  • cargo test -p kernel --lib -- paged:: at 43fa982: exit 0, 22 tests.
    • a_holders_wait_ends_where_its_page_or_its_object_changed: the shrink-and-grow and refused-supply routes end the wait; a withdraw does not, and marks the want.
    • no_interleaving_leaves_a_read_waiting_unasked: a host model of one holder's read against its pager (which reports and answers notices later) and a client that withdraws, fails, shrinks, grows and writes. Every sequence of six steps, each followed by a fair drain, ends the read.
  • Controls, each a checked patch, exit 101, restored identical:
    • the wait ends only on the page (no version exit): both new tests red, the model after [Report, Answer, Supply, Supply, Shrink, Grow]: the read waits for ever;
    • the withdraw marks no waiter: both new tests red, after [Report, Answer, Supply, Supply, Supply, Withdraw];
    • Want::withdrawn never news: those two and a_want_is_named_once_while_waited_and_again_after_a_withdraw red.
  • Clippy with the workspace's adopted lints and -D warnings at 43fa982: -p kernel --lib --tests --features sched-check, -p kernel --target x86_64-unknown-none (default and boot-actuators,test-actuators), -p kernel --target aarch64-unknown-none-softfloat: exit 0 each.
  • Guest: no QEMU row reaches a holder's waiting read. The rows that do, a_pager_s_end_answers_its_waiting_holders_gone (a holder's waiting read, its notice, a whole-object withdraw, the pager's end) and a_served_file_reads_through_its_paged_object (the file server's read through its paged object), run on the metal testcases boot alone. A first dispatch named them as QEMU rows and was refused before running anything: no result.
  • Metal, T14 testcases boot with exactly those two jobs: at ab4ba05 it passed, both exit=0, no "has a read overdue" line, but the fix changes the wait those jobs exercise, so it is restaged at 43fa982 and requested; its readback will be added here.

Evidence: https://github.com/ToyOSOrg/evidence/tree/142a9a18a8011fbd414ae316732af426390026a5 (README.md maps each check to its command, revision, exit and log; r3 is this head, 7ce1e83, and r2 covers 43fa982).

🤖 Generated with Claude Code

`SYS_PAGED_READ` named a reader's absent range in one notice and, while the
reader stayed linked, never again for the same range. A page supplied, the
reader woken, and the page withdrawn before the reader's retry left the
reader asking for the range it had already asked for: no notice went out,
the pager believed it answered, and the reader waited for ever, reported
overdue. Found reading the paged object for 7b's design review.

The request's bookkeeping is now `kernel::paged::Want`, pure and
host-tested: a range is named once while its reader waits, again where it
moved, and again where a withdraw takes back a page of it after its
notice. `withdraw` marks the requests it meets and posts the pager. A
withdraw is the one removal whose pages end absent; 7b's revocation will
end the same way, through the same mark.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
…it go

7b step 2, first part: the paged index's revocation, before any space maps
a paged object. A withdraw, failure, shrink or the object's end now marks a
page revoking instead of removing it. A revoking page reads as absent, takes
no supply (answered present) and no write, keeps its slot and its frame, and
its dirty count goes at once. One walk per object visits each mapper
(`kernel::paged::Mappers`) by epoch; a removal that finds a walk running is
taken by another pass of that walk, known to its caller by the pass's epoch;
a mapper linked during a pass maps nothing revoking and is passed by. The
walk's end gives each frame out with what its page became: absent inside the
object, failed, or removed past the size or with the object.

The kernel's removals go through it. No space maps a paged object yet, so
each walk ends in the hold of the lock that began it; the re-report of #1233
moves to the walk's end, for the pages that end absent.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@Japabu

Japabu commented Nov 11, 2026

Copy link
Copy Markdown
Collaborator Author

Review: #1233 at ab4ba05 (round 1)

Architecture. The fix is in the right place. The request's bookkeeping becomes a pure kernel::paged::Want beside the index it serves. The kernel's withdraw clears reported on the linked requests it meets and posts the pager's watch. That is the single re-report mechanism design rev 4 §3 names for step 2 to reuse.

Withdraw interleavings (verified by reading). Every Want write happens under the pager's lock, and a reader stays linked from its first absent page until it returns. A withdraw that meets a reported request therefore lands either:

  • before the retry's ask: the range is unchanged, so ask does nothing and the notice is still owed; or
  • after it: the withdraw marks the request and posts.

Both re-report. A reader still parked, which never reached its retry, is covered as well; it stranded the same way on main. Each request owes at most one notice, however many withdraws come before the server reads it.

Duplicates do occur, so "no duplicate a pager must tolerate" does not hold. Two cases:

  • a withdraw meets a request the server has read but not yet answered. The file server's own make_room does this whenever it withdraws pages inside a waiting reader's longer range.
  • a withdraw takes a later page of a range whose first page is still awaited.

The file server tolerates both: fill counts present pages as held, so notice returns without failing. Each duplicate costs one device read. Design rev 4 §3 (N1) accepts that cost, so it is not a finding.

Model coverage. Nothing models the interleaving. The host test covers Want alone; its control shows only that withdrawn must report. Deleting the self.ask_again(...) call leaves every test green. For the withdraw case, inspection is enough: there is one lock and no memory ordering, so loom would add nothing. An interleaving model belongs in step 2's paged::tests::mapped.

Required

B1. kernel/src/object/paged.rs:537-556: the same strand stays reachable through a shrink followed by a grow, so the PR's argument is false.

The PR and the commit say a withdraw is "the one removal whose pages end absent", so it is "the one re-report". But a waiter leaves only when ready (lines 538-541) finds its page not Absent, and a page becomes Absent again by two other routes.

  1. A shrink, then a grow, before the woken reader re-checks. Pages::resize (kernel/pure/paged.rs:757) removes pages past the new size. A later grow leaves them Absent for a disk-backed object. The file server does both through Files::truncate (system/fileserver/src/pages.rs:523-535, "cut or grown"); truncated and the refused-write cut-back also shrink.
    • Sequence: reader R requests (p, n) and it is reported. The server supplies p. One client truncates, which shrinks the object and wakes R. Another client extends it. R then runs ready, finds p Absent, and parks again with reported still set.
    • Variant: the server reads the notice between the shrink and the grow. notice finds nothing to read and fails a past-end range (pages.rs:653-661), and Pages::fail inserts nothing past the end. R strands the same way.
    • Either way R waits for ever, reported overdue. That is the R1 defect without a withdraw.
  2. A refused dirty supply over a failed page (kernel/pure/paged.rs:561-571). supply removes the failed slot and then answers DirtyFull, so the page goes from Failed to Absent. A reader woken by the fail that has not yet checked parks again.

Both routes run under a write or a resize, and each moves the object's version. When a holder's read finds the version moved, the loop already answers WouldBlock (Step::Written).

Fix. End the wait on that event: add since.is_some_and(|v| !object.unchanged(v)) to ready. Afterwards, only a withdraw returns a page to Absent without moving the version, and this PR re-reports it.

  • Inspection suffices: the version is monotone, and unchanged is already pure and host-tested.
  • Correct the module header (lines 18-20): the wait also ends on a write or a resize.
  • Correct the PR text's claim that a withdraw is the only route.

Effect on step 2. This also falsifies design rev 4 §3's sentence "a fail or shrink re-reports nothing … its waiters are woken to be refused or answered". Step 2's fault waiters have no read version, so they need a re-report on a grow, or an epoch the waiter compares. Step 2's model must also let a grow fall between a removal's wake and the waiter's re-check. That corrects a detail of the approved design; the orchestrator should decide whether it goes back to the owner.

B2. kernel/pure/paged.rs:819-822: the test's doc comment repeats Want's doc nearly word for word. It is redundant, and the test's name already states the claim. Delete it.

Suggestions

  • S1. Mark the requests in the same lock hold as the removal, for example by giving removing's closure the request list. Between the two holds, a release and an add from another pager thread can reuse the slot. live(id) then names the new object, and its readers get a needless notice. This is harmless but avoidable.
  • S2. Want's second doc sentence says "the pager answered the first notice". A withdraw also re-reports a request the pager has not answered yet. Drop or loosen the sentence.

Evidence, and what the pending boot must show

  • Host test and control (r1/host/host-paged-2.log, mut-withdrawn.log): they check what they claim. git diff 5c487409f ab4ba05ab -- . ':!issues' is empty, and main has not touched either file since b566931.
  • Clippy covers all four kernel shapes.
  • Guest: none, correctly; no QEMU row reaches a waiting holder read.

The queued T14 testcases boot must show:

  • Revision: it runs at the head that carries B1's fix. B1 changes the wait these two jobs exercise, so the boot staged at ab4ba05 no longer covers the head.
  • Jobs: a_pager_s_end_answers_its_waiting_holders_gone and a_served_file_reads_through_its_paged_object both end exit=0.
  • Log: no "has a read overdue" line appears during the boot.

SEND BACK for B1 and B2. After the fix, LAND once the host paged tests and clippy pass at the new head and the T14 boot shows the above.

…ion moved

A waiter left its wait only when its page was no longer absent. A page
becomes absent again by two routes besides a withdraw: a shrink and a grow
before the woken reader looks (the file server's truncate), and a dirty
supply the ceiling refuses over a failed page. Both run under a write or a
resize, which moves the object's version, and a holder's read already
answers `WouldBlock` once its version moved. So the wait now ends there too
(`Pages::wait_over`); afterwards only a withdraw returns a page to absent
without moving the version, and that is the one route re-reported.

The re-report moves into the pure withdraw: `Pages::withdraw` takes the
object's waiters (`Waiters`, which the kernel implements over its request
list) and marks every want its removed range meets in the same hold of the
lock, so a slot released and reused meanwhile gets no stray notice, and the
kernel cannot withdraw without handing its waiters over.

A host model (`paged::tests::wait`) plays one holder's read against its
pager and a client that withdraws, fails, shrinks, grows and writes: every
sequence of six steps, each drained, ends the read. Without the version exit
it strands after a supply, a shrink and a grow; without the marking, after a
supply and a withdraw.

Duplicate notices remain and are accepted: a withdraw marks a request the
server has read and not yet answered, or one whose first page is still
awaited, and the server answers a request for a present page as a supply.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@Japabu

Japabu commented Nov 11, 2026

Copy link
Copy Markdown
Collaborator Author

Response to review r1 (head 43fa982)

  • B1. Fixed as proposed. The wait's ready check is Pages::wait_over (kernel/pure/paged.rs): the page is no longer absent, or the version moved, which the read answers WouldBlock. The module header now lists a write or resize among what ends a wait, and the PR text no longer says a withdraw is the only route.
    • a_holders_wait_ends_where_its_page_or_its_object_changed covers the shrink-and-grow route, the refused dirty supply over a failed page, and a withdraw (which does not end the wait and marks the want instead).
    • no_interleaving_leaves_a_read_waiting_unasked is the interleaving model you asked for: one holder's read against its pager, which reports and answers notices later, and a client that withdraws, fails, shrinks, grows and writes. Every six-step sequence, then drained, ends the read.
    • Both exits are load-bearing: without the version exit the model strands after [Report, Answer, Supply, Supply, Shrink, Grow]; without the marking, after [Report, Answer, Supply, Supply, Supply, Withdraw] (r2/host/mut-*-r2.log in the evidence).
    • Deleting the re-report call is now a type error rather than a silent green: the marking moved into the pure Pages::withdraw, which takes the object's waiters (Waiters, the kernel's Linked over its request list).
  • B2. The test's doc comment is deleted.
  • S1. Taken by the same move: the marking happens in the hold of the lock that removes the pages.
  • S2. Taken: Want's doc no longer says the pager answered the first notice; it says the withdrawn page may have been supplied for it, and points to wait_over for the other routes.
  • Duplicates. The PR text now names both cases and that the design accepts them.
  • Design. The orchestrator's decision is written into design rev 5 §3 (waits end on a version change, so a shrink needs no re-report), with what step 2 relies on: a fault waiter records the version when it parks and requests afresh when its wait ends on a version change.
  • Metal. The T14 testcases boot at ab4ba05 passed (both exit=0, no overdue line) but no longer covers the head; it is restaged at 43fa982 and requested.

Japabu added a commit that referenced this pull request Nov 11, 2026
…ion moved

A waiter left its wait only when its page was no longer absent. A page
becomes absent again by two routes besides a withdraw: a shrink and a grow
before the woken reader looks (the file server's truncate), and a dirty
supply the ceiling refuses over a failed page. Both run under a write or a
resize, which moves the object's version, and a holder's read already
answers `WouldBlock` once its version moved. So the wait now ends there too
(`Pages::wait_over`); afterwards only a withdraw returns a page to absent
without moving the version, and that is the one route re-reported.

The re-report moves into the pure withdraw: `Pages::withdraw` takes the
object's waiters (`Waiters`, which the kernel implements over its request
list) and marks every want its removed range meets in the same hold of the
lock, so a slot released and reused meanwhile gets no stray notice, and the
kernel cannot withdraw without handing its waiters over.

A host model (`paged::tests::wait`) plays one holder's read against its
pager and a client that withdraws, fails, shrinks, grows and writes: every
sequence of six steps, each drained, ends the read. Without the version exit
it strands after a supply, a shrink and a grow; without the marking, after a
supply and a withdraw.

Duplicate notices remain and are accepted: a withdraw marks a request the
server has read and not yet answered, or one whose first page is still
awaited, and the server answers a request for a present page as a supply.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
…it go

7b step 2, first part: the paged index's revocation, before any space maps
a paged object. A withdraw, failure, shrink or the object's end now marks a
page revoking instead of removing it. A revoking page reads as absent, takes
no supply (answered present) and no write, keeps its slot and its frame, and
its dirty count goes at once. One walk per object visits each mapper
(`kernel::paged::Mappers`) by epoch; a removal that finds a walk running is
taken by another pass of that walk, known to its caller by the pass's epoch;
a mapper linked during a pass maps nothing revoking and is passed by. The
walk's end gives each frame out with what its page became: absent inside the
object, failed, or removed past the size or with the object.

#1233's re-report follows the pages: the walk's end names again every
waiter's want a page that ends absent meets, and a withdraw names them for
the failed pages it removes at once, which have no frame to revoke; both
take the waiters (`Waiters`). The kernel's removals go through it. No space
maps a paged object yet, so each walk ends in the hold of the lock that
began it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
Design rev 5 §3 (after review r1 of #1233): a waiter's wait ends on a write
or resize of its object as well as on its page, and a fault, which has no
read to answer `WouldBlock`, then asks for its page afresh. The index gains
the two pieces the fault path will use: `Object::version`, where a fault's
wait begins, and `Want::anew`, a request named in a notice whatever the old
one said.

The model's parked faults record the version they parked at, look again
whether or not their wake was theirs, and ask afresh where the version
moved. `a_fault_answered_then_shrunk_and_grown_asks_afresh` plays the strand
rev 5 names: a fault's request read and answered, then a shrink and a grow
before it looks. Asking the same want instead leaves it parked for ever.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@Japabu

Japabu commented Nov 11, 2026

Copy link
Copy Markdown
Collaborator Author

Review: #1233 at 43fa982 (round 2, follow-up to ab4ba05)

Architecture. The fix is the one review r1 asked for, and it is simpler than r1's head.

  • A holder's wait now ends on Pages::wait_over: the page is no longer absent, or the version moved. This is pure and sits next to lookup.
  • The re-report has moved into the pure Pages::withdraw, which marks every Want its range meets in the same hold that removes the pages. The kernel's separate ask_again pass is gone, and S1's slot-reuse window with it.
  • Waiters is the narrow boundary this needs, because the pure crate cannot walk the kernel's raw request list. Its real implementation is Linked; the other two are test doubles.
  • Size: +357/−39 against b566931 (pure +293/−11, kernel +64/−28), which matches the PR body. There is no ABI change and no manual change. The manual has no page on this wait, and the answer a holder sees after a write or resize is still WouldBlock.

Prior findings

  • B1: resolved. Details in Q1 below.
  • B2: resolved. The redundant doc on a_want_is_named_once_while_waited_and_again_after_a_withdraw is deleted.
  • S1: taken.
  • S2: taken. Want's doc now says the page "may have been supplied for that notice".

The four questions

Q1. Every route that makes a page absent again ends or re-reports the wait. Enumerated from the call sites of Pages::remove (kernel/pure/paged.rs):

  • supply over a failed slot (577), then DirtyFull (583). A dirty supply comes only through PagerObject::supply, so Object::write_begin has already moved the version. supply_pages posts changed after the install hold (kernel/src/object/paged.rs:774), so the wait ends. A clean supply cannot be refused once it has removed the slot: tracked is false, and the slot it freed rules out NoRoom.
  • withdraw (729). This includes a withdraw of a failed slot, whose State::CLEAN passes take's check. The version does not move, so the withdraw marks the overlapping wants in that same hold, news posts the pager's watch, and removing posts changed.
  • resize shrink (788), then a grow. o.version += 1 comes first (778), and removing posts.
  • fail (765). It removes the frame and re-inserts the page Failed, never absent. The re-insert cannot fail because the remove just freed a slot. The woken reader answers Io.
  • invalidate and release. These answer Gone, and wait_over sees Lookup::Gone.

The marking cannot miss a page. Any removed page inside the want's range lies inside the withdraw's range, so the two ranges meet, and removed > 0 holds.

The over-marking that remains is the duplicate case the description accepts. Linked filters by slot, and a waiter's slot cannot be reused while its holder's Named reference lives.

The only notice still lost is a pager's own notices call into a buffer that faults (paged.rs:432). That is unchanged, documented, and a bug in the pager; the reader is reported overdue.

Q2. The model is adequate.

  • Abstraction. One page, one reader, and steps that each correspond to one hold of the pager's lock.
  • Reachable states. While the version is unchanged, the state is: the page (absent, present or failed), whether the want is reported, and whether a request is outstanding. That is 12 states, and each is reachable within four steps. Any version move ends the read at the next Look. So six steps visits every reachable state, and the test drains from each prefix. played > 10_000 guards against a vacuous run.
  • Refused as one step. The model plays write-begin, supply and write-end as a single step. That loses nothing, because the version moves first.
  • The Look guard. The kernel re-looks after ready() even when the state has changed since; the model plays Look only while wait_over holds. A look that finds the page absent with the version unchanged only re-asks the same range, which is a no-op, so the guard drops nothing.
  • Outside the model, by inspection. Multi-page and moving ranges, several readers, and slot filtering, all covered in Q1.
  • The news return value. The model ignores it, but it drives the pager's watch.post(). The unit test's (1, true) holds it, so the unit test is not redundant.

Q3. Not every version move wakes waiters. The version moves in Object::write_begin, Object::write_end, Object::end_write and Pages::resize. changed is posted only at paged.rs:309 (removing), :324 (release), :774 (supply chunk) and :1140 (pager end).

  • Waking moves. A resize wakes through removing. A dirty supply's first move, at write_begin, comes before the post at supply_pages.
  • Silent moves. PagerObject::write (792-800, both moves), PagerObject::end_write (650-657), and a dirty supply's write_end all post nothing. The syscall layer adds no post either (syscall/paged.rs:136,143).
  • Liveness is unaffected. None of these moves changes whether any page is present. Every route in Q1 posts after its version move or its marking. A parked holder therefore wakes at the next supply, removal, release or end, or at its report deadline: wait_until re-evaluates ready there (watch.rs:234-237), finds the wait over, and answers WouldBlock.

Q4. Mostly, with one deviation. Rev 5 §3 is implemented in three respects:

  • waits end on a version change;
  • a shrink re-reports nothing;
  • a withdraw marks its waiters in the hold that removes the pages and posts the pager's watch.

The deviation is Q3: rev 5 says "every move of the object's version (a write's end, a resize, a refused dirty supply inside a write) wakes every request of the object". A pager write and end_write do not. In step 1, a withdraw still posts changed, contrary to rev 5's "a withdraw's end wakes nothing". That clause belongs to step 2's per-request wakes; under step 1's broadcast the woken waiters simply re-park, so it is not a finding.

Required

B3. kernel/src/object/paged.rs:18-22: the module contract rewritten in this round says the wait ends on "a write or resize of the object", but a pager write does not end it.

  • Problem. PagerObject::write and end_write move the version without posting changed. A holder parked across a pager write stays parked until some other post, or its report deadline (up to 10 s).
  • Consequence. No strand, by Q3. But the contract is false, and the code does not implement the rev 5 decision the PR cites. The changed field doc (195-197: "a supply, a failure, a shrink, a release, the end") contradicts the header in turn.
  • Fix (preferred). Post changed at a write's end, in PagerObject::write_end and end_write, after the lock is dropped, and list it in changed's doc. That is two posts, it makes the header true, and it matches rev 5 as decided.
  • Fix (alternative). If the orchestrator prefers not to wake on writes, narrow the header to the events that actually wake a parked holder, and correct rev 5's sentence. That correction is the orchestrator's to make.
  • Evidence needed. For the preferred fix, a compile (one clippy shape) is enough, plus inspection. An added post only makes waiters re-evaluate the pure ready(), so it can end a wait early, but only with the answer the next wake would have given. Neither option invalidates the host tests, the controls, or the queued T14 boot at 43fa982.

Evidence

  • Host tests. cargo test -p kernel --lib -- paged::: exit 0, 22 passed (r2/host/host-paged-r2.log). The tested worktree is clean at 43fa982, and the log was written 19 s before the commit, with no edit in between.

  • Controls. All three exit 101 and were restored identical:

    • no version exit: both new tests red, [Report, Answer, Supply, Supply, Shrink, Grow];
    • no marking: both new tests red, [Report, Answer, Supply, Supply, Supply, Withdraw];
    • withdrawn never news: three tests red.

    Each control targets exactly one mechanism, and its counterexample is the strand B1 described.

  • Clippy. All four kernel shapes exit 0 at 43fa982 (clippy-r2.rev).

  • Guest. None, correctly. No QEMU row reaches a holder's waiting read.

  • Metal. The T14 testcases boot is staged at 43fa982 with exactly a_pager_s_end_answers_its_waiting_holders_gone and a_served_file_reads_through_its_paged_object (r2/metal/stage-t14-r2.log, exit 2 = staged). It must show both jobs exit=0 and no "has a read overdue" line. The boot staged at ab4ba05 is superseded, as the PR says.

Overlaps

SEND BACK for B3. After it, LAND once the T14 boot shows the above. B3 needs no further runs beyond a compile.

The module header says a wait ends on a write or resize of the object, and
design rev 5 says every move of the version wakes the object's waiters, but
a pager's write, its `end_write` and a dirty supply's write end moved the
version without posting `changed`: a holder parked across a pager write
slept on until another post or its report deadline. `write_end` and
`end_write` now post `changed` once the lock is dropped, and `changed`'s doc
lists a write's end. A post only makes a waiter look again at its pure
`ready`, so it can end a wait early, never with another answer.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@Japabu

Japabu commented Nov 11, 2026

Copy link
Copy Markdown
Collaborator Author

Response to review r2 (head 7ce1e83)

  • B3. Fixed as preferred (the orchestrator's decision): write_end and end_write post changed after the lock is dropped, so a holder parked across a pager write is woken at its end; changed's doc now lists a write's end, so it agrees with the header and with design rev 5. The dirty supply ends through write_end too.
  • Checks. Clippy on the x86-64 kernel shape and cargo check of the AArch64 kernel exit 0 at 7ce1e83 (evidence r3/). No host test reaches the post itself, which is kernel code; a wake test would need a guest or loom harness for PagerObject, so none is added. As you note, r2's host tests, controls and the T14 boot staged at 43fa982 stand.

Japabu added a commit that referenced this pull request Nov 11, 2026
The module header says a wait ends on a write or resize of the object, and
design rev 5 says every move of the version wakes the object's waiters, but
a pager's write, its `end_write` and a dirty supply's write end moved the
version without posting `changed`: a holder parked across a pager write
slept on until another post or its report deadline. `write_end` and
`end_write` now post `changed` once the lock is dropped, and `changed`'s doc
lists a write's end. A post only makes a waiter look again at its pure
`ready`, so it can end a wait early, never with another answer.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@Japabu

Japabu commented Nov 11, 2026 •

Copy link
Copy Markdown
Collaborator Author

Review: #1233 at 7ce1e83 (round 3, follow-up to 43fa982)

Scope. This round checks r2's blocker B3 and the one commit that fixes it: git diff 43fa98206 7ce1e832e, which changes only kernel/src/object/paged.rs (+14/−5). Nothing else is reopened.

Architecture. This is r2's preferred fix and nothing more. The commit adds two posts of the existing changed watch, both after the lock is released, and corrects one line of doc. It adds no state or mechanism. The whole branch is now +371/−44 against b566931.

B3: resolved

Every version move now wakes the object's waiters. In kernel/pure/paged.rs the version moves in three places: Object::write_begin (327), Object::write_end (339, which end_write also reaches) and Pages::resize (778). Here is how each reaches a post on the kernel side:

  • A write's begin. PagerObject::write_begin (632) has two callers, a dirty supply (678) and write (802). Each calls write_end unconditionally once its copy returns (683, 807), with no return in between. So the post at the end of the call delivers the move made at its start. Rev 5 §3 names "a write's end" as the event that wakes, so this matches it.
  • write_end (643-651). It posts in both branches of Object::write_end. A short call that leaves the write held does not move the version at its end. Its post still delivers the move the same call made at its begin.
  • end_write (654-666). It posts on Ok only. Its Err paths, a refused live or no held write, move nothing.
  • resize. It runs through removing, which posts on every live call (309), so a grow wakes as a shrink does.
  • A refused dirty supply. supply_pages posts after each chunk (783), and write_end posts again. Every early return from supply_pages is still followed by write_end.

The syscall layer (kernel/src/syscall/paged.rs:107-152) reaches the version only through these methods, and it holds no lock.

No waiter can be lost. wait_until (kernel/src/watch.rs:219-245) registers before it reads ready. ready takes the pager's lock (paged.rs:545-548), the version moves under that lock, and the post comes after the lock is released. That leaves two cases:

  • The post precedes the registration. It also follows the move, so the waiter's next ready reads the moved version under the lock.
  • The post follows the registration. It writes the registered thread's state word, so the thread does not park.

A holder also cannot park between a write's begin and its end. unwritten answers Written once the version has moved (481), and read_begin refuses while writing > 0.

No self-deadlock. Both posts run with no lock held:

  • write_end's guard ends with its block, end_write drops state before its match, and neither caller holds a lock.
  • changed has no polls (it is used only in object/paged.rs), so the poll-ring exception to posting does not arise.
  • A woken reader takes only the pager's lock, which is already released.

The comments are now true.

  • Module header (18-22). It says the wait ends on "a supply, a failure, a write or resize of the object …, a release, the pager's end or a kill". Each of these posts changed after its change: a supply at 783, a failure and a resize at 309, a write at 650 and 661, a release at 324, the pager's end at 1149. A kill ends the park.
  • changed's doc (195-197). It is true too. Replacing "a shrink" with "a resize" also fixes a second inaccuracy, since a grow posts through removing. The list is not exhaustive (a withdraw also posts, through removing), but it does not claim to be, and r2 settled that post as step 1's broadcast.

The evidence is sufficient. For these two posts, r2 asked for one compile plus inspection. The PR supplies both checks at 7ce1e83, each exit 0 (evidence 142a9a1, r3/host/):

  • cargo clippy -p kernel --target x86_64-unknown-none … -D warnings;
  • cargo check -p kernel --target aarch64-unknown-none-softfloat.

The changed code sits under no cfg, so the other clippy shapes would add nothing. Reusing r2's host tests, controls and the T14 staging at 43fa982 is sound. The pure crate is unchanged, and a post can only make a waiter re-run its pure ready sooner, with the answer the next wake would have given.

A wake test is not needed.

  • A pure-side assertion cannot observe the post, because the pure crate has no watch.
  • The pure side's version moves are already asserted, in a_short_call_holds_the_write_until_its_end and a_holders_wait_ends_where_its_page_or_its_object_changed.
  • Enforcing the post by type, with a #[must_use] token from the calls that move the version, would add machinery for two straight-line call sites.

Inspection establishes the claim.

Overlap with main. origin/main (6d0cb3a) has not touched either file since b566931, and git merge-tree --write-tree 6d0cb3ae9 7ce1e832e exits 0.

Suggestion

S3. kernel/src/object/paged.rs:660: delete // As at `write_end`. It only points elsewhere and says nothing itself, and changed's doc now lists a write's end. The comment at 649 may stay, because it says why a write posts even though it removes no page. It may also go for the same reason as 660. Optional either way.

For the orchestrator (PR description)

  • Evidence pointer. The body's "(r2 is this head)" is stale. Evidence commit 142a9a1 has an r3 section for 7ce1e83, while r2 covers 43fa982.
  • Size. "+357 / -39" is the count at 43fa982. At this head it is +371 / −44.

LAND, pending the T14 testcases boot staged at 43fa982. That boot must show both jobs exit=0 and no "has a read overdue" line.

@Japabu

Japabu commented Nov 11, 2026

Copy link
Copy Markdown
Collaborator Author

Orchestrator: T14 testcases boot at 43fa982 (build line 43fa98206… clean; verdict passed) shows ===TEST_END test_rs_a_pager_s_end_answers_its_waiting_holders_gone exit=0=== and ===TEST_END test_rs_a_served_file_reads_through_its_paged_object exit=0===, with no "has a read overdue" line. Review r3 LAND at 7ce1e83, whose only change since 43fa982 is the two post-unlock wakes; reusing the boot was accepted in r2/r3. Queueing.

@Japabu
Japabu marked this pull request as ready for review November 11, 2026 18:02
@Japabu
Japabu added this pull request to the merge queue Nov 11, 2026
Merged via the queue into main with commit 09eedb4 Nov 11, 2026
10 checks passed
@Japabu
Japabu deleted the paged-rereport branch November 11, 2026 18:22
Japabu added a commit that referenced this pull request Nov 11, 2026
…it go

7b step 2, first part: the paged index's revocation, before any space maps
a paged object. A withdraw, failure, shrink or the object's end now marks a
page revoking instead of removing it. A revoking page reads as absent, takes
no supply (answered present) and no write, keeps its slot and its frame, and
its dirty count goes at once. One walk per object visits each mapper
(`kernel::paged::Mappers`) by epoch; a removal that finds a walk running is
taken by another pass of that walk, known to its caller by the pass's epoch;
a mapper linked during a pass maps nothing revoking and is passed by. The
walk's end gives each frame out with what its page became: absent inside the
object, failed, or removed past the size or with the object.

#1233's re-report follows the pages: the walk's end names again every
waiter's want a page that ends absent meets, and a withdraw names them for
the failed pages it removes at once, which have no frame to revoke; both
take the waiters (`Waiters`). The kernel's removals go through it. No space
maps a paged object yet, so each walk ends in the hold of the lock that
began it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
Design rev 5 §3 (after review r1 of #1233): a waiter's wait ends on a write
or resize of its object as well as on its page, and a fault, which has no
read to answer `WouldBlock`, then asks for its page afresh. The index gains
the two pieces the fault path will use: `Object::version`, where a fault's
wait begins, and `Want::anew`, a request named in a notice whatever the old
one said.

The model's parked faults record the version they parked at, look again
whether or not their wake was theirs, and ask afresh where the version
moved. `a_fault_answered_then_shrunk_and_grown_asks_afresh` plays the strand
rev 5 names: a fault's request read and answered, then a shrink and a grow
before it looks. Asking the same want instead leaves it parked for ever.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
Main's #1233 ends a holder's wait for an absent page where the object's
version moved, and the read there answered WouldBlock. Here a holder's
read that meets a write begins again instead, until it met
READ_RESTARTS writes; its want of the page would then be the range it
already named, which the pager answered before the write made the page
absent again, so no notice would name it and the read would wait for
ever. A read that begins again now asks anew (Want::anew), and main's
model of the wait plays the restart. The pager's write is its hold, so
main's tests take and give the write side where they began and ended a
write.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
…it go

7b step 2, first part: the paged index's revocation, before any space maps
a paged object. A withdraw, failure, shrink or the object's end now marks a
page revoking instead of removing it. A revoking page reads as absent, takes
no supply (answered present) and no write, keeps its slot and its frame, and
its dirty count goes at once. One walk per object visits each mapper
(`kernel::paged::Mappers`) by epoch; a removal that finds a walk running is
taken by another pass of that walk, known to its caller by the pass's epoch;
a mapper linked during a pass maps nothing revoking and is passed by. The
walk's end gives each frame out with what its page became: absent inside the
object, failed, or removed past the size or with the object.

#1233's re-report follows the pages: the walk's end names again every
waiter's want a page that ends absent meets, and a withdraw names them for
the failed pages it removes at once, which have no frame to revoke; both
take the waiters (`Waiters`). The kernel's removals go through it. No space
maps a paged object yet, so each walk ends in the hold of the lock that
began it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
Design rev 5 §3 (after review r1 of #1233): a waiter's wait ends on a write
or resize of its object as well as on its page, and a fault, which has no
read to answer `WouldBlock`, then asks for its page afresh. The index gains
the two pieces the fault path will use: `Object::version`, where a fault's
wait begins, and `Want::anew`, a request named in a notice whatever the old
one said.

The model's parked faults record the version they parked at, look again
whether or not their wake was theirs, and ask afresh where the version
moved. `a_fault_answered_then_shrunk_and_grown_asks_afresh` plays the strand
rev 5 names: a fault's request read and answered, then a shrink and a grow
before it looks. Asking the same want instead leaves it parked for ever.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
…it go

7b step 2, first part: the paged index's revocation, before any space maps
a paged object. A withdraw, failure, shrink or the object's end now marks a
page revoking instead of removing it. A revoking page reads as absent, takes
no supply (answered present) and no write, keeps its slot and its frame, and
its dirty count goes at once. One walk per object visits each mapper
(`kernel::paged::Mappers`) by epoch; a removal that finds a walk running is
taken by another pass of that walk, known to its caller by the pass's epoch;
a mapper linked during a pass maps nothing revoking and is passed by. The
walk's end gives each frame out with what its page became: absent inside the
object, failed, or removed past the size or with the object.

#1233's re-report follows the pages: the walk's end names again every
waiter's want a page that ends absent meets, and a withdraw names them for
the failed pages it removes at once, which have no frame to revoke; both
take the waiters (`Waiters`). The kernel's removals go through it. No space
maps a paged object yet, so each walk ends in the hold of the lock that
began it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
Design rev 5 §3 (after review r1 of #1233): a waiter's wait ends on a write
or resize of its object as well as on its page, and a fault, which has no
read to answer `WouldBlock`, then asks for its page afresh. The index gains
the two pieces the fault path will use: `Object::version`, where a fault's
wait begins, and `Want::anew`, a request named in a notice whatever the old
one said.

The model's parked faults record the version they parked at, look again
whether or not their wake was theirs, and ask afresh where the version
moved. `a_fault_answered_then_shrunk_and_grown_asks_afresh` plays the strand
rev 5 names: a fault's request read and answered, then a shrink and a grow
before it looks. Asking the same want instead leaves it parked for ever.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
…it go

7b step 2, first part: the paged index's revocation, before any space maps
a paged object. A withdraw, failure, shrink or the object's end now marks a
page revoking instead of removing it. A revoking page reads as absent, takes
no supply (answered present) and no write, keeps its slot and its frame, and
its dirty count goes at once. One walk per object visits each mapper
(`kernel::paged::Mappers`) by epoch; a removal that finds a walk running is
taken by another pass of that walk, known to its caller by the pass's epoch;
a mapper linked during a pass maps nothing revoking and is passed by. The
walk's end gives each frame out with what its page became: absent inside the
object, failed, or removed past the size or with the object.

#1233's re-report follows the pages: the walk's end names again every
waiter's want a page that ends absent meets, and a withdraw names them for
the failed pages it removes at once, which have no frame to revoke; both
take the waiters (`Waiters`). The kernel's removals go through it. No space
maps a paged object yet, so each walk ends in the hold of the lock that
began it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 11, 2026
Design rev 5 §3 (after review r1 of #1233): a waiter's wait ends on a write
or resize of its object as well as on its page, and a fault, which has no
read to answer `WouldBlock`, then asks for its page afresh. The index gains
the two pieces the fault path will use: `Object::version`, where a fault's
wait begins, and `Want::anew`, a request named in a notice whatever the old
one said.

The model's parked faults record the version they parked at, look again
whether or not their wake was theirs, and ask afresh where the version
moved. `a_fault_answered_then_shrunk_and_grown_asks_afresh` plays the strand
rev 5 names: a fault's request read and answered, then a shrink and a grow
before it looks. Asking the same want instead leaves it parked for ever.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 12, 2026
Design rev 5 §3 (after review r1 of #1233): a waiter's wait ends on a write
or resize of its object as well as on its page, and a fault, which has no
read to answer `WouldBlock`, then asks for its page afresh. The index gains
the two pieces the fault path will use: `Object::version`, where a fault's
wait begins, and `Want::anew`, a request named in a notice whatever the old
one said.

The model's parked faults record the version they parked at, look again
whether or not their wake was theirs, and ask afresh where the version
moved. `a_fault_answered_then_shrunk_and_grown_asks_afresh` plays the strand
rev 5 names: a fault's request read and answered, then a shrink and a grow
before it looks. Asking the same want instead leaves it parked for ever.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 12, 2026
…it go

7b step 2, first part: the paged index's revocation, before any space maps
a paged object. A withdraw, failure, shrink or the object's end now marks a
page revoking instead of removing it. A revoking page reads as absent, takes
no supply (answered present) and no write, keeps its slot and its frame, and
its dirty count goes at once. One walk per object visits each mapper
(`kernel::paged::Mappers`) by epoch; a removal that finds a walk running is
taken by another pass of that walk, known to its caller by the pass's epoch;
a mapper linked during a pass maps nothing revoking and is passed by. The
walk's end gives each frame out with what its page became: absent inside the
object, failed, or removed past the size or with the object.

The re-report of #1233 follows the pages: the walk's end names again every
waiter's want a page that ends absent meets, and a withdraw names them for
the failed pages it removes at once, which have no frame to revoke; both
take the waiters (`Waiters`). The kernel's removals go through it. No space
maps a paged object yet, so each walk ends in the hold of the lock that
began it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 12, 2026
Design rev 5 §3 (after review r1 of #1233): a waiter's wait ends on a write
or resize of its object as well as on its page, and a fault, which has no
read to answer `WouldBlock`, then asks for its page afresh. The index gains
the two pieces the fault path will use: `Object::version`, where a fault's
wait begins, and `Want::anew`, a request named in a notice whatever the old
one said.

The model's parked faults record the version they parked at, look again
whether or not their wake was theirs, and ask afresh where the version
moved. `a_fault_answered_then_shrunk_and_grown_asks_afresh` plays the strand
rev 5 names: a fault's request read and answered, then a shrink and a grow
before it looks. Asking the same want instead leaves it parked for ever.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 12, 2026
…it go

7b step 2, first part: the paged index's revocation, before any space maps
a paged object. A withdraw, failure, shrink or the object's end now marks a
page revoking instead of removing it. A revoking page reads as absent, takes
no supply (answered present) and no write, keeps its slot and its frame, and
its dirty count goes at once. One walk per object visits each mapper
(`kernel::paged::Mappers`) by epoch; a removal that finds a walk running is
taken by another pass of that walk, known to its caller by the pass's epoch;
a mapper linked during a pass maps nothing revoking and is passed by. The
walk's end gives each frame out with what its page became: absent inside the
object, failed, or removed past the size or with the object.

The re-report of #1233 follows the pages: the walk's end names again every
waiter's want a page that ends absent meets, and a withdraw names them for
the failed pages it removes at once, which have no frame to revoke; both
take the waiters (`Waiters`). The kernel's removals go through it. No space
maps a paged object yet, so each walk ends in the hold of the lock that
began it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 12, 2026
Design rev 5 §3 (after review r1 of #1233): a waiter's wait ends on a write
or resize of its object as well as on its page, and a fault, which has no
read to answer `WouldBlock`, then asks for its page afresh. The index gains
the two pieces the fault path will use: `Object::version`, where a fault's
wait begins, and `Want::anew`, a request named in a notice whatever the old
one said.

The model's parked faults record the version they parked at, look again
whether or not their wake was theirs, and ask afresh where the version
moved. `a_fault_answered_then_shrunk_and_grown_asks_afresh` plays the strand
rev 5 names: a fault's request read and answered, then a shrink and a grow
before it looks. Asking the same want instead leaves it parked for ever.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 12, 2026
…it go

7b step 2, first part: the paged index's revocation, before any space maps
a paged object. A withdraw, failure, shrink or the object's end now marks a
page revoking instead of removing it. A revoking page reads as absent, takes
no supply (answered present) and no write, keeps its slot and its frame, and
its dirty count goes at once. One walk per object visits each mapper
(`kernel::paged::Mappers`) by epoch; a removal that finds a walk running is
taken by another pass of that walk, known to its caller by the pass's epoch;
a mapper linked during a pass maps nothing revoking and is passed by. The
walk's end gives each frame out with what its page became: absent inside the
object, failed, or removed past the size or with the object.

The re-report of #1233 follows the pages: the walk's end names again every
waiter's want a page that ends absent meets, and a withdraw names them for
the failed pages it removes at once, which have no frame to revoke; both
take the waiters (`Waiters`). The kernel's removals go through it. No space
maps a paged object yet, so each walk ends in the hold of the lock that
began it.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Japabu added a commit that referenced this pull request Nov 12, 2026
Design rev 5 §3 (after review r1 of #1233): a waiter's wait ends on a write
or resize of its object as well as on its page, and a fault, which has no
read to answer `WouldBlock`, then asks for its page afresh. The index gains
the two pieces the fault path will use: `Object::version`, where a fault's
wait begins, and `Want::anew`, a request named in a notice whatever the old
one said.

The model's parked faults record the version they parked at, look again
whether or not their wake was theirs, and ask afresh where the version
moved. `a_fault_answered_then_shrunk_and_grown_asks_afresh` plays the strand
rev 5 names: a fault's request read and answered, then a shrink and a grow
before it looks. Asking the same want instead leaves it parked for ever.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant