Fuzzing channel-based concurrency runtimes using types and effects
Quentin Stiévenart, Magnus Madsen
Abstract
Modern programming languages support concurrent programming based on channels and processes. Channels enable synchronous and asynchronous message-passing between independent light-weight processes making it easy to express common concurrency patterns.
The implementation of channels and processes in compilers and language runtimes is a difficult task that relies heavily on traditional and error-prone low-level concurrency primitives, raising concerns about correctness and reliability.
In this paper, we present an automatic program generation technique to test such programming language implementations. We define a type and effect system for programs that communicate over channels and where every execution is guaranteed to eventually terminate. We can generate and run such programs, and if a program fails to terminate, we have found a bug in the programming language implementation.
We implement such an automatic program generator and apply it to Go, Kotlin, Crystal, and Flix. We find two new bugs in Flix, and reproduce two bugs; one in Crystal and one in Kotlin.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Builds on2
Related papers
- Automatically detecting and fixing concurrency bugs in go software systemsZiheng Liu, Shuofei Zhu, Boqin Qin, Hao Chen et al.ASPLOS 2021 · 32 citations
- Who goes first? detecting go concurrency bugs via message reorderingZiheng Liu, Shihao Xia, Yu Liang, Linhai Song et al.ASPLOS 2022 · 21 citations
- The Complexity of Testing Message-Passing ConcurrencyZheng Shi, Lasse Møldrup, Umang Mathur, Andreas PavlogiannisPOPL 2026 · 2 citations
- Effective Concurrency Testing for Go via Directional Primitive-Constrained Interleaving ExplorationZongze Jiang, Ming Wen, Yixin Yang, Chao Peng et al.ASE 2023 · 6 citations
- Automated Verification of Go Programs via Bounded Model CheckingNicolas Dilley, Julien LangeASE 2021 · 21 citations
