# Verifying concurrency A **concurrency bug** depends on the timing or interleaving of operations that run at the same time. It is absent from any single sequential run and appears only under one of the many orderings the scheduler is free to choose. This is distinct from parallelism, which runs work at once for *speed*; concurrency is about staying *correct* whatever the interleaving. The bugs span a range, from two threads sharing memory in one process, through services exchanging events, to nodes coordinating over a lossy network, and the methods that catch them change across that range. A **data race** is two threads accessing one location with no synchronization, at least one of them writing. A **race condition** is a wrong result that depends on timing. Code with no data race can still have a race condition: two operations, each correctly locked, run in the wrong order. Removing data races is necessary, not sufficient. ## Shared-memory concurrency Within one process, concurrency bugs sort into a small taxonomy: - **Data races.** Rust's `Send` and `Sync` bounds close them by construction, by forbidding the shared mutable aliasing a race needs ([linear types](https://quality.stereobooster.com/linear-types.md)); [ThreadSanitizer](https://clang.llvm.org/docs/ThreadSanitizer.html) under [fuzzing](https://quality.stereobooster.com/fuzzing.md) catches them at runtime; [linters](https://quality.stereobooster.com/linters.md) flag missing locks. - **Atomicity violations,** the largest class in a study of 105 real-world bugs (Lu et al. 2008)[^lu2008]: a region assumed to run atomically is interleaved partway through. [Systematic concurrency testing](https://quality.stereobooster.com/systematic-concurrency-testing.md) drives the code through its interleavings to find them, and [model checking](https://quality.stereobooster.com/model-checking.md) catches them against the design. - **Order violations:** two operations run in an order the code assumed but never enforced, such as a wait that misses a notify or a use before initialization. Systematic concurrency testing is the direct method. - **Deadlock and liveness.** A lock-ordering cycle is a deadlock, and livelock and starvation are its progress counterparts. Static analysis flags lock-order inversions; systematic concurrency testing checks deadlock-freedom; model checking proves liveness properties expressed in temporal logic. ## Distributed concurrency Across nodes the same interleaving problem returns with partial failure added: a node can be slow, dead, or partitioned, a message can be lost, reordered, or duplicated, and clocks disagree. - **Consistency and linearizability.** The linearizability criterion asks whether concurrent operations appear to take effect in one consistent order (Herlihy and Wing 1990)[^herlihy1990]. [Model checking](https://quality.stereobooster.com/model-checking.md) proves it on a [TLA+](https://lamport.azurewebsites.net/tla/tla.html) spec, [deterministic simulation testing](https://quality.stereobooster.com/deterministic-simulation-testing.md) checks it against the running implementation, and [chaos engineering](https://quality.stereobooster.com/chaos-engineering.md) probes it in production-like conditions (the [Jepsen](https://jepsen.io/) approach). - **Consensus and partitions:** split-brain, a lost leader election, or replicas diverging when the network splits. Model checking runs on the protocol, deterministic simulation testing on the implementation, chaos engineering on the deployment. - **Time and message ordering.** Clock skew and reordered, dropped, or duplicated messages break code that assumed a global order; the happens-before relation is the tool for reasoning about what is actually ordered (Lamport 1978)[^lamport1978]. Deterministic simulation testing and chaos engineering exercise it. - **Liveness under partial failure:** a consensus round that never completes, an election that never settles. Model checking proves temporal properties; deterministic simulation testing checks progress invariants. ## Ordering between services Services that communicate by events are coupled more loosely than nodes of one protocol: each owns its state, and a stream is all they share. Ordering is where that arrangement breaks. A partitioned log — Kafka, Kinesis, a sharded queue — orders messages *within* a partition and promises nothing across partitions, so two producers writing state that a third service later reads back can be delivered in either order. The failure is a read that arrives before the write it depends on. A service enriching an event looks up a record another service is responsible for writing, finds nothing, and carries on. What it does next decides whether anyone notices. Raising surfaces the race; substituting a default yields a well-formed event that every downstream check accepts, which is why a [default is a silenced assertion](https://quality.stereobooster.com/contracts-and-runtime-assertions.md#a-default-is-a-silenced-assertion). This inverts the question model checking, systematic concurrency testing and deterministic simulation testing answer. For those, the ordering nondeterminism belongs to a scheduler or a network, and the work is to search for the interleaving that breaks a program which looks correct. Here the guarantee is one that was configured: the partition key decides what is ordered, so the question is whether that key co-locates the events whose order the code depends on. Checking it is a predicate over the configuration rather than a search over executions. Those three methods do not reach the rest of the case either — each takes control of the schedule, and a managed broker with a third-party delivery hop is not a schedule available to seize, while each also needs a violation that fires, which a defaulted field never produces. Two methods reach the case, and neither needs control of the schedule: - **Permutation invariance.** Replaying the same events in a different delivery order and asserting the output is unchanged is a metamorphic relation, and [metamorphic testing](https://quality.stereobooster.com/metamorphic-testing.md) is the method: the relation supplies the oracle, so no fixture has to predict the right answer for each order. - **Modeling the choreography.** Where the state machines and the messages between them are the system's own, the [P language](https://github.com/p-org/P) expresses them and explores the delivery interleavings, as [model checking](https://quality.stereobooster.com/model-checking.md) does for a consensus protocol. It reaches the design, not a broker's partition guarantee or a vendor's behavior. ## Controlling the schedule Three of these methods take control of nondeterministic execution and differ in the artifact they drive, so they add up rather than replace one another. [Model checking](https://quality.stereobooster.com/model-checking.md) explores a *spec or model* and either proves a property or returns a counterexample trace. [Systematic concurrency testing](https://quality.stereobooster.com/systematic-concurrency-testing.md) drives the *real implementation* through its interleavings, bounded but systematic. [Deterministic simulation testing](https://quality.stereobooster.com/deterministic-simulation-testing.md) runs the whole system under a seeded, controllable scheduler, one reproducible schedule at a time. ## Eliminating races by design Some execution models remove the data-race class without verifying anything, by removing what a race needs: shared state that threads mutate under preemption. Each is a trade, not a win, in the way garbage collection is for memory. - **The single-threaded event loop** (Node.js, Redis, `asyncio`) runs one turn to completion before the next, so nothing interleaves preemptively and data races cannot occur. It gives up CPU parallelism, a blocked turn stalls everything, and ordering race conditions across `await` boundaries survive: the same logical bugs reached by [systematic concurrency testing](https://quality.stereobooster.com/systematic-concurrency-testing.md). - **Share-nothing actors** (Erlang, Akka, [Pony](https://www.ponylang.io/)) give each actor private state and communicate by messages, so there is no shared memory to race on; Pony makes the sharing rules a type-level question ([linear types](https://quality.stereobooster.com/linear-types.md)). Deadlocks and ordering bugs move to the message level, and local reasoning becomes distributed reasoning. - **Software transactional memory** (Haskell's `STM`, Clojure) makes a block atomic by construction and composes without a lock order, so lock-ordering deadlocks cannot arise; the cost is retry and livelock under contention, and side effects that cannot take part in a transaction. - **Immutability** (persistent data structures, a functional core) leaves nothing to mutate concurrently. Each removes the data-race class outright, and software transactional memory the lock-deadlock class, but none of them touches the ordering and liveness classes. The bug moves rather than disappears. ## Referenced by - [Linters](https://quality.stereobooster.com/linters.md) · Methods - [Static analysis](https://quality.stereobooster.com/static-analysis.md) · Methods ## References [^lu2008]: Lu, Shan, Soyeon Park, Eunsoo Seo, and Yuanyuan Zhou. 2008. "[Learning from Mistakes: A Comprehensive Study on Real World Concurrency Bug Characteristics](https://www.cs.columbia.edu/~junfeng/09fa-e6998/papers/concurrency-bugs.pdf)." *Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XIII)*, 329–39. . [^herlihy1990]: Herlihy, Maurice, and Jeannette M. Wing. 1990. "[Linearizability: A Correctness Condition for Concurrent Objects](https://cs.brown.edu/~mph/HerlihyW90/p463-herlihy.pdf)." *ACM Transactions on Programming Languages and Systems* 12 (3): 463–92. . [^lamport1978]: Lamport, Leslie. 1978. "[Time, Clocks, and the Ordering of Events in a Distributed System](https://lamport.azurewebsites.net/pubs/time-clocks.pdf)." *Communications of the ACM* 21 (7): 558–65. .