CMD Guide
Home › Concurrency › Concurrency Foundations

Testing & Verifying Concurrent Code — Proving It, Not Just Arguing It

You can reason your way to "there is a race here." That is necessary and it is not sufficient. At the staff bar the next question is always the same: show me. A design review accepts an argument; an incident post-mortem demands a reproduction. The whole discipline of this page is the gap between arguing correctness (a story about interleavings) and demonstrating it (a test or tool that makes the bad interleaving actually happen, or proves it cannot). The bugs that survive to production are precisely the ones whose argument was convincing and whose evidence was never gathered.

The mechanism: why a green concurrency test lies

A single-threaded test is a function of its inputs: same input, same path, deterministic verdict. A multi-threaded test is a function of its inputs and the scheduler — and the scheduler is not yours to control. The set of possible interleavings is enormous, the buggy ones are a vanishingly small subset, and the OS/JIT will, on any given run, almost always pick a safe one. So the test passes. It passes on your laptop, it passes in CI, it passes ten thousand times. None of that touches the buggy schedule, because the buggy schedule is rare, not absent.

The consequence is brutal and counter-intuitive: "it passed" carries almost no information about a concurrency bug. A green multi-thread test is consistent with correct code and with code that loses an update one run in a million. To get signal you must stop sampling the scheduler at random and instead do one of two things: force or randomize the interleavings so the rare one fires on purpose, or detect the race independent of scheduling so you catch it whenever the racy access is merely executed. Everything below is one of those two moves.

A worked broken example, and the test that flatters it

Take the canonical read-modify-write bug: an unsynchronized counter. count++ is three operations — read, add, write — and two threads can both read the same value, so one increment is lost. We know the argument. Now watch a reasonable-looking test bless the broken code.

Java — the broken counter and the flattering test

// BROKEN: read-modify-write is not atomic
public final class Counter {
    private int count = 0;
    public void increment() { count++; }   // read, +1, write — three steps
    public int get()        { return count; }
}

// Looks fine. Passes on essentially every run.
@Test
void twoThreadsIncrement() throws InterruptedException {
    Counter c = new Counter();
    Thread t1 = new Thread(c::increment);
    Thread t2 = new Thread(c::increment);
    t1.start();
    t2.start();               // t1 has almost always finished before t2 even reads
    t1.join();
    t2.join();
    assertEquals(2, c.get()); // GREEN — and completely misleading
}

The join-based test starts one thread and, by the time the second is spun up and scheduled, the first has usually already committed its write. The contended window — both threads reading before either writes — is microseconds wide and almost never hit. The assertion is true; the code is wrong.

Go — the same bug

type Counter struct{ n int }

func (c *Counter) Inc() { c.n++ } // data race: concurrent read-modify-write

// Naive test — passes almost always.
func TestNaive(t *testing.T) {
    c := &Counter{}
    var wg sync.WaitGroup
    wg.Add(2)
    go func() { defer wg.Done(); c.Inc() }()
    go func() { defer wg.Done(); c.Inc() }()
    wg.Wait()
    if c.n != 2 {
        t.Fatalf("got %d, want 2", c.n)
    }
}

Two increments give the scheduler almost no room to interleave; c.n is 2 nearly every run. The test is green and the reviewer moves on. We need to change the mechanism, not run this more times.

Technique 1 — Latch/barrier-coordinated interleaving: fire the race on purpose

If the losing schedule needs both threads to read before either writes, then engineer that moment. Spin up the threads, have each one block on a shared gate immediately before the contended operation, then open the gate so they are released together with maximal overlap. Repeat tens of thousands of times. This turns a 1-in-100,000 event into something you observe on almost every batch. In Java the gate is a CountDownLatch (or a CyclicBarrier for round-based coordination); in Go it is a closed channel, which broadcasts to every waiting goroutine at once.

Java — CountDownLatch to maximize overlap

