Two integration-driven amendments ahead of the runtime swap:
wake_one_if_idle() realizes RFC 018's "empty-mask fast path is one
relaxed load" soundly: a bare relaxed load is a lost-wake in the Dekker
shape for the lock-free ring queues, so the producer publishes work,
fences (SeqCst), then reads the mask Relaxed — paired with a matching
fence between the consumer's bit-publish and its re-check in park().
The pure-compute hot path (mask 0) never takes the shared mask line
exclusive; the RMW read stays on the rare chain-rule path only. Loom
models 1/2 now drive the fenced pattern end to end.
next_deadline is the earliest KNOWN timer deadline, independent of
whether anyone is parked — which tk_armed cannot give: under saturation
nobody parks, nobody arms, yet due timers must still fire (ratified
design point (a): the busy-path due-check). Maintained under the timers
mutex (note_deadline on insert — which also carries the timekeeper
re-arm wake — refresh_deadline after pop/clear); read lock-free.
deadline_due() costs one Relaxed load and a branch when no timer exists;
the clock is read only when one does.
Schedulers get an IO-agnostic sleep/wake primitive of their own: one
futex Parker per scheduler thread (permit semantics, std::thread::park
shaped — closes the check-then-park race), an AtomicU64 idle mask with a
set-bit → re-check → wait park protocol, wake_one (highest-bit LIFO,
CAS-clear before unpark: exactly one wakeup per call by construction),
wake_all for the terminal path, and the timekeeper role — at most one
parked scheduler holds the timer deadline, with an atomic armed-deadline
snapshot for the busy-path due-check and an insert-side re-arm wake.
Deadlines travel as nanosecond timespecs end to end; the wake pipe's
as_millis truncation is unrepresentable here. The Dekker publish/re-check
shape is resolved by the same-location-RMW handshake (AcqRel), not SeqCst
loads; loom verifies exactly this in four models (no-lost-wake, chain
propagation, timekeeper handoff, termination), run with
LOOM_MAX_PREEMPTIONS=3 — unbounded exploration is impractical for the
looped models. Loom/non-Linux builds park on a Mutex+Condvar via
sync_shim.
Standalone until the runtime swap (next commit): nothing outside tests
constructs a Coordinator yet, hence the temporary dead_code allow in
lib.rs.
State machine extracted to src/slot_state.rs as a standalone unit (StateWord:
publish_queued / try_claim / yield_return / park_return / unpark / set_done /
reclaim, plus the Status view for cold paths). runtime.rs keeps the protocol
rationale and consumes the mechanism; every transition self-asserts its
precondition per the assert-the-invariants rule.
src/sync_shim.rs: std vs loom indirection (atomics + UnsafeCell with the
with/with_mut access API) for the two loom-modeled modules. Loom models run
the PRODUCTION code, not a replica:
- slot_state: no-lost-wakeup (park vs unpark), two-unparkers-one-enqueue,
stale-unpark-never-hits-reused-slot (the ABA theorem), unpark-vs-claim.
- run_queue: mpmc exactly-once through a lap wraparound, push/pop race,
striped two-producer drain.
RUSTFLAGS="--cfg loom" cargo test --lib --release — 7 models, all pass.
RawMutex deliberately not loom-modeled (futexes can't be; textbook mutex3
with stress + unwind coverage).
Assertion sweep (invariants now checked at the point of reliance):
- enqueue debug-asserts the word reads EXACTLY (gen, Queued) — the
at-most-once-enqueued invariant the ring capacity proof leans on.
- RawMutex enforces the leaf rule mechanically: debug-build thread-local
held-count, panics at the acquisition that violates it.
- live_actors underflow (double finalize) asserted.
- StateWord transition preconditions asserted (yield/park/done/reclaim/
publish/claim).
Audit: with_runtime, RawMutex guards, run-queue ops, and trace::record all
gate preemption (and thereby the stop sentinel) for their span; trace was
already self-gating. Sole remaining exception is the channel std MutexGuard
— the documented first post-v0.5 fast-follow.
Review fixes to the branched-in work:
- slot_state::status_for mapped (matching gen, Vacant) to Stale instead of
unreachable!: Pid::new is public, so a forged/never-issued pid (e.g.
monitor(Pid::new(5,0)) on a fresh slab) could reach it — "no such actor"
is the correct total answer; issued pids still can't get there.
- Tightened enqueue's assert from Status::Live to the exact (gen, Queued)
word its own comment argues for.
Validated: 22 suites in debug (all asserts + leaf counter live) for
rq-mutex/rq-mpmc/rq-striped, release for rq-mutex, smarm-trace build +
stress, loom 7/7.
smarm