Appendix N — Memory-Ordering Litmus Reference

Predict the result before reading the verdict:

// Initially X = 0 and Y = 0. Both are AtomicUsize.
// Thread A                    // Thread B
X.store(1, Relaxed);           Y.store(1, Relaxed);
let r1 = Y.load(Relaxed);      let r2 = X.load(Relaxed);

May r1 == 0 && r2 == 0 occur?

Yes. Each atomic has its own modification order, but relaxed operations do not create the cross-location order needed to force either load to observe the other thread’s store. If that answer surprises a reviewer, the design needs a happens-before proof rather than a stronger-sounding comment.

This reference uses small litmus programs to test arguments, not hardware by repetition. A litmus outcome has three useful classifications:

• forbidden by the documented model: a proof identifies the ordering relation that rules it out;
• allowed by the documented model: an implementation may produce it even if a particular run does not;
• outside this reference’s supported reasoning: unsafe aliasing, object lifetime, mixed atomic/non-atomic overlap, or an incomplete part of Rust’s memory model requires specialist analysis.

The cards deliberately keep payload state atomic and object lifetime externally owned. If a proposed proof introduces UnsafeCell, raw pointers, reclamation, FFI atomics, signals, devices, or direct memory access, stop applying the cards as a complete proof and commission specialist review of the larger model.

Rust documents its atomic orderings in relation to C++20, while the Rust Reference warns that Rust does not yet have a complete formal model for all unsafe behavior. Keep arguments inside documented atomic and safe synchronization APIs. Do not turn these cards into an unsafe publication recipe.

Card 1: relaxed counters observe, they do not publish

use std::sync::atomic::{AtomicUsize, Ordering::Relaxed};

static COMPLETED: AtomicUsize = AtomicUsize::new(0);

fn record_completion() {
    COMPLETED.fetch_add(1, Relaxed);
}

fn snapshot() -> usize {
    COMPLETED.load(Relaxed)
}

The read-modify-write updates COMPLETED atomically. Increments are not lost through a non-atomic read/write race, and operations on this location participate in its modification order. The snapshot may still be transient while updates continue.

Use relaxed ordering when the value is observation-only and any allowed concurrent value preserves correctness. Do not let a metrics wrapper expose safe_to_reclaim, initialized, or shutdown_complete methods.

Card 2: release/acquire publication needs an observed handoff

The safe fixture uses atomics for both fields to isolate the ordering relation:

// One publisher only.
payload.store(42, Ordering::Relaxed);
ready.store(true, Ordering::Release);

// Reader
if ready.load(Ordering::Acquire) {
    assert_eq!(payload.load(Ordering::Relaxed), 42);
}

When the acquire load observes true from the publisher’s release, the proof graph is:

payload.store(42, Relaxed)
       │ sequenced-before
       ▼
ready.store(true, Release)
       │ synchronizes-with, only if observed
       ▼
ready.load(Acquire) == true
       │ sequenced-before
       ▼
payload.load(Relaxed) == 42

The transitive path establishes happens-before from the payload store to the payload load.

Release is not a broadcast that every acquire in the process receives. The acquire must read from the relevant release or a release sequence that carries it. The protocol must separately establish number of writers, initialization, lifetime, and reclamation. Prefer OnceLock, a lock, a channel handoff, or an established safe abstraction for real object publication.

Card 3: a compare-exchange has two ordering stories

Consider a bounded increment that saturates at MAX:

use std::sync::atomic::{AtomicUsize, Ordering};

fn try_increment(value: &AtomicUsize, max: usize) -> Result<usize, usize> {
    let mut current = value.load(Ordering::Relaxed);
    loop {
        if current >= max {
            return Err(current);
        }
        match value.compare_exchange_weak(
            current,
            current + 1,
            Ordering::AcqRel,
            Ordering::Acquire,
        ) {
            Ok(previous) => return Ok(previous + 1),
            Err(observed) => current = observed,
        }
    }
}

Do not copy these orderings without the associated contract. Here, successful transition is assumed to consume state published by a prior phase and publish the new phase, hence AcqRel. Failure performs no store; Acquire applies to the observed value before the loop decides what to do next.

If the atomic is only a numeric reservation counter with no dependent memory, Relaxed success and failure may be sufficient. If success only publishes earlier initialization and does not consume another publisher, Release success may be sufficient. The minimum ordering follows the data and state edges, not the syntax of a CAS.

CAS review rules:

1. State what value means before and after success.
2. Name data consumed after reading the old value.
3. Name data published before writing the new value.
4. Treat failure as a load and justify what the retry does with its observation.
5. Update current from Err(observed); otherwise contention can become an avoidable retry loop.
6. Expect compare_exchange_weak to fail spuriously; use it where the loop already retries.
7. Specify overflow, ABA or generation reuse, contention, starvation, and target atomic availability.

The failure ordering cannot be Release or AcqRel, because a failed comparison does not store. The API rejects invalid pairs. Compiler acceptance still does not prove the chosen pair is semantically sufficient.

Card 4: sequential consistency adds an order, not a transaction

Return to store buffering, now with sequentially consistent operations:

// Initially X = 0 and Y = 0.
// Thread A                    // Thread B
X.store(1, SeqCst);            Y.store(1, SeqCst);
let r1 = Y.load(SeqCst);       let r2 = X.load(SeqCst);

