Skip to content

feat(mem): high-memory writeback proof + differential CI; ADR-0021 Accepted (PR-4) - #216

Merged
NickFlach merged 1 commit into
mainfrom
pr4/adr0021-highmem-differential
Jul 13, 2026
Merged

feat(mem): high-memory writeback proof + differential CI; ADR-0021 Accepted (PR-4)#216
NickFlach merged 1 commit into
mainfrom
pr4/adr0021-highmem-differential

Conversation

@NickFlach

Copy link
Copy Markdown
Collaborator

What

Final increment of ADR-0021 (dynamic PMM sizing) — flips the ADR to Accepted. Adds the load-bearing proof that dynamic sizing is safe above 128 MB, plus the differential CI that proves the sizing is live (tracks -m), not a hardcode.

New boot self-tests (kernel/src/memory.c, wired after PMMCLAMP)

  • pmm_highmem_selftest (PMMHIGH) — on RAM past 128 MB, allocate a top-of-pool frame, assert its physical address is genuinely high (>= 128 MB, < 1 GB), then write two distinct sentinels through the returned identity VA and read them back. A boot.S that mapped only 128 MB — or a wrong/stale map — faults or mismatches here instead of silently handing out an unreachable frame. On -m 128M there is no high frame, so it reports the skip branch (proving the guard ran — not a vacuous always-pass).
  • pmm_residency_storm_selftest (PMMSTORM) — extends the single-shot heap-reservation proof to a bulk drain: 1024 frames pulled with the rover aimed straight at the reserved kernel heap, asserting none land in [__heap_start, __heap_end). Catches a multi-allocation rover regression the single-shot PMMHEAP check could miss.

Differential CI legs

make ci-smoke-mem256 / ci-smoke-mem512 (jobs pmm-differential-256/512, both gating release) boot at 256/512 MB and assert:

  1. the frame count lands in that size's window — ~0xFFE0 / ~0x1FFE0, i.e. it ~doubles / ~quadruples the 128M leg's 0x7FE0; and
  2. PMMHIGH took its live writeback branch.

This is the true hardcode-vs-live differential the -m 128M leg alone cannot show: a 128 MB hardcode prints 0x8000 at every -m and never the live PMMHIGH.

-m PMMSIZE PMMHIGH
128M 0x7FE0 skipped (guard path)
256M 0xFFE0 writeback verified
512M 0x1FFE0 writeback verified

Revert-confirmed (anti-vacuous, two independent teeth)

  • Re-hardcoding memory_init to 128 MB → mem256 sizing window reddens (0x8000 outside [65280,65536]).
  • Broadening the high-memory guard so 256 MB wrongly skips → mem256 PMMHIGH-live check reddens while sizing still passes (the two gates are independent).

Every "un-fakeable gate" named in the ADR-0021 design section is now live.

Verification

  • Build clean under -Werror; clang-format / cppcheck / check-api-consistency.sh green; ci.yml YAML validated.
  • ci-smoke (128M), ci-smoke-mem256, ci-smoke-mem512 all pass locally.

🤖 Generated with Claude Code

…cepted (PR-4)

Completes ADR-0021 (dynamic PMM sizing) and flips it to Accepted. Two new
boot self-tests, wired after PMMCLAMP:

- pmm_highmem_selftest (PMMHIGH): the load-bearing proof that dynamic
  sizing is SAFE above 128 MB. On RAM past 128 MB it allocates a
  top-of-pool frame, asserts the physical address is genuinely high
  (>= 128 MB, < 1 GB), then WRITES two distinct sentinels through the
  returned identity VA and reads them back -- so a boot.S that mapped only
  128 MB (or a wrong/stale map) faults or mismatches here instead of
  silently handing out an unreachable frame. On the -m 128M leg there is
  no high frame, so it reports the SKIP branch (proving the guard ran, so
  the pass is not vacuous).
- pmm_residency_storm_selftest (PMMSTORM): extends the single-shot heap
  reservation proof to a bulk drain -- 1024 frames pulled with the rover
  aimed straight at the reserved kernel heap, asserting none land in
  [__heap_start, __heap_end). Catches a multi-alloc rover regression the
  single-shot PMMHEAP check could miss.

Differential CI legs `make ci-smoke-mem256` / `ci-smoke-mem512` (jobs
pmm-differential-256/512, both gating release) boot at 256/512 MB and
assert the frame count lands in that size's window (~0xFFE0 / ~0x1FFE0 --
it ~doubles / ~quadruples the 128M leg's 0x7FE0) AND that PMMHIGH took its
live writeback branch. This is the true hardcode-vs-live differential the
-m 128M leg cannot show: a 128 MB hardcode prints 0x8000 at every -m and
never the live PMMHIGH.

Revert-confirmed two ways: re-hardcoding memory_init to 128 MB reddens the
mem256 sizing window (0x8000 outside [65280,65536]); broadening the
high-memory guard so 256 MB wrongly skips reddens the mem256 PMMHIGH-live
check while sizing still passes (the two gates are independent). Every
"un-fakeable gate" named in the ADR-0021 design is now live.

Build clean under -Werror; format/cppcheck/api-consistency green;
ci.yml validated.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
@NickFlach
NickFlach merged commit 872fed0 into main Jul 13, 2026
43 of 46 checks passed
@NickFlach
NickFlach deleted the pr4/adr0021-highmem-differential branch July 13, 2026 13:51
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants