Learn · All the Ways It Can Break

growing

One Test Contains Many Schedules

A four-operation trace explains why strong atomics do not rescue a non-atomic algorithm.

formal-methods, loom, schedule-exploration, atomics, lost-update, learn

You will reconstruct a failing schedule, diagnose its operation boundary, verify the fetch_add repair, and reduce schedule growth without silently removing the failure.

Predict the counterexample

Write L for the left thread and R for the right:

L: load counter -> 0
R: load counter -> 0
L: store 0 + 1
R: store 0 + 1
main: load counter -> 1

The host scheduler may rarely choose this order in a unit test. Loom treats each modeled atomic access and scheduling point as a choice, so the interleaving becomes an ordinary branch of the test.

Diagnosis — select the smallest repair that changes the needed grain.

Grade failure and repair together

The executable specimen wraps the expected failing model in catch_unwind and asserts that it did fail. That turns the negative control into a passing regression test without weakening the inner assertion. The fixed test runs normally and requires every explored schedule to finish at 2.

To diagnose interactively, temporarily run the broken model without the outer catch and enable Loom logging. Preserve the minimal operation sequence in the bug record. Avoid depending on incidental internal scheduler identifiers; the semantic trace above survives tool updates.

Search grows by choice points

Every thread, synchronization operation, branch influenced by concurrency, and retry loop can multiply executions. Begin with two threads and the smallest state that reproduces the claim. Remove unrelated work. Replace large data with representatives only when the property cannot distinguish the removed values.

Loom reduces equivalent schedules, but the remaining graph can still grow combinatorially. A preemption bound often finds shallow bugs quickly. It also changes the evidence from exhaustive exploration of the unbounded model to exploration under that preemption limit. The next chapter makes those bounds part of the verdict.

A preemption occurs when the scheduler stops a runnable thread to run another. Bounding preemptions retains many short causal schedules while excluding paths that require more forced switches. See Loom's model builder.

Lessons

Sequential consistency orders atomic events; it does not merge several events.
The lost update needs only two loads followed by two stores.
fetch_add repairs the semantic grain with one read-modify-write.
Keep the failing model as an expected negative control.
Minimize threads and operations before imposing search bounds.
A preemption limit is part of the claim, not a performance footnote.

Practice

Retrieval. Write the four operations in the lost-update trace.
Discrimination. Why does changing the store from SeqCst to Release not repair it?
Transfer. Model two threads claiming the same one-use token with a load/store pair, then repair it with compare_exchange.

Worked answers

Left load 0, right load 0, left store 1, right store 1.
The algorithm still has a scheduling point between its read and write; weaker ordering does not make the pair indivisible.
The broken trace lets both threads observe unclaimed before either store. A successful compare-and-exchange permits only one transition from unclaimed to claimed.

References

Loom. Running Loom tests. — release-mode execution and configuration
Rust. AtomicUsize::fetch_add. — atomic read-modify-write semantics

← Instrument the World You Want Explored Memory Order Is Part of the Claim →

Both operations in the broken increment use sequentially consistent atomics. The algorithm still loses an update because load and store are two separately atomic events. Loom can schedule both loads before either store. Each thread then writes 1, and the final counter is 1 rather than 2. fetch_add changes the semantic grain. Each increment becomes one atomic read-modify-write, so the same schedules cannot split the read from its corresponding write. The repair is not “use a stronger ordering”; the broken version already uses the strongest ordering in Rust's enum. It is “make the required compound action indivisible.”