{
  "finding_id": "DF-3093",
  "status": "not_reproduced",
  "reproduced": false,
  "impact": "none",
  "confidence": "likely",
  "verdict": "Premise verified, manifestation not reproduced. MSDOSFS_LOCK_MP/UNLOCK_MP are literally empty macros (msdosfsmount.h:216-218), struct msdosfsmount has no lock member, and a diagnostic kernel (instr.patch: stock code + counters + a print-only form of the INVARIANTS KASSERT at msdosfs_fat.c:381) PROVED the race window opens in practice: >200 clusteralloc critical-section overlap events, up to 3 CPUs deep, under 6 CPU-pinned barrier-synchronized writers. But the claimed double-allocation never occurred: across ~4 hours, ~500 synchronized allocation bursts and 6 adversarial geometries (64MiB-2GiB FAT16/FAT32 volumes, fallback-scan-forcing fragmentation, half-word and word-straddling free runs, 100us/200us delay-injected kernels widening the decide window 1000x), debug.df3093_double stayed 0, every offline FAT in-degree scan was clean, no foreign bytes, no Freeing unused sector messages. The pure-memory scan phase (bitmap read to first bit set) is sub-microsecond and the allocators pm_nxtfree-advance + strictly-greater tie-break (msdosfs_fat.c:756/768) effectively serialize run claiming, so two CPUs never commit the same run. The INVARIANTS-panic and release-kernel cross-link claims remain theoretical on this hardware; the missing lock is still a genuine hardening defect worth fixing (FreeBSD added pm_fatmutex for this surface).",
  "exploit_chain": "",
  "evidence": "trace-excerpts.txt [2]/[2b] (kernel counters: 66 and +137 overlap events, 0 doubles on the timing-unmodified kernel); VERDICT.md What was verified TRUE + Why the race window does not convert; fat_scan clean results in run4.log/run6.log; instr.patch is the exact diagnostic kernel",
  "kernel_refs": [
    "sys/vfs/msdosfs/msdosfsmount.h:216",
    "sys/vfs/msdosfs/msdosfs_fat.c:726",
    "sys/vfs/msdosfs/msdosfs_fat.c:756",
    "sys/vfs/msdosfs/msdosfs_fat.c:768",
    "sys/vfs/msdosfs/msdosfs_fat.c:381"
  ],
  "poc_changes": "Replaced the staggered v1 racestress with race2.c (CPU pinning via usched_set(2), per-cache-line barrier words, pre-created/pre-opened files, single large write(2) per round, errno/timing capture); added fat_scan.c (offline FAT in-degree cross-link detector); added run3-6.sh geometries forcing the fallback scan and word-straddling bitmap RMW overlaps; added instr.patch diagnostic kernel (sysctls debug.df3093_{inflight,overlaps,double}).",
  "attempts": 9,
  "guest_uname": "DragonFly dfbsd 6.5-DEVELOPMENT DragonFly 6.5-DEVELOPMENT #0: Thu Jul  2 06:02:54 UTC 2026 root@dfbsd:/usr/obj/usr/src/sys/X86_64_GENERIC x86_64",
  "runtime_sec": 14400,
  "guest_dirty": 0,
  "build_cmd": "cc -O2 -o race2 race2.c && cc -O2 -o fat_scan fat_scan.c",
  "run_cmd": "sh run2.sh 20 6 3 2097152; sh run4.sh 2 6 2 16777216; sh run6.sh 2 6 2 16777216",
  "code_hash": "28ec543c3b7ca8edf3b3392e1ced415b30cee67bb9837ea83806b8bb83731261",
  "notes": "Guest was reverted to the clean-source snapshot after the diagnostic-kernel work (uname #0 Jul 2, msdosfs_fat.c md5 matches the audited tree). Mount gating: vnconfig+mount_msdos require root (or vfs.usermount=1 with an accessible device); the trigger itself is plain write(2) by any user once the mount exists. Anomaly documented in trace-excerpts.txt [3]: on the DELAY-injected kernels the extend phases serialized completely (0 overlaps) while the timing-unmodified kernel showed free overlap \u2014 unresolved diagnostic artifact, does not affect the stock-kernel measurements. No fix.diff: nothing reproduced to validate against; the recommended fix (real lock behind MSDOSFS_LOCK_MP) stands as hardening.",
  "recommended_fix": "implement a real per-mount lock (or lwkt token) behind MSDOSFS_LOCK_MP/UNLOCK_MP and lockinit/destroy it in msdosfs_mount/unmount, serializing clusteralloc/chainalloc/usemap_* like FreeBSDs pm_fatmutex",
  "fix_status": "not_testable",
  "fix_baseline_reproduced": 0,
  "fix_patched_reproduced": 0,
  "fix_verdict": "n/a \u2014 not reproduced, nothing to A/B",
  "fix_evidence": ""
}