A served file is mapped read-only and shared, and a fault on its absent page waits for its pager

Cargo.toml

@@ -171,6 +171,7 @@ members = [
     "tests/guest/osbench/compare",
     "tests/guest/osbench/lan",
     "tests/guest/osbench/rules",
+    "tests/guest/mapprobe",
     "tests/guest/pagerprobe",
     "tests/guest/pciholder",
     "tests/guest/starveling",

build/ci.rs

@@ -587,6 +587,9 @@ pub(crate) const CONTROLS: &[Control] = &[
     red(KERNEL_LOOM, "tlb-tags-resume-relaxed", Some("tlb_tags"), &[
         Fails("a_change_passing_an_idle_holder_by_is_flushed_when_its_thread_resumes"),
     ]),
+    red(KERNEL_LOOM, "ranges-less-relaxed", Some("paged_ranges"), &[
+        Fails("the_last_to_let_go_sees_every_leaf_cleared"),
+    ]),
     red(KERNEL_LOOM, "shootdown-served-relaxed", Some("counters_round"), &[
         Fails("a_cpu_read_as_answered_is_read_with_its_answer"),
     ]),

build/sourcegate.rs

@@ -137,7 +137,7 @@ const AUTO_TRAIT_IMPLS: &[(&str, usize)] = &[
     ("kernel/src/drivers/panic_console/mod.rs", 3),
     ("kernel/src/arch/x86_64/hw.rs", 1),
     ("kernel/src/mm/mmio.rs", 2),
-    ("kernel/src/object/paged.rs", 1),
+    ("kernel/src/object/paged.rs", 3),
     ("kernel/src/sched/driver.rs", 2),
 ];
 

docs/src/architecture/files.md

@@ -80,5 +80,11 @@ directory, which the child resolves in its own view.
   that server's open files, which then answer that they are gone; a fresh open
   reaches the restarted server. Unsaved changes may be lost; data already
   confirmed durable stays durable.
+- A file server's end revokes every mapping of its files, so a program
+  executing from, or reading a mapping of, that server's files ends at its
+  next access to that mapping, a system service mapping a data file included.
+  A file server's death is the loss of that file system: its parent restarts
+  it, and programs that depended on it fail clearly rather than run on with
+  stale memory.
 - Per-session temporary storage is an ordinary file server holding its
   contents in RAM.

docs/src/architecture/memory.md

@@ -68,6 +68,22 @@
   does keeps the server's writes waiting.
 - Mapped files may be larger than RAM, partially mapped, and coherently shared
   and written; their length is never committed in RAM.
+- A file mapping maps the cache's own pages, so a mapper sees a write as it
+  lands, and a private mapping shares them until it is written. A mapping
+  holds its file as an open handle does: a file mapped and then closed or
+  deleted stays until its last mapping goes. A page leaves the cache only once
+  no mapping reaches it.
+- A wait for a file's page behaves like one for swapped memory: it advances
+  with its file server's progress, is reported when overdue and never becomes
+  an error by timeout. The server failing what it cannot read, and its device
+  waits' own timeouts, bound it.
+- A touch of a mapped page its file server failed, or of a file whose server
+  ended, ends the program with a diagnostic naming the file's page and the
+  cause; a copying system call answers an I/O error instead. A touch of a
+  mapped page wholly past the file's end ends the program the same way, as
+  POSIX's `SIGBUS`, and a copy from one is refused as a bad address. A touched
+  unwritten page of a file held in RAM becomes resident within its server's
+  capacity and is refused once that is full.
 - Clean pages are reclaimed; dirty pages are written back first, without losing
   concurrent writes. Dirty data growth is bounded, and writeback starts ahead
   of pressure.

docs/src/architecture/services.md

@@ -67,6 +67,10 @@ Every server admits its clients the same way, through one shared mechanism:
 - **Recovery restores durable state, not sessions.** File servers recover what
   was on disk, not old opens; network sessions may fail; the memory service
   keeps recoverable swapped contents.
+- **A file server's end is the loss of its file system.** Every mapping of its
+  files is revoked, so a program executing from or reading a mapping of them,
+  a service included, ends at its next access to that mapping rather than run
+  on with stale memory.
 - **Nothing is silently replayed.** An operation with an uncertain outcome is
   reported, and retried only where safe; a write whose acknowledgement was lost
   is never replayed behind the client's back.

issues/libc-refuses-what-toyos-cannot-yet-answer.md

@@ -17,8 +17,13 @@ These answer failure in their POSIX form and do nothing
   LLVM's `getDefaultStackSize` (`llvm/lib/Support/ProgramStack.cpp`) ignores
   the failure and reads the `rlimit` it did not get.
 - `gethostname`, `ENOSYS`: no host name is published to a process.
-- `msync`, `ENOSYS`: no mapping is of a file, so there is nothing to write back.
-- `mmap` of a file, `ENODEV`: the kernel maps no file.
+- `msync`, `ENOSYS`: no call answers which pages of a range are mapped, which
+  POSIX's `ENOMEM` for an unmapped one needs.
+- `mmap` of a file other than `PROT_READ`, `ENODEV`: the kernel maps a file's
+  pages read-only and shared, and a private one shares them until it is written,
+  which waits for 7b's write faults (step 5); a private copy range of a file
+  (`PROT_WRITE` or `PROT_EXEC` with `MAP_PRIVATE`, 7b's R4) is not built either.
+  A file whose server maps no pages answers `ENODEV` too.
 - `fcntl` (`sdk/libc/src/fdreq.rs`): a record lock, `EINVAL`, POSIX's answer
   for a file that supports no locking; `F_GETFL`, `F_SETFL`, `F_GETOWN` and
   `F_SETOWN`, `ENOSYS`.

issues/one-client-can-fill-the-tmp-servers-memory-and-deny-every-other-client.md

@@ -25,16 +25,17 @@ names the client that took it (`issues/no-physical-memory-fairness.md`).
 
 **What one client leaves charged.** The kernel makes a pager's object slots
 256 at a time and keeps every piece for the pager's life (`kernel/pure/slots.rs`).
-A freed slot is taken again, but its piece never goes back. A slot is 216
-bytes since #1258: a 192-byte entry, of which the object's own state is 112
-and the pager's record 64, and two 12-byte marks, one for each notice it can
-owe. Measured with a host replica of the layouts at #1258's merge of main:
-https://github.com/ToyOSOrg/evidence/blob/af88668ec3bf695893aeabf229b7ac3c1bad4a95/r8/slot-sizes.log
-At #1273 it was 72:
-https://github.com/ToyOSOrg/evidence/tree/f81e4b2ddb7d89a92f82f9eb8da1fdf58587a563/pr-1273/sizes
-So the server's job stays charged 216 bytes for each `/tmp` file of the most
+A freed slot is taken again, but its piece never goes back. A slot is 272
+bytes: a 248-byte entry and two 12-byte marks, one for each notice it can
+owe. Of the entry, the object's own state is 152 bytes, the pager's record 64
+and the list of a mapped object's mappers 16. The walk state mapping needs
+adds 40 bytes to the object, and with the list 56 to a slot. Every entry
+carries all of it. Measured by the compiler for both kernel targets; main
+before mapping, measured the same way on x86-64, has 216:
+https://github.com/ToyOSOrg/evidence/tree/94fd400ddab5d9c2ff776ac9df66f1b0bb88b768/r12/sizes
+So the server's job stays charged 272 bytes for each `/tmp` file of the most
 it held at once, until the server ends. A client that makes and removes a
-million files leaves about 216 MB. The manual has unused backing return under
+million files leaves about 272 MB. The manual has unused backing return under
 pressure; this never returns.
 
 Owner: the file server and the kernel's paged objects, once the owner has

issues/process-memory-in-4-kib-pages-still-copies-each-programs-text.md

@@ -95,10 +95,13 @@ live split of a user leaf.
    at its first touch. A program anywhere else is still read whole into
    memory of the spawner's and copied a page at a time, until 7b's step 3.
    A shared segment's mapping is never widened, so a program can no longer
-   make its own read-only segment writable (`mprotect`). Exit for that: 7b's
-   step 2 converts on protect, so a protect that adds write to such a range
-   commits its pages and makes it a copy range of the same object; only a
-   page shared until its first write waits for step 5's write faults. Exit:
+   make its own read-only segment writable (`mprotect`). Exit for that: a
+   protect that adds write to such a range commits its pages and makes it a
+   copy range of the same object (7b's R4, which step 3 builds, since a
+   program's writable segment mapped from its image is a copy range with a
+   paged source; step 2 maps a paged object read-only only, and its range
+   refuses a protect past that); only a page shared until its first write
+   waits for step 5's write faults. Exit:
    two processes of one binary hold its text once, wherever it is served
    from.
 6. **`/apps` image sharing.** Decided by the orchestrator under the owner's
@@ -118,7 +121,8 @@ live split of a user leaf.
 **7b lands in steps**, each a pull request: (1) a range of a memory object
 mapped where the caller says, an immutable one shared and executable, which
 is stage 5 for `/system`: built; (2) a paged object mapped read-only and
-shared: faults that park on the pager, reverse records, revocation; (3) a
+shared: faults that park on the pager, reverse records, revocation: built,
+but for R4's copy ranges of a paged object, which step 3 builds (item 5); (3) a
 spawn maps its image from any pager-backed volume (stage 6), sealed against
 writes in place while it runs; (4) the
 storage track's attributes and names without a request; (5) writable shared
@@ -136,10 +140,46 @@ mappings and write-back; (6) the #1077 retry
   against main after, four boots a side. Main after must be no slower than
   before; a spawn no longer copies a `/system` program's text, and whether
   that makes it faster is not measured on metal.
+- **Owed on metal:** step 2 (#1269), on the T14 and the AMD bench: the whole
+  `testcases` boot, whose `mapped_file` member maps a paged object from a
+  second process (faults that wait, revocation, refusals, kills) and whose
+  `a_pager_s_end_answers_its_waiting_holders_gone` runs only there and
+  exercises the rewritten pager end, and the `shared-debug` and
+  `proctreecase` boots. Main must show every job of each boot exit 0.
+- **Owed on metal:** step 2 (#1269), on the T14 and the AMD bench: osbench's
+  `system` (its pipe rows), `files`, `ipc`, `procs` and `mem` groups, main
+  before #1269 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 (futex bucket walks,
+  shootdowns, table unlinks) where its drop skipped them.
+- **Owed on metal:** step 2 (#1269), on the T14 and the AMD bench: osbench's
+  `map` group on main beside Linux's `mmap` of the same files, recorded with
+  each row's ratio to Linux's: `touch_16m` and `threads_touch_16m` (a cached
+  file's pages faulted through a mapping, by one thread and by eight),
+  `read_4k` (4 KiB read through one) and `truncate_255` (a file 255
+  processes map, truncated). Their correctness runs in a guest
+  (`osbench_map_group_exits_0`); what they measure is unmeasured until then.
+
+Fault waiters wake on their pager's watch, so a supply, a write's end or a
+removal wakes every fault waiter of that pager and not only those its pages
+meet: a departure from the design's per-request wakes (§3, S4). No row
+prices it, since `threads_touch_16m` faults a RAM file's pages, which are
+never absent. Owner: map7b, with step 3, whose spawns fault a DATA image's
+pages cold. Exit: a many-threads cold-fault row on a DATA file larger than its
+pager's capacity, judged against Linux on metal, and per-request wakes where
+it shows the cost. A cold DATA page's miss in stages is the same kind of row
+and waits with it.
+
+Step 2 measures a cached page's fault and a 4 KiB read through a mapping
+against Linux (osbench `fs.*.map_touch_16m`, `fs.*.map_read_4k`). Owed, by
+map7b, with step 3's metal: a cold DATA page's miss in stages, one object
+mapped by 255 children and withdrawn (a revocation's cost grows with its
+mappers), and many threads cold-faulting one large file; each exits as an
+osbench row judged against Linux.
 
-Until step 2's revocation exists, an object a space maps must keep its frames
-for the object's life: ROOT's pages stay non-reclaimable, and ROOT is not
-served through a pager, until then.
+A memory object a space maps keeps its frames for the object's life, since
+only a pager's pages are revoked: ROOT's pages stay non-reclaimable until ROOT
+is served through a pager.
 
 **Paged objects** (memory design §7, `issues/toyos-builds-itself.md` item 13)
 are split in two. **7a**, delivered by the storage track's file-server work:

kernel/Cargo.toml

@@ -58,6 +58,9 @@ reap-raise-relaxed = []
 # `src/shootdown.rs`'s `serve` reads what it owes `Relaxed`, and
 # `tlb_shootdown` reds.
 shootdown-serve-relaxed = []
+# `src/object/paged/ranges.rs`'s `less` goes `Relaxed`, and `paged_ranges`
+# reds.
+ranges-less-relaxed = []
 # `src/shootdown.rs`'s `served` reads `Relaxed`, and `counters_round` reds.
 shootdown-served-relaxed = []
 # `src/shootdown.rs`'s `Asks::serve` takes its asks `Relaxed`, and

kernel/loom/Cargo.toml

@@ -221,6 +221,17 @@ log-ring-loads-swapped = []
 tlb-tags-enter-relaxed = []
 # The same for `Tags::resume`, which must red the idle holder's model.
 tlb-tags-resume-relaxed = []
+# The negative control for a mapped object's range count. It makes
+# `object/paged/ranges.rs`'s `less` `Relaxed` with no fence, so the last range
+# to let go can unlink its node without seeing another's leaf cleared, and
+# `paged_ranges.rs` must red:
+#
+#   cargo test --manifest-path kernel/loom/Cargo.toml --features ranges-less-relaxed \
+#     --test paged_ranges
+#
+# Never on by default and never reachable from a kernel build, which declares
+# the same name only so `cfg` checking knows it.
+ranges-less-relaxed = []
 
 # The negative control for the panic console's published descriptor. It drops
 # the publisher's `Release` fence between its odd mark and its words, so a

kernel/loom/src/lib.rs

@@ -158,6 +158,11 @@ pub mod shootdown;
 #[path = "../../src/tlb_tags.rs"]
 pub mod tlb_tags;
 
+// A mapped object's count of the ranges holding a space's node: its last
+// letting go sees every other's clearing (`tests/paged_ranges.rs`).
+#[path = "../../src/object/paged/ranges.rs"]
+pub mod paged_ranges;
+
 /// The CPU roster and the release/answer word, driven by `tests/smp_bringup.rs`;
 /// under `loom` alone, as is the [`arch::cpu`] shim it names.
 #[cfg(feature = "loom")]

kernel/loom/tests/paged_ranges.rs

@@ -0,0 +1,66 @@
+//! Loom: a mapped object's node leaves its list only after every range of
+//! the space let go of it, each having cleared its leaves first.
+//!
+//! A space's node of a mapped object is held by each of its ranges of the
+//! object and by a fault parked on one of its pages, which holds no space
+//! lock. Whoever lets go last unlinks the node, and from then on a walk of
+//! the object's mappers does not visit the space: it frees a revoked frame
+//! once its pass is done. So the last to let go must see every other's
+//! clearing of its leaves, or a frame is freed under a leaf that may still
+//! reach it. A leaf here is one cell; `CLEARED` read by the last is the
+//! property, and loom reports a read the clearing does not happen before as a
+//! causality violation.
+//!
+//! ```text
+//! cargo test --manifest-path kernel/loom/Cargo.toml --features ranges-less-relaxed \
+//!   --test paged_ranges
+//! ```
+//!
+//! relaxes the count's letting go, and this file must red.
+
+#![cfg(feature = "loom")]
+
+use kernel_loom::paged_ranges::Ranges;
+use loom::cell::UnsafeCell;
+use loom::sync::Arc;
+
+const MAPPED: u64 = 1;
+const CLEARED: u64 = 0;
+
+/// What the last to let go does before the node leaves the list: the walk
+/// it stops visiting will free whatever this leaf maps.
+fn unlink(leaf: &UnsafeCell<u64>) {
+    // SAFETY: loom checks the access; the model's claim is that it is ordered.
+    let seen = leaf.with(|leaf| unsafe { *leaf });
+    assert_eq!(seen, CLEARED, "the node left its list while a leaf of its space still mapped the page");
+}
+
+/// An unmap in the space clears its leaf and lets its range go; a fault
+/// parked on the range's page lets its hold go as it wakes. Either may be
+/// last.
+#[test]
+fn the_last_to_let_go_sees_every_leaf_cleared() {
+    loom::model(|| {
+        let ranges = Arc::new(Ranges::one());
+        ranges.more();
+        let leaf = Arc::new(UnsafeCell::new(MAPPED));
+
+        let unmap = {
+            let (ranges, leaf) = (ranges.clone(), leaf.clone());
+            loom::thread::spawn(move || {
+                // SAFETY: the space's lock is the unmapper's; loom checks it.
+                leaf.with_mut(|leaf| unsafe { *leaf = CLEARED });
+                if ranges.less() {
+                    unlink(&leaf);
+                }
+            })
+        };
+        let parked = loom::thread::spawn(move || {
+            if ranges.less() {
+                unlink(&leaf);
+            }
+        });
+        unmap.join().unwrap();
+        parked.join().unwrap();
+    });
+}