paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Tolerate Control-Flow Changes for Sound Data Race Prediction

容忍控制流变化以实现可靠的数据竞争预测
ICSE 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE)2023匹配度 4/10 · 论文研究并发程序的数据竞争可靠预测,属于程序分析与形式化验证,但未涉及用户画像中的核心方向:LLM/Agent 与静态分析交叉、ML/Agentic 程序分析、浮点程序分析或贝叶斯程序分析。其理论+工业落地特点符合部分研究偏好,但主题匹配度有限。引用 5 inbox
Shihao Zhu, Yuqi Guo, Long Zhang, Yan Cai
crossref: 2026-09-12dblp: 2026-09-12

AI 速览

一句话:提出不动点事件与偏序模型,可可靠推断带控制流变化的见证轨迹,从而检测更多数据竞争。

数据竞争威胁并发程序正确性。已有可靠预测分析假设任一读事件都可能影响预测轨迹的控制流,故要求其读取原轨迹中相同或同一事件的值(或仅略作放松),严重限制预测能力并漏报竞争。本文提出不动点事件概念与新的偏序模型,既能用见证轨迹预测竞争,也能可靠推断存在潜在控制流变化的见证轨迹,提高并发覆盖并可靠检测更多竞争。作者实现 ToccRACE,在七个真实程序和 MySQL(427 条轨迹、3.4TB)上评估;相比 SeqCheck,唯一/动态竞争分别多检出 84.4%/200% 和 52.22%/49.8%,开销合理,且双线程下可靠且完备。

问题
现有基于轨迹的可靠数据竞争预测假设读事件会影响控制流,因而强制读值与原轨迹一致或近似一致,导致预测能力受限并漏报真实竞争。
方法
引入不动点事件(Fix-Point Event)和新的偏序模型,使预测可容忍潜在控制流变化,并用工具 ToccRACE 实现。
评估
在七个真实程序及 MySQL 的大规模轨迹(3.4TB)上,与 SeqCheck 对比,ToccRACE 多检出大量唯一/动态竞争且时间内存开销合理;论文还说明其健全性及双线程完备性。
原文摘要(Abstract)

Data races seriously threaten the correctness of concurrent programs. Earlier works can report false positives. Recently, trace-based predictive analysis has achieved sound results by inferring feasible traces based on sound partial orders or constraint solvers. However, they hold the same assumption: any read event may affect the control-flow of a predicted trace. Thus, being control-flow sensitive, they have to enforce any read event (in an inferred trace) to either read the same value or a value from the same event as that in the original trace, albeit some slightly relax this. This (even with relaxation) severely limits their predictive ability and many true data races can be missed. We introduce the concept of Fix-Point Event and propose a new partial order model. This allows us to not only predict races with witness traces (like existing works with no control-flow changes) but also soundly infer existences of witness traces with potential control-flow changes. Thus, we can achieve a higher concurrency coverage and detect more data races soundly. We have implemented above as a tool ToccRACE and conducted a set of experiments on a benchmark of seven real-world programs and a large-scale software MySQL, where MySQL produced 427 traces with a total size of 3.4TB. Compared with the state-of-the-art sound data race detector SeqCheck,ToccRACE is significantly more effective by detecting 84.4%/200% more unique/dynamic races on the benchmark programs and 52.22%/49.8% more unique/dynamic races on MySQL, incurring reasonable time and memory costs (about 1.1x×43.5x on the benchmark programs and 10x/1.03x on MySQL). Furthermore, ToccRACE is sound and is comnlcte on two threads.

链接与引用

DOI 原文 · DBLP

BibTeX
@inproceedings{ZhuGZC23,
  title = {Tolerate Control-Flow Changes for Sound Data Race Prediction},
  author = {Shihao Zhu and Yuqi Guo and Long Zhang and Yan Cai},
  booktitle = {ICSE},
  year = {2023},
  doi = {10.1109/icse48619.2023.00118}
}