[Japabu]

Draft. On main 29c5f2d. The branch was rebased onto 302fb36 (#1259, #1273, #1271 and #1252 among it). Main with #1258 is merged in (6e43e99), followed by 9a29a35 and ea33f5a. Main 29c5f2d (#1227, #1264, #1280) is merged in after them (202566e), and review r12's text follows (63f18b2). Every commit here is step 2's, composed with #1273's slot table, #1223's per-space futex revocation and #1258's holder writes. Review r1 was answered in acff199..5eadbcd, r2 in 5513d27 and 6455b27, r3 in d594827, r4 in 76bcaa5, r5 in eb7deec, r6 in d1ad82e, r8 in 54c90cc and 54d6a6a, and r9 in ecfb224; populate keeps main's hoisted fault-around shape in every commit. For r8 the branch was rebuilt to restore a line of its first commit's message, and mapprobe's pipe_end takes its endowed pipe end typed, as main's typed handles (#1239, #1242) require, in the probe commit and every later one; nothing else differs from fd13c11's trees.

What changes

Step 2 of mapped paged objects (memory stage 7b, design rev 5): a file's pages are mapped read-only and shared through its holder. A mapping maps the pager's own frames, so a mapper sees a write as it lands; nothing is copied and the file's length is never committed.

• A mapping holds its object. One node per (space, object) on the object's list of mappers, charged to the mapper's job, held by every range of the object in the space. A mapping counts as a holder, so mmap, close, unlink keeps the file until the last mapping goes.
• Revocation. A withdraw, fail, shrink, release or pager end marks its pages revoking; each keeps its frame until a walk of the object's mappers has cleared and shot down every space's leaves of it, then the frame goes back. The object keeps the walk's set, its revoking pages in marking order; a visit reads it 64 at a time under the pager's lock alone and clears that batch's leaves under the space's lock alone, so it holds one lock at a time and costs O(revoking pages). Before any frame of an object a mapper ever linked goes back, the walk ends every futex wait on a frame of its set, after the last pass's visits, in all 64 buckets (revoke_sorted), since such a frame is no one space's. An object no mapper ever linked, as nearly every /tmp file and cache withdraw is, skips that sweep: only a mapping's leaf keys a futex wait on its frames. The object's bit is set by Object::link, the only way a node learns its epoch, and never resets, since an unmap clears its leaves without ending a wait keyed through them. The walk's steps: Pages::walk answers Visit or Sweep, or ends the walk itself (Finished, its private finish giving the frames out), and sweeps again whenever a pass began since it was last told to, so a page marked while a sweep had the lock dropped is swept too and no caller can give frames back off the rule. No wait arms on a frame once its pass's visits are done: no leaf maps a revoking frame, no fault installs one, and a visit's shootdown is counted, so a futex wait that translated before the visit looks at its leaf again (A futex wait translates its word once and checks it with one load #1253's Translation::holds) rather than trust the translation; so a waiter keyed on a frame through a leaf an unmap, discard, protect to none or a space's end cleared earlier, which revoke only frames they own, is ended before the frame is reissued. A page a pager names is placed by checked arithmetic, so no pager input can overflow it. One walker per object; pager end never waits (a removal during a walk is taken by the walker's next pass). A walk's end names again every waiter whose page ended absent.
• A fault on an absent page parks on its pager, holding no lock and no pin: it requests the aligned 64 KiB run, waits until the page is no longer absent, the object's version moved or the pager is gone, and touches it again; a fault whose wait a version change ended asks afresh. Past the pager's report time it is logged overdue and goes on (D6); a kill ends it. The CPU's fault mark is down while it waits and up again on whichever CPU it wakes on, on both architectures.
• A refused page says why. A Ring 3 touch of a page its pager failed, released or can no longer supply (its end, D1) ends the process with the new Fault::Mapping (SIGBUS) and one record naming the pager, object, page and cause. A kernel copy answers Io instead of BadAddress (a per-thread stop word the copy's fault leaves); pipes and paged calls carry it. A touch of a page wholly past the object's end ends the process with Fault::Mapping too (the orchestrator's ruling); nothing is there, so a copy from it, or a futex word in it, answers BadAddress. A futex wait or wake on a mapped page that is absent or lost is a spurious wake, as the manual says of swapped words.
• A touched hole of an anonymous object (a MEMORY volume's, /tmp) gets a zeroed frame of its pager's, drawn and charged as a supply's frame is (pmm::alloc_promised from the pager's core, or a held-aside frame zeroed as supply already does), installed clean under the pager's lock; with no room, the fault is refused NoRoom (N4). There is one draw: spawnperf's first-touch shared memory uses the same alloc_promised, and A draw of many promised frames takes the allocator's lock once #1268's batch draws are not needed by a fault, which draws one frame.
• A process's end empties its space (AddressSpace::end), so a revoker's last reference to a space frees nothing; Drop asserts no paged range is left.
• SDK and libc: Paged::map, files::map (through the descriptor's holder; NotSupported without one); libc mmap of a file PROT_READ, shared or private (B5: a private read-only mapping shares the pages until written). Other protections still answer ENODEV (record updated).

Decision: no wait holds a pin (the orchestrator's ruling)

A kernel copy that holds a page pin never parks on an absent mapped page. Such a copy runs under user_ptr::Pinned; its fault on an absent paged page stops the copy (Stopped::Absent) instead of waiting, and the call lets its pins go, waits for the window's pages holding nothing (wait_in), and copies the rest of the chunk again. Three copies use it. Two are pinned copies, a holder's read into user memory and the pager's write from user memory, and no process reaches them: a pager's process may not map, and every mapping is read-only, so no pinned copy's window can be an absent paged page. The third is #1258's holder write (9a29a35), which stages its bytes into frames drawn from its pager before it takes the write side. Those frames are what that pager's supply draws, so the staging copy stops at an absent page too, gives every frame back, waits holding nothing and draws again. mapprobe's written case shows a holder write sourced from a mapped page not yet supplied landing whole.

Manual

Memory page: a mapping maps the cache's own pages and holds its file; a page leaves the cache only once no mapping reaches it; a wait for a file's page behaves like swapped memory's (D6); a lost page ends the program with a diagnostic and a copy answers an I/O error; a touched RAM-file hole is resident within its server's capacity. Files and services pages: a file server's end revokes every mapping of its files (D1, in the ruling's words).

Checks and evidence

What each check covers, and why it suffices (the owner's testing policy: touched modules only):

• Pure model (cargo test -p kernel --lib paged::, 45 tests with An open file is written and stated through its paged object, one write at a time, against credit #1258's merged in, r8's exploration from a walk begun on an object no mapper has linked, which a mapper links during, among them, the walk's set, r3's sweep sequence, r5's futex wait translated before a visit, and explorations from a waiter an unmap left and from a wait translated before a removal among them, the model's check refusing a waiter keyed on a given-back frame after every step; its visit and its sweep are the kernel's rules with batches of one, each a step others run between, and its oracle includes a futex waiter that translates and arms apart as the kernel's does, keyed through a leaf and ended only by a sweep): the index's revocation with two spaces mapping one object, every interleaving at depth, invariants at every step (each leaf maps the index's frame or a revoking slot's; a frame goes back only after every mapper's visit). That a node is linked exactly while its space has a range holds by construction, since the model's map and unmap are each one step; check does not test it; parked faults all complete once removals stop; a fault answered, shrunk and grown asks afresh. Current controls, each a checked patch: the reviewer's (r3) cursor that reads only the first batch reds both model runs ("maps given-back frame") and the walk's-set test; sweeping before the pass's visits (B8's defect) reds both model runs on the model's own oracle, a futex waiter keyed through a leaf ("frame N given back with a futex waiter keyed on it"); the rule before r3, a visit resetting the sweep flag, reds the exploration from a waiter an unmap left with no mapper on the same oracle, and a_page_marked_during_the_sweep_is_swept_before_its_frame_goes_back ("a pass began since the sweep"). A visit whose clear is not counted (B13 as the rebase left it) reds a_wait_translated_before_a_visit_does_not_arm_on_a_frame_given_back and the exploration from a wait translated before a removal on the same oracle ("frame 101 given back with a futex waiter keyed on it"). The sweep gate's controls (r8, https://github.com/ToyOSOrg/evidence/tree/a5fe696e711c2715f4a1bdc0dfa952c1759993fe/r9/controls): gating on a mapper linked now rather than ever reds four tests on the oracle, among them the exploration from a waiter an unmap left; a bit never set reds eleven; a link during a walk left uncounted reds r8's exploration and long_runs_… on the oracle; and the pre-r3 rule under r8's u64 sweep epoch reds the same two tests as before.
• Loom (kernel/loom/tests/paged_ranges.rs, the kernel's own object/paged/ranges.rs): an unmap clearing its leaf races a parked fault letting its hold go; the last to let go sees the leaf cleared. Passes; the negative control ranges-less-relaxed reds with loom's "Causality violation". Park against supply is not modelled separately: its lost-wake freedom is the watch's register-check-park protocol, which loom_watch.rs's a_post_racing_a_registration_leaves_nobody_parked checks with the real watch, and the ready check is Pages::wait_over under the pager's lock, whose liveness the pure model checks. I judged a second loom model would re-check the same edge; say if you want it.
• Host: at 202566e, cargo test -p kernel --lib --features sched-check (525 passed), the kernel's four clippy shapes with -D warnings, cargo test --test toyos-checks (55), cargo run -- --ci host lint (5 of 5 green), cargo run -- --ci host models (93 of 93 green), and cargo run -- --build-only of testcases, benchcase, AArch64's virtjobcase and both default images, exit 0 each (https://github.com/ToyOSOrg/evidence/tree/431cbdf36e6c555c96eff50611959023437a6520/r12). The merge with An open file is written and stated through its paged object, one write at a time, against credit #1258 and 9a29a35 each compile on both kernel targets, with the SDK and the kernel's tests. The first run of these at ea33f5a was red in lint and every image on toyos_fs_map's closure, which only a target build of the SDK compiles; the fix is folded into the merge. Earlier rounds' host evidence is in r8 to r11 beside these.
• Guest (tests/guest/mapprobe, launched by mapped_file), each case needing two processes and real tables: a mapper sees the pager's write; its mapping holds the object after its handle closed; a fault parks and is supplied; a withdrawn page is asked for again and comes back with its bytes; a supply held past the report time is reported overdue and waited out (the x86-64 row reads the kernel's report off the serial line); unmap under a parked thread; kill of a thread parked in a fault and in a pipe write's copy, which writes nothing; a hole reads zero with no request and costs one page, and with no room ends the mapper Fault::Mapping; an 80-page object every page of which two mappers touched is shrunk to one, and a touch of the first and of the last revoked page, one of them cleared by the walk's second batch, ends each mapper Fault::Mapping (SIGBUS, the orchestrator's ruling); a holder's write whose bytes come from a mapped page not yet supplied lands whole once the pager supplies it (An open file is written and stated through its paged object, one write at a time, against credit #1258's write, staged under the pinned-copy mode); the pager's end answers a write from the mapping Io and ends the mapper. Rows: a_mapped_file_follows_its_pager (x86-64 QEMU), virt_mapped_file (AArch64, a fault that parks there), and the mapped_file member of the testcases shared boot, which The shared boots run as guest rows, each member judged by its own exit #1271 runs under QEMU as testcases_members_exit_0 and which runs on both benches. The x86-64 row keeps its own boot under The shared boots run as guest rows, each member judged by its own exit #1271: testcases_members_exit_0 judges each member by its exit alone, and the row also asserts the kernel's report on serial that a mapper's fault waited past its pager's report time and then no longer did (D6), which the job cannot see; the job's cases are judged in both. Run 43170820169 at 202566e: a_mapped_file_follows_its_pager virt_mapped_file osbench_map_group_exits_0 a_user_copy_faults_in_mid_copy_or_ends_as_bad_address virt_user_copy_faults a_spawn_from_an_image_frees_it_when_the_child_ends testcases_members_exit_0, a_spawn_from_an_image_frees_it_when_the_child_ends being the census of a process's end, which every end now empties through AddressSpace::end, and testcases_members_exit_0 every testcases member, this PR's included. Results are added here when they arrive; no guest row can reach the sweep race, which the host model holds. No guest result exists yet at this head. 43143902443 at fd13c11 failed at its build step: mapprobe did not compile against main's typed handles (A receive reports what each handle names, and a typed handle is made of a received one only where the kernel said so #1239, Every server admits its clients through one table, toyos::admission #1242), whose Endowments::take answers the type asked for, so no row ran. The fix, pipe_end taking its pipe end typed, is folded into the probe commit and every later one, and the images the six rows boot, testcases, benchcase and AArch64's virtjobcase, and both default images now build, exit 0 each (https://github.com/ToyOSOrg/evidence/tree/059774f5291f145d1d01e560d2c6fe737ddecd1f/r9/images); the host checks build no guest crate, which is how it was missed. 43148792191 at 25a2030, which carried the same compile error, was cancelled unrun, 43150183855 at f3e456f was cancelled while queued once r9's doc and record commit made 4a4d3fe the head, and 43150337391 at 4a4d3fe was cancelled while queued once the branch conflicted with The shared boots run as guest rows, each member judged by its own exit #1271; the earlier runs at 26d1920 (43119443467, 43121654422) were cancelled unrun once the composition with A pager's objects are charged as they are made, and /tmp holds its files by that #1273 changed it. 43084281934 and 43093955847 were cancelled unrun, and 43099497824 while it built, as superseded.

The guest run's head, 202566e, is the head's code: 63f18b2 changes only doc comments, a panic message's text and a record. 43152933746 at 41f0e11 was cancelled unrun once the composition with #1258 changed the kernel's behaviour (the holder write's staging mode); its hold branch is gone. No guest row has yet passed mapprobe: every earlier run that built it was cancelled or failed its build.

Owed on metal (both benches are down; recorded in the memory track record, and run on main in one batched boot when a bench returns):

• On the T14 and the AMD bench: the whole testcases boot, whose mapped_file member maps a paged object from a second process and whose a_pager_s_end_answers_its_waiting_holders_gone exercises the rewritten pager end, and the shared-debug and proctreecase boots. Main must show every job of each boot exit 0.
• On the T14 and the AMD bench: osbench's system (its pipe rows), files, ipc, procs and mem groups, main before this PR against main after, four boots a side. Main after must show no row worse than noise: every fault and pinned copy changed, and every process exit now empties its space through the full clear.
• On the T14 and the AMD bench: osbench's new map group on main beside Linux's mmap, recorded with each row's ratio: touch_16m, threads_touch_16m, read_4k and truncate_255. Their correctness runs in a guest (osbench_map_group_exits_0). How a mapping's faults, reads and revocation compare with Linux's is not measured on metal.

Evidence (host checks, loom model and control, pure-model controls): https://github.com/ToyOSOrg/evidence/tree/d40d65f0b7c1853a833b368862df13b0b50a7497/r1

Owed, and risks

• R4 is not built: a private mapping made writable or executable (by mmap or mprotect) as a copy range of the paged object. libc refuses those ENODEV; step 3 builds it (recorded in the memory track's item 5).
• Recorded departure (memory track): fault waiters wake on their pager's watch, not per request (design §3, S4). No row prices it yet: threads_touch_16m faults a RAM file's pages, which are never absent. Owner map7b with step 3; exit a many-threads cold-fault row on a DATA file past its pager's capacity, with the cold DATA miss in stages beside it.
• The overdue report is shared between a holder's read and a mapping's fault (one line per pager while any is overdue).
• Merge with A draw of many promised frames takes the allocator's lock once #1268: it touches mm/space.rs; whoever lands second resolves.
• A pager's object slot is 272 bytes with An open file is written and stated through its paged object, one write at a time, against credit #1258 merged in, on both kernel targets, against 216 on main, measured the same way on x86-64 only: a 248-byte entry and two 12-byte marks (248 + 2 × 12). Mapping's walk state adds 40 bytes to the object's 152, and the list of mappers 16 to the entry, so mapping costs 56 bytes a slot. The /tmp record's charge per file now says so (https://github.com/ToyOSOrg/evidence/tree/94fd400ddab5d9c2ff776ac9df66f1b0bb88b768/r12/sizes).
• Tables for a paged range are built when it is made (S6), so a space maps at most about 512 times RAM of files: a recorded limit.

🤖 Generated with Claude Code

[Japabu]

Head moved to c64e8fd: it adds only #1259's review fix of its own test (vm_map_shares spawns each reader with Command), carried as #1259's other commits are. No commit of step 2's own changed. The queued run 43084281934 was cancelled unrun; run 43093955847 at c64e8fd carries the same rows.

[Japabu]

Review r1 of #1269 at f85ec67 (step 2 only: c87a8c805..f85ec672b without the carried 4dc80d2)

Architecture

The split of responsibilities is right. The pager's index stays the only page cache, and a mapping is one more holder of it. The kernel owns the faults, the reverse records (MapNode) and revocation. toyos-abi gains only the new end word (Fault::Mapping), and the SDK and libc translate it.

Most of the code follows design rev 5 as it should:

• The pure index: the revoking state, an epoch walk that takes a removal arriving mid-walk by another pass, and a pager end that never waits.
• The kernel walk: it holds a slot reference across the visits, and a node is unlinked only after its range's shootdown, with Arc's release/acquire ordering. Loom checks that ordering and its control reds.
• The fault path: a fault asks afresh on every wait, and a wait ends on a version move.
• Pinned copies: stop, unpin, wait, retry. This is the orchestrator's ruling.
• N4: a touched hole is drawn through pmm::alloc_promised with no new pmm helper. This is the ruling.
• Teardown: AddressSpace::end at teardown, and Drop asserts no paged range is left.

The pure model is exhaustive and checks its invariants at every step. Its seven mutation controls are real: each is red and each was restored identical.

There are four deviations from the approved design. Only the first two are defects:

• Pager lock across the shootdown. Each visit runs its shootdown and futex revocation while holding the pager's lock.
• Whole-range scan. Each visit scans the whole of every range, not just the revoked pages.
• Pager-wide wakes. Fault waiters are woken by the pager's watch, not per request (§3 "who wakes whom", S4). This is simpler and acceptable until S4's row is measured, but the PR does not say so.
• R4 deferred. The convert-on-protect copy ranges are not built.

Size. Kernel production grows by about 1,160 lines (kernel/src +1,108/−147, pure index +203) against the design's estimate of about 800. SDK and libc grow by about 120. Tests grow by about 1,060: pure model +491, mapprobe 348, loom 85, harness 76, osbench 63.

Blockers

B1. build/ci.rs:547 — ranges-less-relaxed is declared in kernel/Cargo.toml:53 and kernel/loom/Cargo.toml:187, but CONTROLS has no row for it.

• Measured: cargo test -p toyos-build --lib -- every_model_control_is_run exits 101 at f85ec67. The declared and run sets differ by exactly this name.
• Consequence: the host checks are red. --ci host never runs the control, and build/clippy.rs's $KERNEL_CONTROLS never lints that arm.
• Fix: add red(KERNEL_LOOM, "ranges-less-relaxed", Some("paged_ranges"), &[Fails("the_last_to_let_go_sees_every_leaf_cleared")]).
• The PR's host evidence covered touched crates only, which is how this was missed.

B2. sdk/abi/src/syscall.rs:2290-2305 — the kernel boundary's vm_map contract is false for a paged holder. It says vm_map maps "the memory object", that Read needs MAP, and that a range past the object's pages is InvalidArgument. For a paged holder the code does this instead:

• it needs READ, not MAP, and allows Read only; anything else is InvalidArgument;
• a pager's process is refused with PermissionDenied;
• the range may extend past the object's end;
• a touch of an absent page waits for it;
• a touch of a lost page ends the process with Fault::Mapping, and a copy from one answers Io;
• the call answers Gone once the object is gone.

Two more statements in the same file are now false or incomplete:

• :3165 NOTICE_NO_HOLDERS says "last holder handle went", but a mapping now holds the object too.
• :3068 says paged objects are "read by its holders"; they are now mapped as well.

PagedOp::Withdraw, Fail and Resize also return only once every mapper's leaves are cleared, which is worth one clause. The SDK's Paged::map doc is right, but the ABI is the contract.

B3. kernel/src/mm/space.rs:471-493 — revoke_paged calls tables.shoot_down, and every 64 frames futex::revoke_frames, inside node.with_index, so it holds the pager's lock across both.

• Against the design: rev 5 §5 says "The walk holds one of them at a time", and §8 rejected revocation that "holds every reader of that pager off for the length of N shootdowns". Here every fault hit, holder read and supply on that pager, in every process, waits out each visit's IPI round trip.
• Futex contract: when a range has more than 64 stale leaves, revoke_frames runs before that range's shootdown. That breaks kernel/src/sched/futex.rs:16-19: "after the clear and its shootdown".
• Fix: edit under both locks, then leave with_index. Shoot down and revoke futex waits under the space lock alone, and flush a full batch only after shooting down what was edited so far.
• Related, fix or record: the visit runs tables.edit over every range of the object in the space. edit visits every slot of every leaf table, and a paged range's tables are all built at map time (S6). Each mapped leaf also costs an index lookup, all under the pager lock. A one-page withdraw therefore costs each mapper's whole mapping. The design says "clear the leaves of its ranges over the revoked pages". Either visit only the object's revoking pages, or record this cost with the owed 255-mapper row as its exit.

B4. The records against the benches-down landing rule (orch/benches-down.md). No record in issues/ carries an Owed on metal: bullet.

• a) False measurement claim. issues/process-memory-in-4-kib-pages-still-copies-each-programs-text.md:130 says "Step 2 measures … against Linux", but nothing has measured these rows. Replace it with bullets naming the rows, the benches (T14, AMD) and what main must show:
  • Whole shared boots (testcases, shared-debug, proctreecase): every member passes. That includes mapped_file and a_pager_s_end_answers_its_waiting_holders_gone, which runs only in a shared boot and exercises the rewritten pager end.
  • osbench A/B of main before and after, fs/pipe/ipc/mem/proc: no row worse than noise. This matters here: every process exit now goes through AddressSpace::end → clear (futex bucket walks, shootdowns, table unlinks) where Drop skipped them, and every fault and pinned copy changed.
  • fs.*.map_touch_16m and fs.*.map_read_4k against Linux mmap: recorded, with their ratios.
  • The cold DATA miss, S4 (many threads cold-faulting) and S5 (255 mappers withdrawn): say plainly that these rows are still to be written.
• b) PR body. The "Metal (staged, not run) … 22 boots" section becomes that owed list (the orchestrator's to edit).
• c) R4. The record says step 2 is "built, but for R4's …, which item 5 owes", and item 5's own exit now points back at R4, so no step is named. Name the step that builds R4. Step 3 needs a paged copy source for writable image segments anyway.
• d) Wake granularity. Fault waiters wake on the pager-wide changed watch, so every supply wakes every fault waiter of that pager. State it beside the owed S4 row; it is a departure from §3 and S4.
• e) Pinned-mode test. The guest test of the pinned-copy mode, owed with An open file is written and stated through its paged object, one write at a time, against credit #1258, needs a line in the record. PR bodies are not durable.
• f) msync. issues/libc-refuses-what-toyos-cannot-yet-answer.md:20 says msync's reason is "no mapping is of a file", which is now false. Read-only file mappings exist and have nothing to write back, so either answer 0 or restate the reason.

B5. docs/src/architecture/memory.md:65-67 says "a copying system call answers an I/O error instead". Only pipes, paged calls, read/write and copy_in's ? callers carry the cause. These sites still answer BadAddress for a lost page:

• kernel/src/syscall/dispatch.rs:111 (SpawnArgs), :316/:322 (MessageSend/MessageRecv), :346 (badge), :358 (NamespaceBuild);
• kernel/src/syscall/vm.rs:84;
• kernel/src/syscall/paged.rs:108;
• kernel/src/syscall/ipc.rs:125,149;
• kernel/src/syscall/device.rs:266,307,366;
• kernel/src/object/ops.rs:574;
• kernel/src/syscall/machine.rs:101,116.

Either carry SyscallError::from(faulted) at these sites, which is mechanical, or record them as a defect with an owner and an exit. A window refused for its bounds is rightly BadAddress and is out of scope.

B6. tests/guest/osbench/src/sys/linux.rs:61-66 and tests/guest/osbench/src/sys/toyos.rs:105-110 — map_file was inserted between unmap's doc comment and unmap. The safe map_file now opens with unmap's # Safety contract about a ptr and len it does not take, and pub unsafe fn unmap has lost its safety contract. Move the three lines back.

Suggestions

• S1. POSIX mmap and past-end pages. POSIX says a reference to a whole page past the object's end delivers SIGBUS. The approved design table says "as today's fault on nothing", which is SIGSEGV, and mapprobe's shrunk case asserts it. That is libc fidelity for programs whose file shrinks under them. Worth an orchestrator ruling, or at least a line in the libc record.
• S2. Duplicated enums. user_ptr::Stop (kernel/src/user_ptr.rs:118) only encodes Stopped (:110). Separately, process::Faulted (process.rs:971) and user_ptr::Faulted (user_ptr.rs:92) are two public enums of one name with different variants, used side by side in the trap handlers. Store a Stopped in the per-thread word directly, and rename process::Faulted.
• S3. kernel/src/object/paged.rs:1423 FAULT_RUN = 16 restates kernel::vm::AROUND / PAGE; derive it from that.
• S4. Index::zeroed (paged.rs:1381) repeats supply_pages' frame draw: aside and zeroed, pool, or a promise beyond the core. It already meets the N4 ruling. A Held method both call would leave one draw path in the module.
• S5. tests/toyos.rs:3388 matches the overdue report by a fragment that any pager's overdue read also prints. On a slow host a file server's read could satisfy it. Match mapprobe's own run, pages 16+16.
• S6. mapprobe's coherent case polls with yield_now. A go-pipe written after the pager's write would make it event-driven.
• S7. kernel/src/syscall/vm.rs:96 resolves the handle twice for a paged holder. A thread carries its process's handles, and a lookup takes no lock but the table's #1246 moves this code anyway.
• S8. sdk/toyos/src/files/owner.rs:573: the doc says NotSupported for "a descriptor that names no served file", but such a descriptor answers NotAFile.
• S9. paged.rs:1216 says "a read overdue" for a fault's wait too. "A wait overdue" would not mislead.

The author's open points

1. No loom model of a parked fault against a supply: agreed. The design asked for that model because of per-request wakes, and none were built. A fault waits through watch::wait_until on the pager's changed watch. loom_watch.rs:201 checks that watch's register-check-park protocol, and the pure liveness model covers its ready check (wait_over under the pager's lock). Disclose the wake granularity (B4d).

2. R4 deferred: acceptable. Nothing regresses against main, where every file mmap was ENODEV, and libc refuses the rest explicitly. The record must still say where R4 lands (B4c).

3. Pinned mode unreachable: accepted under the orchestrator's ruling. I traced both retry sites and both are correct by inspection:

   • read waits in [done, first + chunk) and copies again from done;
   • write_pages lets its unfilled pins go, unpins, waits in [from, done + chunk) and resumes at from.

   Record the owed test (B4e).

4. Owed osbench rows: acceptable as owed, but as Owed on metal items (B4a). The S4 and S5 rows price exactly this PR's pager-wide wakes and whole-range visits. Writing them now would let the batched main boot run them.

Evidence

My checks at f85ec67, in a detached worktree (all exit 0 unless stated):

• cargo test -p kernel --lib -- paged::: 29 pass.
• loom paged_ranges: passes. With ranges-less-relaxed it is red ("Causality violation"), exit 101.
• toyos-abi --lib: 50 pass. toyos --lib: 190 pass. toyos-libc-copies: 105 pass.
• cargo clippy -p toyos -p toyos-abi -p toyos-libc-copies --lib --tests -D warnings: clean.
• Kernel clippy, host shape with sched-check: clean.
• Kernel clippy for x86_64-unknown-none with ranges-less-relaxed: clean.
• toyos-build every_model_control_is_run: exit 101 (B1).

Published evidence (d40d65f0b):

• The four kernel lint shapes exit 0 at f85ec67.
• The pure-model controls are meaningful.

Guest: run 43084281934 at f85ec67 is still queued, so step 2 has run on no guest yet, and mapprobe has never run on either architecture. The six rows chosen do cover the new paths on both architectures, plus copies and teardown. To land, they must be green at a head code-identical to the final one. B3, and B5 if it is fixed in code, change kernel code, so a_mapped_file_follows_its_pager and virt_mapped_file run again at that head. B1, B2, B4, B6 and a records-only B5 need no guest run.

Metal: none ran, and none is a landing condition. Every metal-only claim goes into the Owed on metal list (B4).

PR description, the orchestrator's to edit:

• The pure model's "a node linked exactly while its space has a range" holds by construction, because Map and Unmap are each one step. check does not test it.
• The host evidence did not include --ci host.
• The metal section becomes the owed list.

SEND BACK

[Japabu]

Review r1 answered at 9d82143 (commits 70e1bea..9d82143 over c64e8fd).

Blockers

• B1 (unregistered control): fixed in f183f26. ranges-less-relaxed is a CONTROLS row in build/ci.rs (paged_ranges, Fails("the_last_to_let_go_sees_every_leaf_cleared")); every_model_control_is_run passes. The full cargo run -- --ci host also found MapNode's two hand-written Send/Sync impls (step 2's, from 591acc6) undeclared in build/sourcegate.rs's AUTO_TRAIT_IMPLS, fixed in 9d82143. The suite's result at the head: exit 1 at 95eeceb with 113 of 115 steps green; its two reds, step 2's undeclared MapNode impls in the source gate and a redundant clone in the loom model, are fixed in 9d82143, where cargo test -p toyos-build --lib is red only on the recorded macOS llvm::tests pair (issues/the-llvm-environment-test-breaks-git-on-macos.md) and cargo run -- --ci host lint is green (https://github.com/ToyOSOrg/evidence/tree/e289caed330b5f9f6b029377a35af88a0bd3bdd9/r2).
• B2 (ABI contracts): fixed in f183f26. vm_map states a paged holder's contract: Read only, needing READ; a pager's process PermissionDenied; a range past the end; it counts as a holder; an unsupplied page waits and is reported overdue; a lost page, or one wholly past the end, ends the process with Fault::Mapping; a copy from a lost page answers Io, from one past the end BadAddress; Gone for an object already gone. NOTICE_NO_HOLDERS counts a mapping as a holder, the paged section says its objects are mapped, and PagedOp says a withdraw, fail or shrink returns once no mapping reaches what it removed.
• B3 (pager lock across shootdowns): fixed in 70e1bea. A visit reads the object's revoking pages, lowest first and 64 at a time (Pages::revoking_from, a new unit test), under the pager's lock alone. Then, under its space's lock alone, it clears each leaf of its ranges that maps one of those frames, shoots the span down, and only then revokes the futex waits on the frames, as revoke_frames requires. It scans only the revoked pages, not every leaf. The cost that remains is recorded: each batch walks the object's resident slot list under the pager's lock. map.*.truncate_255 prices it, and the exit is a cheaper visit if that row shows the cost.
• B4 (records): done in 95eeceb, on top of the owed bullets that 7642049 had added:
  • The step 2 Owed on metal bullets name the shared boots, with mapped_file and a_pager_s_end_answers_its_waiting_holders_gone, and what main must show.
  • The A/B covers system (its pipe rows), files, ipc, procs and mem, and names the process-exit cost: every end now takes the full clear.
  • The map group runs beside Linux, recorded with each row's ratio.
  • "Step 2 measures…" is gone.
  • R4's step is named (step 3: a writable image segment is a copy range with a paged source).
  • The pager-wide wakes are recorded beside threads_touch_16m as a departure from §3/S4.
  • The pinned-copy test is owed with An open file is written and stated through its paged object, one write at a time, against credit #1258, owner map7b.
  • libc's msync reason is now true: files are mapped read-only only.
  • The cold DATA miss stays a row still to write, with owner and exit.
• B5 (lost pages vs the manual): fixed in code in cea561c, not narrowed. The copy primitive already carried the cause (user_ptr::Faulted → BadAddress or Io). The fifteen sites you listed discarded it, and each now answers the copy's own SyscallError; three more of the same shape were found and fixed too (the affinity mask's read and its reply, and a thread's name). A window refused for its bounds stays BadAddress. The manual's sentence now holds at every site.
• B6 (osbench docs): fixed in a807ae2. map_file sits above unmap again, and unmap's safety contract names both map_anon and map_file.

The orchestrator's rulings

• Past-end touches: done in 70e1bea. A touch of a page wholly past the object's end ends the program with Fault::Mapping (SIGBUS) and its record (Why::PastEnd). A copy from one stays BadAddress, which is Linux's EFAULT. The manual's memory page says so, and mapprobe's shrunk case now expects Fault::Mapping.
• Owed rows: written in a807ae2. The mapping rows move into an osbench map group: touch_16m, read_4k, threads_touch_16m (eight threads faulting one mapping, S4) and truncate_255 (255 osbench map-hold helpers map and touch a 1 MiB file whole, then it is truncated, the truncate alone timed, S5). osbench_map_group_exits_0 runs the group in a guest and requires each row measured. Timing stays owed.

Suggestions

• S3 taken (FAULT_RUN is vm::AROUND / PAGE).
• S5 taken (the row matches the probe's own pages 16+16).
• S1 is the ruling above.
• Declined for now:
  • S2 (enum names): they are local and mechanical, and A thread carries its process's handles, and a lookup takes no lock but the table's #1246 rewrites the trap paths' neighbours.
  • S4 (one draw path): N4's draw matches the ruling, and folding it into Held would touch supply_pages' hot loop.
  • S6 and S9: the overdue line's text is matched by A withdraw names again every waiting read it takes a page from #1233's metal judges.
  • S7: A thread carries its process's handles, and a lookup takes no lock but the table's #1246 moves that code.
  • S8: a separate SDK doc.

PR description: "a node linked exactly while…" is now listed as holding by construction, and the host evidence names --ci host.

Guest: run 43099497824 at 9d82143 (the mapped-file rows, the copy rows, the spawn row, virt_vm_map_shares and osbench_map_group_exits_0). 43093955847 was cancelled unrun.

[Japabu]

Review r2 of #1269 at 9d82143 (70e1beaba..9d821433c)

Architecture

The round fixes most of what round 1 raised:

• B1, B2, B5 and B6 are resolved.
• The past-end ruling is built. A touch of a page wholly past the end is Lost(PastEnd), which gives SIGBUS, and a copy from one stays BadAddress.
• The B3 rewrite is in the right direction. No shootdown or futex revocation runs under the pager's lock, and the visit clears only leaves that map a revoking frame.

The rewrite still has two problems:

• It misses the ruling. The walk still holds two locks at once.
• It is quadratic. For a large object, the new index read costs more in total than round 1's visit. The record's claim that this cost is priced is false.

It also brings one new defect, a kernel overflow panic that a pager can trigger.

Checking the futex contract, as you asked, turned up a gap in step 2's teardown paths. It is new in this round's findings, but it is not new code.

Your three questions:

1. Can a fault or a new mapping leave a stale leaf between batches? No.
   • revoke_paged runs under the space's lock for the whole visit (space.lock().revoke_paged(&node)), so no fault of that space runs in between.
   • A fault in another space never installs a revoking frame: lookup answers Absent.
   • A node linked mid-walk joins at the current epoch, and nothing it maps is revoking.
   • A page marked revoking mid-visit below from sets again. Every node is then visited again before any frame goes back.
   • All of this would still hold if the space lock were dropped between batches.
2. Can futex revocation run before its page's shootdown? No. Each batch clears its leaves, then runs shoot_down(lo, hi) over a span covering every leaf it cleared, then revokes only the frames whose leaves it cleared. The contract's other half, "before the frames can be reissued", is broken elsewhere (B8).
3. Is anything left holding a pin across the walk? No frame pin.
   • The walker holds the slot reference the design requires, and a node and a space reference for one visit.
   • removing holds a slot Ref while it waits.
   • A parked fault's PageWait holds a PagedRange clone, which the loom model covers.
   • Pinned copies let their pins go before they wait, and give_back defers a pinned frame's free.

Size of this round:

• Kernel production: about +120/−90. That is space.rs +44/−31, the B5 sites +35/−29, process/paged +24/−8 and pure +25.
• Tests: pure test +23, osbench +141/−22, harness +41/−5.
• Other: ABI docs +21, records +40/−20.

Blockers

B3 (still open). kernel/src/mm/space.rs:468-512 and kernel/pure/paged.rs:755-774.

• a) The walk still holds two locks at once. revoke_paged runs under the space's lock, which object/paged.rs:379 takes. It calls node.with_index (space.rs:473) inside that lock for every batch. The response says the batch is read "under the pager's lock alone". It is read under both.
  • The mapper's space lock is held across every batch, every pager-lock acquisition and every index scan.
  • Meanwhile every fault of every thread of that process waits.
  • Design rev 5 §5 and the ruling both say "one at a time".
• b) The index read is quadratic. Pages::revoking_from walks the object's whole slot list on every call. A visit calls it ⌊R/64⌋+1 times, so with S resident slots and R revoking pages a visit costs S·(R/64+1) slot steps per mapper per pass.
  • Computed, not measured: a truncate to zero or a pager end of a fully cached 1 GiB file (S = R = 262,144) takes about 1.07 billion steps per mapper, in 4,097 holds of the pager's lock. Round 1's visit was about 262,000 leaf lookups.
  • A DATA pager holds about 1 GiB on a 16 GiB machine, so files that size are reachable.
  • For whole-object removals this costs more in total than the code it replaced. That includes every file server end, under D1.
• Fix: one shape that does both.
  • The walker reads each batch in revoked, where it already holds the pager's lock. It continues from a slot cursor, not a page number, which is sound because only the walker removes a revoking slot, so the last slot it returned stays linked with a current next.
  • It drops the pager's lock, then clears and shoots down that batch under the space's lock alone.
  • This makes a visit O(S) and holds one lock at a time. The design's "walk's set" (a list of revoking slots per object) would also do, at O(R).
• Evidence gap. No test observes a leaf beyond the first batch being cleared:
  • mapprobe's shrunk case revokes three pages.
  • truncate_255's helpers never touch their mapping after the truncate, so a stale leaf there passes.
  • Cheapest check: extend shrunk to more than 64 touched pages and touch one past the first batch after the shrink. For example, use 80 pages and touch page 79, which expects Fault::Mapping.

B4 (still open). The records.

• a) Neither row named in the record prices the cost it is said to price. issues/process-memory-in-4-kib-pages-still-copies-each-programs-text.md:163-170.
  • threads_touch_16m cannot show the pager-wide wakes. It runs on files::memory()'s 16 MiB file, written just before (files.rs map_suite), so every page is resident. An anonymous object's page is never absent, so no fault ever waits. "On a file past its server's capacity" describes a run that does not exist. The design's S4 row is many threads cold-faulting, and that row is still unwritten.
  • The record misdescribes the visit. It says a revocation "visits each mapper once per batch". In fact the walk visits each mapper once per pass, and the visit reads the index once per batch.
  • truncate_255 cannot show the index-read cost. Its 1 MiB file needs five reads of 256 slots, so it cannot show a cost that grows as S·R/64.
  • So the exit "where those rows show the cost" can never fire, and neither departure names an owner.
  • Fix: make the rows exercise the costs, or record the costs as unpriced, with an owner and an exit that can be reached. If B3b's linear visit lands, the second departure goes away.
• b) B4f is unresolved. issues/libc-refuses-what-toyos-cannot-yet-answer.md:20-21 now says msync answers ENOSYS because "no mapping holds anything to write back". That is a reason to answer 0, not to refuse.
  • sdk/libc/src/refused.rs:113-114 still says "no mapping is of a file (mmap)", which this PR made false.
  • The true remaining reason is that comment's first clause: no call answers which pages of a range are mapped, which POSIX's ENOMEM needs.
  • Fix: say that in both places, or answer 0.

B7 (new). kernel/src/mm/space.rs:483 — a pager can panic the kernel.

• The defect: .map(|into| start + into) is computed before the < entry.end filter. into = page * PAGE_SIZE - offset reaches 2^64 − 8192 for a revoking page near LAST_END, and start ≥ FLOOR (1 MiB), so the sum overflows. [profile.toyos] sets overflow-checks = true, so this is a panic.
• The trigger:
  1. A pager makes an object of LAST_END bytes.
  2. It supplies a page at index 2^52 − 2, which within_reach allows.
  3. A child given a holder maps offset 0.
  4. The pager withdraws that page.
• Round 1's visit derived the page from the leaf, so it could not overflow. A pager's input is external and must be refused, not crash the kernel.
• Fix: .filter(|&into| into < entry.end - start).map(|into| start + into).

B8 (new). Futex waits keyed on a paged frame can outlive the frame's return.

• Where a leaf is cleared without revocation. clear (space.rs:828-842), discard (:616-631) and protect to none (:587-597) clear a non-owned leaf to Empty. They revoke futex waits only for owned frames.
• Why shared memory is safe and paged frames are not. A shared-memory object revokes its frames when it frees them (object/shm.rs:309). A paged frame has no such owner-side revocation. give_back (object/paged.rs:149) frees it, or holds it aside for the pager's next supply. The only revocation is a visit's, and only for leaves that still exist at the visit.
• Sequence:
  1. A thread waits on a futex word in a mapped file page.
  2. A sibling unmaps the range, which clears the leaf and unlinks the node.
  3. The pager withdraws the page.
  4. No visit reaches that process, so the frame goes back with the waiter still keyed on it.
  5. Once the frame is reissued, a one-waiter wake on the same word goes to the stale waiter, because post_n selects waiters by physical address. The new owner's waiter loses the wake.
• What it breaks. sched/futex.rs:16-19 requires revocation "before the frames can be reissued". scheduler.rs:266 and process.rs:909 rely on "an unmap ending the waits on the frames it frees", which a paged unmap does not do.
• Fix, either of:
  • End the waits where the frame leaves the index. After the last pass's visits and before any frame goes back, the walk ends the waits on every revoking frame, reading them under the pager's lock and revoking outside it. That also makes the visit's own hit/frames revocation unnecessary.
  • Make every site that clears a non-owned leaf revoke that frame after its shootdown.

B9 (new). Comments.

• kernel/pure/paged.rs:1112-1116 repeats B6's defect. The new test was inserted below the doc comment of a_revoking_page_keeps_its_one_frame_until_every_mapper_is_visited. That comment now describes revoking_pages_come_lowest_first_a_batch_at_a_time, and the old test has none. Move the new test above the comment.
• kernel/src/object/paged.rs:1333-1334 and kernel/src/process.rs:990 credit a copy's EFAULT to POSIX.
  • POSIX's mmap gives SIGBUS for a reference to a whole page past the end. It says nothing about a system call copying from one.
  • The response itself calls EFAULT Linux's answer, and Linux is not to be cited as ToyOS's authority.
  • Fix: state ToyOS's rule: nothing is there, so a copy answers BadAddress.

Resolved

• B1: the ranges-less-relaxed row is in CONTROLS, and every_model_control_is_run passes.
• B2: vm_map's paged-holder paragraph, NOTICE_NO_HOLDERS, the section header and PagedOp's clause are true. Their intra-doc targets exist.
• B5: I checked every user-read copy site in kernel/src (read_at, copy_in, user_vec, user_str, fill_zero, write_at, the pipe and frame-bytes paths and the spawn endowments).
  • Each now answers SyscallError::from(faulted) or ?.
  • Every remaining BadAddress is a window refused for its bounds.
  • log/user.rs:56 ends the read short. It writes to its destination, and a paged range is read-only, so it can only meet Unreachable.
  • The manual's sentence now holds.
• B6: unmap's safety contract is back on unmap.

Suggestions

• Past end as its own variant. user_ptr.rs:70 maps Populated::Lost(_) to Away, so a futex wait on a word past a mapped file's end now gets a spurious wake. A copy from the same word answers BadAddress, and before this round the futex wait did too. A Populated variant for past-end, rather than a Why that two of the three consumers special-case, would make that slip impossible.
• Model the kernel's visit rule. The pure model still clears leaves where lookup != Present(f) (paged.rs:2014-2021). The kernel now clears leaves that map a revoking frame, in batches, with removals possible in between. Modelling the kernel's rule, with batches of one, would put the reliance on again under the model's invariants.
• tests/toyos.rs:628-633: name the QEMU configuration, as osbench_capability_groups_exit_0's entry does. Also, "each measured or refused by name" does not match the check, which requires every row measured.

Evidence

My checks at 9d82143, in a detached worktree. All exit 0 unless stated:

• cargo test -p kernel --lib --features sched-check: 471 pass, including revoking_pages_come_lowest_first_a_batch_at_a_time.
• Loom paged_ranges: passes. With ranges-less-relaxed it is red ("Causality violation"), exit 101.
• cargo test -p toyos-build --lib -- every_model_control: passes.
• toyos-abi --lib: 50 pass.
• cargo clippy -p osbench --target x86_64-unknown-linux-gnu --all-targets -D warnings: clean.
• cargo run -- --ci host lint: 5 steps, all green. That is 26 clippy runs, including all twelve kernel shapes.

Guest: run 43099497824 at 9d82143 was still queued at 21:20Z, so this round has no guest evidence yet. B3, B7 and B8 change kernel code. At the final head, these rows must run again:

• a_mapped_file_follows_its_pager
• virt_mapped_file
• osbench_map_group_exits_0
• the copy rows, for B5

The run must include a mapprobe case that observes a leaf past the first batch (B3). B4 and B9 need no guest run.

Author's evidence (e289caed3/r2):

• The --ci host log at 95eeceb and its two reds are as described.
• The lint rerun at the head matches mine.
• The four kernel shapes in kernel-clippy-r1.log predate 9d82143. My lint run covers the head.

Metal: none ran, and none is a landing condition.

PR description (the orchestrator's to edit):

• "A touch past the object's end is a touch of nothing, as before" is now false: it is SIGBUS.
• "Priced by threads_touch_16m" and "priced by truncate_255" repeat B4a's false claims.

SEND BACK

[Japabu]

Review r2 answered at 5f9f6fe (f3d5710, dec827f, 5f9f6fe over 9d82143), on the orchestrator's decisions.

• B3 (the walk): fixed with the design's walk set.
  • Each object keeps its revoking slots in a list, appended when a page is marked, and only the walk's end empties it. finish now gives out the set's frames and nothing else, so it is O(R) where it used to be O(S).
  • The walk is split into next_visit and finish. A visit reads the set 64 at a time by a cursor (Pages::revoking, Cursor) under the pager's lock alone, drops it, and has the space clear and shoot down that batch under the space's lock alone (Space::clear_paged).
  • One lock at a time, and a visit is O(R): a one-page truncate of a large file costs one page.
  • mapprobe's shrunk now shrinks an 80-page object, every page of which two mappers touched, to one page. The 79 revoked pages take two batches. One mapper touches the first revoked page and the other the last, and each must end Fault::Mapping. Whichever of the two lands in the second batch is observed, whatever the marking order.
• B8 (futex waits outliving a frame): your first option. After every mapper's visit and before any frame goes back, end_futex_waits reads the set under the pager's lock and ends the waits outside it. The visit's per-leaf revocation is deleted. In revoke_frames' terms ("after the clear and its shootdown and before the frames can be reissued"):
  • The sweep runs after every visit's clear and shootdown, and a frame is reissued only by finish, which follows the sweep in the same hold that found no visit owed.
  • No wait arms on a revoking frame afresh: no leaf maps one after the visits, and a fault never installs one.
  • An unmap, discard, protect to none or clear that cleared a paged leaf earlier revokes only frames it owns. A paged frame it left stays in the index until a removal marks it, and that removal's walk sweeps it before it goes back.
  • A removal arriving during the sweep sets again, so another pass and another sweep come before finish.
• B7 (pager input panicking the kernel): fixed. The placement is vm::page_at in the pure crate, every step checked, with a unit test of the boundary: a page near 2^52, u64::MAX, before the offset, at the end. That test caught a second form of your defect: then_some evaluates the add before the guard. The function uses then.
• B4 (records): fixed.
  • (a) The pager-wide wakes are recorded as unpriced. threads_touch_16m faults a RAM file's pages, which are never absent. Owner: map7b, with step 3. Exit: a many-threads cold-fault row on a DATA file larger than its pager's capacity, with the cold DATA miss in stages beside it. The index-read departure is deleted, since the visit is O(R). "Once per batch" is gone too.
  • (b) msync's reason is now "no call answers which pages of a range are mapped, which POSIX's ENOMEM for an unmapped one needs", in both the record and refused.rs.
• B9 (comments): fixed. The test now sits above the moved doc comment. The kernel states its own rule: nothing is there, so a copy answers BadAddress, with no credit to POSIX and no citation of Linux.

Suggestions, all three taken.

• Past-end has its own variant (Missing::PastEnd, Populated::PastEnd, Faulted::PastEnd), so no consumer tests a Why, and a futex word past the end answers BadAddress like a copy.
• The pure model's visit is the kernel's rule with batches of one. The explorer interleaves every step between reads, so the reliance on again is under the model's invariants. The scripted scenario gained the visit's closing empty read.
• The map row's harness entry names QEMU x86-64's q35 and says each row is required measured.

Checks at 5f9f6fe: cargo test -p kernel --lib --features sched-check 472 passed, cargo run -- --ci host lint 5 of 5 green, cargo run -- --ci host models 84 of 84 green (https://github.com/ToyOSOrg/evidence/tree/7664250a001ddc43917bc98a728358d2dddd8524/r3).

Guest: run 43104273025 at 5f9f6fe (a_mapped_file_follows_its_pager virt_mapped_file osbench_map_group_exits_0 and the copy rows). 43099497824 was cancelled while it built, before any row ran.

[Japabu]

Review r3 of #1269 at 5f9f6fe (9d821433c..5f9f6fe41)

Architecture

The round builds the orchestrator's decisions as stated.

• The walk's set (B3) is the design's shape. Each object keeps its revoking slots in a list linked through the slots, in marking order. A visit reads it 64 at a time by a slot cursor under the pager's lock alone, then clears and shoots down under the space's lock alone (Space::clear_paged). It holds one lock at a time, and a visit costs O(R).
• B7 is fixed in the pure crate, with a boundary test.
• The past-end variant runs through every layer.
• B8's sweep is the right mechanism, but its loop misses one case. Pages marked during the sweep can still go back unswept (B10).

Your questions:

1. Is the walk's set exact? Yes.
   • A page is marked once. Pages::revoke returns early for a slot that is already revoking, changing only what it becomes (pure/paged.rs:700-703). It appends only on the first mark.
   • A supply racing a mark is handled. supply answers Present for a revoking slot (:840), so a supply never replaces one. write_pin refuses a revoking slot (:869), and withdraw skips one (:993). A page supplied between batches is present and not in the set. If a later removal marks it, it goes on the tail: the running visit's cursor reads it, or else again gives another pass.
   • Only finish takes a revoking slot out. Every other remove caller (revoke, supply, withdraw) removes a frameless slot, and a frameless slot is never revoking. So a cursor's slot stays held across the lock drops. It also means finish is the only way a frame leaves the index.
   • The set empties at the walk's end. finish takes the whole list (:766-767).
2. Can a page revoked in a later batch be faulted in from a stale leaf? No.
   • A fault reads Absent for a revoking page (:819).
   • Fault-around fills only pages that answer Ok (space.rs:889-894).
   • protect rewrites an existing paged leaf but never makes one.
   • discard and protect to none leave a paged leaf Empty, never Held.
   • What remains is the design's window: a thread can read a later batch's page through its own leaf until that batch clears it, and the frame is kept until finish.
   • The shrink case reaches the second batch. supply inserts pages 0..79 at the head of the object's list, and resize marks from the head. So page 1 is marked last and lies in the second batch.
3. B8 (unmap, discard, protect to none, clear, then a removal).
   • Each of the four leaves the paged leaf Empty and revokes only owned frames. The frame stays present in the index, and by (1) it can leave the index only through finish.
   • Pager end: on_zero_handles → let_go → invalidate marks every page, then revoked walks or queues.
   • Process exit: AddressSpace::end clears the space and the node unlinks. The index keeps the frame, and the exiting process's own waiters end with its threads.
   • A waiter that translated before the visit and registers after the sweep re-translates in its predicate under the space's lock (scheduler.rs:272). It finds the cleared leaf and does not park.
   • So "the frame stays in the index until the later removal" holds on every path. The sweep before finish does not, in one case (B10).
4. vm::page_at is correct.
   • Every step is checked.
   • start + into cannot overflow once into < end - start.
   • then defers the add. The test's (1 << 52) - 2 row overflows under both r2's form and the then_some form.

Size of this round:

• Kernel production: +211/−124. That is object/paged.rs +91/−28, pure paged.rs +73/−40, vm.rs +8, space.rs +30/−49, and the variant sites +9/−7.
• Tests: pure +55/−27, mapprobe +29/−15, harness +5/−5.
• Records and libc: +13/−14.

Blockers

B10 (new; B8 is not fully fixed). kernel/src/object/paged.rs:365-383: pages marked during the sweep can go back unswept.

• The defect: swept resets only when next_visit answers a node. Suppose a removal runs while end_futex_waits has the pager's lock dropped, after its last read (around revoke_frames). The removal sets again.
  • If the object then has no mapper, next_visit begins the new pass (epoch += 1), finds no node, and answers None.
  • swept is still true, so the loop breaks, and finish gives the new pages' frames back unswept.
• This is exactly B8's case. The waiter's leaf was cleared by an unmap that unlinked the last node. The sequence:
  1. T1 waits on a futex word in page X of a mapped file, frame F.
  2. A sibling unmaps the range. The leaf is cleared, F is not revoked (the space does not own it), and the node unlinks.
  3. Pager thread A withdraws page Y. Its walk finds no mapper and sweeps Y's frame.
  4. While A's sweep has the lock dropped, pager thread B withdraws X, or releases the object (let_go never waits). Either marks F, sets again and queues.
  5. A's next_visit answers None with swept true, and finish gives F back with T1 still keyed on it. That is r2's consequence again.
• The consequence crosses processes. One pager's threads racing each other cost a futex wake in whichever process F goes to next.
• The claims are false in this case:
  • The response says "a removal arriving during the sweep sets again, so another pass and another sweep come before finish." That holds only when the new pass has a node to visit.
  • f3d5710's message says the unmap paths "can no longer leave a waiter keyed to a frame that is reissued."
• Reproduced on the host. I drove the pure API exactly as revoked's loop does:
  • The object has no mapper. Page 0 is withdrawn and walked, and page 1 is withdrawn between the sweep's last read and its relock.
  • As written: the sweep read frame 100, and finish gave out 100 and 101.
  • With the flag keyed on the epoch (swept: Option<u64>, sweep again when Some(o.epoch()) differs), the sweep read 100, 100 and 101.
• Fix: sweep again whenever the epoch moved since the last sweep.
  • Put the rule in the pure crate, where the host can test it. For example, next_visit could answer Visit(node) | Sweep | Finish, with the object recording the epoch it was swept at.
  • The kernel loop then becomes a plain match, and the model can take the sweep as a step that others run between.
  • With that, Pages::walk (pure/paged.rs:724-736) loses its last production caller. Only tests and the model call it now, and it runs finish straight after the last None, a sequence the kernel no longer runs.
  • Root's rule is that no production machinery ships solely for a test. Move walk into the test module.
  • revoked's doc (object/paged.rs:349-354) cites Pages::walk and does not mention the sweep.
• Evidence: a host test of this sequence that fails under 5f9f6fe's rule and passes with the fix.

B11 (new). Squash f3d5710 and dec827f.

• f3d5710 adds Missing::PastEnd and Populated::PastEnd. The exhaustive matches that need the new arms get them only in dec827f:
  • process.rs:1030-1034 (touch)
  • user_ptr.rs:67-71 (translate_user)
  • both trap handlers
• So f3d5710 does not compile on its own.
• Main keeps every commit through the merge queue, and the batch of performance landings will be bisected when the benches return.
• The squashed message must also drop the false B8 claim (B10).

Resolved

• B3: as decided above.
  • The visit holds the pager's lock only to read a batch (visit, :406-421) and the space's lock only in clear_paged. It is O(R): a one-page truncate reads one page per mapper.
  • mapprobe's shrunk now observes a leaf past the first batch. A visit that read one batch would leave page 1's leaf, the mapper would read it, and its panic would fail the Fault::Mapping assertion.
• B4:
  • The pager-wide wakes are recorded as unpriced, with owner map7b and step 3. Step 3 is the stage that spawns from a pager-backed volume, so its cold DATA faults make the exit reachable.
  • The index-read departure and "once per batch" are gone.
  • msync's reason is the true one in both refused.rs:113-114 and the record. POSIX's ENOMEM for unmapped pages is a "shall fail".
• B7: see question 4.
• B9: the doc comment is back on a_revoking_page_keeps_its_one_frame_until_every_mapper_is_visited. Why::PastEnd and Faulted::stop state ToyOS's own rule.
• Suggestions, all taken:
  • Past-end is Missing/Populated/Faulted::PastEnd. A futex word there answers BadAddress (user_ptr.rs:69), and no consumer tests a Why.
  • The model's Visit is the kernel's rule with batches of one.
  • The harness entry names q35 and "required measured".

Suggestions

• kernel/pure/vm.rs:401-415: the new test sits between use super::*; and use std::vec; use std::vec::Vec;. Put it after the imports.
• REVOKE_BATCH (object/paged.rs:1492) and mapprobe's SHRUNK are tied only by prose. If the batch ever reaches 79, shrunk silently stops covering a second batch. A word at REVOKE_BATCH naming the case would keep them together.

Evidence

My checks at 5f9f6fe, in a detached worktree:

• cargo test -p kernel --lib --features sched-check: 472 passed, exit 0.
• cargo run -- --ci host lint: 5 steps, all green, exit 0. That is 26 clippy runs, twelve of them kernel shapes, all clean.
• cargo run -- --ci host models: 84 steps, all green, exit 0. paged_ranges passes, and its control ranges-less-relaxed fails as intended, with loom's "Causality violation".
• Model control (mine). I built the pure paged, vm and chunked modules out of tree.
  • Unchanged, paged:: passes 30 of 30.
  • With Pages::revoking's cursor reading only the first batch (Cursor::After(_) => NONE), three tests fail:
    • every_interleaving_keeps_each_leaf_on_its_pages_one_frame and long_runs_…, each with "maps given-back frame".
    • the_walks_set_is_read_a_batch_at_a_time_in_marking_order.
  • So the batches-of-one model would catch a visit that stops early.
• B10 reproduction: the host harness described under B10. It is scratch, not committed.

Author's evidence (7664250a/r3):

• The log keeps only each command's tail, so the per-test output is lost.
• Its counts and exit codes agree with my runs.

Guest: run 43104273025 at 5f9f6fe was still queued when I posted, so this round's kernel changes have no guest evidence yet. That is also the probe's first AArch64 build. At the final head, after B10, these rows must be green:

• a_mapped_file_follows_its_pager
• virt_mapped_file
• osbench_map_group_exits_0
• the copy rows

mapped_file must show shrunk's two mappers each ended Fault::Mapping.

Metal: none ran, and none is a landing condition.

PR description (the orchestrator's to edit):

• "After every visit and before any frame goes back, the walk ends every futex wait on a revoking frame" is true only after B10.
• "Its mutation controls (each red) ran before the rebase; the pure index is byte-identical after it" is stale, because this round rewrote the pure index. My cursor control above is the current evidence for the model.

SEND BACK

[Japabu]

Review r3 answered at 156878e, on the orchestrator's decisions. The branch was rewritten for B11 (force-pushed; my own branch).

• B10 (pages marked during the sweep): fixed the way you described.
  • The rule is in the pure crate. next_visit answers Visit(node), Sweep or Finish. The object records the epoch it was swept at (swept, reset when a walk begins), and the walk answers Sweep again whenever a pass has begun since. finish asserts the sweep is current.
  • The kernel loop is a plain match on that answer.
  • The model takes the sweep as a step of its own, a frame at a time, with every other step free to run between. Its finish refuses a frame the current sweep did not reach.
  • a_page_marked_during_the_sweep_is_swept_before_its_frame_goes_back drives your sequence through the pure API. The object has no mapper; page 0 is withdrawn and swept; page 1 is withdrawn between the sweep's read and its relock; the next answer must be Sweep; and every frame finish gives out must have been swept.
  • It passes at the head. Under the old rule (sweep once per walk, a checked one-line patch) it is red, and so are both model runs, with "given back unswept". Evidence: https://github.com/ToyOSOrg/evidence/tree/5222fb740ab34d8333c0a5b5b6aa03bb5e68d7e7/r4
  • Pages::walk is now a test-module helper, and revoked's doc names next_visit, the sweep and finish.
• B11: squashed. f3d5710 and dec827f are now db0b87e, which compiles on its own. Its message calls B8 fixed only in part, and says a page marked during the sweep is covered by the later rule. The records commit follows as 71e0397, and B10 is 156878e. The final tree is the same as before the squash plus B10.
• Suggestions: both taken. The vm.rs test is after the test module's imports, and REVOKE_BATCH names mapprobe's shrunk case, which needs two batches.
• PR body: it states the sweep rule as now built, and cites your cursor control and my sweep-once control as the current model evidence, replacing the stale sentence.

Checks at 156878e: cargo test -p kernel --lib --features sched-check (473 passed), cargo run -- --ci host lint (5 of 5 green), cargo run -- --ci host models (84 of 84 green).

Guest: run 43108977664 at 156878e (a_mapped_file_follows_its_pager virt_mapped_file osbench_map_group_exits_0 a_user_copy_faults_in_mid_copy_or_ends_as_bad_address virt_user_copy_faults). Run 43104273025 at 5f9f6fe is left queued, on the orchestrator's correction. It gives early signal on the probe's first AArch64 build, the 255-helper row and the 80-page shrink; no guest row can reach the sweep race.

[Japabu]

Review r4 of #1269 at 156878e (9d821433c..156878eac)

Architecture

B10's rule now lives in the pure crate, as the orchestrator decided. next_visit answers Visit, Sweep or Finish, and the kernel's loop is a plain match on that answer. The model takes the sweep as a step of its own. This is the right owner: the rule is now one function that the host can test.

Size of this round:

• Pure production: +33/−26. That is Next, swept, and walk moving out.
• Kernel: +25/−26, almost all of it doc comments.
• Tests: +96/−10. That is the test helper walk, the new test, and the model's sweep step and oracle.

Your checks:

1. Is the epoch rule complete? Yes.
   • Every marking path reaches the rule. Withdraw, fail and resize (through removing), and release and pager end (through let_go), all call revoked in the hold that marked. So Object::revoke sets again whenever a walk is running.
   • again forces a new pass before Finish. next_visit cannot answer Finish while again is set; it begins a new epoch first. swept equals the new epoch only after a Sweep is answered at that epoch, and a Sweep is answered only once that pass has visited every mapper.
   • A mark during a visit: the remaining mappers are visited, then a new pass revisits every mapper, then the walk sweeps.
   • A mark during a sweep (B10): a new pass follows, with or without mappers, then a second sweep.
   • A mark between the last Sweep answer and finish: the only lock drops in that window are the sweep's own, which is the case above. The Finish answer and finish share one hold. In the kernel, break goes straight to finish without dropping the lock. In the model, both happen in one step.
   • So the final sweep is complete. It begins after the last mark and after the last pass's visits, and reads the whole set from Cursor::Start.
2. Does finish's refusal make the defect unrepresentable? No: it catches it at run time, loudly.
   • What the assert checks: o.swept == Some(o.epoch) shows that next_visit answered Sweep at this epoch. It does not show that the sweep ran, because swept is set when the answer is given.
   • Why this is sound today: the kernel's one caller always performs the sweep.
   • Making it unrepresentable is cheap. See S1.
3. Does the model's interleaving cover the reviewer's sequence? The seeded run does. The exhaustive run does not.
   • Long run: with finish's check relaxed, so that only the model's own oracle decides, long_runs_… reds with "frame 104 given back unswept". This holds under both the faithful pre-r3 rule and once-per-walk.
   • Exhaustive run: every_interleaving_… stays green under both controls.
     • Its prefix maps both spaces, so the sequence needs eight more steps: two unmaps, a withdraw, a walk, two sweep reads, a withdraw and a walk. Its depth is five.
     • In the author's control it went red only through finish's assert. That assert compares the mutated next_visit with finish's own unmutated check, so it is not the model's oracle detecting anything.
   • The new unit test pins the exact sequence. Together with the long run, that is enough.
4. Is the kernel's match exactly the pure rule? Yes.
   • Visit → visit.
   • Sweep → end_futex_waits, which reads from Cursor::Start until a short batch. With batches of one, that is the model's stop at an empty read.
   • Finish → break → finish, in the same guard.
5. Does each commit build? Yes (my runs below).
   • db0b87e and 71e0397 each pass five checks:
     • cargo check -p kernel --lib --tests --features sched-check
     • the kernel binary for x86_64-unknown-none and aarch64-unknown-none-softfloat
     • the same two binaries with boot-actuators,test-actuators
   • Exit 0 on all ten.
   • Negative control: f3d5710's x86-64 binary fails with E0004 (Populated::PastEnd(_) not covered), exit 101.
   • 156878e is covered by lint's twelve kernel shapes.
   • 71e0397 changes no kernel file, and its one code edit is a libc doc comment.
6. Is the range-diff only the squash plus B10? Yes.
   • git diff dec827f18 db0b87e3b and git diff 5f9f6fe41 71e03977d are both empty.
   • The range-diff shows f3d5710 and dec827f squashed into db0b87e, 5f9f6fe equal to 71e0397, and 156878e new.
   • db0b87e's message calls B8 fixed only in part.

Blockers

B12 (new). B10 left stale and false comments. All are text-only fixes.

• kernel/pure/paged.rs:18 and kernel/pure/paged.rs:323 both link Pages::walk. The module header says the last pass's end gives the frames out (Pages::walk), and Revoke::Walk says "the caller walks it (Pages::walk) to its end".
  • walk is now a #[cfg(test)] helper, so both links point at nothing the kernel can call.
  • R3 asked for the move together with the docs that cite it. Only revoked's doc was updated.
  • Cite Pages::next_visit / Pages::finish instead.
• kernel/pure/paged.rs:385-386: swept is documented as "the epoch the running walk last ended every futex wait on its set at".
  • It is set when Sweep is answered, before any wait ends.
  • That is exactly the gap between what finish's assert proves and what this doc claims. Say "was last told to sweep at", or equivalent.
• kernel/src/object/paged.rs:351-352: "sweeps the waits on the walk's set after every pass" is false.
  • A pass that a mark interrupts goes straight to the next pass with no sweep of its own.
  • Name the rule's owner instead, e.g. "sweeps as Pages::next_visit directs".
• kernel/src/object/paged.rs:420-423: end_futex_waits's doc restates when the walk sweeps. That is next_visit's rule, now at its one home.
  • The restatement ("and again after any pass a page marked meanwhile began") does not parse.
  • Keep what the function does: it reads under the pager's lock and ends the waits outside it (revoke_frames).
  • Keep why it exists: an unmap, discard, protect to none or a space's end clears a leaf without ending waits on a frame it does not own.
  • Drop the schedule. A rule stated in two places is how B10 arose.

Suggestions

• S1. Make B10 unrepresentable. With Sweep as an answer of the pure rule, the walk's end can be an answer too.
  • Proposed shape: Pages::walk(o, mappers, waiters, out) -> Next answers Visit(node), Sweep or Finished, running finish itself, and finish becomes private.
  • The kernel loop builds Linked and the give-back closure in each iteration, from disjoint fields of the same destructured State, and breaks on Finished.
  • Then no caller can give frames back off-rule, and the assert becomes unnecessary.
  • The test-only walk helper goes, since production would be the same function.
  • next_visit loses a name that is no longer accurate, since it now answers a sweep and a finish.
  • This is optional: the assert fails loudly, and the kernel has one caller.
• S2. Give the model's oracle the property itself. The swept set is a proxy.
  • What it checks: that the last sweep reached every freed frame, so it catches B10.
  • What it misses: whether that sweep followed the pass's visits.
  • Measured: I moved the Sweep answer ahead of the mapper check, so the walk sweeps before visiting. Both model runs stay green. Only the scripted a_fault_answered_then_shrunk_and_grown_asks_afresh fails, because its fixed step list no longer plays. That ordering is B8's defect: a wait arms through a leaf not yet cleared, after the sweep.
  • Proposed oracle:
    • A Wait(s, page) step keys a waiter on the frame its leaf maps.
    • Sweep ends the waiters on the frame it reads.
    • finish asserts that no waiter is keyed on a frame it gives out.
  • That would catch both defects. A no-mapper prefix would also let the exhaustive run reach r3's sequence.
  • Today, inspecting next_visit's order is enough.

Evidence

My checks at 156878e, in a detached worktree:

• cargo test -p kernel --lib --features sched-check: 473 passed, exit 0. That includes a_page_marked_during_the_sweep_is_swept_before_its_frame_goes_back and both model runs.
• cargo run -- --ci host lint: 5 steps, all green, exit 0. That is 26 clippy runs, twelve of them kernel shapes.
• cargo run -- --ci host models: 84 steps, all green, exit 0. paged_ranges passes, and its control ranges-less-relaxed reds with loom's "Causality violation".
• Builds of the earlier commits and the range-diff: as listed above.
• Model controls (mine). I built the pure paged, vm and chunked modules out of tree.
  • Unchanged: 31 of 31 pass.
  • The faithful pre-r3 rule is 5f9f6fe's kernel rule (swept reset on Visit, sweep while unset), with finish's check back to the walk state alone. The new unit test reds ("a pass began since the sweep": Finish, not Sweep), long_runs reds ("frame 104 given back unswept"), and every_interleaving stays green.
  • The author's once-per-walk rule, with finish's check relaxed the same way, gives the same three results.
  • Sweep before visits: see S2.

Author's evidence (5222fb74/r4):

• Its counts and exit codes agree with mine.
• Its control log contradicts the claim about it. The log shows both model runs red at paged.rs:771 with "walk ended with a pass or a sweep owed". That is finish's assert, not the model's "given back unswept", which is what the PR body and the r3 response report.
• The once-per-walk patch is also not "the rule before r3". 5f9f6fe swept again after any visit. The faithful rule gives the same verdicts, as shown above.
• The commit message of 156878e carries the same label. Correct it if that commit is rewritten for B12.

Guest: runs 43108977664 (156878e) and 43104273025 (5f9f6fe) were both still queued when I posted. So no guest row has yet run this PR's r2–r4 kernel changes, nor the probe's first AArch64 build. R3's landing rows still stand at the final head:

• a_mapped_file_follows_its_pager
• virt_mapped_file
• osbench_map_group_exits_0
• the two copy rows

mapped_file must show shrunk's two mappers each ended Fault::Mapping. No guest row can reach the sweep race; the host covers it.

Metal: none ran, and none is a landing condition.

PR description (the orchestrator's to edit):

• The pure-model sentence "sweeping once per walk (the rule before r3 …) reds … both model runs ("given back unswept")" should say what the controls show:
  • The unit test and long_runs red on the model's oracle.
  • every_interleaving reds only through finish's assert, and does not reach the sequence at depth five.
  • The pre-r3 rule was "sweep again after any visit".

SEND BACK

[Japabu]

Rebased onto main 302fb36 (#1252); head ecfb224. The resolution only keeps both sides, so run 43152933746 stays queued at 41f0e11. That head is held on map7b-2-hold.

The conflicts. Both were in one commit, B5's Review r1 of #1269: every copy a syscall makes answers its own cause, in kernel/src/syscall/dispatch.rs and kernel/src/syscall/ipc.rs.

• B5 had converted three copies in the namespace build: its argument record and its two vectors. A child's handles are a list its parent names: labels and namespaces leave the kernel #1252 deleted that code.
• I took main's side in both hunks, so main's removal and SYS_CONNECT stay.
• B5's other sites are unchanged. I reworded the commit's message so that its list no longer names the namespace sites. Its tree is the resolution's.

#1252's own copies. It added two: the spawn's endowment list read, and its copy-out. Both already answer SyscallError::from(faulted), so in the composition they answer the copy's own cause, BadAddress or Io, through this PR's Faulted. A search finds no copy that #1252 added which flattens a failure to BadAddress. No line means something different.

Range-diff 3c5c55584..41f0e1195 against 302fb3698..ecfb2248a: 29 commits are =, and two are !:

• B5's commit (now 5d73370) has no hunks in the namespace code and no ipc.rs change, and its message is reworded.
• A lost mapped page ends a program as SIGBUS and a copy as Io… (now 1e796da) differs only in a hunk header's context line in user_ptr.rs. The content is the same.

Checks at ecfb224, exit 0 each:

• cargo test -p kernel --lib --features sched-check: 514 passed.
• The kernel's four clippy shapes with -D warnings.
• cargo run -- --build-only for testcases and AArch64's virtjobcase, each compiling mapprobe against A child's handles are a list its parent names: labels and namespaces leave the kernel #1252's SDK.

Evidence, including the range-diff: https://github.com/ToyOSOrg/evidence/tree/5a210f12d3bfcb0a205c0a8b967f718030cf2d17/r11

[Japabu]

Orchestrator verification of the rebase onto main 302fb36 (#1252) at ecfb224. I read git range-diff 3c5c55584..41f0e1195 302fb3698..ecfb2248a:

• 29 commits are =.
• 1e796da differs only in one hunk-header context line.
• 5d73370, B5's commit, differs only in dropping its three conversions inside the namespace build. A child's handles are a list its parent names: labels and namespaces leave the kernel #1252 deleted that code, along with B5's ipc.rs hunk, and the commit message's list of sites is reworded to match.

No line of #1269 means anything different. #1252's two new copies, the endowment-list read and its copy-out, already answer SyscallError::from(faulted), so they inherit this PR's Faulted causes.

So run 43152933746 at 41f0e11 (held on map7b-2-hold) stays the landing run, under the rule that a resolution which only keeps both sides keeps a run valid. The merge queue compiles the composition, and the author's kernel tests (514), four clippy shapes and the testcases/virtjobcase image builds at ecfb224 exit 0. Review r11 is LAND, so #1269 lands when 43152933746 is green.

[Japabu]

Composed with #1258 and main 29c5f2d; head 202566e. The composition changes kernel behaviour, so I cancelled 43152933746 and deleted map7b-2-hold. Run 43170820169 at 202566e carries the six rows and testcases_members_exit_0.

A merge, not a rebase.

• Why. 19 of this branch's commits touch the files An open file is written and stated through its paged object, one write at a time, against credit #1258 rewrote: the index, the kernel's paged object, its syscalls and the SDK. A rebase would resolve the composition again in each of them, and none of those intermediate resolutions could be tested on its own.
• What the merge does. 6e43e99 merges main ee15a2e once. Every reviewed commit keeps its hash and tree. The composition is one diff to review, as An open file is written and stated through its paged object, one write at a time, against credit #1258's own merges of main were.
• Caveat. If the branch must be linear, I can replay it with this resolution as the reference.

The merge's resolution (git show 6e43e99f0 against either parent):

• A revoking page takes no write.
  • admit refuses it, as it refuses an absent page.
  • holder_fits finds it Absent, so a holder's write over it goes to the pager, and admit_fresh's checked install never meets it.
• Credit returns as the page is marked. The room a holder's credit paid for comes back as the page is marked revoking, as An open file is written and stated through its paged object, one write at a time, against credit #1258 gives it back for a page gone before its write-back. The walk's end gives nothing back twice. New pure test: a_revoking_page_takes_no_write_and_gives_its_credit_back_once.
• resize. It keeps An open file is written and stated through its paged object, one write at a time, against credit #1258's seal and its trimming of the dirtied range, and revokes the pages past the size. An open file is written and stated through its paged object, one write at a time, against credit #1258's tests of shrinks, fails and releases settle their walks.
• Want::anew is An open file is written and stated through its paged object, one write at a time, against credit #1258's.
• Slots with two lists. A release unmarks both. A mapping's end goes through say_no_holders, which also waits out holders' writes.
• Map and write side by side. Paged::map sits beside write, append and stat, and a map takes the holder with READ. An open file is written and stated through its paged object, one write at a time, against credit #1258's ABI range is abi::PagedRange.
• toyos_fs_map answers An open file is written and stated through its paged object, one write at a time, against credit #1258's on_fd_held closure type.
• mapprobe and the pager's hold. It holds around its write and its shrink, and mints its holders to read. Its pager now has a dirty ceiling of 2: at 0 the coherent case's own write was refused DirtyFull. So no guest has ever passed mapprobe.
• The row reads An open file is written and stated through its paged object, one write at a time, against credit #1258's "wait overdue".

B20's duty: the combined slot. It is 272 bytes, against 216 on main:

• a 248-byte entry and two 12-byte marks;
• the object's 152 bytes include the 48 of mapping's walk state;
• measured by the compiler on both targets, with main measured the same way: https://github.com/ToyOSOrg/evidence/tree/94fd400ddab5d9c2ff776ac9df66f1b0bb88b768/r12/sizes
• the record's "whichever lands second" sentence is gone.

The memory record's duty: the pinned-copy test (9a29a35).

• The risk. An open file is written and stated through its paged object, one write at a time, against credit #1258's holder write stages its bytes into frames drawn from its pager before it takes the write side. A source page of a mapping that is absent parked that copy while it held those frames, which are what the pager's supply draws.
• The fix. The staging copy now runs under user_ptr::Pinned. An absent page stops it, the write gives every frame back, waits for the source pages holding nothing (wait_in), and draws again.
• B5. A copy that faults answers its own cause where An open file is written and stated through its paged object, one write at a time, against credit #1258 flattened it to BadAddress.
• The test. mapprobe's written case has a mapper write an empty, credited object from its mapping's first page, which no one has supplied. The pager supplies the requested run, the write lands whole, and the pager reads the bytes back.
• The record drops its paragraph on the owed test.

ea33f5a: a fault's wait and a touched hole's frame call #1258's wait_changed and draw/materialize instead of their own copies of them.

202566e merges main 29c5f2d (#1227, #1264, #1280), with no conflicts. #1227 removed libc's refuse_files, so a refused map answers through set_errno's one table. A file its server maps no pages of still answers ENODEV.

Checks, full logs: https://github.com/ToyOSOrg/evidence/tree/431cbdf36e6c555c96eff50611959023437a6520/r12

• At 202566e, exit 0 each:
  • kernel tests: 525 passed;
  • the four kernel clippy shapes;
  • toyos-checks: 55 passed;
  • lint: 5 of 5;
  • models: 93 of 93;
  • --build-only of testcases, benchcase, AArch64's virtjobcase and both default images. mapprobe builds for both architectures.
• Each new commit compiles. The merge and 9a29a35 each compile on both kernel targets, with the SDK and the kernel's tests built.
• The first run was red. At ea33f5a's first form, lint and every image failed on the toyos_fs_map closure: only a target build of the SDK compiles it, and none of my host checks did. The fix is folded into the merge.

[Japabu]

Review r12 of #1269 at 202566e

Scope: the four first-parent commits after ecfb224. 6e43e99 was read with git show --remerge-diff and against both parents, then 9a29a35, ea33f5a, and 202566e (its remerge diff is the one refuse_files → set_errno line). I also read the full merged kernel/pure/paged.rs, kernel/src/object/paged.rs, user_ptr.rs, mapprobe, the fault path in process.rs, the fileserver's write and supply loops, and the r12 and r9 evidence.

Architecture

The composition keeps each design whole and joins them at one rule: a revoking page is no longer the file's. So:

• it takes no write;
• holders see it as Absent;
• the room a holder's credit paid for comes back when the page is marked.

This is #1258's "gone before its write-back" rule, applied at the moment the bytes stop counting. Marking resets the page's state, so the walk's remove cannot give the credit back a second time.

The pinned-copy change applies the existing ruling to one more copy that holds pager resources, for about 26 net kernel lines. ea33f5a deletes 25 lines that duplicated the wait and the draw. A merge in place of a rebase is the orchestrator's call, which I don't revisit.

The walk, finish, visit, sweep and link/unlink code is unchanged from ecfb224, so B8's and B10's rules stand as reviewed.

Each requested check:

• Both PRs' invariants hold.
  • One write at a time: resize still needs the pager's hold, so it cannot run during a holder's write.
  • Seal: resize refuses on a sealed object before the version moves.
  • The dirtied range is trimmed on a shrink.
  • dirty_held and credit: each is given back once, at marking.
  • Holders and writers: an unmap goes through say_no_holders, and a release unmarks both lists. Slots::remove also unmarks every list.
  • Want::anew() followed by ask gives the model's fault the same want as the old anew(page, 1). The kernel's fault path still uses a fresh Waiting.
• The pinned-copy loop (holder_write, 1292–1352) is correct.
  • Frames: every iteration draws staged + fresh frames and materializes all of them. A stop gives all of them back with leave(false), which balances the out += 1 that draw and promised made. A short draw gives back what it drew.
  • Credit and pins: neither is taken before take_holder, so a stop loses neither.
  • Waits: the only wait is wait_in, which runs after give_frames with the lock dropped. The HolderWriting count stays held across it, but that only defers the no-holders notice, which a supply does not need.
  • Termination: each retry follows a served page or a change of the object. The wait is reported overdue through wait_changed (D6), a kill ends it, Lost answers Io and Unreachable answers BadAddress.
  • Model: none is owed. Before the side is taken the loop only reads the index (holder_fits). Its frame accounting is local and can be checked by reading it, and Core has its own host test.
• admit/holder_fits leave no window.
  • Both run after take_holder in one hold of the lock. holder_fits refuses a revoking page, so admit_fresh's expect cannot meet one.
  • withdraw skips dirty and write-pinned pages, and resize waits for the side.
  • A fail or release after admission marks the page revoking during the staged copy. The bytes then land in the kept, pinned frame, write_unpin discards them, and the credit comes back once, at the marking. This is An open file is written and stated through its paged object, one write at a time, against credit #1258's semantics for a removal during a copy.
  • The new pure test catches each defect it covers: no credit at marking, a second credit at the walk's end, and a revoking page that holder_fits would accept.
  • Only a holder in another process can see a revoking page, during a file server's removal. It gets WouldBlock and goes to the single-threaded server, which handles it after the removal's walk has ended.
• mapprobe tests what it claims, with one caveat (S2).
  • The hold around coherent's write and shrunk's shrink is required.
  • A dirty ceiling of 0 refused coherent's write DirtyFull. It did so at ecfb224 too, through write_pin, so "never passed" is accurate.
  • In written, page 0 of the source is deterministically absent and the SDK's write is a bare syscall, so the kernel's copy reaches the stop, give-back and retry path every run.
• Evidence.
  • The head logs 01–10 are at 202566e and exit 0. The 525 tests include the new pure test, and the models' 93 steps include the controls reaching their verdicts.
  • The pre-fold commits b84dd6b25, 24fdb44c4 and e1c2794f8 differ from 6e43e99, 9a29a35 and ea33f5a only in owner.rs's closure line (checked with git diff --stat). Their compile logs therefore stand.
  • The sizes were measured at the uncommitted resolution. 9a29a35 and ea33f5a change no field of Entry, Object or Mark, so the sizes hold at the head.
  • No guest result exists yet: 43170820169 is queued at 202566e. It will be the first run of mapprobe ever.

Growth: the pinned-copy loop adds +65/−39 kernel lines, the dedup −25, and the merge resolution's credit-at-marking a few lines plus a 23-line pure test. mapprobe grows by 44 lines (the holding helper and the written case), and the memory record loses 7.

Findings

B1 — issues/one-client-can-fill-the-tmp-servers-memory-and-deny-every-other-client.md:31-32: "the walk state mapping needs is 48 of the object's 152" does not follow from the evidence.

• r12 measures Object at 112 on main and 152 merged. The walk state adds 40 bytes. Its fields total 42: revoking 8, revoke_head 4, revoke_tail 4, epoch 8, walk 1, finished 8, swept 8, linked 1.
• 48 is r9's difference (40 → 88), measured on the layout before An open file is written and stated through its paged object, one write at a time, against credit #1258.
• The record contradicts itself. Its own "272 against 216" makes mapping cost 56 bytes a slot, while its breakdown gives 48 + 16 = 64.
• Fix: state the measured difference (the walk state adds 40 to the object, and with the 16-byte list of mappers, 56 to a slot), or drop the clause. The 272, 248, 152 and 12 figures are right.

B2 — kernel/src/object/paged.rs:1446: draw's doc says each Some is a frame "which [materialize] completes outside the lock".

• Since ea33f5a, Index::zeroed (line 1897) materializes under the pager's lock, as the code it replaced did. Delete "outside the lock".
• In the same file, line 15: the module header still says a holder's write "copies its bytes into frames held aside first". 9a29a35 corrected the identical phrase in holder_write's doc to "frames drawn first", because the frames come from aside, the pool or a fresh promise. Make the header say the same.

S1 — user_ptr::Pinned now means "holds what no wait may hold", and in holder_write nothing is pinned. The 4-line comment at 1324–1327 exists only to explain this, and it repeats the doc comment at 1266–1268 and the module header at 48–51. Naming the mode for what it guards would let that comment go; at the least, drop it as redundant with the doc. faulted()'s doc and panic message, "a copy holding no pin" (user_ptr.rs:160,164), now mean "a copy outside Pinned".

S2 — tests/guest/mapprobe/src/main.rs:25-27: "its copy holds frames of the pager's, so it lets them go and waits for the page holding nothing" describes something the case cannot observe. The code before 9a29a35, a copy parked while holding frames, passes the case too unless the pager's job is out of memory. What the case does establish is that the stop, give-back, redraw and re-copy path completes and lands the right bytes. That frames are given back is established by reading the code. Consider trimming the clause to that.

PR description (the orchestrator's)

• Size bullet. "a 248-byte entry, whose object's 152 bytes include the 48 of mapping's walk state, and the 16-byte list of mappers" leaves out the two 12-byte marks (248 + 24 = 272). The 48 should be 40, per B1.
• Decision section. It cites "(24fdb44c4)", a pre-fold hash that is on neither the branch nor main. The commit is 9a29a35.
• Pure model. "35 tests" is 45 at the head, now that An open file is written and stated through its paged object, one write at a time, against credit #1258's tests are merged in.
• Author's comment. "main measured the same way": main was measured on x86_64 only. The evidence README says so correctly.

Neither blocker is a code change: one is a record line, the other comment text. Neither needs another host or guest run.

SEND BACK

[Japabu]

Review r12 answered; head 63f18b2. It is one text commit on 202566e: doc comments, one panic message's text and a record. Run 43170820169 at 202566e is unchanged and still queued.

• B1. The /tmp record now says the walk state mapping needs adds 40 bytes to the object (152 against main's 112), and 56 to a slot with the list of mappers. It also says main's 216 was measured on x86-64 only.
• B2. draw's doc drops "outside the lock". The module header says a holder's write copies into frames drawn first.
• S1, taken in part. The comment over the staging copy is gone. faulted()'s doc and panic name "a copy outside Pinned". I kept the name Pinned, and its doc now says it guards a pager's frames as well as pins.
• S2, taken. written's doc says what the case establishes: the write stops at the absent page, waits, draws and copies again, and lands whole with the supplied bytes.
• The PR body.
  • The size bullet is 248 + 2 × 12 = 272, with 40 to the object and 56 a slot.
  • The holder write's commit is 9a29a35.
  • The pure model has 45 tests.
  • Main was measured on x86-64 only.

cargo check -p kernel --target x86_64-unknown-none exits 0 at 63f18b2. No other check can change.

[Japabu]

Orchestrator verification at 63f18b2, from 202566e. I read the diff: doc comments in paged.rs and user_ptr.rs, the text of faulted()'s panic, mapprobe's written doc and the /tmp record. No logic changes.

• r12's B1: walk state adds 40 to the object and 56 to a slot, and main's 216 is noted as x86-64 only.
• r12's B2: draw's doc and the module header.
• S1 (in part) and S2 taken.

The body corrections are in. Run 43170820169 at 202566e, which is code-identical, is the landing run, and #1269 is queued when it is green.