julia

4741f50f - devdocs: Model spinner accounting in the scheduler-wakeup TLA+ spec

devdocs: Model spinner accounting in the scheduler-wakeup TLA+ spec Extend SchedulerWake.tla with the spinner protocol: per-thread spinner slots with the pool n_spinning counter, the gated jl_wakeup_threadpool (wake nobody while a spinner exists), the slot release as a separate atomic step before the sleeping-store so TLC explores the race window the store-buffering fences close in the C code, and wake propagation by the last spinner to exit with work. TLC passes the full MCFixed state space (no deadlock, NoLostWakeup and the new SpinCountOK invariant hold). Toggling the model to release the spinner slot only at ParkCommit makes TLC report a NoLostWakeup violation, confirming the decrement-before-publish ordering is the load-bearing piece. Modeling the extension also surfaced a gap in the original spec: the recheck-abort path did not consume a racing waker in-flight increment of n_threads_running the way set_not_sleeping does, which the added wake sources made reachable as a TypeOK violation. The abort is now split into self/raced variants matching the C code. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>