#### DF-0918 run.log (deterministic models) ####
## (run on the unpatched #0 kernel, as maxx uid 1001)

==== [1] UNFIXED model — should CONFIRM the NULL-ohd primitive ====
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
DF-0918 deterministic NULL-ohd harness
modeling fuse_ipc_wait early-return (fuse_ipc.c:163,169,173)
         vs fuse_mount_kill+fuse_device_clear (fuse_vfsops.c:69 + fuse_device.c:111-115)
         + fuse_ipc_tx:274-275 (ohd = fuse_out(fip); KKASSERT(ohd))
fip=0x8004a0630 reply.buf=0x0 (NULL by design, fuse_ipc.c:104)

(UNFIXED model: waiter trusts replied without dead recheck)

[tx-waiter] replied set -> return 0 (NO dead recheck)
[tx-waiter] *** NULL-ohd CONFIRMED *** fuse_out(fip)=NULL;
          fuse_ipc.c:275 KKASSERT(ohd) PANIC (INVARIANTS) or
          fuse_ipc.c:276 ohd->error NULL-deref.
[tx-waiter] RESULT: primitive reproduced (NULL fuse_out -> panic).

RESULT: NULL-ohd PRIMITIVE reproduced deterministically.
The early-return trusted `replied` without rechecking dead;
fuse_device_clear set replied with reply.buf still NULL, so
fuse_ipc.c:275 KKASSERT(ohd) fires (panic on default GENERIC).
harness(unfixed) rc=0

==== [2] FIXED model — should show NO NULL-deref (dead recheck) ====
DF-0918 deterministic NULL-ohd harness
modeling fuse_ipc_wait early-return (fuse_ipc.c:163,169,173)
         vs fuse_mount_kill+fuse_device_clear (fuse_vfsops.c:69 + fuse_device.c:111-115)
         + fuse_ipc_tx:274-275 (ohd = fuse_out(fip); KKASSERT(ohd))
fip=0x8004a0630 reply.buf=0x0 (NULL by design, fuse_ipc.c:104)

(FIXED model: waiter rechecks dead after replied — fix.diff)

[tx-waiter] replied set by teardown + dead=1 -> ENOTCONN (fix)
[tx-waiter] RESULT: fix returned ENOTCONN (no NULL deref).

RESULT: FIXED model — NO NULL-deref.  dead-recheck after replied
(fix.diff) returns ENOTCONN when fuse_device_clear set replied
during teardown, so fuse_ipc_tx:275 never derefs NULL ohd.
harness(fixed) rc=0