@Test
void raceSurfacesUnderLatch() throws InterruptedException {
    final int trials = 100_000;
    int lostRuns = 0;

    for (int i = 0; i < trials; i++) {
        final Counter c = new Counter();
        final CountDownLatch start = new CountDownLatch(1);

        Runnable body = () -> {
            try { start.await(); }              // park at the gate
            catch (InterruptedException e) { return; }
            c.increment();                       // released together → overlap
        };
        Thread t1 = new Thread(body);
        Thread t2 = new Thread(body);
        t1.start();
        t2.start();
        start.countDown();                       // open the gate for both at once
        t1.join();
        t2.join();

        if (c.get() != 2) lostRuns++;            // a lost update happened this run
    }
    assertEquals(0, lostRuns,
        "lost updates observed — count++ is not atomic");   // FAILS, as it should
}

Now the test does its job: across 100k coordinated trials it reports nonzero lostRuns and fails. The gate removes the startup skew that was hiding the bug. (CyclicBarrier is the tool when every thread must rendezvous at the start of each round of a loop, not just once.)

Go — a closed channel as a broadcast start gate

func TestRaceSurfacesUnderBarrier(t *testing.T) {
    const workers = 8
    c := &Counter{}
    start := make(chan struct{})   // unbuffered; closing broadcasts to all
    var wg sync.WaitGroup
    wg.Add(workers)

    for i := 0; i < workers; i++ {
        go func() {
            defer wg.Done()
            <-start        // every goroutine parks here
            c.Inc()        // ...and is released simultaneously by close()
        }()
    }
    close(start)           // one broadcast unblocks all N at once
    wg.Wait()

    if c.n != workers {
        t.Fatalf("lost updates: got %d, want %d", c.n, workers)  // fires often
    }
}

A closed channel is the idiomatic Go broadcast: every <-start returns at once, so all N goroutines hit c.Inc() in a tight window. With eight racers instead of two the collision probability rises sharply and the assertion fails routinely. Coordination beats repetition.

Technique 2 — Dynamic race detectors: catch it whenever the path runs

Latches force a schedule; race detectors sidestep scheduling entirely. Go's -race flag builds your program with ThreadSanitizer (TSan) instrumentation. TSan is happens-before based: it records, for every memory access, the vector clock of synchronization events (locks, channel ops, atomics) and flags any pair of accesses to the same location where at least one is a write and no happens-before edge orders them. The key property: it does not need the racy interleaving to actually occur — it only needs the racy accesses to be executed, in any order, even on a run that happened to produce the “right” answer. That is what makes it strong: it converts a rare timing bug into a deterministic report.

$ go test -race ./...

==================
WARNING: DATA RACE
Write at 0x00c0000b4008 by goroutine 8:
  counter.(*Counter).Inc()
      /src/counter.go:6 +0x2c
Previous write at 0x00c0000b4008 by goroutine 7:
  counter.(*Counter).Inc()
      /src/counter.go:6 +0x2c
Goroutine 8 (running) created at:
  counter.TestNaive.func2()
      /src/counter_test.go:11 +0x9c
==================
--- FAIL: TestNaive (0.00s)
    testing.go: race detected during execution of test
FAIL

The report names both conflicting accesses, both stacks, and the shared address. Even the naive two-goroutine test — the one that returned c.n == 2 and looked green — fails under -race, because the two writes to c.n were executed with no synchronization between them. The verdict no longer depends on luck.

What -race can and cannot do. It catches data races (unsynchronized conflicting memory access) on paths you exercise — so your tests must actually drive the concurrent code. It will not catch: (a) races on code paths a test never runs; (b) higher-level atomicity/logic bugs that use synchronization correctly on each access but still have a broken check-then-act across two properly-locked operations (each access is race-free, the composite is wrong); (c) deadlocks or liveness bugs. It costs roughly 2–20× CPU (slower execution) and ~5–10× memory (the figures the Go race-detector docs quote), so you do not ship with it — you run it in CI and in load tests where the interesting paths get exercised. The same engine (TSan, via -fsanitize=thread) covers C, C++, and Rust.

Technique 3 — jcstress: the only sound way to test the Java Memory Model

