[Japabu]

Problem

Since #1045 every frame and kernel object a process causes is refused at its call when memory runs out. The charges went to the machine, though. When one process took everything, every other process was refused too, the supervisor and the input path included, and a service refused its restart for memory stayed down for good.

The owner asked for:

• per-job accounting, after the machine-level charges;
• no fixed per-app limits;
• system controls that stay usable under exhaustion, which "allocation errors alone do not establish".

What changes

Every charge is counted to the job that caused it. The scheduler's job is the account (kernel::frames::Ledger on kernel::sched::job::Job). Promises, page tables, runs (pipe rings, device memory) and kernel-heap charges each name their job:

• the caller's, for what a call makes (charge::current);
• the child's, for everything a spawn builds for it. The job is resolved before the spawn builds anything (loader::Commit). The spawner's handle to the child and the child's notice are the spawner's.
• the space's, for its tables and commitments;
• the creator's, for an object;
• the creating job's, for both rings of a pipe (pipe.rs), so a connection's rings are the connecting job's. A server's reply therefore costs it nothing, and no client can spend a server's floor by connecting to it. A pipe a server makes and hands out, such as fileserver's stream pipe or netstack's bells, is the server's, which chose and bounds it.

Ordinary work is the job that uses it:

• A login authority is handed its session's controls as a namespace and connects its own control connection; a session owner connects its own link (toyos_session::CONTROL, LINK). The supervisor accepts the link without blocking (ACCEPT_NONBLOCK).
• A spawn takes its program's image as the object its server holds it in where there is one (main's fs::IMAGE), and otherwise reads a copy for the child's job (Image::read_for). A launch is endowed its job before prepare reads the image.

SYS_ACCOUNT_INFO reads an account on a job handle carrying READ: floor, committed, kernel, peak, what the last refusal wanted, and how many requests were refused. An ended job asserts its ledger is empty.

