tests: cover kernel view reclaim and the 256-table pool

tools/test-view-reclaim.c drives a monitor-shaped kernel tree (one root,
one level 1, four level 2, 512 level 3) the way the retypes do: prepare,
detach, commit, refresh, with kernel_views_quiesce's steps as the
quiesce. After every step, independently of the library: each CPU's
walk of all 16,384 leaves gives the canonical descriptor or, for
selector2/4, its translation under that CPU's PPERM; no reachable page
holds an unpublished store; copies are distinct and never sources; no
store reaches a retired page before the TLBI after its unlinking.
Scenarios: fill to 256, a full pool and a one-slot-short path refuse
with no change, release and reclaim (TXM import, the level-2 ancestor),
reuse of the retired pages before any allocation, reclaim down to the
root, the restart of a two-frame change, read failure, nothing to
retire, unconfigured views and a failed quiesce. A quiesce without its
TLBI and a dropped protected table are caught (harness self-checks).

tools/test-view-reclaim.py runs it, nine weakened sprr-view.c copies
(each must fail: all do), test-kernel-pperm-variants.c with and without
the define, the wiring (default off, guarded uses, cycle, report place
and decoder) and, with --build, the monitor identities.
test-kernel-pperm-variants.c gains reclaim steps under the define:
positions move under the reuse snapshot, publication rows and variant
columns while both machines keep agreeing.

Tests that hard-coded the 128-table shape now derive it from
SPRR_VIEW_TABLES / USER_PUBLISH_MAX (test-tpro-view.c's RAM,
test-user-prepare-fused.c, test-user-fused-compare.c,
test-user-publish.c, test-user-tree-memo.c); define-off they check
exactly what they did.

Results on this tree (host, ASan/UBSan):
  python3 tools/test-view-reclaim.py              PASS (model 20,578
      checks; 9/9 mutants caught; consumers; wiring)
  python3 tools/test-view-reclaim.py --build --qualification
      .../installed-fresh-desktop-20261024-next1/qualification.json
                                                  PASS (absent == =0 ==
      86bb02ea9e03...; =1 459,904 bytes, 15,232 headroom)
  the 26 C suites linking sprr-view.c, with and without
      -DSNAP_VIEW_RECLAIM=1                      PASS (define-off check
      counts equal the base commit's)
Hardware: not run.

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-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])