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.
64 lines
1.0 KiB
TOML
64 lines
1.0 KiB
TOML
[package]
|
|
name = "smarm"
|
|
version = "0.4.0"
|
|
edition = "2021"
|
|
rust-version = "1.95"
|
|
|
|
[lints.rust]
|
|
unexpected_cfgs = { level = "warn", check-cfg = ["cfg(loom)"] }
|
|
|
|
[features]
|
|
default = ["rq-mutex"]
|
|
smarm-trace = []
|
|
# Run-queue selection: exactly one, compile-time (see src/run_queue.rs).
|
|
# Non-default variants need --no-default-features (features are additive).
|
|
rq-mutex = []
|
|
rq-mpmc = []
|
|
rq-striped = []
|
|
|
|
[dependencies]
|
|
libc = "0.2"
|
|
|
|
[target.'cfg(loom)'.dependencies]
|
|
loom = "0.7"
|
|
|
|
[dev-dependencies]
|
|
libc = "0.2"
|
|
tokio = { version = "1", features = ["rt", "rt-multi-thread", "macros", "sync", "time"] }
|
|
|
|
[profile.dev]
|
|
panic = "unwind"
|
|
|
|
[profile.release]
|
|
panic = "unwind"
|
|
lto = "thin"
|
|
codegen-units = 1
|
|
|
|
[[bench]]
|
|
name = "primes"
|
|
harness = false
|
|
|
|
[[bench]]
|
|
name = "multi_scheduler"
|
|
harness = false
|
|
|
|
[[bench]]
|
|
name = "general"
|
|
harness = false
|
|
|
|
[[bench]]
|
|
name = "smarm_favored"
|
|
harness = false
|
|
|
|
[[bench]]
|
|
name = "tokio_favored"
|
|
harness = false
|
|
|
|
[[bench]]
|
|
name = "rq_micro"
|
|
harness = false
|
|
|
|
[[bench]]
|
|
name = "rq_runtime"
|
|
harness = false
|