The CPR snapshot phase handshake in src/snapshot.rs uses Release/Acquire between the worker and the manager. TLA+ modelling and Miri tests both show that this is not sufficient: the handshake breaks under Release/Acquire, and SeqCst is required.
SeqCst is needed on the stores and on the loads paired with them. Changing only one side is not enough, because the SeqCst total order constrains SeqCst operations only.
Draft pull request marking the sites, with both reproducers and no fix applied: tiagonapoli#1
Repro
TLA+
A model for x86-TSO (total store order), checked with TLC. tla/X86TSO.tla - each core has a private queue of pending stores, and a store becomes visible to other cores only once that queue drains. On top of that, the handshake specs were built - TLC then explores every reachable state and reports both invariants violated.
The specs and the runner are in the pull request above, under tla/:
Needs only a JRE; tla2tools.jar is downloaded on first run. There is a Dockerfile alongside it if you would rather not install Java.
Miri
Miri is an official part of the Rust toolchain (rustup +nightly component add miri). Instead of running native machine code, it interprets the program and checks each operation against the rules of the Rust memory model, so it can flag undefined behavior that a native run would silently tolerate. It also simulates weak memory: an atomic load may return an older value if the language rules allow it, so a reordering that might take days of stress testing to hit on real hardware shows up in under a second.
The pull request adds Miri tests that drive the real CPRSnapShotMgr, rather than a model of it. Both fail:
cargo +nightly miri test --lib snapshot::cpr_handshake_miri
iteration 0: worker committed to the old state 0x0, but the manager
advanced to 0x2000000000000000 and reported the phase complete
The control is the -Zmiri-disable-weak-memory-emulation flag, which leaves thread interleaving exploration unchanged but makes every atomic load return the latest value:
|
as-is |
weak memory simulation off |
| test 1 |
assertion fires |
passes |
| test 2 |
undefined behavior: use-after-free |
passes |
With SeqCst on both sides, both tests pass and TLC reports the invariants hold.
The existing Shuttle tests cannot find this, since Shuttle treats every atomic operation as sequentially consistent and so explores thread interleavings but not memory reordering.
The CPR snapshot phase handshake in
src/snapshot.rsusesRelease/Acquirebetween the worker and the manager. TLA+ modelling and Miri tests both show that this is not sufficient: the handshake breaks underRelease/Acquire, andSeqCstis required.SeqCstis needed on the stores and on the loads paired with them. Changing only one side is not enough, because theSeqCsttotal order constrainsSeqCstoperations only.Draft pull request marking the sites, with both reproducers and no fix applied: tiagonapoli#1
Repro
TLA+
A model for x86-TSO (total store order), checked with TLC.
tla/X86TSO.tla- each core has a private queue of pending stores, and a store becomes visible to other cores only once that queue drains. On top of that, the handshake specs were built - TLC then explores every reachable state and reports both invariants violated.The specs and the runner are in the pull request above, under
tla/:Needs only a JRE;
tla2tools.jaris downloaded on first run. There is a Dockerfile alongside it if you would rather not install Java.Miri
Miri is an official part of the Rust toolchain (
rustup +nightly component add miri). Instead of running native machine code, it interprets the program and checks each operation against the rules of the Rust memory model, so it can flag undefined behavior that a native run would silently tolerate. It also simulates weak memory: an atomic load may return an older value if the language rules allow it, so a reordering that might take days of stress testing to hit on real hardware shows up in under a second.The pull request adds Miri tests that drive the real
CPRSnapShotMgr, rather than a model of it. Both fail:cargo +nightly miri test --lib snapshot::cpr_handshake_miriThe control is the
-Zmiri-disable-weak-memory-emulationflag, which leaves thread interleaving exploration unchanged but makes every atomic load return the latest value:With
SeqCston both sides, both tests pass and TLC reports the invariants hold.The existing
Shuttletests cannot find this, sinceShuttletreats every atomic operation as sequentially consistent and so explores thread interleavings but not memory reordering.