Files
smarm/ROADMAP_v0.5.md
T
Claude 039703dbeb 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.
2026-06-09 21:27:45 +00:00

9.7 KiB
Raw Blame History

smarm v0.5 — Runtime decomposition & run-path scaling

Goal: dismantle the single Mutex<SharedState> along the run path so the runtime scales to dozens of cores, with crash isolation hardened so a torn write or a stray cancellation can never poison shared runtime state.

Guiding rules established this cycle:

  • Lock count that matters is hot-path locks. Cold lifecycle paths (spawn/join/monitor/link/finalize) may keep a small per-slot lock; the run path (yield/park/unpark/pop/resume) targets zero locks.
  • Lock ordering: io-before-shared, and slot locks are leaves (never hold two slot locks at once). Any new lock states its position in this order.
  • No unwind inside a runtime critical section. The stop sentinel only fires at lock-free observation points.
  • Never hold a thread-local guard across a possible switch point. An actor can be preempted at any allocation and resume on a different OS thread; a live RefCell borrow (or std MutexGuard) then pairs its acquire/release across two threads' locals — count underflow / UB. with_runtime, with_shared, and every RawMutex guard disable preemption for exactly this reason (phase 2 found this the hard way).

Phase 1 — State decomposition: easy peel-offs DONE

Split independent concerns out of SharedState so the global lock guards less.

  • next_monitor_idAtomicU64 on RuntimeInner (lock-free id minting).
  • timers → own Mutex<Timers> (only drain-winner + blocking prims touch it).
  • io → own Mutex<Option<IoThread>> (completion queue already self-locked).
  • pending_closures: Vec → folded into Slot::pending_closure (per-actor data).
  • Termination check split: read io liveness before shared; ordering argument documented in schedule_loop.
  • Poison fix: gate check_cancelled() in maybe_preempt behind PREEMPTION_ENABLED, so a cancellation sentinel can never unwind while a std::sync::Mutex (shared/channel) is held. Regression test: tests/poison_stop.rs.

SharedState now holds only: slots, free_list, run_queue, root_pid.

Phase 2 — Slot table split DONE

Make slot lookup lock-free and per-slot state independently mutable.

  • Fixed slab: Box<[Slot]>, slots never move → stable addresses, lock-free index. Assert on exhaustion with a panic message naming Config::max_actors(n) as the fix. Default max_actors = 16_384. (Mental note: must become unbounded or configurable-bounded later — see "Deferred" below. Do not let the fixed cap calcify into an assumption.)
  • Generation packed INTO the state word (better than the planned separate AtomicU32): one AtomicU64 = (gen << 32) | state, so the gen check is atomic with every transition — no ABA, no spurious unparks, by CAS.
  • Per-slot CAS state machine Vacant/Queued/Running/RunningNotified/ Parked/Done replacing state + pending_unpark. Also fixed a latent lost wakeup in the Blocking-IO completion path (result set for a still-Running actor without a flag).
  • sp → relaxed AtomicUsize; stop flag + first-resume closure as AtomicPtrs — resume path fully lock-free.
  • Per-slot raw non-poisoning futex mutex (src/raw_mutex.rs) for the cold collections. Guard enters NoPreempt.
  • Free list → RawMutex<Vec<u32>> (a leaf lock). Treiber/striped only if the phase-4 spawn-storm bench shows contention — revisit then.
  • finalize_actor link cascade locks peers one at a time; acyclicity argument written at the site. link() registers target-first with the race argument at the site.
  • live_actors atomic; termination = io_out == 0 (read pre-queue-lock) && queue empty && live == 0; decrement-last ordering documented as the correctness crux at the site.

Phase 3 — Pluggable run queue DONE (shootout = phase 4 harness)

  • RunQueue alias in src/run_queue.rs, compile-time selected, compile_error! guards for zero / >1 features. No runtime dispatch. All variants compile in every build (unit tests always run); the feature only picks the alias. Non-default variants: --no-default-features --features rq-…. - rq-mutexMutex<VecDeque>, the control/baseline. - rq-mpmc — single hand-rolled Vyukov bounded MPMC ring (per-cell seq numbers). Strict FIFO; "one hot cache line". - rq-striped — M Vyukov rings, fetch-add ticket distribution. Relaxed FIFO, reordering bounded by ~M. Predicted winner @20c.
  • Bounded rings sound via slab cap + at-most-once-enqueued (occupancy ≤ max_actors); mpmc capacity = next_pow2(max_actors), striped Σcapacity ≈ 2×max_actors with probe-from-home-stripe. A full ring panics as an invariant violation (double enqueue), never spins.
  • All hand-rolled, dependency-free.
  • Two contracts surfaced by the extraction, documented + debug-asserted in run_queue.rs: queue ops require preemption disabled (a producer suspended mid-publish stalls every consumer behind its cell — livelock); and pop-None is a snapshot, not a fence — termination is counter-first (live == 0 alone implies the queue holds nothing actionable; argument rewritten at the schedule_loop site).

