Use the instrumented world

Loom controls threads and synchronization operations created through its own modules. The lab uses loom::thread, loom::sync::Arc, and loom::sync::atomic::AtomicUsize. A standard-library atomic hidden inside the model would be invisible to Loom's scheduler.

use loom::sync::atomic::{AtomicUsize, Ordering};
use loom::sync::Arc;
use loom::thread;

fn run_increment(increment: fn(&AtomicUsize)) -> usize {
    let counter = Arc::new(AtomicUsize::new(0));
    let left = Arc::clone(&counter);
    let right = Arc::clone(&counter);
    let first = thread::spawn(move || increment(&left));
    let second = thread::spawn(move || increment(&right));
    first.join().expect("first modeled thread must finish");
    second.join().expect("second modeled thread must finish");
    counter.load(Ordering::SeqCst)
}

fn read_then_write(counter: &AtomicUsize) {
    let before = counter.load(Ordering::SeqCst);
    counter.store(before + 1, Ordering::SeqCst);
}

fn atomic_increment(counter: &AtomicUsize) {
    counter.fetch_add(1, Ordering::SeqCst);
}

#[test]
fn loom_finds_the_lost_update() {
    let result = std::panic::catch_unwind(|| {
        loom::model(|| assert_eq!(run_increment(read_then_write), 2));
    });
    assert!(result.is_err(), "the broken increment must have a counterexample");
}

#[test]
fn atomic_increment_survives_every_modeled_interleaving() {
    loom::model(|| assert_eq!(run_increment(atomic_increment), 2));
}

The example has a standalone manifest and lockfile. From the directory holding them, run:

cargo test --locked

loom_finds_the_lost_update catches the panic from a model that asserts the final counter is two. The test then requires that panic to exist. The repaired test uses fetch_add and expects every modeled schedule to satisfy the same assertion.

Reconstruct the schedule

Call the threads left and right. Loom can choose this order:

left:  load 0
right: load 0
left:  store 1
right: store 1
main:  load 1

No data race occurs at the Rust memory-safety level because every access uses an atomic. The application invariant still fails. fetch_add(1) turns the read-modify-write sequence into one atomic operation, so the two increments cannot overwrite each other.

Keep the model finite

Two threads perform one increment each. The model uses sequential consistency and no application I/O. The result does not cover an unmodeled mutex, a third thread, relaxed ordering, retries, allocator behavior, or a surrounding async runtime. Adding operations can multiply schedules sharply.

Start with the smallest schedule that can violate the property. Keep hidden work out of the modeled closure. If production code uses wrappers, inject Loom types behind a small synchronization interface so the test and production implementations share the algorithm.

Practice

1. Add a third incrementing thread. Predict the smallest final value.
2. Replace fetch_add with a compare-exchange loop and state the retry condition.
3. Explain why a passing Loom model that uses std::sync::atomic::AtomicUsize gives weak evidence.

Worked answer

1. All three threads can load zero before any store, so the smallest final value is one.
2. Retry when compare-exchange reports that another thread changed the observed value. Recompute from the returned value.
3. Loom cannot intercept the standard atomic's operations, so the checker cannot enumerate their ordering choices.

Lessons

• Loom explores schedules exposed through Loom synchronization types.
• Atomic operations do not make a multi-operation algorithm atomic.
• A short counterexample can explain a race better than a stress-test frequency.
• The number of threads, operations, and memory orderings defines the model scope.
• Production and modeled synchronization need a deliberate interface boundary.

References

1. Tokio Project. “Loom.” docs.rs. — model execution, instrumented types, and limitations.