repo: merge the kernel view pool reclaim (view-reclaim)

A 256-table kernel view pool with lazy reclaim of copies that no longer hold a protected leaf, behind --view-reclaim (SNAP_VIEW_RECLAIM); CODE_AT moves down 16 KiB so the monitor keeps 15 KiB of headroom with --edp-backlight; the pool's count, high-water mark and reclaims are reported as VIEWRCL1. next1 stopped at 1104 s when the 128-table pool was full (exit 7, ROZONE RETYPE refused).

compat/pauth-switch.h

@@ -1,7 +1,14 @@
 /* SPDX-License-Identifier: MIT */
 #pragma once
 #define PAUTH_BANK_STRIDE 256
+/* struct context's pauth_bank (asserted in probes/xnuboot/context.c). With
+ * SNAP_VIEW_RECLAIM, 65 struct sprr_views before it (kernel_views and the 64
+ * define-free user_views) are 8,192 bytes wider each (sprr-view.h). */
+#if SNAP_VIEW_RECLAIM
+#define PAUTH_BANK_CONTEXT 3172736
+#else
 #define PAUTH_BANK_CONTEXT 2640256
+#endif
 #define PAUTH_BANK_ENABLES 176
 #define PAUTH_BANK_ACTIVE 184
 #define PAUTH_BANK_ENTRIES 192

docs/RUNNING.md

@@ -147,6 +147,7 @@ The flags fall into these groups:
 | Clocks and bandwidth | `--thermal-guard`, `--gpu-dvfs`, `--gpu-dvfs-ceiling`, `--cpu-dvfs`, `--ddr-vote`, `--llcc`, `--bw-probe` |
 | Storage | `--nvme-async`, `--nvme-converted` |
 | Wi-Fi | `--qcc2072-wifi`, `--qcc2072-auxkc`, `--qcc2072-auxkc-sha256` |
+| Kernel view pool | `--view-reclaim` |
 | Monitor performance | `--fine-locks`, `--root-cache-wide`, `--user-hw-walk`, `--fast-timer-irq`, `--fast-ipi`, `--lean-traps`, `--sptm-fine`, and others |
 | Kernel patches | `--kernel-sysreg-zero`, `--kernel-user-4k`, `--kernel-refmod-skip` ([KERNEL-PATCHES.md](KERNEL-PATCHES.md)) |
 
@@ -205,6 +206,18 @@ PWM-pin mode to DPCD control. `tools/survey-edp-aux.py` checks, read-only from
 q1n1, that the clocks and the AUX controller the call needs are on.
 `tools/test-edp-backlight.py` is the offline test.
 
