Claude
039703dbeb
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.
38 lines
1.1 KiB
Rust
38 lines
1.1 KiB
Rust
//! std vs loom indirection for the modules that loom model-checks
|
|
//! (`slot_state`, `run_queue`). Everything else uses std paths directly —
|
|
//! the full runtime (context switches, futexes, real TLS) is not loom-able
|
|
//! and is never executed under `cfg(loom)`.
|
|
//!
|
|
//! Build the loom models with: `RUSTFLAGS="--cfg loom" cargo test --lib --release`
|
|
|
|
#[cfg(loom)]
|
|
pub(crate) use loom::sync::atomic::{AtomicU64, AtomicUsize, Ordering};
|
|
|
|
#[cfg(not(loom))]
|
|
pub(crate) use std::sync::atomic::{AtomicU64, AtomicUsize, Ordering};
|
|
|
|
/// `UnsafeCell` with loom's `with`/`with_mut` access API; pass-through cost
|
|
/// is zero in normal builds (`#[inline]`, newtype over std's cell).
|
|
#[cfg(loom)]
|
|
pub(crate) use loom::cell::UnsafeCell;
|
|
|
|
#[cfg(not(loom))]
|
|
pub(crate) struct UnsafeCell<T>(std::cell::UnsafeCell<T>);
|
|
|
|
#[cfg(not(loom))]
|
|
impl<T> UnsafeCell<T> {
|
|
pub(crate) fn new(v: T) -> Self {
|
|
Self(std::cell::UnsafeCell::new(v))
|
|
}
|
|
|
|
#[inline]
|
|
pub(crate) fn with<R>(&self, f: impl FnOnce(*const T) -> R) -> R {
|
|
f(self.0.get())
|
|
}
|
|
|
|
#[inline]
|
|
pub(crate) fn with_mut<R>(&self, f: impl FnOnce(*mut T) -> R) -> R {
|
|
f(self.0.get())
|
|
}
|
|
}
|