paperbot · PL 论文追踪

全部论文 待读 收藏

P2 The Complexity of Testing Message-Passing Concurrency

消息传递并发测试的复杂度
POPL 10(POPL)2026匹配度 3/10 · 论文属于程序验证/并发一致性测试,和静态分析、程序验证有方法论上的间接交集,也有理论刻画与工程实现;但它不涉及 LLM/Agent、Agentic 程序、浮点程序分析或贝叶斯程序分析,未命中用户当前核心研究方向。引用 2 inbox
Zheng Shi, Lasse Møldrup, Umang Mathur, Andreas Pavlogiannis
crossref: 2026-09-10

AI 速览

一句话:系统刻画通道式消息传递并发一致性测试的复杂度版图,给出近最优算法与实验验证。

并发程序自动化测试与验证的核心问题之一是一致性:给定部分执行历史,能否一致地补全?共享内存模型与数据库隔离级别已有大量研究,但现代语言(Go、Rust、Kotlin)常用的通道式消息传递并发尚缺乏理解。本文研究通道并发的一致性复杂度,考虑线程数、通道数和通道容量等参数,建立复杂度的上下界:当某些参数固定时上界为多项式时间,同时给出硬度下界,并确定导致难解性的最小参数组合,表明所给算法常近最优。作者实现主一致性检查算法并设计优化,在103个开源Go项目实例上评估,可扩展至约100万事件,且显著快于约束求解方法。

问题
通道式(消息传递)并发程序的一致性测试与验证:给定部分执行历史,能否以一致方式补全?该问题此前在通道模型下理解不足。
方法
以线程数、通道数、通道容量等为参数进行复杂度分析,给出多项式时间上界算法与硬度下界,并实现主一致性检查算法及其优化。
评估
在103个来自开源Go项目的实例上评估,与约束求解方法对比;算法可扩展至约100万事件,且运行时间显著更快。
原文摘要(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. We have also implemented our main consistency checking algorithm and designed optimizations to enhance its performance. We evaluated the performance of our implementation over a set of 103 instances obtained from open source Go projects, and compared it against a constraint-solving based algorithm. Our experimental results demonstrate the power of our consistency-checking algorithm; it scales to around 1M events, and is significantly faster in running-time performance, compared to a constraint-solving approach.

链接与引用

DOI 原文 · arXiv · PDF(开放获取) · DBLP

BibTeX
@article{ShiMMP26,
  title = {The Complexity of Testing Message-Passing Concurrency},
  author = {Zheng Shi and Lasse Møldrup and Umang Mathur and Andreas Pavlogiannis},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {10},
  number = {POPL},
  year = {2026},
  doi = {10.1145/3776643}
}