+`--view-reclaim` gives the monitor `SNAP_VIEW_RECLAIM`. The kernel's per-CPU
+private page-table copies (`shadow/sprr-view.h`) hold 256 tables instead of
+128, and when a protecting RETYPE (read-only zone, TXM) finds them full, the
+copies that no selector2 or selector4 leaf needs any more are retired: every
+CPU's copies are synced back to the shared tables, published and invalidated
+before their pages are reused. Without it, a desktop session stops with exit 7
+(RETYPE to ROZONE refused) once the read-only zone has grown past about 120
+frames (installed-fresh-desktop-20261024-next1: after 1,104 s). The report's
+`VIEWRCL1` record (and `summary.json` `view_reclaim`) has the count, its
+high-water mark and the reclaims. `tools/test-view-reclaim.py` is the offline
+test.
+
 `--input-fnkeys FLAGS` (needs `--input`) adds the guest boot-arg
 `snap_i2c_fnkeys=FLAGS` for SnapI2CHID's keyboard Fn-key layer, which only a
 SnapI2CHID built with `PROFILE=desktop-fnkeys` has (`I2C_PROFILE=desktop-fnkeys

probes/run.py

@@ -205,17 +205,27 @@ CONSOLE_OFFSET = LOG_OFFSET + LOG_BYTES
 # fault, it would write into the shadow tables the hardware is walking, and the
 # failure would look like a page-table bug anywhere in the run.
 # tools/test-classify.py checks the whole report fits.
-CODE_AT = 0x400000
-# 448 KiB for probe code since native tables 3b: phase 3b's monitor is 320,526
-# bytes and the lock-free trap paths add 6,288, which left under 1 KiB of the
-# previous 320 KiB (itself raised from 256 KiB for the ANS2 M2 monitor,
-# docs/ANS2-M2-20260925.md). Only the report moves: it stays below the SMP
-# configuration page, which stays below WORK_AT. q1n1's heap, CODE_AT,
-# SECONDARY_CONFIG_AT and WORK_AT are unchanged, the monitor binary does not
-# change (the report address is passed at setup), and every consumer reads the
-# report through run.OUT_AT (tools/test-monitor-reservation.py).
-OUT_AT = 0x470000          # heap_base + this; 448 KiB reserved for probe code
+# 464 KiB for probe code since SNAP_VIEW_RECLAIM: the next1 qualification's
+# monitor (--edp-backlight) was 458,552 bytes, 200 short of the previous
+# 448 KiB, and the reclaim adds 1,352 (with VIEWRCL1). CODE_AT moves down
+# 16 KiB instead of OUT_AT up: the report ends exactly where the stopped-probe
+# scratch begins (heap+0x480000, tools/probe-a16-cpus.py), which
+# tools/secondary-runtime.py collect writes after the monitor returns and
+# before this file reads the report, so a higher report would lose its tail
+# (thermal and DVFS records). Below CODE_AT nothing in q1n1's heap is in use
+# during a run; the only other user of that range is the fresh-stage
+# qualification of tools/qualify-txm-image4-native.py (heap+0x100000, 3 MiB).
+# 448 KiB came from native tables 3b (phase 3b's monitor is 320,526 bytes and
+# the lock-free trap paths add 6,288, over the previous 320 KiB, itself raised
+# from 256 KiB for the ANS2 M2 monitor, docs/ANS2-M2-20260925.md) by moving
+# OUT_AT. The report, SECONDARY_CONFIG_AT and WORK_AT are unchanged, the
+# monitor binary does not depend on its load address, and every consumer reads
+# the code through run.CODE_AT and the report through run.OUT_AT
+# (tools/test-monitor-reservation.py).
+CODE_AT = 0x3fc000
+OUT_AT = 0x470000          # heap_base + this; 464 KiB reserved for probe code
 REPORT_RESERVE = 0x10000   # includes metrics for all 24 descriptor slots
+STOPPED_PROBE_AT = 0x480000     # stopped-probe scratch, from the report's end (tools/probe-a16-cpus.py)
 SECONDARY_CONFIG_AT = 0x4f0000  # the SMP secondaries' configuration page (tools/secondary-runtime.py)
 WORK_AT = 0x500000         # generic probe scratch; xnuboot stores its work locator here
 # The report must end before the next thing in the heap, the SMP configuration page.
@@ -1789,6 +1799,16 @@ def run_xnuboot(proxy, info, code, guest_profile='j700ap-26A428',
     early_record = early_names.decode(proxy.readmem(out + EARLY_STOP_OFFSET, early_names.SIZE))
     for line in early_names.summary(early_record, host.timer_hz):
         print(f'  {line}')
+    if '-DSNAP_VIEW_RECLAIM=1' in FLAGS:
+        perf = runpy.run_path(str(ROOT/'tools/perf_counters.py'))
+        offset, size = perf['view_reclaim_spec']()
+        try:
+            views = perf['decode_view_reclaim'](proxy.readmem(out + offset, size))
+            print(f"  kernel views: {views['count']} of {views['capacity']} tables (high water "
+                  f"{views['high_water']}), {views['reclaims']} reclaims retired {views['retired']}, "
+                  f"{views['full']} refused with nothing to retire")
+        except ValueError as error:
+            print('  kernel views record unreadable:', error)
     thermal_record = None
     if early is not None and early.thermal:
         thermal_names = runpy.run_path(str(ROOT/'tools/a16_thermal.py'))

probes/xnuboot/context.c

@@ -238,6 +238,14 @@ struct context {
     struct service_detail service_detail[GUEST_CPU_COUNT];
     struct sprr_publish_state kernel_publish_state;
     struct sprr_reuse_state kernel_reuse_state;
+#if SNAP_VIEW_RECLAIM
+    /* kernel_views_prepare_change: reclaims that retired tables, tables they
+     * retired, refusals that found nothing to retire, the highest count. With
+     * this define every offset from kernel_views on moves anyway (the wider
+     * struct sprr_views); placed after pauth_bank so PAUTH_BANK_CONTEXT moves
+     * by whole views only. */
+    struct kernel_view_reclaim {uint64_t reclaims,retired,full,high_water;} kernel_view_reclaim;
+#endif
     uint64_t user_fused_syncs;
     struct sprr_class_proof kernel_class_proof;
     struct sprr_user_prepare_stats user_prepare_stats;

probes/xnuboot/kernel_views.c

@@ -194,6 +194,50 @@ static void shadow_tlb_sync(struct context *c)
     __asm__ volatile("dsb ishst; tlbi alle1is; dsb ish; isb" ::: "memory");
     c->shadow_tlb_syncs++;
 }
+#if SNAP_VIEW_RECLAIM
+/* sprr_views_reclaim's quiesce. The reuse snapshot and the publication rows
+ * name tables by position, which just moved: drop both, then shadow_tlb_sync
+ * syncs all six views in full (a retired table's parent entries name its
+ * canonical source again), publishes every remaining copy and completes the
+ * all-VMID TLBI. After that no walk, cached or new, reaches a retired page.
+ * The variant columns need nothing: the refresh's save makes them inexact. */
+static int kernel_views_quiesce(void *ctx)
+{
+    struct context *c=ctx;
+#if SNAP_KERNEL_VIEW_REUSE
+    sprr_reuse_invalidate(&c->kernel_reuse_state);
+#endif
+#if SNAP_KERNEL_DIRTY_PUBLISH
+    sprr_publish_reset(&c->kernel_publish_state);
+#endif
+    shadow_tlb_sync(c);
+    return !c->kernel_view_failed;
+}
+/* The private paths of every leaf a protecting retype changes, before its
+ * first detach (the callers' shadow_tlb_sync). A full pool refuses with no
+ * change; then the copies no protected leaf needs are retired and the whole
+ * change is prepared again from its first leaf: the reclaim retires any path
+ * an earlier leaf of this change prepared, since that leaf is not protected
+ * until the commit. A second refusal (nothing to retire) fails the retype as
+ * before. */
+static int kernel_views_prepare_change(struct context *c,const struct sptm_papt_change *change)
+{
+    struct sprr_views *v=&c->kernel_views;struct kernel_view_reclaim *r=&c->kernel_view_reclaim;
+    struct shadow s=kernel_shadow(c);
+    for(int again=0;;again=1) {
+        unsigned i=0;
+        while(i<change->count && sprr_views_prepare(v,&s,change->leaf[i].va))i++;
+        if(i==change->count) {
+            if(r->high_water<v->count)r->high_water=v->count;
+            return 1;
+        }
+        if(again || v->count+3<=SPRR_VIEW_TABLES)return 0;
+        int retired=sprr_views_reclaim(v,&s,kernel_views_quiesce,c);
+        if(retired<=0) {r->full+=!retired;return 0;}
+        r->reclaims++;r->retired+=(unsigned)retired;
+    }
+}
+#endif
 #if SNAP_USER_UPDATE_KERNEL_SKIP
 /* User-root UPDATE_DISJOINT: sptm_mac_update_user_disjoint reaches only the
  * user backend (user canonical shadow, user private copies, guest PTE memory
@@ -333,7 +377,7 @@ static int kernel_change_pperm_impl(struct context *c,uint64_t pperm,int invalid
     const struct sprr_publish_state *ps=&c->kernel_publish_state;
     skip=current && !((before^pperm)&SPRR_KERNEL_VIEW_PPERM) &&
         ps->root==c->kernel_views.canonical_root && ps->count==c->kernel_views.count &&
-        !ps->pending[cpu][0] && !ps->pending[cpu][1];
+        sprr_publish_row_empty(ps,cpu);
 #if SNAP_KERNEL_PPERM_VARIANTS
     if(!skip && current && ((before^pperm)&SPRR_KERNEL_VIEW_PPERM) &&
        (swap=kernel_variant_swap(c,&s,cpu,before,pperm))<0)return 0;

probes/xnuboot/multipage.c

@@ -216,7 +216,7 @@ static int multipage_close(struct context *c,uint64_t elr,const struct sptm_mult
     /* P20: the patched copy pages through their own publication, so every pending row is empty again (the PPERM
      * skip and the variant swap require it). */
     for(unsigned cpu=0;cpu<GUEST_CPU_COUNT;cpu++)
-        if((c->kernel_publish_state.pending[cpu][0] || c->kernel_publish_state.pending[cpu][1]) &&
+        if(!sprr_publish_row_empty(&c->kernel_publish_state,cpu) &&
            !kernel_publish_cpu(c,cpu)) {
             record(c,EV_UPDATE_FAILED,elr,SPTM_SHADOW_FAILED,g->target,g->aperture_flags);return 0;
         }

probes/xnuboot/report.c

@@ -171,6 +171,18 @@ uint64_t xnuboot_report(uint64_t *out)
         out[OUT_DART_MEMO + 2 + n] = ((const uint64_t *)&c->root_ext->dart_memo.stats)[n];
     out[OUT_DART_MEMO + 2 + DART_MEMO_STATS_WORDS] = c->root_ext->dart_memo.live;
 #endif
+#if SNAP_VIEW_RECLAIM
+    out[OUT_VIEW_RECLAIM] = VIEW_RECLAIM_MAGIC;
+    out[OUT_VIEW_RECLAIM + 1] = (uint64_t)(8 * VIEW_RECLAIM_WORDS) << 32;
+    out[OUT_VIEW_RECLAIM + 2] = c->kernel_views.count;
+    /* A refused prepare leaves no count above the last success's. */
+    out[OUT_VIEW_RECLAIM + 3] = c->kernel_view_reclaim.high_water > c->kernel_views.count ?
+                                c->kernel_view_reclaim.high_water : c->kernel_views.count;
+    out[OUT_VIEW_RECLAIM + 4] = c->kernel_view_reclaim.reclaims;
+    out[OUT_VIEW_RECLAIM + 5] = c->kernel_view_reclaim.retired;
+    out[OUT_VIEW_RECLAIM + 6] = c->kernel_view_reclaim.full;
+    out[OUT_VIEW_RECLAIM + 7] = SPRR_VIEW_TABLES;
+#endif
 #if SNAP_TOKEN_TRIM
     out[OUT_TOKEN_TRIM] = TOKEN_TRIM_MAGIC;
     out[OUT_TOKEN_TRIM + 1] = (uint64_t)sizeof(struct token_trim_stats) << 32;

probes/xnuboot/report_layout.c

@@ -757,3 +757,32 @@ _Static_assert(OUT_IB_ASYNC+2+ADRENO_IB_FLIGHT_WORDS==OUT_TOKEN_TRIM,"the IB asy
 _Static_assert(OUT_IB_ASYNC+2+ADRENO_IB_FLIGHT_WORDS+2+16==OUT_DART_MEMO,"the IB async record's slot");
 #endif
 #endif
+#if SNAP_VIEW_RECLAIM
+/* The kernel views' pool (shadow/sprr-view.h): count and high-water mark, the
+ * reclaims that retired tables and how many, refusals that found nothing to
+ * retire, and the capacity, behind "VIEWRCL1" and a word of value bytes << 32,
+ * at a fixed place just below the IB async slot (used or not); each chained
+ * record must end before it. tools/perf_counters.py decode_view_reclaim. */
+#define VIEW_RECLAIM_WORDS 6u
+#define OUT_VIEW_RECLAIM (OUT_THERMAL - 98 - 3 - 8 - 2 - 16 - 2 - 36 - 2 - VIEW_RECLAIM_WORDS)
+#define VIEW_RECLAIM_MAGIC UINT64_C(0x314c435257454956)   /* "VIEWRCL1" */
+_Static_assert(OUT_EARLY_STOP+EARLY_STOP_STATE_WORDS<=OUT_VIEW_RECLAIM,"view reclaim report overlap");
+#if SNAP_FAST_EL0_SYSREG || SNAP_SERVICE_SUBCLASS
+_Static_assert(OUT_EXIT_PROFILE+2+EXIT_PROFILE_WORDS<=OUT_VIEW_RECLAIM,"view reclaim report overlap");
+#endif
+#if SNAP_FINE_LOCKS
+_Static_assert(OUT_FINE_PROFILE+2+GUEST_CPU_COUNT*FINE_PROFILE_WORDS<=OUT_VIEW_RECLAIM,"view reclaim report overlap");
+#endif
+#if SNAP_TOKEN_COSTS
+_Static_assert(OUT_TOKEN_COSTS+2+TOKEN_COSTS_WORDS<=OUT_VIEW_RECLAIM,"view reclaim report overlap");
+#endif
+#if SNAP_FAST_TIMER_IRQ
+_Static_assert(OUT_FAST_IRQ+2+GUEST_CPU_COUNT*FAST_IRQ_WORDS<=OUT_VIEW_RECLAIM,"view reclaim report overlap");
+#endif
+#if SNAP_GUEST_NET
+_Static_assert(OUT_GUEST_NET+2+GUEST_NET_LINK_WORDS+GUEST_NET_VIEW_WORDS<=OUT_VIEW_RECLAIM,"view reclaim report overlap");
+#endif
+#if SNAP_ADRENO_IB_ASYNC
+_Static_assert(OUT_VIEW_RECLAIM+2+VIEW_RECLAIM_WORDS==OUT_IB_ASYNC,"the view reclaim record ends at the IB async slot");
+#endif
+#endif

probes/xnuboot/sptm_retype.c

@@ -15,10 +15,15 @@ static int sptm_retype_rozone(void *ctx,uint64_t pa,uint64_t old_type,uint64_t n
     if(sptm_papt_prepare(&m,&b,&a,&moved,pa,old_type,new_type,&change)!=SPTM_OK)return 0;
     /* A SLIDE_REGION-moved frame also has the alias XNU's phystokv uses;
      * both leaves need private paths before either becomes selector2. */
+#if SNAP_VIEW_RECLAIM
+    for(unsigned i=0;i<change.count;i++)if(sprr_pte_class(change.leaf[i].after)==9)return 0;
+    if(!kernel_views_prepare_change(c,&change))return 0;
+#else
     struct shadow s=kernel_shadow(c);
     for(unsigned i=0;i<change.count;i++)
         if(sprr_pte_class(change.leaf[i].after)==9 ||
            !sprr_views_prepare(&c->kernel_views,&s,change.leaf[i].va))return 0;
+#endif
     /* Detach copied paths while canonical descriptors still have their old
      * permissions. No guest CPU may see an untranslated raw selector2 leaf. */
     shadow_tlb_sync(c);if(c->kernel_view_failed)return 0;
@@ -41,10 +46,15 @@ static int sptm_retype_txm_default(void *ctx,uint64_t pa,uint64_t old_type,uint6
     struct sptm_aperture a={p->mem_low,p->ram_aperture_va,p->mem_high-p->mem_low};
     struct sptm_moved moved=xnu_moved(c);struct sptm_papt_change change;
     if(sptm_papt_prepare(&m,&b,&a,&moved,pa,old_type,new_type,&change)!=SPTM_OK)return 0;
+#if SNAP_VIEW_RECLAIM
+    for(unsigned i=0;i<change.count;i++)if(sprr_pte_class(change.leaf[i].after)!=4)return 0;
+    if(!kernel_views_prepare_change(c,&change))return 0;
+#else
     struct shadow s=kernel_shadow(c);
     for(unsigned i=0;i<change.count;i++)
         if(sprr_pte_class(change.leaf[i].after)!=4 ||
            !sprr_views_prepare(&c->kernel_views,&s,change.leaf[i].va))return 0;
+#endif
     /* Detach every CPU's path while the canonical aperture is still class3.
      * After commit, private class4 is always EL1 RO/NX, with no EL0 access. */
     shadow_tlb_sync(c);if(c->kernel_view_failed)return 0;

shadow/sprr-publish.h

@@ -1,14 +1,16 @@
 /* SPDX-License-Identifier: MIT */
 #pragma once
 #include "sprr-view.h"
-_Static_assert(SPRR_VIEW_TABLES==128 && SPRR_VIEW_CPUS==6,"publication bitmap ABI");
+_Static_assert((SPRR_VIEW_TABLES==128 || (SNAP_VIEW_RECLAIM && SPRR_VIEW_TABLES==256)) &&
+               SPRR_VIEW_CPUS==6,"publication bitmap ABI");
 
 /* Publication bookkeeping only: never skips descriptor validation or TLBI.
  * Caller holds the service lock, reports every changed private-copy store,
  * and completes a bit only AFTER publishing that whole page. View metadata
- * must be append-only and copies must not be recycled during this lifetime. */
+ * must be append-only and copies must not be recycled during this lifetime,
+ * except across sprr_publish_reset (sprr_views_reclaim). */
 struct sprr_publish_state {
-    uint64_t root,count,pending[SPRR_VIEW_CPUS][2];
+    uint64_t root,count,pending[SPRR_VIEW_CPUS][SPRR_VIEW_TABLES/64];
     uint64_t writes,publishes,pages,flushed,skipped,errors;
 };
 static inline int sprr_publish_prepare(struct sprr_publish_state *p,const struct sprr_views *v)
@@ -48,3 +50,26 @@ static inline int sprr_publish_complete(struct sprr_publish_state *p,unsigned cp
     if(!sprr_publish_needed(p,cpu,n)) {p->errors++;return 0;}
     p->pending[cpu][n/64]&=~(UINT64_C(1)<<(n%64));p->flushed++;return 1;
 }
+/* No page of this CPU's copies waits for publication. */
+static inline int sprr_publish_row_empty(const struct sprr_publish_state *p,unsigned cpu)
+{
+#if SNAP_VIEW_RECLAIM
+    uint64_t any=0;
+    for(unsigned w=0;w<SPRR_VIEW_TABLES/64;w++)any|=p->pending[cpu][w];
+    return !any;
+#else
+    return !p->pending[cpu][0] && !p->pending[cpu][1];
+#endif
+}
+#if SNAP_VIEW_RECLAIM
+/* sprr_views_reclaim moved the tables: a pending bit would name another
+ * page. Every row goes and the next prepare marks every remaining copy, so
+ * the caller's next publication cleans all of them; a retired page is
+ * rewritten and published again before any reuse links it. */
+static inline void sprr_publish_reset(struct sprr_publish_state *p)
+{
+    for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++)
+        for(unsigned w=0;w<SPRR_VIEW_TABLES/64;w++)p->pending[cpu][w]=0;
+    p->count=0;
+}
+#endif

shadow/sprr-variants.h

@@ -69,7 +69,7 @@ static inline int sprr_variants_swap(struct sprr_view_variants *a,struct sprr_vi
     const struct sprr_publish_state *p,unsigned cpu,uint64_t before,uint64_t saves)
 {
     if(!sprr_variants_shape(v,cpu) || !saves || p->root!=v->canonical_root ||
-       p->count!=v->count || p->pending[cpu][0] || p->pending[cpu][1] ||
+       p->count!=v->count || !sprr_publish_row_empty(p,cpu) ||
        (before&~SPRR_PPERM_MUTABLE)!=SPRR_PPERM_INITIAL) {a->errors++;return 0;}
     for(unsigned n=0;n<v->count;n++)
         if(!a->copy[n][cpu] || (a->copy[n][cpu]&4095)) {a->errors++;return 0;}

shadow/sprr-view.c

@@ -99,8 +99,22 @@ static int add(struct sprr_views *v,const struct shadow *s,uint64_t source,unsig
     if(found>=0)return v->tables[found].level==level;
     if(v->count>=SPRR_VIEW_TABLES || !source || (source&4095) || level>3)return 0;
     struct sprr_view_table *t=&v->tables[v->count];
+#if SNAP_VIEW_RECLAIM
+    /* Pages still waiting for sprr_views_reclaim's invalidation stay unused. */
+    if(t->level)return 0;
+#endif
     for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++) {
+#if SNAP_VIEW_RECLAIM
+        /* A retired set, or pages a failed add kept: no CPU can reach them
+         * any more, and they pass the same alias checks as fresh pages. The
+         * next sync stores every word that differs from its translation
+         * before a parent links them, and the publication rows mark every
+         * position at or past their count, so the whole page is cleaned
+         * before the next TLBI. */
+        uint64_t pa=t->copy[cpu] ? t->copy[cpu] : shadow_alloc_page(s);
+#else
         uint64_t pa=shadow_alloc_page(s);
+#endif
         if(!pa || (pa&4095) || pa==source)return 0;
         for(unsigned n=0;n<v->count;n++) {
             if(pa==v->tables[n].source)return 0;
@@ -144,6 +158,13 @@ static int prepare_path(struct sprr_views *v,const struct shadow *s,uint64_t va,
             table=pte&PT_OA_MASK;
         }
     }
+#if SNAP_VIEW_RECLAIM
+    /* Room for the whole path or no change: a full pool refuses before any
+     * add, so the caller can reclaim and prepare again from a clean state. */
+    unsigned missing=0;
+    for(unsigned level=0;level<4;level++)missing+=find(v,path[level])<0;
+    if(v->count+missing>SPRR_VIEW_TABLES)return 0;
+#endif
     for(unsigned level=0;level<4;level++)if(!add(v,s,path[level],level))return 0;
     return 1;
 }
@@ -154,6 +175,44 @@ int sprr_views_prepare_user_leaf(struct sprr_views *v,const struct shadow *s,uin
     if(va>=(1UL<<47) || (va&4095))return 0;
     return prepare_path(v,s,va,1);
 }
+#if SNAP_VIEW_RECLAIM
+int sprr_views_reclaim(struct sprr_views *v,const struct shadow *s,int (*quiesce)(void *),void *ctx)
+{
+    if(!configured(v,s) || !quiesce)return -1;
+    unsigned count=(unsigned)v->count,kept=0;
+    for(unsigned n=0;n<count;n++)if(v->tables[n].level>3)return -1;
+    uint8_t keep[SPRR_VIEW_TABLES];
+    /* Levels 3 to 0, so every copied child is judged before its parent. A
+     * child at the wrong level is kept (its parent's sync refuses it anyway). */
+    for(unsigned level=4;level--;)for(unsigned n=0;n<count;n++) {
+        const struct sprr_view_table *t=&v->tables[n];
+        if(t->level!=level)continue;
+        int need=!level;
+        for(unsigned i=0;i<512 && !need;i++) {
+            uint64_t d;
+            if(s->read(s->ctx,t->source+8UL*i,&d))return -1;
+            if(!(d&1))continue;
+            if(level<3 && (d&3)==3) {
+                int child=find(v,d&PT_OA_MASK);
+                need=child>=0 && (v->tables[child].level!=level+1 || keep[child]);
+            } else need=(UINT32_C(0x214)>>sprr_pte_class(d))&1;  /* selector 2, 4 or 9 */
+        }
+        keep[n]=(uint8_t)need;kept+=(unsigned)need;
+    }
+    if(kept==count)return 0;
+    /* Stable for the kept tables; a retired entry keeps its own six pages. */
+    unsigned w=0;
+    for(unsigned n=0;n<count;n++)if(keep[n]) {
+        struct sprr_view_table t=v->tables[w];
+        v->tables[w++]=v->tables[n];v->tables[n]=t;
+    }
+    for(unsigned n=w;n<count;n++) {v->tables[n].source=0;v->tables[n].level=SPRR_VIEW_RETIRED;}
+    v->count=w;
+    if(!quiesce(ctx))return -1;
+    for(unsigned n=w;n<count;n++)v->tables[n].level=0;
+    return (int)(count-w);
+}
+#endif
 
 static int entry_decode(const struct sprr_views *v,unsigned n,uint64_t d,
                   unsigned index,unsigned cpu,uint64_t pperm,

shadow/sprr-view.h

@@ -15,7 +15,28 @@
  * commit. A failing write callback is terminal: never resume a partial sync.
  * alloc must return fresh, zeroed pages that cannot alias any source table. */
 #define SPRR_VIEW_CPUS 6u
+/* SNAP_VIEW_RECLAIM (opt-in; cycle.py installed-fresh --view-reclaim): the
+ * pool holds 256 tables instead of 128, and sprr_views_reclaim gives back the
+ * kernel copies no protected leaf needs any more. Off, every layout and the
+ * monitor are unchanged.
+ *
+ * Why: installed-fresh-desktop-20261024-next1 stopped after 1,104 s (exit 7,
+ * RETYPE to ROZONE refused) when its kernel views held 128 tables: 1 + 1 + 8
+ * upper and 118 level-3 copies. Its context shows 114 of those 118 still held
+ * selector2 leaves (122 ROZONE protects, 3 releases: each 16K RO-zone frame
+ * lands in its own 2 MiB table), so the live set itself had reached the pool.
+ * In the 86 preserved installed-fresh runs of 6 minutes or more, releases
+ * stayed at 2 to 8 while protects reached 122 (OBSERVED, context.bin).
+ * Reclaim covers released frames and TXM imports; the wider pool covers the
+ * live set. */
+#ifndef SNAP_VIEW_RECLAIM
+#define SNAP_VIEW_RECLAIM 0
+#endif
+#if SNAP_VIEW_RECLAIM
+#define SPRR_VIEW_TABLES 256u
+#else
 #define SPRR_VIEW_TABLES 128u
+#endif
 /* A bounded, read-only mapping of an entire canonical 4K table. The backend
  * validates the allocation span and keeps the bytes and mapping stable under
  * the service token through preflight and commit. No pointer is retained. */
@@ -24,6 +45,9 @@ typedef sprr_table_reader sprr_user_table_reader;
 struct sprr_view_table {
     uint64_t source, copy[SPRR_VIEW_CPUS], level;
 };
+/* tables[0..count) are the copied tables, the root first. With
+ * SNAP_VIEW_RECLAIM, entries past count may hold the pages of retired tables
+ * (source 0) or of a failed add, kept for the next add at that position. */
 struct sprr_views {
     uint64_t canonical_root, count;
     uint64_t syncs[SPRR_VIEW_CPUS];
@@ -35,6 +59,34 @@ struct sprr_views {
 int sprr_views_init(struct sprr_views *, const struct shadow *);
 int sprr_views_prepare(struct sprr_views *, const struct shadow *, uint64_t va);
 uint64_t sprr_views_root(const struct sprr_views *, unsigned cpu);
+#if SNAP_VIEW_RECLAIM
+/* Kernel views only: the selector2/4 decode of sprr_views_sync_cpu*, never
+ * a user view, a native view or views carrying an sprr_view_memo (whose
+ * claims assume append-only metadata).
+ *
+ * A copy is needed while some leaf under it translates differently from its
+ * raw descriptor on some CPU under some PPERM: a valid selector2 or selector4
+ * leaf (selector9, which a sync refuses, is kept too), or an upper-level entry
+ * leading to a needed copy. Every other copied table is retired; the root
+ * never is. Kept tables move to the front in their order, so positions change.
+ *
+ * Order: every source is read before anything changes (a read failure or an
+ * unconfigured view returns -1 unchanged; nothing to retire returns 0
+ * unchanged). Then the metadata is compacted: a retired table's six pages wait
+ * past count with source 0 and level SPRR_VIEW_RETIRED. quiesce(ctx) must drop
+ * every record kept by table position (reuse snapshot, publication rows), sync
+ * every CPU's copies -- a retired table's parent entries then name its
+ * canonical source again, which translates identically -- publish them and
+ * complete a broadcast invalidation of every EL1&0 translation (TLBI
+ * ALLE1IS, every VMID) before it returns 1. Only
+ * then do the pages become reusable (level 0): the next add() at that position
+ * takes them instead of allocating, and its sync rewrites every word before a
+ * parent links them. Returns the number retired, or -1 after a failed quiesce
+ * (terminal, as a failed sync: the views hold only kept tables and the
+ * retired pages are never reused). Caller holds the service lock throughout. */
+#define SPRR_VIEW_RETIRED 4u
+int sprr_views_reclaim(struct sprr_views *,const struct shadow *,int (*quiesce)(void *),void *ctx);
+#endif
 /* Translate selector2 A/B. Selector9 2/3 state is accepted only with the
  * caller's proof that the canonical/user views contain no affected leaves;
  * mutation paths must retain that exclusion. This is not a general SPRR MMU. */

shadow/user-publish.h

@@ -3,7 +3,12 @@
 #include "root-publish.h"
 #include "sprr-private-pages.h"
 
+/* SPRR_VIEW_TABLES: one user view's copies at most (sprr-view.h). */
+#if SNAP_VIEW_RECLAIM
+#define USER_PUBLISH_MAX 256u
+#else
 #define USER_PUBLISH_MAX 128u
+#endif
 struct user_publish_stats {
     uint64_t calls, complete, considered, published, skipped, errors;
 };
@@ -23,7 +28,7 @@ static inline int user_publish_flush(struct root_publish_state *dirty,
     stats->calls++;
     if(!pages || !count || count>USER_PUBLISH_MAX || !publish_page ||
        !root_publish_geometry(first,allocated))goto fail;
-    unsigned indices[USER_PUBLISH_MAX];uint64_t selected[2]={0,0};unsigned changed=0;
+    unsigned indices[USER_PUBLISH_MAX];uint64_t selected[USER_PUBLISH_MAX/64]={0};unsigned changed=0;
     for(unsigned n=0;n<count;n++) {
         uint64_t pa=pages[n];
         if((pa&4095) || pa<first || pa>=allocated)goto fail;

tools/cycle.py

@@ -283,6 +283,11 @@ def parse(argv=None):
                         'change switch a panel the firmware left in PWM-pin mode to DPCD control (level written first, '
                         'only the two mode bits changed, read back; on failure the old mode is restored and the '
                         'monitor stops)')
+    p.add_argument('--view-reclaim', action='store_true',
+                   help='opt-in kernel view pool (shadow/sprr-view.h): monitor define SNAP_VIEW_RECLAIM, 256 private '
+                        'kernel view tables instead of 128 and, when a protecting RETYPE finds them full, the copies no '
+                        'selector2/4 leaf needs any more retired (after an all-CPU sync, publication and TLBI) and their '
+                        'pages reused; report record VIEWRCL1. Monitor only')
     p.add_argument('--present-latch-us', type=int, default=None,
                    help='with --present-latch: guest boot-arg adreno_latch_us, the slack kept before row 0 (default '
                         '3000; 0 = the beam kext\'s aim before the vblank)')

tools/cycle_lib/installed_fresh.py

@@ -673,6 +673,10 @@ GPU_COHERENT_FORCE_DEFINE = '-DSNAP_ADRENO_COHERENT_FORCE=1'
 # flag adds. Monitor define only (no loader change). Appended after every earlier flag; off, the monitor is
 # byte-identical.
 EDP_BACKLIGHT_DEFINE = '-DSNAP_EDP_BACKLIGHT=1'
+# --view-reclaim (agents/view-reclaim): shadow/sprr-view.h SNAP_VIEW_RECLAIM, a 256-table kernel view pool and the
+# reclaim of copies no protected leaf needs when a protecting RETYPE finds it full (next1 stopped at 128, exit 7).
+# Monitor define only (no loader change). Appended after every earlier flag; off, the monitor is byte-identical.
+VIEW_RECLAIM_DEFINE = '-DSNAP_VIEW_RECLAIM=1'
 # agents/dvfs (FAILURE-MODES.md): opt-in governors on vCPU 0's locked tick, state at the end of root_ext (so
 # --root-cache-wide), report DVFSREP1 after the thermal record, restored at the stop; both need --thermal-guard (they
 # never write without the guard's readings). compat/cpu-dvfs.h SNAP_CPU_DVFS: SCMI PERF LEVEL_SET fastchannels of the
@@ -1096,6 +1100,8 @@ def variant_flags(sets, args, variant=None):
         flags.append(GPU_COHERENT_FORCE_DEFINE)
     if getattr(args, 'edp_backlight', False):
         flags.append(EDP_BACKLIGHT_DEFINE)
+    if getattr(args, 'view_reclaim', False):
+        flags.append(VIEW_RECLAIM_DEFINE)
     return flags
 
 

tools/cycle_lib/speed_test.py

@@ -459,6 +459,8 @@ def decode(ws, dest, record):
             token_costs=exits.get('token_costs'), fast_ipi=(exits.get('fast_ipi') or {}).get('summary'))
         if exits.get('token_trim'):
             summary['token_trim'] = exits['token_trim']   # SNAP_TOKEN_TRIM runs only
+        if exits.get('view_reclaim'):
+            summary['view_reclaim'] = exits['view_reclaim']   # SNAP_VIEW_RECLAIM runs only
     write(dest / 'decoded.json', dict(cpus=cpus, perf=counters, host_hz=hz, exits=exits))
     write(dest / 'summary.json', summary)
     return summary

tools/perf_counters.py

@@ -792,10 +792,42 @@ def decode_ib_async(record, hz=None, recover=False):
     return out
 
 
+# SNAP_VIEW_RECLAIM (shadow/sprr-view.h; probes/xnuboot.c OUT_VIEW_RECLAIM): the kernel views' pool -- tables in use,
+# the highest count, reclaims that retired tables and how many, refusals that found nothing to retire, the capacity --
+# behind "VIEWRCL1" and a word of value bytes << 32, at a fixed place: the 8 words just below the IB async slot
+# (used or not).
+VIEW_RECLAIM_MAGIC = 0x314c435257454956   # "VIEWRCL1"
+VIEW_RECLAIM_DEFINE = '-DSNAP_VIEW_RECLAIM=1'
+VIEW_RECLAIM_FIELDS = ('count', 'high_water', 'reclaims', 'retired', 'full', 'capacity')
+
+
+def view_reclaim_spec():
+    """(byte offset in report.bin, byte length) of the view reclaim record."""
+    offset, _ = ib_async_spec()
+    size = 8 * (2 + len(VIEW_RECLAIM_FIELDS))
+    return offset - size, size
+
+
+def decode_view_reclaim(record):
+    n = len(VIEW_RECLAIM_FIELDS)
+    if len(record) != 8 * (2 + n):
+        raise ValueError(f'expected {8 * (2 + n)} bytes, got {len(record)}')
+    words = struct.unpack(f'<{2 + n}Q', record)
+    if words[0] != VIEW_RECLAIM_MAGIC or words[1] != (8 * n) << 32:
+        raise ValueError('no view reclaim record here (magic or size word differs)')
+    out = dict(zip(VIEW_RECLAIM_FIELDS, words[2:]))
+    # The root is never retired; every reclaim retires at least one table.
+    if not 1 <= out['count'] <= out['high_water'] <= out['capacity'] or out['capacity'] != 256 or \
+            out['retired'] < out['reclaims']:
+        raise ValueError('inconsistent view reclaim counters')
+    out['free'] = out['capacity'] - out['count']
+    return out
+
+
 def decode_report(report, defines, hz=None):
     """report.bin's records for a SNAP_FAST_EL0_SYSREG / SNAP_SERVICE_SUBCLASS monitor: the exit profile,
     then (as its defines have them) the converted-call profile, the token costs, the fast IRQ and fast IPI
-    outcomes, the DART memo and the token-trim record."""
+    outcomes, the DART memo, the token-trim record, the IB flight and the kernel views' pool."""
     offset, size = exit_profile_spec(defines)
     out = decode_exit_profile(report[offset:offset + size], defines, hz=hz)
     if '-DSNAP_FINE_LOCKS=1' in defines:
@@ -822,6 +854,9 @@ def decode_report(report, defines, hz=None):
         offset, size = ib_async_spec()
         out['ib_async'] = decode_ib_async(report[offset:offset + size], hz=hz,
                                           recover=any(d.startswith('-DSNAP_ADRENO_RECOVER=') for d in defines))
+    if VIEW_RECLAIM_DEFINE in defines:
+        offset, size = view_reclaim_spec()
+        out['view_reclaim'] = decode_view_reclaim(report[offset:offset + size])
     return out
 
 

tools/test-edp-backlight.py

@@ -197,6 +197,8 @@ class Wiring(unittest.TestCase):
         src = (ROOT / 'tools/cycle_lib/installed_fresh.py').read_text()
         body = src[src.index('def variant_flags('):]
         body = body[:body.index('\n    return flags\n')]
+        # Only defines added after this one (tools/test-view-reclaim.py) may follow it.
+        body = body.replace("\n    if getattr(args, 'view_reclaim', False):\n        flags.append(VIEW_RECLAIM_DEFINE)", '')
         self.assertTrue(body.rstrip().endswith('flags.append(EDP_BACKLIGHT_DEFINE)'), 'the define is not appended last')
 
 

tools/test-kernel-ops-perf-source.py

@@ -103,7 +103,9 @@ order = ['sprr_reuse_current', 'sprr_reuse_invalidate', 'pperm_tpro_preflight',
          'tlbi alle1is', 'sprr_reuse_repin']
 positions = [impl.index(token) for token in order]
 check(positions == sorted(positions), 'PPERM proof, invalidate, write, publish, TLBI, repin order')
-check('SPRR_KERNEL_VIEW_PPERM' in impl and '!ps->pending[cpu][0] && !ps->pending[cpu][1]' in impl,
+publish_h = (ROOT / 'shadow/sprr-publish.h').read_text()
+check('SPRR_KERNEL_VIEW_PPERM' in impl and 'sprr_publish_row_empty(ps,cpu)' in impl and
+      'return !p->pending[cpu][0] && !p->pending[cpu][1];' in publish_h,
       'skip requires the unchanged kernel permission bit and no pending publication')
 check(re.search(r'if\(invalidate\) \{\s*__asm__ volatile\("dsb ishst; tlbi alle1is', impl),
       'the PPERM TLBI is omitted only when the caller folds it')

tools/test-kernel-pperm-variants.c

@@ -17,6 +17,12 @@
  * samples 1 in 64). -DVARIANTS_PRE_CHANGE=1 drops the snapshot-generation
  * check from the exact predicate and must fail.
  *
+ * With -DSNAP_VIEW_RECLAIM=1 both machines also retire the copies of the three
+ * ordinary tables now and then (sprr_views_reclaim with kernel_views_quiesce's
+ * steps: snapshot invalidated, publication rows reset, refresh) and prepare one
+ * again on a retired set: every check above must keep holding while table
+ * positions move under the snapshot, the publication rows and the variants.
+ *
  * cc -std=gnu11 -O1 -g -fsanitize=address,undefined -fno-sanitize-recover=all \
  *    -Icompat -Ishadow tools/test-kernel-pperm-variants.c shadow/sprr-view.c \
  *    shadow/shadow.c shadow/mmu.c -o build/test-kernel-pperm-variants
@@ -111,7 +117,7 @@ static int reuse_skip(struct machine *m,unsigned cpu,int current,uint64_t before
     const struct sprr_publish_state *ps=&m->publish;
     return current && !((before^pperm)&SPRR_KERNEL_VIEW_PPERM) &&
         ps->root==views.canonical_root && ps->count==views.count &&
-        !ps->pending[cpu][0] && !ps->pending[cpu][1];
+        sprr_publish_row_empty(ps,cpu);
 }
 /* The unchanged monitor: kernel_change_pperm_impl with SNAP_KERNEL_PPERM_REUSE. */
 static int pperm_reference(unsigned cpu,uint64_t pperm)
@@ -269,6 +275,27 @@ static void both_prepare(uint64_t va)
     enter(&ref);s=kshadow();CHECK(sprr_views_prepare(&views,&s,va));leave();
     enter(&cand);s=kshadow();CHECK(sprr_views_prepare(&views,&s,va));leave();
 }
+#if SNAP_VIEW_RECLAIM
+static uint64_t reclaims,retired;
+/* kernel_views_quiesce on the active machine: refresh() is kernel_refresh
+ * (a miss: full sync, publication, saves++) and its ALLE1IS. */
+static int machine_quiesce(void *ctx)
+{
+    (void)ctx;
+    sprr_reuse_invalidate(&active->reuse);
+    sprr_publish_reset(&active->publish);
+    return refresh();
+}
+static void both_reclaim(void)
+{
+    struct shadow s;int a,b;
+    enter(&ref);s=kshadow();a=sprr_views_reclaim(&views,&s,machine_quiesce,0);leave();
+    enter(&cand);s=kshadow();b=sprr_views_reclaim(&views,&s,machine_quiesce,0);leave();
+    CHECK(a==b && a>=0 && ref.views.count==cand.views.count);
+    if(a>0) {reclaims++;retired+=(unsigned)a;}
+    invariants();
+}
+#endif
 static const uint64_t deltas[4]={0,0x100,SPRR_UPERM_TPRO_WRITE,0x100|SPRR_UPERM_TPRO_WRITE};
 static void canonical_change(void)
 {
@@ -378,8 +405,15 @@ int main(void)
             enter(&cand);CHECK(pperm_candidate(cpu,cand.pp[cpu]^0x100));leave();
             mutate(BASE+0x3000,5,old);both_refresh();
         } else if(op<34) {
-            if(prepared>=3) {both_refresh();continue;}
             static const uint64_t vas[3]={0x200000,0x401000,0x600000};
+#if SNAP_VIEW_RECLAIM
+            if(prepared>=3) {
+                /* Their leaves are ordinary: the three copies retire; the one
+                 * prepared again takes the first retired set. */
+                both_reclaim();both_prepare(vas[rnd(3)]);both_refresh();continue;
+            }
+#endif
+            if(prepared>=3) {both_refresh();continue;}
             if(prepared==1) {
                 mutate(BASE+0x2000,2,BASE+0x5000+3);
                 mutate(BASE+0x5000,1,DATA+3+ATTR+PT_UXN+PT_PXN);
@@ -400,6 +434,9 @@ int main(void)
         if(failed>20)break;
     }
     CHECK(prepared==3);
+#if SNAP_VIEW_RECLAIM
+    CHECK(reclaims>10 && retired>=reclaims);
+#endif
     CHECK(cand.exact>800 && cand.synced>=30 && cand.fallbacks>10 && !cand.mismatches);
     /* A synced swap is a CPU's first flip after a re-save (or after an
      * in-place flip, or its first ever); every other bit-8 flip is exact. */
@@ -416,6 +453,9 @@ int main(void)
            (unsigned long long)cand.exact,(unsigned long long)cand.synced,
            (unsigned long long)cand.inplace,(unsigned long long)cand.fallbacks,
            (unsigned long long)cand.skipped,(unsigned long long)cand.var.reserved);
+#if SNAP_VIEW_RECLAIM
+    printf("reclaim: %llu reclaims retired %llu tables\n",(unsigned long long)reclaims,(unsigned long long)retired);
+#endif
     printf("%s: %u kernel PPERM variant checks, %u failures\n",failed ? "FAIL" : "PASS",checks,failed);
     return failed ? 1 : 0;
 }

tools/test-monitor-reservation.py

@@ -1,11 +1,15 @@
 #!/usr/bin/env python3
 # SPDX-License-Identifier: MIT
 """The q1n1 heap layout the loader uses (probes/run.py) after the monitor's
-code reservation grew to 448 KiB: code, report, SMP configuration page and work
-locator stay in that order without overlapping, and only OUT_AT moved. Host
-only; the monitor binary itself does not depend on the reservation (the report
-address is passed to xnuboot_setup)."""
+code reservation grew to 464 KiB: code, report, stopped-probe scratch, SMP
+configuration page and work locator stay in that order without overlapping.
+The 448 KiB step moved OUT_AT; the 464 KiB step moved CODE_AT down, because
+the report must end where the stopped-probe scratch begins (secondary-runtime
+collect writes it before the report is read). Host only; the monitor binary
+itself does not depend on the reservation (the report address is passed to
+xnuboot_setup)."""
 from pathlib import Path
+import re
 import sys
 import unittest
 
@@ -17,19 +21,43 @@ import run  # noqa: E402
 
 class HeapLayout(unittest.TestCase):
     def test_regions_in_order(self):
-        self.assertEqual(run.OUT_AT - run.CODE_AT, 448 << 10)
-        self.assertLessEqual(run.OUT_AT + run.REPORT_RESERVE, run.SECONDARY_CONFIG_AT)
+        self.assertEqual(run.OUT_AT - run.CODE_AT, 464 << 10)
+        self.assertLessEqual(run.OUT_AT + run.REPORT_RESERVE, run.STOPPED_PROBE_AT)
+        self.assertLess(run.STOPPED_PROBE_AT, run.SECONDARY_CONFIG_AT)
         self.assertEqual(run.OUT_HEADROOM, run.SECONDARY_CONFIG_AT - run.OUT_AT)
         self.assertLessEqual(run.SECONDARY_CONFIG_AT + 4096, run.WORK_AT)
         # The work locator host tools read from a stopped A16 is at WORK_AT.
         self.assertEqual(monitor_work.LOCATOR_OFFSET, run.WORK_AT)
 
-    def test_only_the_report_moved(self):
-        # Where code starts, the SMP page, the work locator and the report's
-        # size are protocol with running stages and stopped-state tools.
-        self.assertEqual((run.CODE_AT, run.SECONDARY_CONFIG_AT, run.WORK_AT, run.REPORT_RESERVE),
-                         (0x400000, 0x4f0000, 0x500000, 0x10000))
+    def test_only_the_code_start_moved(self):
+        # The report's place and size, the SMP page and the work locator are
+        # protocol with running stages and stopped-state tools.
+        self.assertEqual((run.OUT_AT, run.SECONDARY_CONFIG_AT, run.WORK_AT, run.REPORT_RESERVE),
+                         (0x470000, 0x4f0000, 0x500000, 0x10000))
+        self.assertEqual(run.CODE_AT, 0x3fc000)
 
+    def test_stopped_probes_use_the_scratch_after_the_report(self):
+        # The probes run between the monitor's return and the report read
+        # (tools/secondary-runtime.py collect) or on a stopped A16; their code
+        # and output pages must stay clear of the code and report reservations.
+        for name, pattern in (('probe-a16-cpus.py', r"heap_base'\]\+(0x[0-9a-f]+), info\['heap_base'\]\+(0x[0-9a-f]+)"),
+                              ('probe-el2-memory.py', r"heap_base'\]\+(0x[0-9a-f]+), info\['heap_base'\]\+(0x[0-9a-f]+)")):
+            text = (ROOT / 'tools' / name).read_text()
+            found = [int(x, 16) for m in re.finditer(pattern, text) for x in m.groups()]
+            self.assertTrue(found, name)
+            for offset in found:
+                self.assertGreaterEqual(offset, run.STOPPED_PROBE_AT, name)
+                self.assertLess(offset, run.SECONDARY_CONFIG_AT, name)
+
+    def test_below_the_code_only_a_fresh_stage_tool(self):
+        # tools/qualify-txm-image4-native.py places 3 MiB at heap+0x100000,
+        # up to 0x400000, which now covers the code reservation's first
+        # 16 KiB. It requires a fresh stage: no resident monitor to keep.
+        text = (ROOT / 'tools/qualify-txm-image4-native.py').read_text()
+        self.assertIn('Requires a fresh stage', text)
+        self.assertIn("work = (info['heap_base'] + 0x100000 + 0x3fff) & ~0x3fff", text)
+        self.assertGreaterEqual(run.CODE_AT, 0x100000)
+        self.assertEqual(run.CODE_AT % 0x4000, 0)
 
 if __name__ == '__main__':
     unittest.main()

tools/test-multipage-fast.c

@@ -605,7 +605,7 @@ static int multipage_close(struct context *c,uint64_t elr,const struct sptm_mult
 #if MUTANT_PENDING_LEFT
         if(0 &&
 #else
-        if((c->kernel_publish_state.pending[cpu][0] || c->kernel_publish_state.pending[cpu][1]) &&
+        if(!sprr_publish_row_empty(&c->kernel_publish_state,cpu) &&
 #endif
            !kernel_publish_cpu(c,cpu)) {
             record(c,EV_UPDATE_FAILED,elr,SPTM_SHADOW_FAILED,g->target,g->aperture_flags);return 0;

tools/test-reuse-match-mapped.py

@@ -35,7 +35,7 @@ SOURCE = read_source(ROOT / 'probes/xnuboot.c')
 HEADER = (ROOT / 'shadow/sprr-reuse.h').read_text()
 TEST_C = 'tools/test-reuse-match-mapped.c'
 LINKED = ['shadow/sprr-view.c', 'shadow/shadow.c', 'shadow/mmu.c']
-BUDGET = 0x470000 - 0x400000          # probes/run.py OUT_AT - CODE_AT
+BUDGET = 0x470000 - 0x3fc000          # probes/run.py OUT_AT - CODE_AT
 
 
 def arguments():

tools/test-tpro-view.c

@@ -5,7 +5,8 @@
 
 #define BASE UINT64_C(0x40000000)
 #define DATA UINT64_C(0x94050c000)
-#define BYTES (4u<<20)
+/* Room for a full pool of six-copy tables (SNAP_VIEW_RECLAIM: 256). */
+#define BYTES (SPRR_VIEW_TABLES>128 ? (8u<<20) : (4u<<20))
 #define ATTR (PT_AF|(3UL<<8)|(1UL<<11))
 static _Alignas(4096) unsigned char ram[BYTES],before[BYTES],expected[BYTES];
 static uint64_t next,fail_read;

tools/test-user-fused-compare.c

@@ -117,14 +117,15 @@ int main(void)
     s=setup();CHECK(sprr_views_init(&views,&s));stats.calls=63;blank_table=1;
     CHECK(!fused_compare(&s,state,modes));blank_table=0;
     /* Fill both mapping arrays to their supported maximum: three upper
-     * tables and125distinct TPRO leaf tables, with768private destinations. */
-    s=setup();next=BASE+0x100000;
-    for(unsigned i=0;i<125;i++) {
+     * tables and SPRR_VIEW_TABLES-3 distinct TPRO leaf tables, with six
+     * private destinations each. */
+    s=setup();next=BASE+0x80000+4096UL*SPRR_VIEW_TABLES;
+    for(unsigned i=0;i<SPRR_VIEW_TABLES-3;i++) {
         uint64_t table=BASE+0x80000+4096UL*i;
         put(BASE+0x2000,i,table+3);put(table,0,leaf(DATA+4096UL*i,9));
     }
     CHECK(sprr_views_init(&views,&s));CHECK(fused_compare(&s,state,modes));
-    CHECK(views.count==SPRR_VIEW_TABLES && source_maps==128 && copy_maps==768);
+    CHECK(views.count==SPRR_VIEW_TABLES && source_maps==SPRR_VIEW_TABLES && copy_maps==6*SPRR_VIEW_TABLES);
     CHECK(candidate_attempts<baseline_attempts);
     printf("Fused callbacks: %llu compared / %llu reference\n",
         (unsigned long long)candidate_attempts,(unsigned long long)baseline_attempts);

tools/test-user-prepare-fused.c

@@ -116,7 +116,7 @@ int TEST_PREPARE_ENTRY(void)
     struct sprr_state state[6]={0};int modes[6];
     for(unsigned cpu=0;cpu<6;cpu++){sprr_root_reset(&state[cpu],0xa);modes[cpu]=cpu&1;}
     struct shadow s=setup();CHECK(sprr_views_init(&views,&s));
-    CHECK(sizeof(plan)==67608 && sizeof(stats)==56);
+    CHECK(sizeof(plan)==24+16*SPRR_VIEW_TABLES+8*8192 && sizeof(stats)==56);
     CHECK(compare(&s,state,modes));CHECK(plan.source_count==6 && plan.required_count==4);
     for(unsigned pattern=0;pattern<64;pattern++) {
         for(unsigned cpu=0;cpu<6;cpu++) {
@@ -179,7 +179,7 @@ int TEST_PREPARE_ENTRY(void)
     CHECK(!compare(&s,state,modes));CHECK(plan.source_count==8192);
     /* The required-path union is independently bounded before allocations. */
     s=setup();CHECK(sprr_views_init(&views,&s));next=BASE+0x200000;
-    for(unsigned i=0;i<128;i++) {
+    for(unsigned i=0;i<SPRR_VIEW_TABLES;i++) {
         uint64_t table=BASE+0x80000+4096UL*i;
         put(BASE+0x2000,i,table+3);put(table,0,leaf(DATA+4096UL*i,9));
     }

tools/test-user-publish.c

@@ -6,7 +6,9 @@
 
 static unsigned checks;
 #define CHECK(x) do {checks++;if(!(x)){fprintf(stderr,"line %d: %s\n",__LINE__,#x);exit(1);}}while(0)
-#define PAGES 257u
+/* Twice the largest selection plus one: USER_PUBLISH_MAX distinct private
+ * pages always fit after the three runtime pages. */
+#define PAGES (2u*USER_PUBLISH_MAX+1u)
 #define BASE UINT64_C(0xae1400000)
 #define END (BASE+(uint64_t)PAGES*4096)
 static struct root_publish_state dirty;
@@ -89,10 +91,10 @@ static void rejected(void)
         if(which==1)pages[1]=BASE-4096;
         if(which==2)pages[1]=END;
         if(which==3)pages[1]=pages[0];
-        if(which==4)pages[1]=BASE+256*4096; /* canonical page */
+        if(which==4)pages[1]=BASE+(PAGES-1)*4096; /* canonical page */
         if(which==5){private.bitmap[0]|=1;pages[1]=BASE;} /* runtime even if mislabeled */
         if(which==6)count=0;
-        if(which==7)count=129;
+        if(which==7)count=USER_PUBLISH_MAX+1;
         if(which==8)first++;
         if(which==9)end++;
         memcpy(saved,dirty.bitmap,sizeof(saved));

tools/test-user-tree-memo.c

@@ -500,7 +500,7 @@ static void random_cases(unsigned rounds,unsigned steps)
 int main(void)
 {
     CHECK(sizeof(struct sprr_table_memo)==32+112+8*SPRR_TABLE_MEMO_PAGES);
-    CHECK(sizeof(struct sprr_view_memo)==24+96+16);
+    CHECK(sizeof(struct sprr_view_memo)==24+96+8*(SPRR_VIEW_TABLES/64));
     deterministic_cases();
     shared_source_case();
     unnoted_cases();

tools/test-view-reclaim.c

@@ -0,0 +1,430 @@
+/* SPDX-License-Identifier: MIT */
+/* SNAP_VIEW_RECLAIM (shadow/sprr-view.h sprr_views_reclaim; probes/xnuboot
+ * kernel_views_prepare_change): kernel copies no protected leaf needs any more
+ * are retired and their pages reused, in a 256-table pool.
+ *
+ * A canonical kernel 4K tree (one root, one level 1, four level 2 and 512
+ * level-3 tables) is driven the way the monitor drives it: every protecting
+ * change prepares its path, detaches it (sync, publish, TLBI), then stores the
+ * selector2/4 leaves and refreshes; a release stores ordinary leaves and
+ * refreshes. The quiesce callback is kernel_views_quiesce's model: publication
+ * rows reset, every CPU synced and published, then an all-CPU TLBI.
+ *
+ * Checked after every step, independently of the library:
+ *  - every CPU's walk from its own root gives, for all 16,384 leaves, the
+ *    canonical descriptor, or for selector2/4 its translation under that CPU's
+ *    PPERM (the only leaves that may differ);
+ *  - no page reachable from a root holds an unpublished store;
+ *  - every live copy page is distinct and no source; entries past count are
+ *    empty, parked (source 0, level 0) or retired (level SPRR_VIEW_RETIRED);
+ *  - no store reaches a retired page between its unlinking and the TLBI that
+ *    follows (a walk cache may still hold it), and after the quiesce's sync no
+ *    root reaches one.
+ * Scenarios: fill to 256; a full pool refuses with no change; release and
+ * reclaim (with the level-2 ancestor of fully released tables); reuse of the
+ * retired pages before any new allocation; reclaim down to the root; a source
+ * read failure, nothing to retire, an unconfigured view and a failed quiesce
+ * (no partial state, retired pages never reused). Harness self-checks: a
+ * quiesce without its TLBI and a protected table removed by hand must both be
+ * caught.
+ *
+ * cc -std=gnu11 -O1 -g -fsanitize=address,undefined -fno-sanitize-recover=all \
+ *    -DSNAP_VIEW_RECLAIM=1 -Icompat -Ishadow tools/test-view-reclaim.c \
+ *    shadow/sprr-view.c shadow/shadow.c shadow/mmu.c -o build/test-view-reclaim
+ */
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include "sprr-view.h"
+#include "sprr-publish.h"
+#include "sprr.h"
+#if !SNAP_VIEW_RECLAIM
+#error "build with -DSNAP_VIEW_RECLAIM=1"
+#endif
+
+#define BASE UINT64_C(0x40000000)
+#define BYTES (32u<<20)
+#define PAGES (BYTES/4096)
+#define DATA UINT64_C(0x900000000)
+#define ATTR (PT_AF|(3UL<<8))
+#define L1 (BASE+0x1000)
+#define L2(k) (BASE+0x2000+0x1000UL*(k))
+#define L3(k,j) (BASE+0x10000+0x1000UL*((k)*128u+(j)))
+#define COPIES (BASE+0x400000)
+#define SEL3 (ATTR+PT_PXN+PT_UXN+3)     /* ordinary RW/NX page: class 3 */
+#define SEL2 (ATTR+PT_UXN+3)            /* selector2 (ROZONE): class 2 */
+#define SEL4 (ATTR+(1UL<<6)+3)          /* selector4 (TXM aperture): class 4 */
+#define SEL11 (ATTR+(2UL<<6)+PT_UXN+PT_PXN+3)   /* fixed RO/NX: class 11 */
+
+static unsigned char ram[BYTES],dirty[PAGES],stale[PAGES];
+static struct sprr_views views;
+static struct sprr_publish_state pub;
+static uint64_t pp[SPRR_VIEW_CPUS],next_copy,read_fail,allocs,alloc_budget;
+static unsigned checks,failed,stale_writes,tlbis,quiesces,quiesce_fails,quiesce_no_tlbi;
+#define CHECK(x) do {checks++;if(!(x)){failed++;printf("FAIL %u: %s\n",__LINE__,#x);}} while(0)
+
+static unsigned page(uint64_t pa) {return (unsigned)((pa-BASE)/4096);}
+static int rd(void *ctx,uint64_t pa,uint64_t *out)
+{
+    (void)ctx;if(pa<BASE || pa>BASE+BYTES-8 || (pa&7) || pa==read_fail)return -1;
+    memcpy(out,ram+(pa-BASE),8);return 0;
+}
+/* kernel_table_write: identical stores elided; a changed one marks its copy
+ * pending (SNAP_KERNEL_DIRTY_PUBLISH) and leaves the page unpublished. */
+static int wr(void *ctx,uint64_t pa,uint64_t value)
+{
+    uint64_t old;
+    if(rd(ctx,pa,&old))return -1;
+    if(old==value)return 0;
+    if(stale[page(pa)])stale_writes++;
+    if(!sprr_publish_note(&pub,&views,pa))return -1;
+    memcpy(ram+(pa-BASE),&value,8);dirty[page(pa)]=1;return 0;
+}
+/* private_kernel_alloc: zeroed with plain stores, unpublished. */
+static uint64_t alloc(void *ctx)
+{
+    (void)ctx;
+    if(!alloc_budget || next_copy>BASE+BYTES-4096)return 0;
+    alloc_budget--;allocs++;
+    uint64_t pa=next_copy;next_copy+=4096;
+    memset(ram+(pa-BASE),0,4096);dirty[page(pa)]=1;return pa;
+}
+static struct shadow shadow_of(void)
+{return (struct shadow){.txsz=17,.root=BASE,.alloc=alloc,.read=rd,.write=wr};}
+static void put(uint64_t pa,uint64_t value)
+{memcpy(ram+(pa-BASE),&value,8);}
+static uint64_t get(uint64_t pa) {uint64_t v;memcpy(&v,ram+(pa-BASE),8);return v;}
+static uint64_t va_of(unsigned k,unsigned j,unsigned i)
+{return ((uint64_t)k<<30)|((uint64_t)j<<21)|((uint64_t)i<<12);}
+static uint64_t frame(unsigned k,unsigned j,unsigned i)
+{return DATA+(((uint64_t)k*128+j)*512+i)*4096;}
+
+static void tlbi(void) {memset(stale,0,sizeof stale);tlbis++;}
+static int publish_cpu(unsigned cpu)
+{
+    if(!sprr_publish_prepare(&pub,&views))return 0;
+    for(unsigned level=4;level--;)for(unsigned n=0;n<views.count;n++) {
+        if(views.tables[n].level!=level || !sprr_publish_needed(&pub,cpu,n))continue;
+        dirty[page(views.tables[n].copy[cpu])]=0;
+        if(!sprr_publish_complete(&pub,cpu,n))return 0;
+    }
+    return sprr_publish_row_empty(&pub,cpu);
+}
+static int sync_publish(void)
+{
+    struct shadow s=shadow_of();
+    for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++)
+        if(!sprr_views_sync_cpu(&views,&s,cpu,pp[cpu]) || !publish_cpu(cpu))return 0;
+    return 1;
+}
+/* shadow_tlb_sync: refresh every copy, publish, all-VMID TLBI. */
+static int refresh(void) {int ok=sync_publish();if(ok)tlbi();return ok;}
+static int reachable_bad(uint64_t table,unsigned level,int stale_only)
+{
+    if(table<BASE || table>=BASE+BYTES)return 1;
+    if(stale_only ? stale[page(table)] : dirty[page(table)])return 1;
+    for(unsigned i=0;i<512 && level<3;i++) {
+        uint64_t d=get(table+8UL*i);
+        if((d&3)==3 && reachable_bad(d&PT_OA_MASK,level+1,stale_only))return 1;
+    }
+    return 0;
+}
+/* kernel_views_quiesce's model. */
+static int quiesce(void *ctx)
+{
+    (void)ctx;quiesces++;
+    unsigned retired=0;
+    for(unsigned n=views.count;n<SPRR_VIEW_TABLES;n++)if(views.tables[n].level==SPRR_VIEW_RETIRED) {
+        retired++;CHECK(!views.tables[n].source);
+        for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++)stale[page(views.tables[n].copy[cpu])]=1;
+    }
+    CHECK(retired);
+    if(quiesce_fails)return 0;
+    sprr_publish_reset(&pub);
+    if(!sync_publish())return 0;
+    for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++)
+        CHECK(!reachable_bad(sprr_views_root(&views,cpu),0,1));
+    if(!quiesce_no_tlbi)tlbi();
+    return 1;
+}
+static uint64_t expected(uint64_t d,unsigned cpu)
+{
+    if((d&3)!=3)return d;
+    unsigned c=sprr_pte_class(d);
+    if(c!=2 && c!=4)return d;
+    d=(d&~(PT_AP|PT_PXN|PT_UXN))|PT_PXN|PT_UXN;
+    return c==4 || !(pp[cpu]&0x100) ? d|(2UL<<6) : d;
+}
+/* An independent walk of CPU cpu's view for every leaf of the tree. */
+static unsigned view_mismatches(void)
+{
+    unsigned bad=0;
+    for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++) {
+        uint64_t root=sprr_views_root(&views,cpu);
+        if(!root || root==BASE)return 1;
+        for(unsigned k=0;k<4;k++)for(unsigned j=0;j<128;j++)for(unsigned i=0;i<8;i++) {
+            uint64_t va=va_of(k,j,i),table=root,d=0;
+            for(unsigned level=0;level<4;level++) {
+                d=get(table+8UL*mmu_index(12,level,va));
+                if(level<3) {if((d&3)!=3)break;table=d&PT_OA_MASK;}
+            }
+            bad+=d!=expected(get(L3(k,j)+8UL*i),cpu);
+        }
+    }
+    return bad;
+}
+static void invariants(void)
+{
+    struct shadow s=shadow_of();
+    CHECK(!view_mismatches());
+    for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++) {
+        CHECK(sprr_views_verify_cpu(&views,&s,cpu,pp[cpu]));
+        CHECK(!reachable_bad(sprr_views_root(&views,cpu),0,0));
+    }
+    CHECK(views.count && views.count<=SPRR_VIEW_TABLES && views.tables[0].source==BASE);
+    static unsigned char seen[PAGES];memset(seen,0,sizeof seen);
+    for(unsigned n=0;n<SPRR_VIEW_TABLES;n++) {
+        const struct sprr_view_table *t=&views.tables[n];
+        if(n<views.count) {CHECK(t->source>=BASE && t->source<COPIES && t->level<=3);}
+        else CHECK(!t->source && (!t->level || t->level==SPRR_VIEW_RETIRED));
+        for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++) {
+            uint64_t pa=t->copy[cpu];
+            if(!pa) {CHECK(n>=views.count);continue;}
+            CHECK(pa>=COPIES && pa<next_copy && !seen[page(pa)]);seen[page(pa)]=1;
+        }
+    }
+    CHECK(!stale_writes);
+}
+/* sprr_views_reclaim, and what a completed one must leave: one quiesce and
+ * its TLBI after the unlinking, no root reaching a retired page, and the
+ * retired sets parked past count. */
+static int reclaim(void)
+{
+    struct shadow s=shadow_of();unsigned q=quiesces,t=tlbis,count=(unsigned)views.count;
+    int got=sprr_views_reclaim(&views,&s,quiesce,0);
+    if(got<=0)return got;
+    CHECK(quiesces==q+1 && (tlbis==t+1 || quiesce_no_tlbi) && views.count==count-(unsigned)got);
+    static unsigned char tail[PAGES];memset(tail,0,sizeof tail);
+    for(unsigned n=(unsigned)views.count;n<count;n++) {
+        CHECK(!views.tables[n].source && !views.tables[n].level);
+        for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++)tail[page(views.tables[n].copy[cpu])]=1;
+    }
+    static unsigned char keep[PAGES];memcpy(keep,stale,sizeof keep);memcpy(stale,tail,sizeof stale);
+    for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++)CHECK(!reachable_bad(sprr_views_root(&views,cpu),0,1));
+    memcpy(stale,keep,sizeof stale);
+    return got;
+}
+static int find_source(uint64_t source)
+{
+    for(unsigned n=0;n<views.count;n++)if(views.tables[n].source==source)return (int)n;
+    return -1;
+}
+/* kernel_views_prepare_change for a change of `leaves` frames: every path,
+ * and on a refusal with the pool nearly full a reclaim and a restart from
+ * the first leaf. only_failing is a deliberately wrong variant (retry the
+ * refused leaf alone) the walk check must catch. */
+static int only_failing;
+static int prepare_change(const unsigned (*leaf)[2],unsigned leaves)
+{
+    struct shadow s=shadow_of();unsigned i=0;
+    for(int again=0;;again=1) {
+        if(!only_failing)i=0;
+        while(i<leaves && sprr_views_prepare(&views,&s,va_of(leaf[i][0],leaf[i][1],0)))i++;
+        if(i==leaves)return 1;
+        if(again || views.count+3<=SPRR_VIEW_TABLES)return 0;
+        if(reclaim()<=0)return 0;
+    }
+}
+/* sptm_retype_rozone/txm_default: prepare, detach, commit, refresh. */
+static int protect_change(const unsigned (*leaf)[2],unsigned leaves,uint64_t selector)
+{
+    if(!prepare_change(leaf,leaves) || !refresh())return 0;
+    for(unsigned n=0;n<leaves;n++)for(unsigned i=0;i<4;i++)
+        put(L3(leaf[n][0],leaf[n][1])+8UL*i,frame(leaf[n][0],leaf[n][1],i)+selector);
+    return refresh();
+}
+static int protect(unsigned k,unsigned j,uint64_t selector)
+{
+    const unsigned leaf[1][2]={{k,j}};
+    return protect_change(leaf,1,selector);
+}
+static int release(unsigned k,unsigned j)
+{
+    for(unsigned i=0;i<4;i++)put(L3(k,j)+8UL*i,frame(k,j,i)+SEL3);
+    return refresh();
+}
+static void build(void)
+{
+    memset(ram,0,sizeof ram);memset(dirty,0,sizeof dirty);memset(stale,0,sizeof stale);
+    memset(&views,0,sizeof views);memset(&pub,0,sizeof pub);
+    next_copy=COPIES;allocs=0;alloc_budget=PAGES;read_fail=0;
+    stale_writes=quiesce_fails=quiesce_no_tlbi=0;
+    put(BASE,L1+3);
+    for(unsigned k=0;k<4;k++) {
+        put(L1+8UL*k,L2(k)+3);
+        for(unsigned j=0;j<128;j++) {
+            put(L2(k)+8UL*j,L3(k,j)+3);
+            for(unsigned i=0;i<8;i++)put(L3(k,j)+8UL*i,frame(k,j,i)+SEL3);
+        }
+    }
+    for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++)pp[cpu]=SPRR_PPERM_INITIAL|(cpu&1 ? 0x100 : 0);
+    struct shadow s=shadow_of();
+    CHECK(sprr_views_init(&views,&s) && refresh());
+}
+static unsigned char saved_ram[BYTES];
+static struct sprr_views saved_views;
+static void snapshot(void) {memcpy(saved_ram,ram,sizeof ram);saved_views=views;}
+static int unchanged(void)
+{return !memcmp(saved_ram,ram,sizeof ram) && !memcmp(&saved_views,&views,sizeof views);}
+
+int main(void)
+{
+    struct shadow s;
+    build();s=shadow_of();invariants();
+    /* Fill: 128 level-3 tables under level 2 #0, 64 under #1 (the first eight
+     * TXM selector4), then #2 until the pool holds 256 (root, level 1, three
+     * level 2, 251 level 3). */
+    unsigned filled=0;
+    for(unsigned k=0;k<3 && views.count<SPRR_VIEW_TABLES;k++)
+        for(unsigned j=0;j<(k==1 ? 64u : 128u) && views.count<SPRR_VIEW_TABLES;j++) {
+            if(views.count==SPRR_VIEW_TABLES-1) {
+                /* One slot left, a path needing two: refused before any add. */
+                snapshot();uint64_t allocated=allocs;
+                CHECK(!sprr_views_prepare(&views,&s,va_of(3,0,0)) && unchanged() && allocs==allocated);
+            }
+            CHECK(protect(k,j,(k==1 && j<8) ? SEL4 : SEL2));filled++;
+        }
+    CHECK(views.count==SPRR_VIEW_TABLES && filled==251 && !quiesces && allocs==6u*SPRR_VIEW_TABLES);
+    invariants();
+    /* Full: the next path needs a level-2 and a level-3 copy. Nothing changes,
+     * nothing is allocated, and a reclaim finds nothing to retire. */
+    snapshot();uint64_t before=allocs;
+    CHECK(!sprr_views_prepare(&views,&s,va_of(3,0,0)) && unchanged() && allocs==before);
+    CHECK(sprr_views_reclaim(&views,&s,quiesce,0)==0 && unchanged() && !quiesces);
+    CHECK(!protect(3,0,SEL2) && unchanged() && !quiesces);
+    /* Refusals before any change: unconfigured, no quiesce, a read failure. */
+    struct shadow wrong=s;wrong.root=L1;
+    CHECK(sprr_views_reclaim(&views,&wrong,quiesce,0)==-1 && unchanged());
+    CHECK(sprr_views_reclaim(&views,&s,0,0)==-1 && unchanged());
+    CHECK(release(0,5) && release(0,6));
+    snapshot();
+    read_fail=L3(0,5)+8*300;   /* no protected leaf: its scan reads every word */
+    CHECK(sprr_views_reclaim(&views,&s,quiesce,0)==-1 && unchanged() && !quiesces);
+    read_fail=0;
+    /* Release: two tables under level 2 #0, the eight TXM tables turned
+     * fixed RO selector11 (an import), and every table under level 2 #2: that
+     * level-2 copy goes too. */
+    for(unsigned j=0;j<8;j++)for(unsigned i=0;i<4;i++)put(L3(1,j)+8UL*i,frame(1,j,i)+SEL11);
+    for(unsigned j=0;j<128;j++)if(find_source(L3(2,j))>=0)CHECK(release(2,j));
+    CHECK(refresh());invariants();
+    uint64_t order[SPRR_VIEW_TABLES];unsigned kept=0;
+    unsigned under2=0;
+    for(unsigned j=0;j<128;j++)under2+=find_source(L3(2,j))>=0;
+    for(unsigned n=0;n<views.count;n++) {
+        uint64_t src=views.tables[n].source;
+        int dead=src==L3(0,5) || src==L3(0,6) || src==L2(2) || (src>=L3(1,0) && src<L3(1,8)) ||
+                 (src>=L3(2,0) && src<L3(3,0));
+        if(!dead)order[kept++]=src;
+    }
+    unsigned count=(unsigned)views.count;
+    uint64_t retired_pages[SPRR_VIEW_TABLES*SPRR_VIEW_CPUS];unsigned retired=0;
+    for(unsigned n=0;n<views.count;n++)if(find_source(views.tables[n].source)>=0) {
+        uint64_t src=views.tables[n].source;
+        int dead=src==L3(0,5) || src==L3(0,6) || src==L2(2) || (src>=L3(1,0) && src<L3(1,8)) ||
+                 (src>=L3(2,0) && src<L3(3,0));
+        if(dead)for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++)retired_pages[retired++]=views.tables[n].copy[cpu];
+    }
+    unsigned tlbis_before=tlbis;
+    int got=reclaim();
+    CHECK(got==(int)(2+8+under2+1) && views.count==count-(unsigned)got && quiesces==1 && tlbis==tlbis_before+1);
+    CHECK(views.count==kept);
+    for(unsigned n=0;n<kept;n++)CHECK(views.tables[n].source==order[n]);
+    CHECK(find_source(L2(2))<0 && find_source(L2(0))>=0 && find_source(L1)>=0);
+    for(unsigned n=views.count;n<count;n++)CHECK(!views.tables[n].level && !views.tables[n].source);
+    invariants();
+    /* Reuse: new paths take the retired pages, in position order, before the
+     * allocator is asked again; their stale words are rewritten by the sync. */
+    before=allocs;unsigned reused=0;
+    for(unsigned j=0;j<128 && views.count<count;j++) {
+        unsigned n=(unsigned)views.count;
+        uint64_t want[SPRR_VIEW_CPUS];memcpy(want,views.tables[n].copy,sizeof want);
+        CHECK(protect(3,j,SEL2));
+        for(unsigned m=n;m<views.count;m++)for(unsigned cpu=0;cpu<SPRR_VIEW_CPUS;cpu++) {
+            int known=0;
+            for(unsigned r=0;r<retired;r++)known|=retired_pages[r]==views.tables[m].copy[cpu];
+            CHECK(known);reused++;
+        }
+        CHECK(!memcmp(want,views.tables[n].copy,sizeof want));
+    }
+    CHECK(allocs==before && reused==(unsigned)got*SPRR_VIEW_CPUS && views.count==count);
+    invariants();
+    /* Full again: a protect reclaims inside (kernel_views_prepare_change's
+     * retry) and lands on the retired sets. */
+    for(unsigned j=0;j<8;j++)CHECK(release(3,j));
+    before=allocs;unsigned q=quiesces;
+    CHECK(protect(2,0,SEL2) && quiesces==q+1 && allocs==before && views.count==SPRR_VIEW_TABLES-8+2);
+    invariants();
+    /* A failed quiesce: the views hold only kept tables, the retired pages are
+     * never written or reused (the slot refuses), nothing is allocated. */
+    CHECK(release(3,8) && release(3,9));
+    quiesce_fails=1;before=allocs;count=(unsigned)views.count;
+    CHECK(sprr_views_reclaim(&views,&s,quiesce,0)==-1 && views.count==count-2);
+    CHECK(views.tables[views.count].level==SPRR_VIEW_RETIRED && views.tables[views.count+1].level==SPRR_VIEW_RETIRED);
+    unsigned writes_before=stale_writes;
+    CHECK(!sprr_views_prepare(&views,&s,va_of(3,8,0)) && allocs==before && stale_writes==writes_before);
+    CHECK(views.tables[views.count].level==SPRR_VIEW_RETIRED);
+    /* Everything released: the views shrink to the root. */
+    build();s=shadow_of();
+    for(unsigned k=0;k<4;k++)for(unsigned j=0;j<16;j++)CHECK(protect(k,j,SEL2));
+    for(unsigned k=0;k<4;k++)for(unsigned j=0;j<16;j++)CHECK(release(k,j));
+    CHECK(reclaim()==1+4+64 && views.count==1);
+    invariants();
+    CHECK(protect(1,1,SEL4) && views.count==4 && allocs==6u*(1+1+4+64));
+    invariants();
+    /* Past the 69 parked sets the allocator serves again. */
+    for(unsigned j=0;j<71;j++)CHECK(protect(3,j,SEL2));
+    CHECK(views.count==4+1+71 && allocs==6u*(1+1+4+64+6));
+    invariants();
+    for(unsigned j=0;j<71;j++)CHECK(release(3,j));
+    CHECK(reclaim()==72 && views.count==4);
+    /* Harness self-checks. A quiesce without its TLBI lets the reuse store
+     * into a page a walk cache may still hold: caught. */
+    CHECK(release(1,1));quiesce_no_tlbi=1;
+    CHECK(reclaim()==3);
+    CHECK(sprr_views_prepare(&views,&s,va_of(2,2,0)) && sync_publish() && stale_writes);
+    /* A two-frame change (a SLIDE_REGION alias) at 255 tables: its first
+     * path fits, its second needs two tables. The reclaim retires the first
+     * one too (its leaves are not protected yet), so the whole change is
+     * prepared again; retrying the refused leaf alone would leave the first
+     * frame's raw selector2 leaves in a shared table. */
+    for(int wrong=0;wrong<2;wrong++) {
+        build();s=shadow_of();
+        for(unsigned j=0;j<127;j++)CHECK(protect(0,j,SEL2));
+        for(unsigned j=0;j<124;j++)CHECK(protect(1,j,SEL2));
+        CHECK(views.count==SPRR_VIEW_TABLES-1 && release(1,5) && release(1,6));
+        const unsigned two[2][2]={{0,127},{3,100}};
+        only_failing=wrong;unsigned q2=quiesces;
+        CHECK(protect_change(two,2,SEL2) && quiesces==q2+1);
+        only_failing=0;
+        CHECK(find_source(L2(3))>=0 && find_source(L3(3,100))>=0 && find_source(L3(1,5))<0);
+        CHECK((find_source(L3(0,127))>=0)==!wrong && !view_mismatches()==!wrong);
+        if(!wrong) {CHECK(views.count==SPRR_VIEW_TABLES);invariants();}
+        else {
+            CHECK(view_mismatches()==4*SPRR_VIEW_CPUS);
+            const unsigned again[1][2]={{0,127}};
+            CHECK(prepare_change(again,1) && refresh() && !view_mismatches());
+        }
+    }
+    /* A protected table dropped from the views is visible to the walk check. */
+    build();s=shadow_of();
+    CHECK(protect(0,0,SEL2) && protect(0,1,SEL2) && !view_mismatches());
+    struct sprr_views good=views;
+    int victim=find_source(L3(0,1));CHECK(victim==(int)views.count-1);
+    views.count--;sprr_publish_reset(&pub);
+    CHECK(sync_publish() && view_mismatches()==4*SPRR_VIEW_CPUS);
+    views=good;sprr_publish_reset(&pub);CHECK(sync_publish() && !view_mismatches());
+    printf("view reclaim: %u quiesces, %u TLBIs, %llu pages allocated\n",quiesces,tlbis,
+           (unsigned long long)allocs);
+    printf("%s: %u view reclaim checks, %u failures\n",failed ? "FAIL" : "PASS",checks,failed);
+    return failed ? 1 : 0;
+}

tools/test-view-reclaim.py

@@ -0,0 +1,200 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: MIT
+"""--view-reclaim, offline: the kernel view pool's reclaim against a monitor-shaped model, weakened implementations it
+must reject, the consumers that index tables by position, the opt-in wiring and (on request) the monitor's identity
+and size. No hardware.
+
+    python3 tools/test-view-reclaim.py                                    # model, mutants, consumers, wiring
+    python3 tools/test-view-reclaim.py --build --qualification QUAL.json  # + monitors: define absent, =0, =1
+
+Model: tools/test-view-reclaim.c (ASan/UBSan, -DSNAP_VIEW_RECLAIM=1) fills the 256-table pool, releases, reclaims,
+reuses the retired pages and checks every CPU's walk, publication and the no-store-before-TLBI rule (its header lists
+them). Each MUTANTS entry weakens one property in a copy of shadow/sprr-view.c; the same program must FAIL on every one.
+Consumers: tools/test-kernel-pperm-variants.c (reuse snapshot, publication rows, PPERM variant columns) with and
+without the define.
+
+Wiring: shadow/sprr-view.h defaults SNAP_VIEW_RECLAIM to 0 and every monitor use sits under it; installed-fresh
+--view-reclaim appends the define last; the report record's place agrees between probes/xnuboot/report_layout.c and
+tools/perf_counters.py, whose decoder refuses an inconsistent record.
+
+--build: xnuboot with each --qualification's flags, define absent, =0 and =1: absent == =0 == the qualification's
+monitor_sha256; =1 differs and fits the code budget (probes/run.py OUT_AT - CODE_AT), its headroom printed.
+"""
+from pathlib import Path
+import argparse
+import json
+import re
+import shutil
+import struct
+import subprocess
+import sys
+import tempfile
+import types
+import unittest
+
+ROOT = Path(__file__).resolve().parents[1]
+sys.path.insert(0, str(ROOT / 'tools'))
+
+_ap = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter)
+_ap.add_argument('--build', action='store_true')
+_ap.add_argument('--qualification', action='append', default=[])
+_ap.add_argument('--out')
+ARGS, REST = _ap.parse_known_args() if __name__ == '__main__' else (_ap.parse_args([]), [])
+CC = ['cc', '-std=gnu11', '-O1', '-g', '-fsanitize=address,undefined', '-fno-sanitize-recover=all',
+      '-Wall', '-Wextra', '-Werror', '-Icompat', '-Ishadow']
+VIEW = ['shadow/shadow.c', 'shadow/mmu.c']
+MUTANTS = (
+    ('selector2 tables retired', 'need=(UINT32_C(0x214)>>', 'need=(UINT32_C(0x210)>>'),
+    ('retired pages dropped by the compaction',
+     '        struct sprr_view_table t=v->tables[w];\n        v->tables[w++]=v->tables[n];v->tables[n]=t;',
+     '        v->tables[w++]=v->tables[n];'),
+    ('no room check before the adds', '    if(v->count+missing>SPRR_VIEW_TABLES)return 0;\n', '    (void)missing;\n'),
+    ('a retired set reused before its invalidation', '    if(t->level)return 0;\n', '\n'),
+    ('pages freed before the quiesce',
+     '    v->count=w;\n    if(!quiesce(ctx))return -1;\n    for(unsigned n=w;n<count;n++)v->tables[n].level=0;',
+     '    v->count=w;\n    for(unsigned n=w;n<count;n++)v->tables[n].level=0;\n    if(!quiesce(ctx))return -1;'),
+    ('the quiesce before the unlinking',
+     '    for(unsigned n=w;n<count;n++) {v->tables[n].source=0;v->tables[n].level=SPRR_VIEW_RETIRED;}\n'
+     '    v->count=w;\n    if(!quiesce(ctx))return -1;',
+     '    if(!quiesce(ctx))return -1;\n'
+     '    for(unsigned n=w;n<count;n++) {v->tables[n].source=0;v->tables[n].level=SPRR_VIEW_RETIRED;}\n'
+     '    v->count=w;'),
+    ('an upper table kept for a retired child',
+     'need=child>=0 && (v->tables[child].level!=level+1 || keep[child]);', 'need=child>=0;'),
+    ('the root retired', '        int need=!level;\n', '        int need=0;\n'),
+    ('retired sets never reused', '        uint64_t pa=t->copy[cpu] ? t->copy[cpu] : shadow_alloc_page(s);',
+     '        uint64_t pa=shadow_alloc_page(s);'),
+)
+
+
+def work():
+    return Path(ARGS.out) if ARGS.out else Path(tempfile.mkdtemp(prefix='view-reclaim-'))
+
+
+def compile_run(test, view, binary, *defines):
+    b = subprocess.run([*CC, *defines, test, str(view), *VIEW, '-o', str(binary)], cwd=ROOT,
+                       capture_output=True, text=True)
+    if b.returncode:
+        return None, b.stderr[-2000:]
+    r = subprocess.run([str(binary)], cwd=ROOT, capture_output=True, text=True, timeout=1800)
+    return r.returncode, (r.stdout + r.stderr)
+
+
+class Model(unittest.TestCase):
+    def test_model_passes(self):
+        rc, out = compile_run('tools/test-view-reclaim.c', ROOT / 'shadow/sprr-view.c', work() / 'model',
+                              '-DSNAP_VIEW_RECLAIM=1')
+        self.assertEqual(rc, 0, out[-3000:])
+        self.assertIn('PASS:', out)
+        print('\n' + out.strip().splitlines()[-1], file=sys.stderr)
+
+    def test_mutants_fail(self):
+        source = (ROOT / 'shadow/sprr-view.c').read_text()
+        out_dir = work()
+        for n, (name, old, new) in enumerate(MUTANTS):
+            self.assertEqual(source.count(old), 1, name)
+            d = out_dir / f'mutant-{n}'
+            d.mkdir(parents=True, exist_ok=True)
+            (d / 'sprr-view.c').write_text(source.replace(old, new))
+            rc, out = compile_run('tools/test-view-reclaim.c', (d / 'sprr-view.c').resolve(), (d / 't').resolve(),
+                                  '-DSNAP_VIEW_RECLAIM=1')
+            self.assertIsNotNone(rc, f'{name}: {out}')
+            self.assertNotEqual(rc, 0, f'{name}: not caught')
+
+
+class Consumers(unittest.TestCase):
+    def test_variants_snapshot_publication(self):
+        for defines in ([], ['-DSNAP_VIEW_RECLAIM=1']):
+            rc, out = compile_run('tools/test-kernel-pperm-variants.c', ROOT / 'shadow/sprr-view.c',
+                                  work() / f'variants{len(defines)}', *defines)
+            self.assertEqual(rc, 0, out[-3000:])
+            self.assertIn('PASS:', out)
+            self.assertEqual('reclaim:' in out, bool(defines))
+
+
+class Wiring(unittest.TestCase):
+    def test_default_off(self):
+        header = (ROOT / 'shadow/sprr-view.h').read_text()
+        self.assertIn('#ifndef SNAP_VIEW_RECLAIM\n#define SNAP_VIEW_RECLAIM 0\n#endif', header)
+        self.assertIn('#if SNAP_VIEW_RECLAIM\n#define SPRR_VIEW_TABLES 256u\n#else\n#define SPRR_VIEW_TABLES 128u\n#endif',
+                      header)
+        for path in ('probes/xnuboot/sptm_retype.c', 'probes/xnuboot/kernel_views.c', 'probes/xnuboot/report.c',
+                     'probes/xnuboot/context.c'):
+            stack = []
+            for number, line in enumerate((ROOT / path).read_text().splitlines(), 1):
+                d = line.strip()
+                if d.startswith('#if'):
+                    stack.append([d == '#if SNAP_VIEW_RECLAIM', False])
+                elif d.startswith('#el') and stack:
+                    stack[-1][1] = True
+                elif d.startswith('#endif'):
+                    stack.pop()
+                elif re.search(r'kernel_views_prepare_change|kernel_view_reclaim|sprr_views_reclaim', line):
+                    self.assertTrue(any(on and not other for on, other in stack), f'{path}:{number} unguarded')
+
+    def test_cycle(self):
+        from cycle_lib import installed_fresh as f
+        import importlib.util
+        spec = importlib.util.spec_from_file_location('cycle_cli', ROOT / 'tools/cycle.py')
+        cli = importlib.util.module_from_spec(spec)
+        spec.loader.exec_module(cli)
+        base = ['installed-fresh', '--prefix', 'x', '--variant', 'fast', '--check']
+        self.assertFalse(cli.parse(base).view_reclaim)
+        self.assertTrue(cli.parse(base + ['--view-reclaim']).view_reclaim)
+        self.assertEqual(f.VIEW_RECLAIM_DEFINE, '-DSNAP_VIEW_RECLAIM=1')
+        src = (ROOT / 'tools/cycle_lib/installed_fresh.py').read_text()
+        body = src[src.index('def variant_flags('):]
+        body = body[:body.index('\n    return flags\n')]
+        self.assertTrue(body.rstrip().endswith('flags.append(VIEW_RECLAIM_DEFINE)'), 'the define is not appended last')
+        self.assertNotIn('view_reclaim', f.boot_addition(types.SimpleNamespace(view_reclaim=True)))
+
+    def test_report_record(self):
+        import runpy
+        pc = runpy.run_path(str(ROOT / 'tools/perf_counters.py'))
+        layout = (ROOT / 'probes/xnuboot/report_layout.c').read_text()
+        expr = re.search(r'#define OUT_VIEW_RECLAIM \(OUT_THERMAL([^)]*)\)', layout).group(1)
+        thermal = int(re.search(r'#define A16_THERMAL_REPORT_OFFSET (0x[0-9a-f]+)u',
+                                (ROOT / 'compat/a16-thermal.h').read_text()).group(1), 16) // 8
+        terms = re.findall(r'-\s*(\w+)', expr)
+        self.assertEqual(''.join(re.findall(r'\S', expr)), ''.join('-' + t for t in terms))
+        word = thermal - sum(6 if t == 'VIEW_RECLAIM_WORDS' else int(t) for t in terms)
+        offset, size = pc['view_reclaim_spec']()
+        self.assertEqual((offset, size), (16 + 8 * word, 64))
+        good = struct.pack('<8Q', pc['VIEW_RECLAIM_MAGIC'], 48 << 32, 140, 256, 2, 9, 0, 256)
+        self.assertEqual(pc['decode_view_reclaim'](good)['free'], 116)
+        for bad in (dict(magic=0), dict(count=0), dict(count=257), dict(high=139), dict(retired=1), dict(cap=128)):
+            w = [pc['VIEW_RECLAIM_MAGIC'], 48 << 32, 140, 256, 2, 9, 0, 256]
+            w[0] = bad.get('magic', w[0]); w[2] = bad.get('count', w[2]); w[3] = bad.get('high', w[3])
+            w[5] = bad.get('retired', w[5]); w[7] = bad.get('cap', w[7])
+            with self.assertRaises(ValueError, msg=str(bad)):
+                pc['decode_view_reclaim'](struct.pack('<8Q', *w))
+
+
+@unittest.skipUnless(ARGS.build, 'pass --build to compile the monitor (minutes)')
+class Build(unittest.TestCase):
+    def test_monitor(self):
+        import monitor_build_offline as mbo
+        out = work() / 'monitors'
+        run = (ROOT / 'probes/run.py').read_text()
+        budget = int(re.search(r'^OUT_AT = (0x[0-9a-fA-F]+)', run, re.M).group(1), 16) - \
+            int(re.search(r'^CODE_AT = (0x[0-9a-fA-F]+)', run, re.M).group(1), 16)
+        results = {}
+        for path in ARGS.qualification:
+            record = json.loads(Path(path).read_text())
+            name, blobs = Path(path).parent.name, {}
+            for label, extra in (('default', []), ('off', ['-DSNAP_VIEW_RECLAIM=0']), ('on', ['-DSNAP_VIEW_RECLAIM=1'])):
+                d = out / f'{name}-{label}'
+                if d.exists():
+                    shutil.rmtree(d)
+                r = mbo.build(ROOT, d, list(record['flags']) + extra)
+                blobs[label] = r['sha256']
+                results[f'{name}-{label}'] = dict(bytes=r['bytes'], headroom=budget - r['bytes'], sha256=r['sha256'])
+                self.assertGreater(budget - r['bytes'], 0, f'{name}-{label} exceeds the code budget')
+            self.assertEqual(blobs['default'], record['monitor_sha256'], name)
+            self.assertEqual(blobs['off'], blobs['default'], name)
+            self.assertNotEqual(blobs['on'], blobs['default'], name)
+        print(json.dumps(results, indent=1), file=sys.stderr)
+
+
+if __name__ == '__main__':
+    unittest.main(argv=[sys.argv[0], *REST])