The Complexity of Testing Message-Passing Concurrency

TL;DR

This work initiates a systematic complexity analysis of consistency testing for channel-based message-passing concurrency, parameterized by thread count, channel count, and channel capacities. It introduces two problems, VCh and VCh-rf, and develops frontier-graph based algorithms that yield tractable upper bounds when parameters are fixed, while establishing strong hardness results (including NP-hardness and OV-based lower bounds) in several natural regimes. The authors also provide linear-time solutions for fully synchronous channels and quadratic-time solutions on acyclic topologies, together with SETH-based lower bounds that pinpoint optimality of the approaches in those cases. An extensive empirical evaluation demonstrates that frontier-graph methods, especially when augmented with saturation, outperform SMT-based encodings on real Go benchmark traces and scale to large instances. Overall, the paper delineates a sharp boundary between tractable and intractable channel-consistency verification and offers practical algorithms for conjunction with predictive testing and model-checking workflows.

Abstract

A key computational question underpinning the automated testing and verification of concurrent programs is the consistency question - given a partial execution history, can it be completed in a consistent manner? Due to its importance, consistency testing has been studied extensively for memory models, as well as for database isolation levels. A common theme in all these settings is the use of shared-memory as the primal mode of interthread communication. On the other hand, modern programming languages, such as Go, Rust and Kotlin, advocate a paradigm shift towards channel-based (i.e., message-passing) communication. However, the consistency question for channel-based concurrency is currently poorly understood. In this paper we lift the study of fundamental consistency problems to channels, taking into account various input parameters, such as the number of threads executing, the number of channels, and the channel capacities. We draw a rich complexity landscape, including upper bounds that become polynomial when certain input parameters are fixed, as well as hardness lower bounds. Our upper bounds are based on algorithms that can drive the verification of channel consistency in automated verification tools. Our lower bounds characterize minimal input parameters that are sufficient for hardness to arise, and thus shed light on the intricacies of testing channel-based concurrency. In combination, our upper and lower bounds characterize the boundary of tractability/intractability of verifying channel consistency, and imply that our algorithms are often (nearly) optimal.

Figures (13)

• Figure 1: A buggy Go code snippet on channels with two possible executions
• Figure 2: Four executions on two channels $\mathtt{ch}_1$ and $\mathtt{ch}_2$ with capacities $\mathsf{cap}\mathsf{(\mathtt{ch}_1)} = 2$ and $\mathsf{cap}\mathsf{(\mathtt{ch}_2)} = 0$. Execution $\sigma_1$ is well-formed but $\sigma_2, \sigma_3, \sigma_4$ are not.
• Figure 3: A positive $\textsf{VCh}\xspace$ instance (\ref{['fig:vch-demo']}) and a negative $\textsf{VCh\xspace{-}rf}\xspace$ instance (\ref{['fig:vch-rf-demo']}). $\mathsf{cap}_1(\mathtt{ch}) = \mathsf{cap}_2(\mathtt{ch}) = 1$. Event subscripts are used to distinguish send/receive events. The same convention applies in subsequent figures.
• Figure 4: A $\textsf{VCh}\xspace$ instance (\ref{['fig:frontier-algo-demo-trace']}) and its frontier graph (\ref{['fig:frontier-algo-demo-graph']}), witnessing the consistency of $\langle \mathcal{X}, \mathsf{cap} \rangle$. There is a path from source (dotted node) to sink (dashed node), and the events labelling this path form a valid concretization, i.e., $\sigma = \mathtt{\color{colorSND}snd}_1 \cdot \mathtt{\color{colorSND}snd}_2 \cdot \mathtt{\color{colorRCV}rcv}_3 \cdot \mathtt{\color{colorRCV}rcv}_4$. Therefore, $\langle \mathcal{X}, \mathsf{cap} \rangle$ is consistent.
• Figure 5: A $\textsf{VCh\xspace{-}rf}\xspace$ instance $\langle \mathcal{X}, \mathsf{cap}, {\textsf{rf}\xspace}_{} \rangle$ (\ref{['fig:vsc-sync-graph-1']}) and the corresponding send-receive graph $G_{\mathsf{sync}}$ (\ref{['fig:vsc-sync-graph-2']}). As $G_{\mathsf{sync}}$ is acyclic, $\langle \mathcal{X}, \mathsf{cap}, {\textsf{rf}\xspace}_{} \rangle$ is consistent.

Theorems & Definitions (24)

• Remark 1
• Theorem 1.1
• Theorem 1.2
• Theorem 1.3
• Theorem 1.4
• Theorem 1.5
• Theorem 1.6
• Theorem 1.7
• Theorem 1.8
• Theorem 1.9