Java has no -race equivalent, and for a deeper reason: many Java concurrency bugs are not data races at the address level at all — they are visibility and reordering bugs permitted by the Java Memory Model. A missing volatile lets a compiler or CPU reorder a write, so one thread sees a half-published object. No happens-before detector on a single run will reliably show this; you need to explore memory-model-hostile schedules at scale. That is exactly what jcstress (the OpenJDK concurrency stress harness, from the JMH family) does. You write tiny @Actor methods that each run on a separate thread against shared @State; jcstress runs the pair billions of times under aggressive JIT settings and irritators, records every observed result tuple, and checks it against an @Outcome table you declare. Results you didn't list show up as FORBIDDEN; a listed-but-surprising one is ACCEPTABLE_INTERESTING — the flag that a reordering actually manifested.

// Minimal jcstress test: is our counter actually atomic?
@JCStressTest
@Outcome(id = "2", expect = ACCEPTABLE,             desc = "both increments applied")
@Outcome(id = "1", expect = ACCEPTABLE_INTERESTING, desc = "one update LOST — race proven")
@State
public class CounterStress {
    int count;                                   // plain field, no sync

    @Actor public void actor1() { count++; }     // thread 1
    @Actor public void actor2() { count++; }     // thread 2
    @Arbiter public void arbiter(I_Result r) { r.r1 = count; }  // read the final state
}

Run it and jcstress prints a distribution: mostly 2, and a real, nonzero population of 1 marked Interesting. That count of 1-outcomes is your proof of a lost update — not an argument, an observed frequency.

The payoff: a bug pure reasoning and plain tests miss

Here is the case that justifies the whole apparatus — unsafe publication. A thread creates an object and stores its reference in a non-volatile, non-final field. Another thread reads the field. The JMM permits the reader to observe the reference before it observes the constructor's field writes, because nothing establishes happens-before between them. So the reader can see a non-null object whose fields are still at their zero defaults. On x86 this almost never manifests; on a weakly-ordered ARM core it does. A plain test cannot catch it (the object is “there”); -race in Go's model would; in Java, jcstress nails it.

@JCStressTest
@Outcome(id = "-1", expect = ACCEPTABLE,             desc = "not published yet (null)")
@Outcome(id = "42", expect = ACCEPTABLE,             desc = "fully constructed and visible")
@Outcome(id = "0",  expect = ACCEPTABLE_INTERESTING, desc = "reference visible, field write NOT — reordering!")
@State
public class UnsafePublication {
    static final class Data { int v = 42; }
    Data data;                                   // NOT volatile, NOT final — the bug

    @Actor public void writer() {
        data = new Data();                       // publish: ctor writes v=42, then assigns ref
    }
    @Actor public void reader(I_Result r) {
        Data d = data;
        r.r1 = (d == null) ? -1 : d.v;           // can be 0: ref seen before v=42
    }
}

jcstress will, on a weak-memory host, report a nonzero 0 population flagged ACCEPTABLE_INTERESTING: the reader saw the reference but not the field. Declaring volatile Data data; (or making v a final field) inserts the release/acquire edge, the 0 outcome vanishes, and you can flip it to FORBIDDEN to lock the guarantee in regression. That transition — from “0 observed” to “0 forbidden and never seen” — is the proof that the fix works. No amount of staring at the code produces it.

Technique 4 — Stress, soak, and property/invariant checks

When you can't enumerate the contended moment, brute-force the schedule space: run many threads doing many operations for a long time (soak), and if the runtime offers it, randomize the scheduler (e.g. inject preemptions, or use -race's scheduling jitter) so runs don't all take the same path. Pair this with invariant/property checks rather than fixed expected values: after N concurrent deposit/withdraw calls, assert the conserved quantity (total balance) equals the algebraic sum of operations; after a concurrent map workload, assert size equals inserts minus deletes. Properties catch whole classes of interleaving failures that a hard-coded assertEquals(2, ...) cannot, because you are asserting a law the system must obey under every schedule, not one expected output.

Technique 5 — Model checking: exhaustive exploration when stress isn't enough

Stress testing samples the interleaving space; model checking enumerates it (up to a bound) and gives you soundness for that bound. Reach for it when the cost of a missed race is high and the state space is small enough to explore:

Rule of thumb: exhaustive exploration for small, critical cores (a lock-free queue, a lease protocol) where you need certainty; stress/soak for large, integrated systems where the state space is unbounded and you're buying probability, not proof.