r1 == 0 && r2 == 0 is forbidden. Sequentially consistent operations participate in one total order consistent with each thread’s order. For both loads to read the initial values, each load would need to precede the other thread’s store in that total order:

X.store < Y.load < Y.store < X.load < X.store

That cycle is impossible.

The stronger verdict is narrow:

Sequential consistency is a legitimate policy when the algorithm needs its total order or when a deliberately stronger order simplifies a correct proof. It is not a repair for missing ownership, composite atomicity, or lifetime reasoning.

Cross-examine common invalid arguments

“It is atomic, so the surrounding data is safe.” Atomicity applies to the atomic access. Identify how surrounding data is synchronized and kept alive.

“The writer executes first in source code.” Source order within one thread provides sequenced-before edges. Cross-thread visibility needs a documented synchronization edge.

“Release flushes the cache; acquire reloads it.” This hardware metaphor is neither the portable contract nor a proof. Name which acquire observes which release and which operations become ordered.

“The flag is eventually visible.” Memory ordering does not promise a deadline, wake a parked task, or ensure the observing thread is scheduled. Liveness needs a wake/wait protocol and progress assumptions.

“It never failed on x86-64.” Absence of an allowed outcome does not make it forbidden. The architecture, compiler, optimizer, and schedule may be stronger or merely unhelpful to the experiment.

“The test ran a million iterations.” A stress test samples executions. It does not enumerate the language model, and its barriers or channels may accidentally add synchronization.

“SeqCst is a full barrier, so the whole object is consistent.” The guarantee concerns sequentially consistent atomic operations and their ordering effects. It does not turn several locations into a transaction.

“A relaxed load is stale.” “Stale” is too vague. Ask which write the load may observe under the location’s modification order and which correctness decision depends on it.

“The CAS failed, so nothing happened.” No store happened through that CAS, but it did perform a load and returned an observed value that may affect the retry or state decision.

“Lock-free means every caller finishes quickly.” Lock-free is a system-wide progress property under an algorithm’s assumptions; an individual participant may starve. It also says nothing about cache-line contention or end-to-end latency.

Know what experiments can establish

The canonical safe fixture is examples/rust-engineering-handbook/part-09/synchronization-memory-lab. It contains an observation-only relaxed counter, one-publisher release/acquire handoff, and compare-exchange job-state transitions.

cd examples/rust-engineering-handbook/part-09/synchronization-memory-lab
cargo +1.97.0 fmt --all -- --check
cargo +1.97.0 check --locked --all-targets --all-features
cargo +1.97.0 test --locked --all-features
cargo +1.97.0 test --locked --doc --all-features
cargo +1.97.0 clippy --locked --all-targets --all-features -- -D warnings

Use evidence in layers:

Set up litmus participants without contaminating the measured interval. Barriers used before operations and joins used afterward can coordinate iterations, but a channel between the stores and loads may introduce the ordering being tested. Record compiler, target, optimization profile, tool versions, iteration count, and the exact question.

Specialized concurrency explorers can strengthen evidence, but pin their version and state what they model. If correctness relies on non-atomic memory, unsafe cells, FFI atomics, signals, devices, DMA, or reclamation, the proof has moved beyond these cards.

Exercise: prosecute the ordering comment

Review this state:

struct Registry {
    initialized: AtomicBool,
    next: AtomicUsize,
    completed: AtomicUsize,
    phase: AtomicU8,
}

Its comment says: “All fields are atomic. Initialization uses a relaxed flag, indices use load then store, completion is SeqCst, and the registry is freed when completed == next, so the barrier makes shutdown safe.”

Deliver a replacement evidence packet:

1. Classify each field as observation, publication, unique transition, or global-order participant.
2. Give a two-thread litmus that exposes relaxed initialization.
3. Replace load-then-store index claiming with a justified read-modify-write or owner protocol.
4. Explain why two loads do not form a coherent completion snapshot.
5. Provide a lifetime proof based on joins, epochs/hazard ownership, or a lock—not counter equality alone.
6. Write success and failure ordering sentences for every remaining CAS.
7. State whether SeqCst is required by an actual total-order argument or merely retained as a conservative policy.
8. Separate model proof, concurrency exploration, stress, and benchmark plans.
9. Check target_has_atomic requirements and specify a fallback.

The strongest answer may replace the registry with a mutex-protected state machine and keep only an observation counter relaxed.

Ordering lookup card

Before approving an atomic, draw the event graph, label every operation and ordering, identify the write each decisive read may observe, and trace a happens-before path to every dependent access. If the argument depends on “flush,” “latest,” “eventually,” or “works on this CPU,” it is not complete.

Once the coordination proof is sound, optimization is still only a hypothesis. Any claim that a weaker ordering or lock-free mechanism is worth its review cost needs a separately controlled performance experiment.

Sources and version notes

• std::sync::atomic module documentation
• Ordering documentation
• AtomicUsize::compare_exchange
• The Rustonomicon: atomics
• The Rust Reference: behavior considered undefined
• The Rust Reference: memory model

The examples target safe Rust 2024 and the manuscript snapshot is Rust 1.97.0. Rust’s atomic orderings follow the documented C++20 ordering model, but Rust’s complete unsafe memory model is not fully specified. Instruction selection, cache behavior, progress, atomic width availability, and observed litmus frequency are target and toolchain properties. The fixture declares Rust 1.85.0 as MSRV; verify it separately before editorial acceptance.