Learn · All the Ways It Can Break

growing

Memory Order Is Part of the Claim

A readiness flag publishes a payload only when the operations create the required happens-before edge.

formal-methods, loom, memory-ordering, release-acquire, happens-before, learn

You will model a two-atomic publication pattern, explain release/acquire synchronization, vary ordering as a negative control, configure Loom's search bounds, and write a verdict that preserves Loom's documented memory-model limitations.

The ordering is an input to the model

rust code/all-the-ways-it-can-break/concurrency-loom/model.rs#publication concurrency.rs Payload uses Relaxed. The flag orderings are parameters so the same model checks the broken and repaired synchronization claims.

The writer's release store orders its preceding payload store before publication. When the reader's acquire load observes that release, subsequent reads observe effects that happened before it. The assertion is conditional: if the reader sees ready = false=, it makes no progress claim.

Happens-before is the memory model's ordering relation for effects whose visibility must be consistent across threads. Rust documents the available atomic orderings and their load/store restrictions.

Publication — identify the edge that carries the payload.

Bounds are fields, not folklore

loom::model uses a default builder. For a model that needs explicit limits:

let mut builder = loom::model::Builder::new();
builder.max_threads = 3;
builder.max_branches = 200;
builder.preemption_bound = Some(2);
builder.max_permutations = Some(50_000);
builder.check(|| exercise_protocol());

max_threads limits modeled threads. max_branches limits thread switches within a permutation and detects executions that exceed it. A preemption bound excludes schedules requiring more forced switches. max_permutations and max_duration stop exploration before exhaustion. Checkpoints can resume a long exhaustive search; location capture helps diagnosis but is deliberately expensive.

If a permutation or duration cap stops the run, report partial exploration. If a preemption bound is set, report the exact bound. Never translate “no failure in 50,000 permutations with at most two preemptions” into “thread-safe.”

Preserve the implementation limits

Loom simulates many valid executions and performs state reduction. Its own documentation says relaxed memory ordering is not modeled completely because some within-thread and cross-atomic reorderings cannot be emulated. It also models only the instrumented primitive set. These are categorical gaps, not larger numerical bounds.

Pair Loom with ordinary tests on supported targets, compiler checks, targeted stress tests, and—when the claim depends on weak-memory completeness—a tool or argument whose memory model covers the required behavior. Evidence can stack; its meanings must not blend.

Unlike transfer: publish immutable configuration

Model one writer that stores a configuration identifier and publishes a ready flag, plus two readers that may race before or after publication. Require that any reader observing ready sees the chosen identifier, and that readers never observe two identifiers. Use more than one payload value so the assertion cannot pass because the initialized and published values coincide.

Complete the transfer with a relaxed negative control, release/acquire repair, explicit thread and preemption bounds, and a result sentence naming Loom's incomplete relaxed-memory coverage.

Lessons

Atomicity at one location does not publish another location.
Release/acquire can create the required cross-thread ordering edge.
Orderings are part of the property and must vary in the negative control.
Builder limits determine which schedules were explored.
Loom does not model every relaxed-memory behavior.
A safety assertion conditional on observing ready does not prove eventual readiness.

Practice

Retrieval. What does the release/acquire pair order in the specimen?
Discrimination. Does a green bounded Loom run prove eventual publication?
Transfer. Complete the immutable-configuration model with two nonzero payload choices and two readers.

Worked answers

The writer's payload store before the release is ordered before the reader's payload load after the observing acquire.
No. The assertion is safety-conditional, and finite schedule exploration supplies no fairness or real-time progress guarantee.
Choose the payload before spawning, publish it with release, read the flag with acquire, and assert every ready reader sees the chosen value; retain the relaxed failure and exact builder limits.

References

Loom. Crate documentation for 0.7.2. — memory-model scope, combinatorial limits, and caveats
Loom. model::Builder for 0.7.2. — thread, branch, permutation, duration, preemption, checkpoint, and diagnostic controls
Rust. Ordering. — Relaxed, Release, Acquire, AcqRel, and SeqCst semantics

← One Test Contains Many Schedules Choose by Question, Not Reputation →

The writer stores payload 42 and then sets ready. The reader loads ready and, when true, expects payload 42. If both flag operations are relaxed, each access is atomic but the flag does not publish the earlier payload write. A release store observed by an acquire load creates the synchronization edge the claim needs. Loom finds a failure in the relaxed specimen and accepts the release/acquire repair over its explored executions. That evidence must retain a prominent limit: Loom 0.7.2 does not implement every behavior allowed by the full C11 memory model, including some relaxed reorderings. A green Loom run is therefore strong schedule-testing evidence, not a complete proof of all hardware memory behaviors.