Floors. SYS_JOB_FLOOR holds memory back for a job for as long as the job object it was set through lives. It needs SysCap FLOOR, which only the supervisor's carries; no manifest name grants it. The allocator holds every floor job's unused floor against every other job: its frames exactly, and the whole superframes they make for its runs and its own heap pool (kernel/pure/frames.rs's header has the rule).

Each charge takes from the pool its job charges at the time (frames::PoolSplit). So the supervisor's handle table and range charge, made before its floor is set, grow from the floor afterwards. A floor job's own pool stays entitled as far as its floor, so a superframe the heap still holds is never counted free for it.

system.toml declares floors (memory-floor-mib, and [supervisor] memory-floor-mib). The supervisor sets its own floor, and each floor row's at the creation of that row's job. An installed package's row never has one. images/system.toml and images/console.toml give the supervisor 96 MiB and ps2server 24 MiB.

The retry. A job handle becomes readable once its last refused request would be granted: the allocator asks admit and the row a run needs, the same rule the request met, so a floor job counts what its own floor holds for it. A waiter that is not ready arms what it lacks under the allocator's lock, and is armed again when it gives back to its floor or is refused again. Every give-back path posts one IrqWatch once some waiter may be granted, after the lock is let go. That condition is necessary for some waiter's grant and exact for a single waiter without a floor. The post frees nothing.

The supervisor keeps each service's job across its starts. When a restart was refused memory that the job's account recorded, the service keeps its ports and starts again on that readiness, and the supervisor says so both ways. Any other refusal, such as a limit or the supervisor's own memory, closes the ports and is reported as what it was, so a stale want cannot spin the loop. A service closed for good drops its job and floor.

While a storage service waits for memory, the supervisor's file calls answer at once instead of blocking its loop for FILES_BOUND.

Children's log rings are their own. SHM_FOR_JOB counts a region to a job handle the caller holds with WRITE. The supervisor's rings for its children now go to each child's job.

Consequential decisions

• The floor is a protected total allowance (owner, 2026-10-24). It guarantees the first floor of a job's use, cgroup v2 memory.min's contract. It is not an emergency allowance on top of the job's use, so each floor's size includes its job's running footprint.
• The compositor gets no floor (owner, 2026-10-24). The next step is to investigate a bounded emergency path in the existing compositor, in which ordinary rendering cannot spend protected capacity. A separate control-view process is not assumed necessary or sufficient.
• usbd gets no floor: it drives disks too, so it is a mixed service, and a USB keyboard is unprotected. A driver split only to assign a floor is not presumed (owner, 2026-10-24).
• No exhaustion recovery is claimed for visible controls or USB input. The follow-ups are the compositor's emergency path and a review of the whole path from input to the visible controls to the stop, USB input included, before any recovery is claimed (owner, 2026-10-24). The proving test stands a system holder in for the controls.

Checks and evidence

Evidence:

• round 1: https://github.com/ToyOSOrg/evidence/tree/f21a4ec1871b95dd5338c8f572dd666ad8eb2a1f/r1
• round 2: https://github.com/ToyOSOrg/evidence/tree/28b60c4c744922caa52c45a08c998321bc83933a/r2
• round 3: https://github.com/ToyOSOrg/evidence/tree/db37c51e785164253479d4ee440e999abfb206da/r3
• round 4: https://github.com/ToyOSOrg/evidence/tree/72961cfc327484e1d90f6ac7436f2a1e3ba1737b/r4
• round 5: https://github.com/ToyOSOrg/evidence/tree/65c6633e52dae3ad486f503bdf780db0c0ee6da8/r5
• round 6: https://github.com/ToyOSOrg/evidence/tree/039052205f47c7b3b0d03ac9af3db7f29779a01a/r6
• round 7 (the rebase): https://github.com/ToyOSOrg/evidence/tree/d1e6652b5ad4ecbb05a5c42d1e29a47f299063dd/r7
• round 8: https://github.com/ToyOSOrg/evidence/tree/81614cc6bcad9dcd7bbcd47d8f09462d1da7c957/r8

The branch is 38f3c282b, one commit rebased onto eba9e8eac, and 4bfe7e489, which fixes one comment and one issue sentence. At it, from a clean tree: cargo run -- --build-only, cargo run -- --ci host (103 steps green), the proving test ×3, and session_lifecycle, console_image_boots and kernel_objects_refused_alone, each exit 0. The other runs below are at 4635148fd (round 5) and 825114d83 (round 6), except the measurements and the regression rows, which are round 3's at c06cc695e. Rounds 4 and 5 changed only frames.rs's readiness, the proving test's take step, the std spawn path's comments and error kind, and one compositor log line, so those still apply.

• cargo run -- --ci host: 103 steps, all green, exit 0.

• Host laws in kernel/pure/frames.rs: 15 new, covering:

  • a floor held against every other job;
  • a floor job's heap drawing on its floor and keeping it;
  • a job past its floor treated as ordinary;
  • a floor set only where it is free, and let go of whole;
  • whole superframes kept apart from scattered free frames;
  • a floor let go of releasing its pool;
  • a charge made before its floor growing from it;
  • memory-returned answered once, and only when enough came back;
  • a wait for a superframe, on a fragmented model, answered by a whole superframe and not by scattered frames;
  • a floor job's wait answered by its own floor's superframe once its pin goes, and not while the floor is short (review r3's trace; red on c06cc695e's rule);
  • a wait for a run answered by a row, not by superframes apart;
  • a smaller request refused while waiting being what memory coming back answers;
  • the kernel splitting a kept superframe answering a waiter;
  • a 40 000-step model with two floors, pins and runs, asserting after every step that no account still waits whose request admit would grant;
  • a fragmentation model holding a floor exact over 30 000 mixed operations.

  Nineteen mutations, each red and each restored.

• The proving test, memory_floor_holds_the_controls, runs on QEMU Profile::Metal (the T14's shape: q35, i8042, no USB keyboard) in its own boot of tests/images/floorcase.toml. Green three times at this head, and six at round 4's. It needs the guest because it holds the kernel's accounts and floors, the supervisor's restart and the input path together. It judges order and completion only, with no timing. With one ordinary job holding every frame:

  • a server's reply leaves the server's account unchanged;
  • an ordinary spawn is refused;
  • the supervisor answers a stop's request;
  • a service refused memory ends, its restart is refused, and it keeps its port;
  • a typed key reaches the owner of input through ps2server;
  • the system holder kills the greedy job;
  • the starved service serves the waiting client;
  • every service the supervisor refused for memory, fileserver data among them, starts again.

• Controls, each one change:

  • floors not held: red;
  • no retry: red;
  • no memory-returned post: red;
  • only ps2server's floor removed: red at the key, because the connection's first write needs a ring;
  • a ring counted to its first writer: red;
  • only the supervisor's floor removed: green, four runs of four. The test makes no claim for the supervisor's floor. Round 4's reds came from the take step waiting on fileserver's writeback crash (now fixed): that crash's restart was refused for the supervisor's own memory.

• Floor jobs' accounts, committed + kernel, which the supervisor now prints once its boot is done:

  image	supervisor (floor 96 MiB)	ps2server (floor 24 MiB)
  images/console.toml	36.9 MiB, peak 38.9 MiB	12.0 MiB
  images/system.toml, at its loop	37.0 MiB, peak 39.0 MiB	12.0 MiB
  images/system.toml, desktop session and 4 launches	41.7 MiB, peak 43.7 MiB	14.0 MiB

  Round 2 measured 66 MiB after the same launches, growing about 1 MiB a launch for the children's images. Now the four launches add 15 KiB in all.

• Regression:

  • at 4bfe7e489, after the rebase: the 22 QEMU rows green on a second run. The first run, with every build cold, stalled session_lifecycle when keys typed through QMP were lost (detach /pholder); sessioncase has no floors, and the row is green alone ×3 (r8 evidence). The rows include kernel_objects_refused_alone, session_lifecycle and console_image_boots (the session protocol changed), the spawn, drives, device-memory, usbd, stream, compositor and state rows, and 8 AArch64 virt rows;
  • before the rebase, at c06cc695e: the 88 shared Rust members in one q35 boot: 81 green on the shipping kernel, and the 7 actuator members green on the test kernel. No kernel panic.

• T14 at c06cc695e: all three boots passed: floorcase (memory_floor, without the key, which no bench can type), benchcase (osbench) and testcases-refused (kernel_objects_refused). In memory_floor the greedy job held 15 599 MiB. On metal the supervisor held 36.9 MiB (peak 40.9) and ps2server 12.0 MiB, matching QEMU.

• T14 at 71e3b8d78: floorcase passed.

• T14 at e8829f986: floorcase passed.

• T14 at 38f3c282b, after the rebase: floorcase passed. The greedy job held 15 604 MiB, and on metal the supervisor held 36.9 MiB (peak 38.9) and ps2server 11.3 MiB.

The test needs a few contrivances, each in its own image or programs:

• the greedy job takes again whatever comes back;
• starveling gives back most of its stack before it ends, so its end frees less than a start needs;
• logkeeper has a floor in floorcase.toml, so the job can read the supervisor's refusal while every frame is held.

The reason: a dead process's memory is freed after its end is published, so a restart otherwise races whoever asks first.

Unresolved

• No test shows reliably that the supervisor's floor is needed. The controls that would draw on it under exhaustion (the stop UI, a kill on request) are not built.
• A sign-out or power notice sent to a session whose owner has not yet connected its link is dropped with a log line, where before it queued on the link. The window is the owner's start-up.
• These are recorded in issues/no-physical-memory-fairness.md, each with an owner and an exit:
  • the stop UI;
  • a restart refused for the supervisor's own memory closing the service;
  • a few KiB of the supervisor's per live launched program (handle, notice, connectors), bounded only by the process table;
  • connect-time receive capacity;
  • floor deficits pooled across floor jobs;
  • the unprotected USB keyboard;
  • no memory retry for drives starts;
  • kill on transient heap;
  • account_info without resident, retained or live-process counts.

🤖 Generated with Claude Code

[Japabu]

Review of #1057, round 1 (head aa89ed2db)

Architecture

Using the scheduler's job as the account is the right owner. Resolving the child's job before a spawn builds anything (Commit::job, checked again with ptr_eq at commit) and counting the child's log ring to the child (SHM_FOR_JOB) are clean, and they fix the ring-on-the-supervisor defect. Only the supervisor's SysCap carries FLOOR (loader/mod.rs:478), and syscap_rights has no name for it. The retry is level-triggered: a post forces a look that calls has_data → pmm::ready again (inbox/mod.rs:633-655), and read_posts_are_readiness is false for Job, so it uses no timer and loses no wakeup. The service keeps its job and ports across a refused restart. The kernel/pure/frames.rs laws, with 8 mutations and a 30 000-step fragmentation model, are good host coverage.

Several things defeat the protection the PR claims:

• connection rings charge a floor for client work;
• the supervisor's own long-lived charges never reach its floor;
• one floor goes to a mixed service;
• the floor sizes are not measured on the shipped images.

Net: +2428/−568. About 450 lines are frames.rs tests and about 470 are the guest test, its two helper programs and the image.

Blockers

1. kernel/src/pipe.rs:170: a ring is charged to its first writer, so clients can spend the floors. A connection's server→client ring is allocated by the server's first reply, which charges 2 MiB to the server's job. The supervisor accepts up to MAX_PENDING_LAUNCHES = 32 launcher connections (system/supervisor/src/main.rs:160). Any program that opens them and draws one reply each takes 64 MiB of the supervisor's 96 MiB floor, on top of the 40 MiB measured, before any exhaustion. Item 52 forbids this ("Do not spend protected control capacity on unbounded ordinary work"). It is also the opposite of the design's rule that a receiver pays its own queue. The PR records it as a risk but makes it worse, because the ring now lands on the floor rather than on the machine. Cheap fix: charge both rings of a connection to the connecting job. Pipe already holds the creator's Charge, so Run::new(self.charge.job(), 1) would do it. Hold it with a law or a guest check: a client's connect and the server's reply leave the server's account unchanged.

2. kernel/src/mm/charge.rs:74-75: the supervisor's pre-floor charges stay in the shared pool for good. Charge::none fixes its pool when it is created. The supervisor's handle table (loader/mod.rs:455), its space's ranges charge (loader/mod.rs:243, mm/space.rs:333) and its process charge are all made before main.rs:571 sets its floor, so they are Pool::Shared forever. Under exhaustion a shared-pool growth needs a spare superframe the greedy job has already taken. That makes the floor useless for two of the supervisor's control-path growths:

   • its handle table doubling on an accept;
   • its range charge growing every 32 ranges, and it maps one range per child's log ring.

   The test passed because neither boundary was crossed. Fix the representation so that a job's growth after its floor draws on the floor, for example by recording the pool per grow or moving the job's shared bytes at set_floor. Show it with a law, or a guest step that crosses a grain under exhaustion.

3. Retry readiness can spin on a stale wanted (frames.rs:565, main.rs:1480-1483, 2061-2081). sdk/std/sys/pal/mod.rs:31 maps every ResourceExhausted to OutOfMemory, so is_memory() also accepts refusals the service's ledger never recorded:

   • the supervisor's own refusals, including blocker 2;
   • its handle table at MAX_HANDLES;
   • the pid, depth and PCID limits (process.rs:596-601).

   The job's wanted is then stale or 0, so lacks is 0 and the job polls readable at once. memory_returned retries, is refused, logs "still short of memory" and re-arms, without end, which means 100% CPU in the supervisor with a log flood. Make readiness mean a refusal recorded against this job since the attempt, and treat any other refusal as a non-memory failure.

4. The usbd floor (images/system.toml:312, images/console.toml:121) contradicts design §5 and item 52. §5 says "A mixed service gets no floor", and usbd also drives disks for the block service. Its DMA (pcidev::dma_alloc → charge::current()) and buffers would draw on protected capacity, and the 20 MiB it was sized from was measured "with the stick", that is with storage running. As a drives instance it also gets a new job and floor at every start (main.rs:1203), and drops it when it ends. So a usbd that crashes under exhaustion is refused its floor ("cannot be held") and stays down until the next inventory read. Remove the floor and record that USB keyboards are unprotected, or get the owner's explicit exception.

5. The floor sizes are unmeasured on the shipped images, and images/system.toml:14-21 has a false and historical comment. Under the PR's usage-inclusive semantics an undersized floor gives no headroom, and nothing reports that. The only figures come from floorcase.toml, which has 12 rows and no compositor, sessions or apps. Read each floor job's account_info peak on a boot of images/system.toml with a desktop session and a few launches, and on console.toml, and state the margin in the evidence. In the comment, "the input servers, which do no ordinary client work" is false for usbd, and the measurement sentence is history, which belongs in the commit or evidence. Delete both.

6. The evidence does not isolate the floors it credits.

   • The g1 log shows the test job itself aborting (exit=134) right after "an ordinary job's spawn is refused", because test-runner's own floor was gone too. The evidence README's "the stop's request is never answered" does not describe that run.
   • Nothing shows that the supervisor's floor is what answers the stop, or that ps2server's floor is what delivers the key. The key goes over connections warmed before the exhaustion, so it may need no allocation at all.
   • Needed: controls that each remove one floor in floorcase.toml (supervisor 0; ps2server 0), each red on its step. If one stays green, the claim it supports goes.
   • The handoff says fileserver data "is restarted once memory returns, and the floorcase runs show this". Every run shows it starved, and no captured log shows it coming back. Assert it in memory_floor_holds_the_controls: it is one more line in the existing check.

7. Debt is not recorded. These gaps appear in the PR body only, not in issues/:

   • drives instances are not retried on the memory event, which a-service-refused-its-restart-for-memory-stays-down.md covered before it was deleted;
   • kill relies on transient heap;
   • account_info has no resident, retained or live-process counts;
   • floor deficits pool across floor jobs. held and whole are machine-wide, so one floor job's pinned or fragmented shortfall can refuse another floor job inside its own floor (frames.rs:496-506).

   Add them to no-physical-memory-fairness.md or a new issue, with owner and exit.

8. T14 has not run. The floorcase, benchcase (osbench: the allocator now does more under its lock, and each Charge::current clones an Arc<Job>) and testcases-refused boots are all owed.

Suggestions

• kernel/src/object/job.rs:72 with frames.rs:863: refused(l, u64::MAX) saturates wanted, and u.wanted * PAGE_SIZE then panics under the kernel's overflow-checks. It is hard to reach today, but it is a userland-triggerable kernel panic class. Use a saturating multiply.
• kernel/src/object/mod.rs:109: "the one that made it" is false for new_core_for objects (SHM_FOR_JOB, a child's minted console). For the PR text: the ProcessObject and NoticeObject of a spawn are charged to the spawner (loader/mod.rs:352-353), not to "everything a spawn builds". That is fine by design §5's per-live-process control state, but say so.
• main.rs:2038-2043 (storage_fed): one starved storage service refuses every supervisor file call, including roles that are unaffected (a boot-role launch while fileserver data waits). Scope it to the role the call needs.
• A service whose ports were closed for good keeps its job, and so its floor, for the machine's life. Drop it there.

Decisions put to review

1. Floor as "the first floor of use". This is defensible on its merits: it is cgroup v2 memory.min's protected-usage contract, withholds less, and needs no provenance. It is not equivalent to §5, though. The design gives a floor job its full floor beyond its current use at exhaustion; this gives floor − use. It changes an approved contract, so it goes to the owner. I recommend accepting it, with the "equivalent" claim corrected and sizing per blocker 5.
2. No floor for the compositor. This is correct under §5 and item 52: floor eligibility covers the whole account, and the compositor serves every app. Its protection is meant to be precommitted overlay state plus connect-time capacity, and neither is built. As a result, on the shipped images nothing a person can reach survives exhaustion, and the issue says so. Item 71 says usable controls "remain required". Whether this lands as a stage before the stop UI is the owner's call, not the implementer's.
3. usbd's floor. Reject (blocker 4).
4. Sizes from one test boot. Insufficient (blocker 5).

Checks

• Ownership on the paths read. Charges, promises, tables and runs go to the right job, with two exceptions: rings (blocker 1) and the supervisor's pool (blocker 2).

• Ended job. Job::drop asserts an empty ledger, a zero floor and zero entitlement. Every charge, run, space and table holds Arc<Job>, so the assert checks that the counters are consistent.

• Floor authority. Only FLOOR on a SysCap can set a floor, plus WRITE on the job handle, and only the supervisor holds FLOOR. A floor ends with the job object it was set through.

• The supervisor's 30 s file block. Fixed for the starved-storage case, though over-broad (see suggestions).

• Test contrivances. They are disclosed and fit the stated purpose:

  • the greedy job re-takes what comes back;
  • starveling gives back most of its stack;
  • logkeeper has a floor so the test can read the supervisor's line;
  • test-runner stands in for the stop UI.

  The pre-warmed connections hide blocker 1 for every connection except power::cancel.

SEND BACK

[Japabu]

Response to review r1 (head 87636be37)

Evidence: https://github.com/ToyOSOrg/evidence/tree/28b60c4c744922caa52c45a08c998321bc83933a/r2

1. Rings (pipe.rs): a ring is counted to the job that made the pipe, so both rings of a connection are the connecting job's. memory_floor now checks that a server in an ordinary job of its own answers a connection with its account's kernel bytes unchanged; control g6, the ring counted to its first writer again, is red there.
2. Pre-floor charges: a charge records what it holds of each pool (frames::Held), and each growth takes from the pool its job charges then, giving back the floor's part first. Law a_charge_made_before_its_floor_grows_from_it; mutation m9, the pool fixed at the first growth, is red.
3. Retry spin: a job's account counts its memory refusals (AccountInfo::refusals). The supervisor waits only when a start raised its job's count. Any other refusal closes the ports and says its job was refused no memory, so it is a limit or the supervisor's own refusal. Mutation m10, an uncounted refusal, is red in the wait law.
4. usbd: no floor in system.toml, console.toml or floorcase.toml; the USB-keyboard gap is in the fairness issue.
5. Sizes: measured on images/system.toml with the desktop session and four launches (supervisor 66 MiB of 96, ps2server 13.6 of 24) and on console.toml (53 and 11.4). The margins are in the evidence README; the false usbd sentence and the history are gone from the comment.
6. Isolating controls:
   • only the supervisor's floor removed: green, so the test's claim for the supervisor's floor is withdrawn (header, image comment, PR). Answering the stop takes nothing of the supervisor's own once rings are the client's.
   • only ps2server's floor removed: red at the key.
   • The g1 description is corrected in the r2 README.
   • Every service the supervisor refused for memory must start again; fileserver data does, asserted.
7. Debt: recorded in issues/no-physical-memory-fairness.md with owners and exits:
   • drives retries;
   • the kill path's transient heap;
   • account_info's missing fields;
   • floor deficits pooled across floor jobs;
   • the USB keyboard.
8. T14: restaged at 87636be37 (floorcase, benchcase, testcases-refused).

Suggestions taken:

• the saturating account report;
• the ObjectCore::job doc;
• a closed service drops its job.

The PR text now says the spawner holds the child's process object and notice. storage_fed stays machine-wide: the supervisor's file calls carry no role.

Item 80: the floor's meaning is unchanged, with "equivalent" corrected to say what it is not. The compositor still has no floor.

Checks at the head: --ci host 103 green; the proving test 4×; 22 rows; the shared sweep 81 + 7 on the test kernel.

[Japabu]

Review of #1057, round 2 (head 87636be37)

Architecture

The round fixes the right representation in two places.

• frames::Held records which pool each charge's bytes came from, so a growth draws on the pool its job charges at that moment. This removes the fixed-pool defect without a second mechanism.
• pipe.rs now counts a ring to the pipe's creator, so a connection's rings go to the job that connected.

The retry now waits only on a refusal counted on the service's own job. usbd's floor is gone. Withdrawing the claim for the supervisor's floor after g4 came back green was the honest call. The round adds +283/−96 over 14 files: about 70 lines of laws, 60 lines of guest test, and the rest supervisor and kernel.

Two problems remain. The creator rule charges a broker for connections that others use. Readiness counts frames only, so the restart retry can still spin, by a different route than round 1's.

Round 1, resolved

1. Rings. Resolved for a client that connects for itself. g6 is red, and the guest step checks it. See blocker 1 for brokered connections.

2. Pre-floor charges. Resolved. grow takes from the pool the job charges now and shrink gives back the floor's part first. I traced the floor-change cases:

   • Floor dropped to 0 with own-pool bytes outstanding: set_floor trims the entitlement to own.div_ceil(SUPER), and the later uncharge(Own) releases the rest. Job::drop's zero-entitlement assert holds.
   • Floor raised while shared bytes exist: those bytes stay in the shared pool and are not counted against the floor, because floor_used counts only the own entitlement. That matches the floor's meaning.

   The accounting stays exact through these changes. The law and m9 hold it, and no other Pool-fixed holder remains in kernel/src.

3. Stale-want spin. Resolved for that route: a refusal not counted on the job now closes the service and names the cause. Blocker 2 is a separate route.

4. usbd. Resolved, and the gap is recorded.

5. Sizes and comment. Measured, and the comment is fixed. Blocker 1 covers what the margin has to absorb.

6. Controls. Resolved.

   • g5 is red at the key.
   • g4 is green, so the claim is withdrawn.
   • The fileserver data restart is asserted in the host check (tests/toyos.rs:5206).
   • The g1 description is corrected.

7. Debt. Recorded with owners and exits, apart from what blocker 3 adds.

8. T14. Queued at this head and not yet run. Landing still waits on floorcase, benchcase (osbench) and testcases-refused.

Blockers

1. system/supervisor/src/sessions.rs:87, :265; kernel/src/pipe.rs:170: under the creator rule, the supervisor pays for connections it opens and that others use. Together with its per-launch growth, ordinary work spends its floor.

   • handed_to opens a control connection for each login request and hands the client end to the opener. Under creator-pays, both rings count to the supervisor, although the opener and the session owner do all the writing on it. Under first-writer they were theirs.
   • Each session's link is also opened by the supervisor (:265). The owner's sends now count to the supervisor too, which makes up to 4 MiB per session.
   • sshserver opens a session per authenticated connection (sshserver/src/spawn.rs:33), up to MAX_SESSIONS = 16. Fifteen sessions can therefore add about 60 MiB of rings to the supervisor's account.
   • The evidence also shows the supervisor growing about 1 MiB per live launched program, with no bound short of Pid::MAX.
   • Against the 30–43 MiB margin of the 96 MiB floor, client-driven work uses up the protected capacity. That is the class item 52 forbids, and the same class as round 1's blocker 1.

   Cheapest fix for the control connection: hand the opener a namespace holding the session's controls connector, as the launcher already is (:86), so the opener connects and pays. For the link and the per-launch state, either:

   • make them the owner's or the launched job's (the owner connects its own link; the per-launch state is identified and charged to the child's job), or
   • size the floor for MAX_SESSIONS and bound live launches.

   If neither is done in this PR, record it with an owner and exit (blocker 3).

   The same rule moves fileserver's STREAM write pipe (fileserver/src/main.rs:844), which the client writes, onto fileserver. That is acceptable, because fileserver chose and bounded it (bounds::stream), but the issue's wording has to match (blocker 3).

2. kernel/pure/frames.rs:589 with :511, :798-803, :893-898; system/supervisor/src/main.rs:2091-2094: readiness counts frames only, so the retry can spin.

   • refused records a shortfall in frames. ready and the refill post compare it with room() alone.
   • A refusal at superframe grain does not depend on that frame count. Two such cases:
     • alloc_run_for's take_run finding no whole superframe;
     • charge needing a spare superframe while scattered frames are free.
   • In either case the job reads ready at once while the retry is still refused. That refusal is counted on the job, so memory_returned takes the (e, true) arm, says "still short of memory … it waits on" and re-arms. The job handle is level-readable (ops.rs:730), so the poller returns at once.
   • The result is round 1's consequence by another route: 100% CPU in the supervisor and a log flood, for as long as the machine stays fragmented. That is exactly the state after exhaustion that the fairness issue describes.

   Fix: record the refused superframes alongside the frames, and make ready and the want post require spare_supers() for them as well.

   Cheapest proof: a law on a fragmented model where a run is refused while frames are free, and the job is not ready until a whole superframe comes back.

3. issues/no-physical-memory-fairness.md:15-22, :109: the record overstates what holds.

   • "memory_floor_holds_the_controls … hold it" still covers the supervisor's floor, which g4 shows the test does not exercise. Say that the test holds ps2server's floor and the retry, and that the supervisor's floor is unexercised.
   • Record whatever of blocker 1 this PR leaves open: per-launch and per-session growth on the supervisor's account against its floor, with owner and exit.
   • The class statement's "Their memory is now counted to the client's job" is not true under the creator rule for pipes a server makes and hands out, such as fileserver's stream pipe and netstack's bells. Correct it.

On the questions put

• A declared but unproven 96 MiB floor. Acceptable to keep at this size. The owner's design names the supervisor as a floor holder. The size rests on measured use of 53–66 MiB plus headroom, and the cost is only floor − use withheld on 2020+ machines. A smaller floor would not cover the measured use plus blocker 1's growth. Deferring it would leave the supervisor's heap-grain growths unprotected, such as the handle-table doubling and range growth from round 1, and process objects charged to the spawner, which g4 survived only because it stayed under a grain boundary. What is required is that the record not claim the test holds it (blocker 3).
• Sizes. ps2server: 24 MiB against 11.4/13.6 MiB, with a fixed set of connections and no clients. Fine. Supervisor: see blocker 1. Both figures are from QEMU Profile::Metal, not the T14.

Suggestions

• kernel/pure/frames.rs:175: frames::Held shares its name with object::Held (kernel/src/object/mod.rs:41), which the same layer uses for object references. Something like PoolSplit reads unambiguously.
• sdk/abi/src/syscall.rs:2718-2721: the refusals doc puts the supervisor's interpretation into the kernel ABI ("a start that raised it …"). "How many of its requests were refused for memory." is the contract.
• tests/images/floorcase.toml:1-4: the supervisor's floor here is 64 MiB, not the system image's 96, and the test claims nothing for it. "whose floor the system image declares too" suggests otherwise. Either say it mirrors the shipped image's shape, or drop the floor.
• Reading the floor jobs' accounts on the queued T14 floorcase boot would cost nothing extra and check the QEMU sizes on metal.

SEND BACK

[Japabu]

Review r2: response (head c06cc695e)

Evidence: https://github.com/ToyOSOrg/evidence/tree/db37c51e785164253479d4ee440e999abfb206da/r3

Blocker 1, the supervisor paying for others' connections. Fixed by moving each charge to the job that uses it, not by sizing the floor:

• A login authority is now handed its session's controls as a namespace (toyos_session::CONTROL) and connects for itself. A session owner opens its own link from a namespace (LINK), and the supervisor accepts it without blocking. Under the creator rule, both connections' rings are now the opener's and the owner's.
• The roughly 1 MiB per launch was each child's program image, read into the supervisor's account. A spawn now reads the image for the child's job (Image::read_for, read_image_for), and a launch is endowed its job before prepare.

On images/system.toml with four launches, the supervisor holds 41.7 MiB, against 66 MiB in round 2. The four launches add 15 KiB in all.

What remains is the handle, notice and connectors the supervisor keeps per live program, a few KiB each. It is bounded only by the process table and is recorded with an owner and exit. No guest control isolates the session change; the measurement and sessions.rs carry it.

Blocker 2, the retry spinning on fragmentation. Fixed:

• A refusal records the whole superframes it lacked: a run's count, or a heap growth's superframes.
• ready and the refill post both require that many spare whole superframes as well as the frames.

New law: a_wait_for_a_superframe_is_answered_by_one_and_not_by_frames. On a fragmented model, it frees scattered frames, and the job stays unready with no post; it becomes ready once a whole superframe comes back. Mutation m11 (readiness counting frames only) turns it red.

Blocker 3, the record. Corrected:

• The test holds ps2server's floor and the retry; the supervisor's floor is unexercised.
• The supervisor's per-launch growth is recorded.
• The class statement says a pipe is counted to whichever job made it, naming fileserver's stream pipe and netstack's bells as the server's.

Suggestions. All four taken:

• frames::Held is now PoolSplit.
• The refusals ABI doc is now the contract only.
• floorcase.toml's header no longer claims the system image's floor.
• The supervisor prints each floor job's account once its boot is done, so the floorcase T14 boot reads them on metal at no extra cost.

Checks at c06cc695e:

• host CI green;
• 33 laws, with 11 mutations red;
• the proving test green three times;
• g1–g6 as in round 2 (g4 green, the others red);
• 22 rows green;
• sweep: 81 + 7 green, no panic.

T14 is restaged at this head: floorcase, benchcase, testcases-refused.

[Japabu]

Review of #1057, round 3 (head c06cc695e)

Architecture

Moving each charge to the job that causes it is the right fix, and it beats sizing the floor:

• the opener connects its own control connection;
• the owner connects its own link;
• the child's job pays for its program image.

It removes the supervisor's per-session and per-launch growth by representation rather than by margin. The round adds +292/−86 over 18 files: about 30 lines of law, about 110 of session protocol (mostly the Link state), 10 for the kernel accept flag, and the rest SDK plumbing and the record.

Session authority, which you asked about:

• Controls. The namespace holds only the session's unbadged controls connector, which is the port the old connection reached. Namespace exposes open, duplicate and delegation through Builder::keep, and never the connector itself. Repeated opens give no more than repeated MSG_OPENs gave before. The session owner bounds them (MAX_CONTROLS), and the opener now pays for their rings.
• Link. Only the owner receives the LINK namespace. The first queued connection is accepted, and dropping the acceptor then refuses any later one. So nothing else can become the link, and spoofing would need the owner's own cooperation.
• The non-blocking accept never parks. An acceptor is readable only while a connection is pending (ops.rs:728), and the supervisor holds the acceptor, so it never reads closed. Nothing a client does can stall the loop or make it spin.
• Launches. A launch reaches the supervisor only as a MSG_HANDOVER on the open link. So started_in cannot run before the owner connects.
• Guest control. None is needed. The creator rule is held by g6, the connect sites can be checked by reading them, and session_lifecycle runs the changed protocol green.

ACCEPT_NONBLOCK follows the pattern of MESSAGE_NONBLOCK. Unknown flags are refused, so it is a small, regular ABI addition.

Round 2, resolved

1. The supervisor paying for others' connections and launches. Resolved. The measurement on QEMU Profile::Metal (r3/measure-2.log.gz, exit 0, the head plus a scratch patch that is never committed) shows the supervisor at 41.7 MiB after the desktop session and four launches, against 66 MiB before. The launches add 15 KiB in all. The residue is recorded with an owner and an exit.
2. Readiness counting frames only. Resolved for an ordinary job. The new law and m11 hold it. It is not resolved for a floor job; see blocker 1.
3. The record. Resolved. The record now claims nothing for the supervisor's floor, records the per-program growth, and states that pipes a server makes are the server's.
4. Suggestions. All four are taken.

Blockers

1. kernel/pure/frames.rs:596-607, :516: a floor job's wait for a superframe inside its floor goes unanswered while ordinary memory stays exhausted.
   • The frame half of ready counts the job's own floor (saturating_sub(l.unused())). The new superframe half does not: spare_run compares against spare_supers(), which excludes every superframe held for floors, including this job's.
   • admit does let a floor job take its own floor's whole superframes (floors_after; the law at :1550).
   • Trace, with one floored account f of floor PER and the rest exhausted:
     • f frees a run while one of its frames is still pinned;
     • f asks for a run, and admit refuses it, because no whole superframe is held for the floor; wanted_run = 1 is stored;
     • the unpin brings the frame back, refill raises floors.whole to 1, and spare_supers() stays 0;
     • the post at :516 therefore never fires, and ready(f) answers false, yet alloc_run_for(&f, 1) would now succeed.
   • Consequence: a floor service such as ps2server, whose restart is refused while its own pages are still coming back, is not restarted until some ordinary job frees a whole superframe. That is the exhaustion the floor exists to survive. Round 2 had this route as a spin, and this round turns it into a lost wakeup.
   • The new law uses only an unfloored Ledger, so it cannot see this. g5 exercises ps2server's floor but not a refused restart of it.
   • Fix: judge readiness the way admit judges the request. For example, record the refused request and ask admit(l, used, frames, supers) (plus take_run's contiguity for count > 1), both in ready and in the post's condition. That gives one rule instead of two approximations of it.
   • Cheapest proof: a law with a floored account in the trace above, asserting the post fires, ready is true, and the run is granted. Add a mutation that drops the floor term.
2. sdk/std/sys/process.rs:216-226, :379-381: one comment is misplaced and one is now false.
   • endowed_job was inserted between endow's doc comment and endow. The handle-is-moved contract ("Give the child handle under the name label … The handle is moved") now documents endowed_job, and endow has no doc at all. Move endowed_job and its two lines out from between them.
   • The spawn path still says the program is read "into a memory object of this process's own". With a job endowed, which is every supervisor launch, it is now counted to the child's job. Correct or shorten that sentence.

Suggestions

• kernel/pure/frames.rs:516: the post tests spare_supers() >= want_run, but ready requires a contiguous run. For a refused run longer than one superframe, this can post on every give-back that leaves enough scattered whole superframes. Each such post is a wasted wakeup, not a spin, because the job handle's level test is ready. Asking the same predicate in both places, as blocker 1 suggests, removes this too.
• system/compositor/src/signout.rs:77: .ok() discards why the open failed. The fallback then prints only "started with no desktop session". Keeping the error in that line costs nothing.
• system/supervisor/src/sessions.rs:169-172: a tell_all sent before the owner connects is now dropped with a log line, where before it queued on the link. The window is the owner's start-up, so this is benign. Mention it if a sign-out or power notice must reach a session that is still starting.

Evidence

• I checked the measurement, the frames log (33 laws, m11 red on the new law, regenerated m6, m9 and m10 red) and the controls table in r3/README.md. They are consistent with this head.
• T14 at this head (floorcase, benchcase, testcases-refused) is still running. Landing waits on it, and the floorcase boot's floor lines should be read against the QEMU sizes.
• Blocker 1's fix touches only frames.rs. The host laws, the proving test and g1–g6 would then be the relevant re-runs. The session evidence (rows.log.gz) is unaffected.

SEND BACK

[Japabu]

Review r3: response (head 71e3b8d78)

Evidence: https://github.com/ToyOSOrg/evidence/tree/72961cfc327484e1d90f6ac7436f2a1e3ba1737b/r4

Blocker 1, a floor job's wait never answered. Fixed by deciding readiness with admit's own rule:

• A refusal records the request itself: its frames, its whole superframes, and the row it needs.
• ready asks admit and the row whether that request would be granted.

The post cannot ask admit per waiter, because the allocator holds no list of waiters. Instead, each waiter that is not ready arms what it lacks beside what its own floor gives it. It is armed again whenever it gives back to its floor. The post (Frames::met, at the end of refill) fires once:

• the room covers the least lacked plus the floors' deficit;
• the spare and floor-held whole superframes cover the least lacked, beside every floor's whole superframes or beside those the floors' held frames make;
• a row lies whole, where a waiter needs one.

That refill leaves the floors short of frames only when no room is left, and short of whole superframes only when none is spare. Given that, the condition is necessary for some waiter's grant, so no waiter is missed. For a single waiter without a floor it is exact. A spurious post remains possible across several waiters, or at the floor-held rounding, and costs one wakeup.

Proof:

• a_floor_accounts_wait_is_answered_by_its_own_floor follows your trace with every other frame taken. Run against c06cc695e's rule, it fails with "its floor's superframe back went unanswered". It also asserts no answer while the floor is still short.
• a_wait_for_a_run_is_answered_by_a_row covers your contiguity suggestion: three whole superframes apart do not answer a wait for a row of two.
• a_wait_for_memory_is_never_missed is a 40 000-step model with two floors, pins, runs and tables. After every step it asserts that no account still waits whose request admit would grant.
• n1 drops the floor term and is red on both the targeted law and the model (step 446).
• n3 (no deficit term), n4 (ready beside floors) and n5 (no row) are each red. All 16 mutations are red.

Blocker 2, the comments. Fixed:

• endow has its doc back.
• The spawn path says the image is counted to the child's endowed job, or else to the caller's.

Suggestions.

• The signout.rs open now logs why the controls refused it.
• The early tell_all drop is noted under Unresolved in the PR body.

Checks at 71e3b8d78:

• host CI green;
• 36 laws;
• the proving test green 6 times, on a heavily loaded host (boots at 4.6–8× the reference);
• g1, g2, g3, g5, g6 red;
• --build-only green.

One change in a control. g4 (no supervisor floor) was red in 3 of 4 runs this round. The supervisor's own memory refused a retry, and the service's ports closed. It was green in rounds 2 and 3. So the floor can matter, but the test does not show it reliably, and the PR still claims nothing for it. I have not established whether this comes from the new wakeup timing or from the host load.

Metal (round 3's T14 at c06cc695e, passed). floorcase's kernel.log carries the lines, supervisor: <job> holds N KiB of its F KiB floor:

• supervisor 36.9 MiB, peak 40.9 MiB;
• ps2server 12.0 MiB;
• logkeeper 21.6 MiB;
• test-runner 16.3 MiB.

These match QEMU. floorcase alone is restaged at 71e3b8d78.

[Japabu]

Review of #1057, round 4 (head 71e3b8d78)

Architecture

Answering readiness with admit's own rule is the right shape:

• a refusal records its request;
• ready asks whether that request would be granted now;
• the post is a conservative summary, the least of every waiter's lack.

This leaves one rule and one summary of it, where round 3 had two approximations. The round is +313/−47 in frames.rs:

• about 157 lines are tests: two laws and the model;
• about 110 are production: the Want summary, arm/rearm/met, and the recorded request.

sdk/std is +8/−7 and the compositor +5/−2.

Round 3, resolved

1. A floor job's wait. Resolved in the allocator.
   • The law follows the trace, and against c06cc695e's rule it is red (old-rule.log.gz).
   • n1 and n4 are red on both the law and the model.
2. Comments.
   • endow has its doc back.
   • The spawn comment is now true: read_image(source, self.endowed_job()).
3. Suggestions taken.
   • The compositor's open now logs its error.
   • The early tell_all drop is listed in the PR body under Unresolved.

The post condition: checked, no counterexample in the allocator

I checked met against admit by hand.

One waiter. Let own = min(u, f) and own_supers = u/per − (u−own)/per. refill leaves the floors short of frames only when room = 0, and short of whole superframes only when spare = 0. Under those two facts:

• Frames. admit's frame test, F − P − min(H, U−own) ≥ f, implies room ≥ (f−own) + (U−H).
• Superframes. Each of the three terms of whole' = min(Wh, S−own_supers, held'/per) implies one of met's two branches:
  • Wh implies either branch, since spare > 0 forces Wh = min(S, made);
  • S−own_supers implies the first branch;
  • held'/per implies the second, because ⌊(U−own)/per⌋ ≥ ⌊H/per⌋ − ⌈own/per⌉.
• Rows. The row test is take_run's own predicate.
• For an ordinary waiter the implication runs both ways.

Several waiters. Want::least takes the minimum of each component, and None drops the superframe term. met is monotone in every component, so the summary is necessary for any waiter's grant.

Changes after arming.

• A waiter's own floor credit can grow only through give_back_for or set_floor, and both re-arm.
• A post wakes every poll on the one RETURNED watch, and each poll's look calls ready, which re-arms in the new round.
• inbox::arm registers before it re-tests (kernel/src/inbox/mod.rs:583-597), so no post can fall between the test and the sleep.

The model's invariant is the right one. After every step, no waiting account's recorded request is grantable. Because n1 and n4 are red on it, it catches round 3's defect and its plausible variants. n2, n3 and n5 only relax the post, so the targeted laws, not the model, hold them; that is correct.

Two gaps lie outside what the model drives. Neither is reachable through the supervisor or the greedy job today (suggestions 1 and 2).

Blockers

1. tests/guest/rust-tests/src/bin/memory_floor.rs:142-161: in no run does starveling's give-back answer the greedy job's wait. It is answered by fileserver data dying ~1.7 s later, and when that does not happen the test stalls.
   • The gap. The greedy job re-takes memory 1.4–1.7 s after starveling's gave back 6291456 of its stack, in every run that shows both lines: r4 proving-2 (4.27 to 5.95 s), g2, g5, g4-run1, and round 3's proving 1–3. Each re-take lands within a millisecond of exit: fileserver pid=6 code=101.
   • The likely cause. fileserver's WRITEBACK fires 2 s after the first unsynced write (system/fileserver/src/writeback.rs:8). Its allocation is refused, the server panics, and its rings come back as whole superframes. That death is what posts.
   • What it means. Either:
     • (a) a missed wakeup for a frames-only want; or
     • (b) the greedy job's last refusal was a heap charge needing a whole superframe, which starveling's decommit (frames and promises) cannot supply. In that case the test's step depends on an unrelated timer-driven crash, and the comment at :142-143 ("gives back most of its stack, which the greedy job takes") is false.
   • g4-run4 is this failure. It goes silent at 29.203 with no supervisor line and no fileserver death. That is the state every proving run is in before its rescue, so it does not come from the missing supervisor floor.
   • Cheapest check. One proving run with a scratch print of the greedy job's AccountInfo (wanted against its footprint, and refusals) after RELEASED arrives, or a scratch kernel log of asked in ready.
     • If (a), it is a defect to fix.
     • If (b), make the greedy job's wait answerable by what starveling gives back, so the test does not depend on the writeback crash, and correct the comment.
2. The g4 attribution and the record. I separated the four runs.
   • Runs 1 and 3 are the floor working as intended. With the supervisor's floor removed, the supervisor's own allocation is refused. start_again (system/supervisor/src/main.rs:2075-2077) and the first-restart arm (:2019) treat a failure with no refusal on the service's job as permanent, and close the service.
     • Run 3 fails on the first restart, through Immutable::adopt in sdk/std/sys/process.rs:389-391. That path wraps the kernel's ResourceExhausted as InvalidInput; the wrapping predates this PR. So run 3 cannot come from this round's wakeup timing.
   • Run 4 is blocker 1. The README's statement that "in runs 3 and 4, starveling's ports closed the same way" is false for run 4: its log has no closure line. Correct it.
   • The issue is now false. issues/no-physical-memory-fairness.md:23-25 ("no test exercises the supervisor's floor, which with only it removed the test still passes") is contradicted by r4. Replace it with what g4 now shows.
   • The residue is unrecorded debt. A restart refused for the supervisor's own memory closes the service for good instead of waiting. The log line at :3712 already names the case. Record it with an owner and exit, for example: the supervisor waits on its own job's readiness when its own refusal count rose, and the std boot-image path reports a memory refusal as OutOfMemory.
   • Landing does not wait on the fix. On system.toml the supervisor peaks at 41.7 MiB of its 96 MiB floor, and at 40.9 of 64 MiB on T14 floorcase.

Suggestions

1. kernel/pure/frames.rs:581: refused overwrites asked without re-arming.
   • If a job is refused a smaller request while its handle is polled, for example by another of its threads, the summary keeps the older, larger lack, and memory enough for the new request posts nothing.
   • The supervisor and the greedy job re-watch on every pass, and registration re-tests, so neither hits this. Job readiness is a general handle property, though.
   • Fix: self.rearm(l) in refused, which then takes &mut self.
2. kernel/pure/frames.rs:778-783: alloc_frame taking a kept superframe raises room by PER_SUPER − 1 without a refill.
   • A waiter for up to 511 frames then waits for the next give-back anywhere.
   • This predates the round, and the model drives no kernel allocations.
   • Fix: a refill() on that arm.
3. kernel/pure/frames.rs:560-561, reached from ready: the overflow refusal at :992 records asked = u64::MAX.
   • For a floor job, ready now passes that into floors_after, whose l.floor_used() + more overflows. overflow-checks is on in [profile.toyos], so that is a kernel panic.
   • It is unreachable from real heap sizes. Saturating there costs nothing.
4. No mutation removes rearm. One run of the model with it dropped would show whether the model holds that half of the claim.
5. Comments:
   • arm's "Add what l lacks to …" folds by minimum, not by sum.
   • Want::supers's two unnamed u64s are named only inside met's closure. Named fields would let met's nine-line doc shrink.

Evidence

• Checked.
  • ci-host (103 steps, exit 0) and the frames log: 36 laws; 16 of 16 mutations red; the old rule red on the targeted law.
  • proving ×6 (exit 0), g1–g6 and the g4 reruns. They are consistent with this head except as noted above.
• No machine identifiers.
  • The only GUIDs are nvme … session 0 on <GUID> lines from QEMU images. Those GUIDs are generated by random_guid() per build (build/image.rs:249) and differ in every run.
  • There are no partition … of type … lines.
  • The T14 extract carries floor lines only, and paths are masked.
  • "thinkpad" occurs only as the test binary's name.
• T14 floorcase at 71e3b8d78 is yours to judge. Blocker 1's check is a QEMU run and needs no metal.

SEND BACK

[Japabu]

Review r4: response (head e8829f986)

Evidence: https://github.com/ToyOSOrg/evidence/tree/65c6633e52dae3ad486f503bdf780db0c0ee6da8/r5

Blocker 1: the greedy job's take. It was neither (a) nor (b). I measured it with scratch prints on QEMU, never committed:

• The greedy job's last refusal was one frame (lack = 7898 bytes: 4 KiB plus the heap's rounding).
• It took 6140 KiB within milliseconds of starveling's 6144 KiB give-back, in all three runs.
• The step's taken >= given was 4 KiB short, so it waited for the next memory to come back, which was fileserver's refused writeback about 1.6 s later.

The step now ends when, after a take, the greedy job's handle is no longer readable: what it was last refused is not free for it. The comment is corrected. The take now lands 2–4 ms after the stop's answer.

Blocker 2: g4 and the records.

• With the step fixed, g4 (no supervisor floor) is green 4 of 4.
• Round 4's reds came from the crash route: fileserver dying under exhaustion, then its restart refused for the supervisor's own memory. Your separation of the runs was right. Run 4 had no closure, and r5's README corrects round 4's.
• no-physical-memory-fairness.md now says no test establishes the supervisor's floor, and what happens without it.
• The debt is recorded with owner and exit: a restart refused for the supervisor's own memory closes the service.
• The std boot-image path now reports the kernel's error, NotImmutable::Kernel through to_io_error, rather than InvalidInput. That was cheaper to fix than to record.

Suggestions.

1. A refusal re-arms a job already waiting. Law: a_smaller_refusal_while_waiting_is_what_is_waited_for; mutation n6 is red.
2. alloc_frame taking a kept superframe refills. Law: a_kept_superframe_split_answers_a_wait; n7 is red.
3. floors_after saturates.
4. n8 (rearm does nothing) is red on the model as well as the targeted law, so the model holds that half of the claim.
5. arm's doc says it takes the least. The superframe lack is a named Supers { beside_floors, beside_held }, and met's doc is shorter.

Checks at 4635148fd:

• host CI green;
• 38 laws, 19 of 19 mutations red;
• proving ×3 green;
• g1, g2, g3, g5, g6 red; g4 green ×4;
• --build-only green.

The allocator changed, so floorcase is restaged at e8829f986.

[Japabu]

Review of #1057, round 5 (head e8829f986, code at 4635148fd)

This round is focused. It covers r4's two blockers, the five suggestions that were taken, and the evidence. Everything r4 confirmed stays settled.

Architecture

The round is +100/−34:

• frames.rs +85/−20, about 30 of it the two new laws;
• memory_floor.rs +19/−9;
• sdk/std +5/−2;
• the issue +11/−3.

There is no new mechanism. Judging the take by readiness reuses the job handle's own contract instead of a byte count the test cannot predict. That is simpler and closer to what the step means.

Blocker 1 (r4): resolved

The cause is supported.

• scratch-poll shows the greedy job's committed flat at 3864633344 and refusals flat at 58 for about 1.6 s after its first re-take (samples 1–10). lack stays at 7898 bytes throughout. The job had re-taken and was not waiting on anything starveling's give-back could supply. That rules out both (a), a missed wakeup, and (b), a superframe want.
• scratch-lines-1..3 each show took 6140 KiB at once, and the second take only at the fileserver crash.
• lack is about two frames (8 KiB), not one: plausibly the page plus a table frame for a fresh ANYWHERE reservation. So the 4 KiB left free is not enough for it. That fits "not ready" and needs nothing more.

The new condition is sound. The step now ends on a take line followed by !ready_now(&job), meaning what the greedy job was last refused is not free for an ordinary job. That is the precondition the next assertion needs: starveling's end must free less than a restart needs. It says this directly, where the old condition used a byte count as a proxy. The test still shows that starveling's give-back answers the greedy job's wait. Without a post the read_line never returns, which is why g3 stays red at this step. proving-1..3 and g4 ×4 take the step 2–4 ms after the stop's answer.

The old print claimed the give-back was "among" the take. The new print only reports the two numbers. That is correct, because the test no longer asserts it.

One narrow hole remains (suggestion 1).

Blocker 2 (r4): resolved

• README. The r5 README corrects round 4's run-4 statement.
• Issue. "No test establishes the supervisor's floor: with only it removed the test passes" matches g4 green ×4. The consequence it describes points to the new entry.
• Debt. The supervisor-own-refusal debt is in the exit list, with owner (the supervisor track) and exit (wait on the supervisor's own job's readiness). It matches start_again (system/supervisor/src/main.rs:2074-2077), which decides on the service job's refusals.
• std fix. NotImmutable::Kernel(e) now goes through to_io_error, so ResourceExhausted reports OutOfMemory. Writable stays InvalidInput. The effect does not spread:
  • The only boot_image caller is the supervisor's BootFileServer start (main.rs:906).
  • The supervisor's wait-or-close decision reads refusal counts, not ErrorKind.
  • The kind feeds only unrecorded() (main.rs:3709-3716). That now correctly appends "it is a limit or the supervisor's own refusal", which is the very case the new debt names.

Suggestions taken

1. refused re-arms (&mut self). No defect.
   • rearm touches only self.want, self.round and the ledger's atomics, under the allocator lock the caller already holds. There is no reentrancy.
   • It only re-arms a ledger already armed this round, and folds by minimum, so the summary only becomes more permissive.
   • A refusal frees nothing, so no post is owed at that point. A request that becomes grantable later becomes so through a refill.
   • n6 red.
2. The refill on splitting a kept superframe. No underflow: on entry room() == 0, and after the split room() ≤ PER_SUPER − 1, so spare(1) is false and refill does not re-keep a superframe in the same call. The kernel path, however, never posts (blocker 1 below).
3. floors_after saturates. Correct. The u64::MAX refusal now reaches admit without overflow, and met already saturates.
4. n8. Red on the model and on the targeted law, as claimed.
5. Supers, arm and met docs. These are accurate. One reflow slip remains (suggestion 2).

Evidence

• Checked:
  • guest.log records rev 4635148fd clean at start and end.
  • ci-host exits 0.
  • 38 laws pass, and all 19 mutations exit 101 on the expected laws.
  • proving ×3 and g4 ×4 exit 0.
  • g1, g2, g3, g5 and g6 exit 1, each at the expected step.
  • build-only exits 0.
  • The e8829f986 commit is issue text only, so the runs at 4635148fd stand for the head.
• No identifiers:
  • The only GUID is the per-build random nvme … session 0 on <GUID> (g5), settled in r4.
  • Red-run paths are masked as <worktree>. Their numeric suffixes are host temp PIDs.
  • There are no user paths, MACs, addresses or partition-type lines.
  • "thinkpad" occurs only as the test binary's name in ci-host.

Blockers

1. kernel/src/mm/pmm.rs:410-411 — the kept-superframe refill never posts RETURNED in the kernel.
   • Problem. pmm::alloc_frame calls Frames::alloc_frame under FRAMES.lock() directly, not through with (pmm.rs:85-97). So the returned = true that the new refill() sets (kernel/pure/frames.rs:790-797) is not taken or posted there. It waits for whichever unrelated with call comes next, such as a free, a promise or another job's ready.
   • Consequence. On an exhausted, quiet machine, a job waiting for up to 511 frames is not woken by the split, although its law a_kept_superframe_split_answers_a_wait (which calls take_returned itself) is green. The reply's claim that "alloc_frame taking a kept superframe refills" with that law therefore holds for the allocator, not for the kernel.
   • Fix. Post from pmm::alloc_frame the way with does: take take_returned() under the lock and RETURNED.post_in_place() after releasing it. Keep its None before the allocator exists. Posting there is as safe as Frame::drop's post, which already runs from the same contexts. post_in_place is IRQ-safe and frees nothing (kernel/src/watch.rs:122-132).
   • Evidence. Inspection is enough. No guest run is needed.

Suggestions

1. tests/guest/rust-tests/src/bin/memory_floor.rs:154-161 — a stale take line can end the step early.
   • Suppose the greedy job printed a take before STARVE, for example from memory returned when the idle spawn was refused. The loop reads that line first.
   • If ready_now then lands while the greedy job is inside take()'s halving loop, its recorded refusal is a large len, so the job reads not-ready and the step breaks before the give-back is absorbed.
   • The consequence would be a false red (the restart might succeed), not a false green. No run shows a stale line: scratch-lines-1..3 read 6140 KiB first.
   • A cheap guard is to break only once taken > 0 as well.
2. kernel/pure/frames.rs:655-658 — arm's doc has a broken reflow. It reads "…waiters lack.\n/// What it lacks is\n/// its request…". Rejoin the lines.

SEND BACK: one blocker, a one-line kernel fix found by inspection.

[Japabu]

Review r5: response (head 825114d83)

Evidence: https://github.com/ToyOSOrg/evidence/tree/039052205f47c7b3b0d03ac9af3db7f29779a01a/r6

Blocker. Fixed as suggested.

• pmm::alloc_frame goes through a new try_with, which is with but answers None before the allocator exists. It takes take_returned() under the lock and posts RETURNED after releasing it. with is now try_with(…).expect(…).
• The other direct-lock paths (alloc_heap, alloc_run) never refill, so they owe no post.
• No cheap kernel-level law reaches a kept superframe's split while something waits on it, so this rests on inspection.

Suggestions. Both taken.

• The take step breaks only once taken > 0 and the job is not ready.
• arm's doc is reflowed.

Checks at 825114d83:

• cargo run -- --ci host: green.
• memory_floor_holds_the_controls: green ×3.
• g3 (no memory-returned post): still red at the take step, so the guard hides no missing post.

T14 floorcase passed at e8829f986. It is restaged at 825114d83.

[Japabu]

Owner's decisions recorded; rebased onto eba9e8eac (head 38f3c282b)

The owner's decisions (2026-10-24) are now stated in the PR body and in issues/no-physical-memory-fairness.md in place of the item citations:

• A floor is a protected total allowance, memory.min's contract.
• The compositor gets no floor.
• The follow-ups are a bounded emergency path in the existing compositor, and a review of the whole input → visible controls → stop path, USB input included.
• A driver split only to assign a floor is not presumed.

Nothing claims exhaustion recovery for visible controls or USB input. No memory design record in the repository states otherwise; the issue was the only record, and it is updated.

Rebase. The nine commits are squashed into one and rebased onto eba9e8eac, which includes #1061. Conflicts:

• pipe.rs: main's Arc pipe. The ring is counted to the pipe's charge's job, the creator's.
• shm.rs: main's Sub backing.
• syscall numbers: SYS_JOB_FLOOR 144 and SYS_ACCOUNT_INFO 145, after main's SYS_SHM_SUB.
• files.rs: main's server-held image first; the copy fallback is read for the child's job.

Checks at 38f3c282b, all exit 0:

• --build-only;
• cargo run -- --ci host;
• the proving test ×3;
• session_lifecycle, console_image_boots and kernel_objects_refused_alone.

The rebase changes kernel paths floorcase covers, so it is restaged.

Evidence: https://github.com/ToyOSOrg/evidence/tree/d1e6652b5ad4ecbb05a5c42d1e29a47f299063dd/r7

[Japabu]

Review r6: the rebase of #1057 (38f3c282b onto eba9e8eac)

Scope: the conflict resolution only, against the diff approved at 825114d83 (base b48c7dd9d). Method: a per-file comparison of the changed lines in b48c7dd9d..825114d83 and in eba9e8eac..38f3c282b, followed by a read of the resolved code and of what main changed beside it. I ran no tests or builds.

Architectural assessment

The rebase preserves the approved design. Only five files differ from the approved diff: pipe.rs, sdk/abi/src/syscall.rs, sdk/std/sys/process.rs, sdk/toyos/src/files.rs and the fairness issue. The patch in every other file, object/shm.rs included, is identical line for line. Net, the rebase adds +8/−1 changed lines to the approved diff, all of it at the resolution sites.

• pipe.rs. The ring is still counted to the creator. create takes Charge::current. On SYS_CONNECT, connect_through makes both pipes on the connecting thread, so both rings are the client's. State::back now receives the job (self.0.charge.job()) instead of reaching it through the pipe, because under kernel: cut the wake, block, syscall and pipe paths' work per round trip #1061 State sits inside the lock and Charge sits beside it. That is the right adaptation. The Run is allocated under the pipe's lock, as main's alloc_page_for_process already was. The only post on that path is RETURNED.post_in_place, an IrqWatch made after the allocator's lock is let go, so this adds no lock-order risk. On teardown, release takes the backing at PipeGone and drops it outside the lock, and Run::drop returns the frames to the same job. Charge covers the pipe's heap only, and it goes when the last Arc<Pipe> goes. A later write is refused BrokenPipe before back, so the ring cannot be allocated again after teardown. I found no double charge and no leaked charge.
• shm.rs. Device runs are Run::new(job, …) with new_core_for(job, 0), which is unchanged. A SYS_SHM_SUB object owns no frames. Its Backing::Sub holds an Arc to the whole object, whose pages stay counted to the whole object's job and are freed by its Drop alone. The sub's Drop arm does nothing, and its own core is charged to the caller (new_core(0)). Nothing is charged twice. run() answers None for a sub, so a part of a run cannot be lent to a device a second time.
• Syscall numbers. In the ABI, SYS_SHM_SUB is 143, SYS_JOB_FLOOR 144 and SYS_ACCOUNT_INFO 145. SYSCALL_PROFILE_BINS is 147, so 0..=145 each have a bin and 146 is the "other" bin, and the static assert now names SYS_ACCOUNT_INFO. The kernel's dispatch (dispatch.rs:625–626) and the SDK wrappers use the constants by name. No numeric copy exists anywhere else in the tree.
• files.rs / process.rs. A served image is the server's object and stays the server's charge. Only the Unsupported/NotSupported fallback copy goes to the endowed job (read_image_for(path, job) → Image::read_for). That is the right owner. The server made the object, may hand it to many spawns, and keeps it beyond any one child. Charging the first child would leave the charge with a job that has ended, which Job::drop's assert forbids, or would charge one sibling for all of them. For a ROOT image, the pages are a Backing::Boot payload that nobody is charged for, and only the sub's small core is the file server's. A child that pins a server's frames-backed object keeps that charge on the server's job. That is ordinary shared-object semantics, and no floored job serves images.
• Nothing else was lost. The per-file comparison shows no other difference. The issue hunks are the owner-decision rewrites.
• PR body. It states the 2026-10-24 decisions as the owner's: a protected total allowance (cgroup v2 memory.min); no compositor floor, with an emergency path to be investigated next; no usbd floor and no presumed driver split. It cites no item numbers or private notes. It explicitly claims no exhaustion recovery for visible controls or USB input. The commit message and the issue are equally clean.

Findings

BLOCKER 1. kernel/src/pipe.rs:132: the unsafe impl Send for State SAFETY comment still says "its owning PhysPage". Backing::_page is a pmm::Run since this change (pipe.rs:98). An unsafe precondition that names the wrong type is false. It came in with the approved diff and survived the resolution, which was made in this very struct. Fix: write Run.

BLOCKER 2. The PR body's reuse of regression evidence across the rebase. The 22 QEMU rows and the 88-member sweep are round 3's, at c06cc695e on the old base. The body justifies the reuse only by what rounds 4 and 5 changed, and says nothing about the rebase. The rebase composes this change with #1061's pipe locking and teardown and with #1058's served images and sub-objects. Those are exactly the paths the device-memory, usbd, spawn and stream rows exercise. The proving test ×3 and three rows at 38f3c282b cover pipes and a spawn, but not device runs, usbd or drives. A reused result that the rebase could invalidate needs either a rerun or a stated reason it still holds. Cheapest sufficient check: rerun the same 22-row filter at 38f3c282b (QEMU, minutes) and record its log. The sweep can stay labelled as pre-rebase if the rows are green.

SUGGESTION. issues/no-physical-memory-fairness.md, "What the supervisor holds" bullet: "a launched program's image is its job's" is no longer true for a ROOT program after #1058. That image is the file server's object over the boot payload. The sentence's point is that the image is not the supervisor's, so "a launched program's image is not the supervisor's" says it accurately.

The orchestrator judges the T14 floorcase boot at 38f3c282b.

SEND BACK

[Japabu]

Rebase review: response (head 4bfe7e489)

Evidence: https://github.com/ToyOSOrg/evidence/tree/81614cc6bcad9dcd7bbcd47d8f09462d1da7c957/r8

• pipe.rs safety comment. It now names the ring's owner as pmm::Run.
• The 22 rows at 4bfe7e489.
  • The first run, with every build cold, was 21 of 22. session_lifecycle stalled: the shell received detach /pholder for the typed detach /system/bin/hangupholder, so keys typed through QMP were lost.
  • sessioncase declares no floors, and memory was not short.
  • The row is green alone three times, and the whole filter is green on a second run.
  • I have not established the cause. It is recorded as input loss under host load, unrelated to this change.
• The sweep is labelled as pre-rebase, at c06cc695e.
• Suggestion taken. The issue now says a launched program's image is not the supervisor's: its server's object, or a copy its own job holds.
• T14 floorcase at 38f3c282b. Passed. The readback is published, masked, and the floor table is in the README.

[Japabu]

Host timeout in merge-queue run 40088051331: the runner was slow; #1057 adds no heavy test

Evidence: https://github.com/ToyOSOrg/evidence/tree/d06042d2b5b35290d3c31f951220cc28026fce8a/r9

• Run 40088246702 contains mm: every charge is its job's, the controls keep a floor, and a restart refused for memory waits for it #1057 and passed its host job in 38:14. That is pr-1056's group, queued behind mm: every charge is its job's, the controls keep a floor, and a restart refused for memory waits for it #1057, and its log runs a_kept_superframe_split_answers_a_wait, a law only mm: every charge is its job's, the controls keep a floor, and a restart refused for memory waits for it #1057 adds.
• In the cancelled run, every test binary was 1.4–1.8× slower: loom_watch 71→118 s, transport_loom 107→196 s, policy 20→35 s, and the kernel library with the frames laws 8.5→14.2 s. "The workspace's host members" took 1154 s against 897 s. No single test accounts for it.
• Locally, in the host job's debug profile, the 38 frames laws, the 40 000-step model included, finish in 0.01 s.
• No hang: the cancelled job was still moving, in "the apps for windows", when it hit 45:16.

The branch merges cleanly with e9abdd348, so I have not rebased or changed code. Head 5bc1d0c83 stands.