feat(safety): phase 5 — loom model checking + invariant audit/assertion sweep
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.
This commit is contained in:
+94
-5
@@ -47,9 +47,8 @@
|
||||
//! - `len()` is approximate (stats only).
|
||||
|
||||
use crate::pid::Pid;
|
||||
use std::cell::UnsafeCell;
|
||||
use crate::sync_shim::{AtomicUsize, Ordering, UnsafeCell};
|
||||
use std::mem::MaybeUninit;
|
||||
use std::sync::atomic::{AtomicUsize, Ordering};
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// Feature selection
|
||||
@@ -208,7 +207,7 @@ impl MpmcRing {
|
||||
Ok(_) => {
|
||||
// SAFETY: the claim gives us exclusive write access
|
||||
// to this cell until we publish below.
|
||||
unsafe { (*cell.pid.get()).write(pid) };
|
||||
cell.pid.with_mut(|p| unsafe { (*p).write(pid) });
|
||||
cell.seq.store(pos + 1, Ordering::Release);
|
||||
return true;
|
||||
}
|
||||
@@ -237,7 +236,7 @@ impl MpmcRing {
|
||||
// SAFETY: the claim gives us exclusive read access;
|
||||
// the producer's Release publish made `pid` visible
|
||||
// to our Acquire load of `seq`.
|
||||
let pid = unsafe { (*cell.pid.get()).assume_init_read() };
|
||||
let pid = cell.pid.with(|p| unsafe { (*p).assume_init_read() });
|
||||
// Release the cell for the next lap.
|
||||
cell.seq.store(pos + self.mask + 1, Ordering::Release);
|
||||
return Some(pid);
|
||||
@@ -344,7 +343,7 @@ impl StripedRing {
|
||||
// Tests — all variants, in every build (the feature only picks the alias)
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
#[cfg(test)]
|
||||
#[cfg(all(test, not(loom)))]
|
||||
mod tests {
|
||||
use super::*;
|
||||
use std::collections::HashSet;
|
||||
@@ -467,3 +466,93 @@ mod tests {
|
||||
assert_eq!(seen.len(), 64);
|
||||
}
|
||||
}
|
||||
|
||||
// ---------------------------------------------------------------------------
|
||||
// loom model tests — RUSTFLAGS="--cfg loom" cargo test --lib --release
|
||||
// ---------------------------------------------------------------------------
|
||||
|
||||
#[cfg(all(test, loom))]
|
||||
mod loom_tests {
|
||||
use super::*;
|
||||
use loom::sync::Arc;
|
||||
use loom::thread;
|
||||
|
||||
fn pid(i: u32) -> Pid {
|
||||
Pid::new(i, 0)
|
||||
}
|
||||
|
||||
/// Two producers, main-thread consumer: both elements arrive exactly
|
||||
/// once, across every interleaving — including through a lap wraparound
|
||||
/// (capacity 2 forces cell reuse).
|
||||
#[test]
|
||||
fn mpmc_two_producers_exactly_once() {
|
||||
loom::model(|| {
|
||||
let q = Arc::new(MpmcRing::with_capacity(2));
|
||||
let mut hs = Vec::new();
|
||||
for i in 0..2u32 {
|
||||
let q = q.clone();
|
||||
hs.push(thread::spawn(move || q.push(pid(i))));
|
||||
}
|
||||
let mut got = Vec::new();
|
||||
while got.len() < 2 {
|
||||
match q.pop() {
|
||||
Some(p) => got.push(p.index()),
|
||||
None => thread::yield_now(),
|
||||
}
|
||||
}
|
||||
for h in hs {
|
||||
h.join().unwrap();
|
||||
}
|
||||
got.sort_unstable();
|
||||
assert_eq!(got, vec![0, 1]);
|
||||
assert!(q.pop().is_none());
|
||||
});
|
||||
}
|
||||
|
||||
/// Producer races a consumer on a single element: the consumer either
|
||||
/// gets it or sees a clean None — never a torn/duplicated element.
|
||||
#[test]
|
||||
fn mpmc_push_pop_race() {
|
||||
loom::model(|| {
|
||||
let q = Arc::new(MpmcRing::with_capacity(2));
|
||||
let q2 = q.clone();
|
||||
let prod = thread::spawn(move || q2.push(pid(7)));
|
||||
let seen = q.pop();
|
||||
prod.join().unwrap();
|
||||
match seen {
|
||||
Some(p) => {
|
||||
assert_eq!(p.index(), 7);
|
||||
assert!(q.pop().is_none());
|
||||
}
|
||||
None => assert_eq!(q.pop().map(|p| p.index()), Some(7)),
|
||||
}
|
||||
});
|
||||
}
|
||||
|
||||
/// Striped: two producers landing in (potentially) different stripes,
|
||||
/// main-thread consumer drains both exactly once.
|
||||
#[test]
|
||||
fn striped_two_producers_exactly_once() {
|
||||
loom::model(|| {
|
||||
let q = Arc::new(StripedRing::new(2, 4));
|
||||
let mut hs = Vec::new();
|
||||
for i in 0..2u32 {
|
||||
let q = q.clone();
|
||||
hs.push(thread::spawn(move || q.push(pid(i))));
|
||||
}
|
||||
let mut got = Vec::new();
|
||||
while got.len() < 2 {
|
||||
match q.pop() {
|
||||
Some(p) => got.push(p.index()),
|
||||
None => thread::yield_now(),
|
||||
}
|
||||
}
|
||||
for h in hs {
|
||||
h.join().unwrap();
|
||||
}
|
||||
got.sort_unstable();
|
||||
assert_eq!(got, vec![0, 1]);
|
||||
assert!(q.pop().is_none());
|
||||
});
|
||||
}
|
||||
}
|
||||
|
||||
Reference in New Issue
Block a user