Phase 4 — Bench harness DONE (harness; real numbers from the 20-core box)

  • benches/rq_micro.rs: raw structures, threads × p:c ratio sweep. One binary covers all three structures (types compile in every build).
  • benches/rq_runtime.rs: yield-storm, ping-pong-pairs, spawn-storm, sweeping scheduler count; variant baked in by feature.
  • scripts/bench_rq.sh: rebuilds per rq-* feature, aggregates RQCSV lines into bench_results/summary.csv. Knobs via SMARM_BENCH_* env; e.g. SMARM_BENCH_THREADS="1 2 4 8 16 20" ./scripts/bench_rq.sh.
  • Harness validated end-to-end at smoke scale on the 1-core sandbox; contention curves and the actual variant decision come from the 20-core box.

Phase 5 — Safety hardening & model checking DONE

  • State machine extracted to src/slot_state.rs (mechanism only; the protocol rationale stays in runtime.rs) so loom checks the PRODUCTION transitions. Models: lost-wakeup (park vs unpark), at-most-once (two unparkers), ABA (stale unpark vs reclaim+reuse), claim coalescing.
  • Loom on the rings via src/sync_shim.rs (std normally, loom::sync under --cfg loom): exactly-once through lap wraparound, push/pop race, striped two-producer drain. [target.'cfg(loom)'.dependencies]; run with RUSTFLAGS="--cfg loom" cargo test --lib --release. RawMutex is deliberately NOT loom-modeled: futexes can't be, and it is Drepper's textbook mutex3 with stress + unwind tests.
  • NoPreempt / no-unwind / TLS-guard audit: with_runtime + RawMutex guards + run-queue ops + trace::record all gate preemption (and thereby the stop sentinel) for their span. Sole remaining exception: channel's std MutexGuard — the documented first fast-follow.
  • Invariant-assertion sweep (the fast-follow, pulled forward): every StateWord transition self-asserts its precondition; enqueue asserts exactly (gen, Queued); live_actors underflow asserted; RawMutex enforces the leaf rule with a debug-build held-count; slab overflow and ring overflow stay loud panics. House style from here on.

Fast follow (post-v0.5, written down so it isn't lost)

  • Assert the invariants we lean on. This cycle accumulated load-bearing invariants: at-most-once-enqueued, queue-ops-under-NoPreempt, never two cold locks, cold-path generation re-verify under the lock, finalize's decrement-last, pushes-pair-with-Queued-transitions, thread-local guards never crossing a switch point. Whenever code RELIES on one and a cheap check exists, assert it at the point of reliance — debug_assert! on hot paths, full assert!/loud panic on cold ones — so a violation fails at the breakage site, not three modules downstream (the slab-overflow panic and the queue-op preemption debug_assert are the pattern). Sweep the existing code for missed spots; new code adopts it as house style. The phase-5 audit is the natural vehicle for the sweep.
  • Channel mutex migration. channel::Inner<T> is Arc<Mutex<_>> of the same poison class as the old shared lock; recv_match even runs a user predicate under it. The Phase-1 check_cancelled gating already removes the unwind source globally, so channels are poison-safe today — but phase 2 surfaced a second, sharper reason to migrate: the std MutexGuard is held with preemption ENABLED, so a timeslice switch inside a channel critical section migrates the actor and unlocks the pthread mutex from a different OS thread — technically UB (Linux futexes happen to tolerate it). The RawMutex guard disables preemption and is cross-thread-release sound by construction. Migrate as the first post-v0.5 change.

Deferred / explicitly out of scope for v0.5

  • Unbounded / configurable-bounded actor count. v0.5 ships a fixed slab with a loud assert. Revisit with a segmented slab (array of AtomicPtr<Segment>, doubling segment sizes, append-only) once we actually hit the cap or a workload demands it.
  • Idle-wakeup eventcount. Idle scheduler threads keep the current 100µs poll-sleep. A futex-based eventcount is a later optimization if benches show idle latency matters.
  • User-facing safe data structures (ArcSwap-style cells, structurally- shared persistent maps). Context for the runtime work, not in scope here.
  • IO fd hygiene on actor death (pre-existing v0.2 TODO in io.rs).