Skip to content

test(core): loom model for the std-atomic concurrency primitives (id counter first) #88

Description

@joeldsouzax

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)].
  • Add a 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 @model law uses).
  • 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_shutdown AtomicBool 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.

Metadata

Metadata

Assignees

No one assigned

    Labels

    Type

    No type

    Fields

    No fields configured for issues without a type.

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions