# Systematic concurrency testing Systematic concurrency testing takes control of a concurrent program's scheduler and drives the *real implementation* through its possible interleavings. It checks an invariant on each thread or task schedule. When a schedule violates the invariant (a data race, a deadlock, a failed assertion), the tool reports the exact sequence of scheduling decisions that produced it and replays it on demand. The technique is also called **stateless model checking**: it explores the interleaving space like a model checker, but over the running code rather than an abstract model, and without storing visited states. It sits between two neighbors that also reach interleavings that hand enumeration never could: - [Model checking](https://quality.stereobooster.com/model-checking.md) explores an abstract **spec** exhaustively; systematic concurrency testing explores the **implementation**, so there is no spec-to-code gap, and no protocol-level guarantee either. - [Deterministic simulation testing](https://quality.stereobooster.com/deterministic-simulation-testing.md) (DST) controls the implementation's nondeterminism too, but samples schedules at **random** across a whole distributed system; systematic concurrency testing explores in-process schedules **systematically**, with a stronger coverage guarantee over a narrower space. ## What it catches - **Data races and atomicity violations.** Concurrent read/write or write/write on shared state with no enforced order; an `await` between a read and a dependent write of the same field. - **Deadlocks and lost wakeups.** Lock-ordering cycles, a notify that races ahead of its wait, a signal dropped on an empty queue. - **Ordering and TOCTOU bugs across turn boundaries.** Single-threaded async code (JavaScript, Python `asyncio`) has no memory races, but interleavings across `await` / event-loop turns produce the same logical bugs. - **Bugs a fixed test schedule never reaches.** Real-world concurrency bugs cluster at shallow interleaving depths: exactly the small-group interleavings a scheduler explorer covers. This is the failure class a [linear type system](https://quality.stereobooster.com/linear-types.md) does *not* close: Rust's `Send` / `Sync` forbid data races by construction, but deadlocks, lost wakeups, and logical ordering races survive. ## Approaches and tools ### Systematic — partial-order reduction, context-bounding Systematic exploration enumerates distinct interleavings, pruning provably-equivalent ones, and is exhaustive up to a bound. - **[CHESS](https://www.microsoft.com/en-us/research/project/chess-find-and-reproduce-heisenbugs-in-concurrent-programs/)** (Microsoft Research) — takes over scheduling of a C/C++ or .NET program and explores its interleavings under a bound on preemptions, which keeps the search tractable (Musuvathi et al. 2008)[^musuvathi2008]. - **[Coyote](https://github.com/microsoft/coyote)** (Microsoft) — CHESS's open-source successor for .NET. Explores the interleavings of `async` / `await` C# with deterministic repro, engineered for industrial CI use (Deligiannis et al. 2023)[^deligiannis2023]. - **[GenMC](https://github.com/MPI-SWS/genmc)** and **[Nidhugg](https://github.com/nidhugg/nidhugg)** — stateless model checkers for C/C++ under relaxed memory models (C11, TSO/PSO). They use partial-order reduction to keep the search tractable; Nidhugg's *chronological traces* extend that reduction to the relaxed models, distinguishing only executions that are genuinely inequivalent (Abdulla et al. 2017)[^abdulla2017]. - **[loom](https://github.com/tokio-rs/loom)** (Rust) — explores every permitted interleaving of atomic operations under a bounded model. ### Randomized — sampling with a probabilistic bound Where the interleaving space is too large to enumerate, a randomized scheduler samples schedules instead. - **PCT** (Probabilistic Concurrency Testing) — a randomized scheduler with a proven per-run lower bound on the probability of finding a bug of depth *d* (Burckhardt et al. 2010)[^burckhardt2010]. Coyote ships PCT as a prioritization strategy; [shuttle](https://github.com/awslabs/shuttle) uses PCT-style randomization for Rust. Either strategy needs control of every scheduling decision. In-process tools instrument the runtime or the synchronization primitives; a heavier alternative is a deterministic platform underneath the program — [rr](https://rr-project.org/) (record/replay with a chaos-scheduling mode), [Hermit](https://github.com/facebookexperimental/hermit) (a deterministic Linux container), or a deterministic hypervisor (see [DST](https://quality.stereobooster.com/deterministic-simulation-testing.md)). Such a platform also captures threads, the OS scheduler, and native code an in-process scheduler cannot reach. ## When to use, when not **Use:** - In-process concurrent code where rare interleavings hide bugs: lock-free data structures, work-stealing schedulers, async state machines, actor mailboxes. - Where a failing run must be reproducible. As in DST, every failure carries the schedule that triggered it; unlike stress testing, the bug does not vanish on the next run. - Single-threaded async code (JavaScript, `asyncio`), where the bugs come from `await`-boundary ordering rather than threads. **Don't:** - For whole-distributed-system fault behavior: partitions, node death, clock skew. That is [DST](https://quality.stereobooster.com/deterministic-simulation-testing.md)'s territory; this method controls the scheduler, not the network and disk. - When a [linear type system](https://quality.stereobooster.com/linear-types.md) can forbid the race outright. A type that rules out the race by construction is cheaper than searching for it. - Where the interleaving space is unbounded. Systematic exploration runs into the same state-space explosion as model checking; that is what the context bound and PCT's sampling are for. ## Evidence - **CHESS found and reproduced bugs in shipping Microsoft code** that had survived ordinary stress testing (Musuvathi et al. 2008)[^musuvathi2008]. - **PCT gives a quantified guarantee, not a heuristic.** For a program with *n* threads, *k* steps, and a bug of depth *d*, the randomized scheduler finds it with probability at least $\frac{1}{n \cdot k^{d-1}}$ per run (Burckhardt et al. 2010)[^burckhardt2010]. - **The bug class is shallow.** ~92% of 105 studied real-world concurrency bugs reproduce by ordering no more than four memory accesses (Lu et al. 2008)[^lu2008], so a bounded interleaving search is far more effective than its worst-case state space suggests. ## Classification - **Quality dimensions:** Reliability, Functionality. - **Area:** Concurrent and lock-free data structures, async/await state machines, schedulers, in-process message passing — implementation-level interleaving bugs. - **Guarantee:** Exhaustive, Empirical (Randomized scheduling). ## Referenced by - [Effect scope](https://quality.stereobooster.com/effect.md) · The axes - [Deterministic simulation testing](https://quality.stereobooster.com/deterministic-simulation-testing.md) · Methods - [Fuzzing](https://quality.stereobooster.com/fuzzing.md) · Methods - [Model checking](https://quality.stereobooster.com/model-checking.md) · Methods - [Verifying concurrency](https://quality.stereobooster.com/concurrency.md) · Methods - [Verifying memory safety](https://quality.stereobooster.com/memory.md) · Methods ## References [^musuvathi2008]: Musuvathi, Madanlal, Shaz Qadeer, Thomas Ball, Gérard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. 2008. "[Finding and Reproducing Heisenbugs in Concurrent Programs](https://www.usenix.org/legacy/event/osdi08/tech/full_papers/musuvathi/musuvathi.pdf)." *Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation (OSDI '08)*, 267–80. [https://www.usenix.org/legacy/event/osdi08/tech/full\\\_papers/musuvathi/musuvathi.pdf](https://www.usenix.org/legacy/event/osdi08/tech/full\_papers/musuvathi/musuvathi.pdf). [^deligiannis2023]: Deligiannis, Pantazis, Aditya Senthilnathan, Fahad Nayyar, Christopher Lovett, and Akash Lal. 2023. "[Industrial-Strength Controlled Concurrency Testing for C# Programs with Coyote](https://link.springer.com/content/pdf/10.1007/978-3-031-30820-8_26.pdf)." *Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2023)*, 433–52. [https://doi.org/10.1007/978-3-031-30820-8\\\_26](https://doi.org/10.1007/978-3-031-30820-8\_26). [^abdulla2017]: Abdulla, Parosh Aziz, Stavros Aronis, Mohamed Faouzi Atig, Bengt Jonsson, Carl Leonardsson, and Konstantinos Sagonas. 2017. "[Stateless model checking for TSO and PSO](https://link.springer.com/content/pdf/10.1007%2Fs00236-016-0275-0.pdf)." *Acta Informatica* 54 (8): 789–818. . [^burckhardt2010]: Burckhardt, Sebastian, Pravesh Kothari, Madanlal Musuvathi, and Santosh Nagarakatte. 2010. "[A Randomized Scheduler with Probabilistic Guarantees of Finding Bugs](https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/paper-83.pdf)." *Proceedings of the 15th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS XV)*, 167–78. . [^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. . ## Acronyms - DST — deterministic simulation testing - PCT — probabilistic concurrency testing - TOCTOU — time-of-check to time-of-use - TSO/PSO — total store order / partial store order