Verifying Concurrent Code

A data race is two threads accessing the same memory location, at least one of them writing, with no synchronization ordering the accesses. A dynamic detector instruments every load, store and synchronization event at runtime and checks whether each pair of conflicting accesses is ordered.

A virtual clock is a time source the test controls: it only advances when the test says so. Injecting it lets you test timeouts, retry backoff, cache expiry, rate limiting, and scheduled jobs instantly and deterministically, with no real waiting.

Take several dumps a few seconds apart and compare. Near-zero processor use means nobody is running, so look for threads blocked on a lock (and who owns it), waiting on a condition or a remote response, and for whole worker pools stuck in the same stack — that shared frame is the culprit.

Shrink the code under test so the bad window is a large fraction of it, start all threads from a barrier so they collide instead of running sequentially, perturb timing with randomized delays and varied thread counts, check a real invariant rather than a crash, and record the seed and observed state so a failure is reproducible.

A runtime builds a wait-for graph of which thread waits for which lock owner and reports a cycle as a deadlock. Distinguish by evidence: deadlock is permanent with identical stacks and no processor use; livelock burns processor with changing stacks and no progress; a slow remote call has threads in socket reads and eventually times out.

A litmus test is a tiny fixed program — usually two threads with a handful of memory operations — run many times to see which final states are observable. It answers a narrow yes/no question: can this outcome ever occur on this platform or under this implementation?

Make time and execution injected dependencies: pass in a clock and an executor/scheduler rather than calling the system clock or spawning threads inline, and give async operations an observable completion handle. Tests then substitute a fake clock and a same-thread or manually pumped scheduler.

Observation changes timing. Logging and breakpoints add delay and internal synchronisation that widen or close the racy window, so the interleaving that triggered the bug stops occurring. Collect evidence with low-overhead, always-on instruments instead: sampling, counters, in-memory ring buffers, and post-mortem dumps.

It records every nested lock acquisition as an edge "A acquired before B" in a global lock-order graph, usually keyed by lock class rather than instance. A cycle in that graph means two code paths take the same locks in opposite orders, which is a deadlock waiting for the right interleaving — no actual hang required.

Each thread carries a vector clock: one counter per thread, its own bumped on synchronization. Releasing a lock copies the releaser's clock into the lock; acquiring joins that clock into the acquirer's. Each memory location stores the clock value of its last write and reads. An access races if the prior conflicting access's stamp is not covered by the current thread's vector clock.

First make it repeatable: derive all nondeterminism from a logged seed, or record and replay the schedule under a controlling scheduler. Then minimize by delta debugging — repeatedly drop operations, threads and delay points, keeping any reduction that still fails — until every remaining element is necessary. Keep the result as a permanent regression test.

It makes the interleaving a test input: you choose the order tasks run, so a specific race is reproduced exactly and every run behaves identically. It cannot catch bugs that live below task granularity — memory-visibility and instruction-reordering effects, true parallel data races, or contention and performance problems.

Profile where threads wait, not just where they run: use off-CPU or blocked-time profiling, or sample thread dumps and count how often threads sit blocked on the same lock. Rising context-switch rates and flat throughput with growing thread counts confirm contention; the top blocked-on stack names the lock.

Lockset detection tracks, per location, the intersection of locks held on every access; an empty intersection means no consistent lock, so it warns. It finds bugs the observed schedule hid, but false-alarms on correct code that uses ordering instead of locks. Happens-before detection reports only genuinely unordered pairs — precise, but blind to schedules it did not run. Hybrids combine both.

You describe the system as states and transitions plus properties it must satisfy, then a checker exhaustively explores every reachable state and interleaving to prove the properties or produce a counterexample trace. The reachable state count grows exponentially in components and interleavings, so the entire practical craft is keeping the model small and pruning equivalent explorations.

The test runs on a scheduler you control: threads only advance when it says so, and it picks the next thread by a seeded random policy. That makes coverage of interleavings deliberate rather than accidental, makes any failure replayable from its seed, and lets you bias toward bug-prone schedules such as few well-placed preemptions.

Treat flakiness as a defect with an owner, not noise: detect and track it automatically, quarantine loudly with a deadline instead of blanket retries, then fix each test by removing the timing dependency — signals and virtual clocks instead of sleeps, isolated state, no ordering assumptions — and check whether the flake is actually a product bug.

Pre-install evidence collection: per-pool metrics (queue depth and oldest-item age, wait time versus service time, active workers, rejections), always-on sampling profiling on and off processor, watchdog-triggered thread dumps stored durably, and a capture-before-restart rule. A few percent steady overhead is a fair price.

Only that no race appeared on the code paths, data and schedules that actually executed. Dynamic detection is bounded by code coverage, thread-interleaving coverage, and the classes of bug it models. Cover the gaps with schedule perturbation, static checking with ownership annotations, and design choices that make whole categories unrepresentable.