DF-1061 / verify.sh
#!/bin/sh # DF-1061 โ pmap_inval LOOPRECOVER watchdog silent TLB-invalidation abandonment # Static source verification (runtime trigger needs host-induced vCPU stall > 2s). # # Confirms (per the finding's static-verification fallback, finding markdown lines # 124-132) that: # (1) CPUMASK_ASSZERO(info->done) is the force-clear in both "A" and "B" paths # (2) info->failed is written but never read (dead) โ no caller can detect abandonment # (3) the target clears its done bit only AFTER cpu_invlpg() (so a still-set bit means # the invalidation has NOT happened on that cpu) # (4) the sibling "C" path does NOT abandon โ it re-broadcasts the IPI # # Run from the repo root (sys/ must be present). set -e F=sys/platform/pc64/x86_64/pmap_inval.c echo "=== (1) force-clear in 'A' (pmap_inval_smp) and 'B' (pmap_inval_smp_cmpset) ===" grep -nE "CPUMASK_ASSZERO\(info->done\)|loopdebug\(\"[AB]\"|XXX recover" "$F" echo echo "=== (2) info->failed: writers only, no readers ===" echo "writers (5 expected):" grep -n "info->failed" "$F" echo "readers (any non-assignment use, expect 0):" grep -nE "info->failed[^[:space:]]*=|if.*info->failed|return.*info->failed| [!]?info->failed" "$F" | grep -v "info->failed[[:space:]]*=" || echo " (none โ confirmed dead)" echo echo "=== (3) target clears done AFTER cpu_invlpg (pmap_inval_intr) ===" sed -n '750,775p' "$F" | grep -nE "cpu_invlpg|info->done|npgs" echo echo "=== (4) sibling 'C' path re-broadcasts (does NOT abandon) ===" sed -n '780,800p' "$F" | grep -nE "loopdebug\(\"C\"|ATOMIC_CPUMASK_NANDMASK|smp_invlpg|recover" echo echo "=== (5) LOOPRECOVER is unconditionally #define-d (not a kernel option) ===" grep -nE "^#define LOOPRECOVER\b|LOOPRECOVER_TIMEOUT1|LOOPRECOVER_TIMEOUT2" "$F" echo echo "=== (6) Xinvltlb fires at interrupt level (mp_machdep.c) โ cannot be held off ===" sed -n '1160,1175p' sys/platform/pc64/apic/mpapic.c 2>/dev/null || true grep -nE "Xinvltlb|INTRTYPE" sys/platform/pc64/x86_64/mp_machdep.c 2>/dev/null | head -5 || true echo echo "DONE: all six static checks executed." |