The Kf-family spinlock exports were registered as stubs:
KfAcquireSpinLock → stub_return_zero (didn't write lock)
KfReleaseSpinLock → stub_success (didn't clear lock)
KeReleaseSpinLockFromRaisedIrql → stub_success (same)
KeTryToAcquireSpinLockAtRaisedIrql → returned 1 but didn't set lock value
Guest code that read the lock value back (e.g. nested
acquire/release sanity checks, debug assertions) saw 0 even after
"acquiring", and could enter critical regions without contention
serialization. Under `--parallel` the coarse Arc<Mutex<KernelState>>
already serializes us, so the audit's P0-under-parallel ranking is
about correctness of the lock value visible to guest code, not
mutual-exclusion (which is provided by the host mutex).
Implementation mirrors canary's
`xenia-canary/src/xenia/kernel/xboxkrnl/xboxkrnl_threading.cc`:
- KfAcquireSpinLock: write 1 to *SpinLock, return 0 (old IRQL)
- KfReleaseSpinLock: write 0 to *SpinLock
- KeReleaseSpinLockFromRaisedIrql: write 0 to *SpinLock
- KeTryToAcquireSpinLockAtRaisedIrql: write 1 to *SpinLock, return 1
Single-threaded HLE: contention can never be observed (we never run
two guest threads simultaneously without holding the kernel mutex),
so the spin-loop can degenerate to an unconditional acquire.
Verification at -n 100M lockstep:
swaps: 2 → 2 (unchanged)
draws: 0 → 0 (gated by F2/F3/G)
packets: ~59M (within noise)
Tests: 76 kernel pass (no count change; existing harness covers the
new write semantics implicitly via guest-memory smoke tests).
Closes KRNBUG-017 (P0 under --parallel).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
e7d0fcf2c9