You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Gap surfaced by #77. The core wiring (#77) exercises @linearizability/@model scenarios with real tokio::spawn + Barrier overlap — but that runs ONE scheduling per CI run. It reliably catches non-atomicity (a torn fetch_add produces a wrong result set on essentially any schedule), but a rare Relaxed/Acquire/Release memory-ordering bug can pass a green run. CLAUDE.md rule 5 ("Relaxed requires a structural proof, not a comment") is exactly what loom mechanically verifies, and we deferred it from #77.
loom only exercises real interleavings against #[cfg(loom)]-instrumented source (swap std::sync::atomic/UnsafeCell/Arc for loom::sync::*).
Scope
Instrument the smallest, most self-contained atomic FIRST: ActorId::generate's process-wide AtomicUsize in src/actor/id.rs, under #[cfg(loom)].
Keep it OUT of the default nix flake check (loom runs are slow) — behind a loom cfg / a separate cargo test --cfg loom invocation or an opt-in flake check.
THEN optionally extend to the refcount paths (actor_ref.rs) and the supervision parent_shutdownAtomicBool Release/Acquire flag (links.rs) — the test(core): wire core feature scenarios to the SUT #77 links @model law's deterministic store-before-load arm is the non-loom stand-in today.
Done when id.rs has a passing loom model and the harness for adding more is documented.
Gap surfaced by #77. The core wiring (#77) exercises
@linearizability/@modelscenarios with realtokio::spawn+Barrieroverlap — but that runs ONE scheduling per CI run. It reliably catches non-atomicity (a tornfetch_addproduces a wrong result set on essentially any schedule), but a rareRelaxed/Acquire/Releasememory-ordering bug can pass a green run. CLAUDE.md rule 5 ("Relaxedrequires a structural proof, not a comment") is exactly whatloommechanically verifies, and we deferred it from #77.loomonly exercises real interleavings against#[cfg(loom)]-instrumented source (swapstd::sync::atomic/UnsafeCell/Arcforloom::sync::*).Scope
ActorId::generate's process-wideAtomicUsizeinsrc/actor/id.rs, under#[cfg(loom)].loom::model(|| …)test asserting the uniqueness + contiguous-range invariant under exhaustive interleavings (the same oracle the test(core): wire core feature scenarios to the SUT #77@modellaw uses).nix flake check(loom runs are slow) — behind aloomcfg / a separatecargo test --cfg loominvocation or an opt-in flake check.actor_ref.rs) and the supervisionparent_shutdownAtomicBoolRelease/Acquire flag (links.rs) — the test(core): wire core feature scenarios to the SUT #77 links@modellaw's deterministic store-before-load arm is the non-loom stand-in today.Done when
id.rshas a passing loom model and the harness for adding more is documented.