Learn · All the Ways It Can Break

growing

Instrument the World You Want Explored

A concurrency checker can schedule only the threads and synchronization operations it can see.

formal-methods, loom, rust, concurrency, instrumentation, learn

You will create a blank Loom 0.7.2 test, instrument threads and synchronization, run a modeled closure, and identify code that remains outside the exploration boundary.

Start with a dedicated test target

cargo new concurrency-check --lib
cd concurrency-check
cargo add --dev loom@0.7.2

Create tests/concurrency.rs. For a small standalone specimen, import Loom types directly:

rust code/all-the-ways-it-can-break/concurrency-loom/model.rs#instrumented-counter concurrency.rs Every modeled thread, shared owner, and atomic operation comes from Loom. The two increment functions differ only in the atomicity of the whole update.

Run the test with cargo test --test concurrency --release. Release mode often makes large schedule suites materially faster; the modeled semantics come from Loom, not from whether host compilation enables optimization.

If Cargo cannot resolve loom from the integration test, confirm that version 0.7.2 appears under [dev-dependencies] and that the file lives at tests/concurrency.rs. If the deliberately broken test never fails, inspect every thread, shared owner, and synchronization import: one std primitive can leave the decisive operation outside Loom's scheduler.

Instrumentation replaces operations with observable equivalents so a tool can control or record them. Loom's writing-tests guide shows how to switch a library between loom and std types using conditional compilation.

Put construction inside the model

Create modeled threads and synchronization objects inside the closure passed to loom::model. Loom maintains execution-specific state for those objects. A modeled primitive that escapes the closure, or an object created before the model begins, breaks the lifecycle the checker expects.

Production libraries usually define one small synchronization module:

#[cfg(loom)]
pub(crate) use loom::sync::{Arc, Mutex};

#[cfg(not(loom))]
pub(crate) use std::sync::{Arc, Mutex};

Then the algorithm imports from that module. This lets the same logic run with modeled primitives in a Loom build and standard primitives in production. It also makes the boundary reviewable: a stray direct std::sync import is a coverage hole.

Instrumentation — choose the test Loom can actually schedule.

The boundary is narrower than Rust

Loom explores the modeled closure, not every behavior of an operating system, allocator, filesystem, signal handler, device, foreign function, or network. Its types intentionally approximate corresponding standard-library APIs, but some APIs differ. Keep adapters small and test production configuration separately for compilation and integration correspondence.

Lessons

loom::model repeatedly explores one instrumented closure.
Modeled threads and synchronization must use Loom primitives.
Construct modeled values inside the closure.
A conditional synchronization module keeps production and model code aligned.
Code outside the instrumentation boundary remains outside the verdict.
A known failing schedule is the negative control for the setup.

Practice

Retrieval. Name the three Loom primitive families in the counter specimen.
Discrimination. Does wrapping std::thread::spawn inside loom::model make it modeled?
Transfer. Instrument a two-thread once-initialization helper without copying the counter.

Worked answers

Modeled threads, reference-counted ownership, and atomics.
No. The host thread remains outside Loom's scheduler.
Put the flag, payload, and both threads inside the closure; import every concurrency primitive through a switchable module; assert that any observed initialized state has a valid payload.

References

Loom. Crate documentation for 0.7.2. — model execution, instrumentation pattern, limitations, and debugging
Loom. Source at release 0.7.2. — implementation and maintained examples

← A Contract Can Replace an Implementation One Test Contains Many Schedules →

Loom runs a test closure repeatedly while controlling modeled threads and synchronization primitives. It can choose a different valid schedule on each execution and reduce schedules that are equivalent for the observed model. It cannot control an ordinary std::thread or inspect an ordinary std::sync::atomic::AtomicUsize merely because both appear inside loom::model. The specimen uses loom::thread, loom::sync::Arc, and Loom atomics. Two threads increment one counter. The broken increment performs a load followed by a store. The repair performs one atomic read-modify-write. Keeping both tests proves that the model still exposes the known lost update.