Selection & trade-offs — which tool, and why not the others

ToolHow it gets signalCoverage / soundnessCostReach for it when
Latch/barrier testForces the contended moment, then repeatsOnly the interleaving you engineered; you must know where the race isCheap; runs in normal unit testsYou can name the critical section and want a deterministic-ish repro in CI
go -race / TSanHappens-before analysis at runtimeSound for data races on executed paths; misses unexercised paths & atomicity/logic bugs~2–20× CPU, 5–10× memGo/C/C++/Rust; default CI + load tests. First tool to reach for.
jcstressBillions of runs under JMM-hostile JIT schedules; outcome tableThe only sound way to probe JMM visibility/reordering; scoped to tiny actor testsMinutes–hours per test; separate harnessJava, and the bug is visibility/publication/reordering, not just a plain race
Stress / soak + propertiesSamples the schedule space at volumeProbabilistic — no guarantee; scales to whole systemsLong wall-clock; flaky if under-runIntegrated systems where you can't isolate the moment; catch-all safety net
loom / CHESS / TLA+Exhaustively enumerates interleavings (bounded)Sound within the bound; replayable counterexampleExplodes with state size; needs modeling effortSmall critical cores or protocols where a missed race is unacceptable

The through-line: -race/jcstress detect regardless of schedule but only on exercised code; latches force a known schedule; stress buys probability across the whole system; model checkers buy certainty for a small one. They compose — -race in CI as the floor, jcstress for JMM guarantees, a latch test for a targeted regression, loom for the lock-free core, soak in staging as the net.

Pitfalls that separate a plausible answer from a staff one

Takeaways

Synthesized for this guide; SVG diagrams hand-authored. Sources: OpenJDK jcstress harness & samples; the Go race detector docs and ThreadSanitizer; the Rust loom model checker; Microsoft Research CHESS; Leslie Lamport's TLA+; and Goetz et al., Java Concurrency in Practice, ch. 12 (Testing Concurrent Programs). See also: Race Conditions, Memory Model & Visibility, Atomics & CAS.

🤖 Don't fully get this? Learn it with Claude

Stuck on Testing & Verifying Concurrent Code — Proving It, Not Just Arguing It? Open Claude, copy a block below, and it'll teach you this exact concept — visually and interactively.

🎨 Explain it visually

Build the mental picture, not memorization.

I just read a lesson on **Testing & Verifying Concurrent Code — Proving It, Not Just Arguing It** (Concurrency) and want to truly understand it. Explain Testing & Verifying Concurrent Code — Proving It, Not Just Arguing It from first principles using ONE vivid real-world analogy and a visual mental model — draw it as ASCII art or a clear step-by-step diagram — with a concrete example using real numbers. Then ask me one question to check I got the mental picture, and wait for my reply. If you're unsure or a claim isn't standard, say so and reason from first principles instead of guessing.
🤔 Walk me through it (interactive)

Socratic — adapts to where you're stuck.

Teach me **Testing & Verifying Concurrent Code — Proving It, Not Just Arguing It** interactively. Ask me ONE guiding question at a time, wait for my answer, and adapt to my confusion — build the idea with me step by step instead of explaining it all at once. If you're unsure or a claim isn't standard, say so and reason from first principles instead of guessing.
🧪 Quiz me & fix my gaps

Active recall exposes what you missed.

Quiz me on **Testing & Verifying Concurrent Code — Proving It, Not Just Arguing It** with 5 questions, easy to tricky, ONE at a time. Tell me if each answer is right; at the end, explain clearly what I got wrong and why. If you're unsure or a claim isn't standard, say so and reason from first principles instead of guessing.
🧠 Make it stick

Intuition + hook + flashcards for long-term memory.

Help me remember **Testing & Verifying Concurrent Code — Proving It, Not Just Arguing It** for the long term: give the one-sentence intuition, a memorable hook/mnemonic, a tiny worked example, and 3 active-recall flashcards (Q -> A). If you're unsure or a claim isn't standard, say so and reason from first principles instead of guessing.

📝 My notes

← Go vs Java — How Concurrency WorksHow a Lock Is Built — From Test-an →