fix: seqlock writer-enter missing Release fence — torn reads on weak memory (#40)#77
Merged
Merged
Conversation
…40) write_lock() published the odd ("writer active") sequence number with a Release store and then mutated data. A Release store orders only the operations that *precede* it, so on weak-memory hardware (ARM64) the subsequent data writes can float ahead of the odd-seq store. A reader can then observe mutated data while seq still reads even at both read_begin and read_validate, and falsely validate a torn read — wrong results returned through the safe cross-process backend, not just an extra retry. (x86 is TSO, so it cannot manifest there.) Add `atomic::fence(Release)` immediately after the odd-seq store — the textbook seqlock writer-enter. The release fence orders the odd publish before the following data writes; paired with the reader's existing `fence(Acquire)` in read_validate, a reader that observes any mutated data is guaranteed to also observe the odd seq and retry. The exit side (write_unlock's Release store) was already correct but only covers the even publish, not the entry side. Add a loom model of the seqlock's reader/writer ordering (gated behind `cfg(loom)`, so loom is not a normal/release/CI dependency). Loom exhaustively explores interleavings and reorderings: without the fence it finds an execution that validates a torn read (d0=0, d1=1); with the fence, no such execution exists. Run with `RUSTFLAGS="--cfg loom" cargo test --lib seqlock_ordering`. Document the invariant in ARCHITECTURE. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Closes #40
What & why
ShmSeqLock::write_lock()publishes the odd ("writer active") sequence number withseq.store(prev+1, Release)and then the caller mutates data. A Release store orders only the operations that precede it — it places no constraint on the data writes that follow. So on weak-memory hardware (ARM64/PPC) the data writes can become globally visible before the odd-seq store propagates.A reader can then:
read_begin→ load seq, see even (old),read_validate→ still see the same even seq (odd store not yet visible) → validates a torn read as consistent.That's wrong results returned through the safe cross-process backend, not merely an extra retry. (x86 is TSO, so it can't manifest there — which is why this is medium, weak-memory-only.)
The fix
Add
atomic::fence(Release)immediately after the odd-seq store — the textbook seqlock writer-enter:The release fence orders the odd publish before the following data writes. Paired with the reader's existing
fence(Acquire)inread_validate, this forms a synchronizes-with edge: a reader that observes any mutated data is guaranteed to also observe the odd seq, so it retries instead of validating. The exit side (write_unlock's Release store) was already correct, but it only covers the even publish — it can't cover the entry side.Test — model-checked with
loomA behavioral test can't prove this: it can't manifest on x86, and the ARM64 window is effectively impossible to hit deterministically. So I added a
loommodel of the seqlock's reader/writer ordering (src/shm/lock.rs, behind#[cfg(loom)]). Loom exhaustively explores all interleavings and weak-memory reorderings:assertion left == right failed ... left: 0, right: 1(one data word old, one new)loomis acfg(loom)-only dependency ([target.'cfg(loom)'.dependencies]) — absent from normal, release, and CI builds; the model module is#[cfg(loom)]so it's excluded from the regularcargo test. Verified locally by toggling the model's fence (fail → pass).Gates run (risky change —
src/shm/lock.rs, concurrency/locking)make fmt/make lint(ruff, ty, clippy-D warnings) ✓ — loom module excluded under normal cfgmake test—cargo test(11) + pytest (92) ✓make test-matrix— Python 3.10–3.13 ✓ (3.14 skipped locally via the documenteduv-resolves-stale-alpha guard; CI covers 3.14 final)make bench— no regression: shared backend ~9.0M ops/s, hit-rate 72.9% (the fence is onedmb ishper insert, dominated by the existing lock + serialization)RUSTFLAGS="--cfg loom" cargo test --lib seqlock_ordering✓ (and fails as expected without the fence)🤖 Generated with Claude Code