Finding Race Conditions in Erlang with QuickCheck and PULSE
📜 Abstract
We address the problem of testing and debugging concurrent, distributed Erlang applications. In concurrent programs, race conditions are a common class of bugs and are very hard to find in practice. Traditional unit testing is normally unable to help finding all race conditions, because their occurrence depends so much on timing. Therefore, race conditions are often found during system testing, where due to the vast amount of code under test, it is often hard to diagnose the error resulting from race conditions. We present three tools (QuickCheck, PULSE, and a visualizer) that in combination can be used to test and debug concurrent programs in unit testing with a much better possibility of detecting race conditions. We evaluate our method on an industrial concurrent case study and illustrate how we find and analyze the race conditions.
✨ Summary
Summary
The paper presents an approach for finding and diagnosing race conditions in concurrent Erlang programs by combining three components:
- Parallel property-based testing with QuickCheck: The authors extend QuickCheck’s state-machine testing to execute two independent command sequences concurrently. Correctness is defined through an atomicity or linearizability-style criterion: the observed results must be explainable by some sequential ordering of the operations. QuickCheck’s shrinking reduces failing executions to small, minimally parallel counterexamples.
- PULSE: PULSE is a cooperative, user-level Erlang scheduler that instruments selected processes and randomly controls relevant scheduling events, including message delivery, process creation, receiving, linking, and selected external side effects. It produces repeatable executions when given the same random seed and can expose fine-grained interleavings that the standard Erlang scheduler may rarely produce.
- Trace visualization: Execution traces are rendered as process-oriented graphs. The visualizer uses message-flow information and Lamport’s happens-before relation to suppress redundant ordering edges, making potentially problematic side-effect orderings easier to inspect.
The industrial case study is an optimized Erlang process registry implemented with ETS tables and asynchronous server communication. The method exposed two race conditions. One involved message overtaking and inconsistent cleanup of forward and reverse registry entries. The other arose when multiple clients attempted to register a dead process concurrently after independently auditing the registry. The authors fixed the defects and identified a further design-level race that would require three concurrent branches to expose. They therefore simplified the production API so that a process could register only itself.
The paper’s main technical contribution is a practical testing workflow that combines randomized parallel test generation, repeatable scheduling, automated shrinking, and graphical trace analysis. The authors deliberately use two concurrent branches because the number of possible interleavings grows combinatorially with additional branches. The approach does not attempt exhaustive exploration and depends on deterministic external inputs and adequate probability of provoking a race in a given test.
Subsequent influence
The approach was directly extended in later Erlang research. Hughes and Bolinder applied the same combination of QuickCheck-generated parallel tests, randomized scheduling, and sequential-consistency checking to dets, a substantially larger database component of Erlang/OTP. They reported finding five race conditions, including two that could plausibly explain production failures. (research.chalmers.se)
The paper also served as cited prior work for Concuerror, a later Erlang tool that moved from randomized schedule probing toward systematic exploration of process interleavings, with instrumentation, replay, and preemption bounding. Concuerror’s published descriptions explicitly position the earlier QuickCheck/PULSE method as part of the foundation for testing concurrent Erlang programs. (researchgate.net)
Bibliographic and publisher records confirm the paper’s authorship, conference venue, publication date, and pages. (doi.org)