paperbot · PL 论文追踪

全部论文 待读 收藏

P2 Data race detection on compressed traces

压缩轨迹上的数据竞争检测
FSE Proceedings of the 2018 26th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering2018匹配度 2/10 · 论文研究压缩轨迹上的数据竞争检测,属于并发程序分析与动态分析算法,与用户核心方向(PL与AI/LLM交叉、浮点程序分析、贝叶斯程序分析)没有直接关联。仅在“程序分析算法”这一广义层面上有弱联系。引用 14 inbox
Dileep Kini, Umang Mathur, Mahesh Viswanathan
crossref: 2026-09-12

AI 速览

一句话:提出在 SLP 压缩的轨迹表示上直接进行数据竞争检测的线性时间算法,覆盖 happens-before 与 lockset 两种经典方法。

程序执行轨迹往往极为庞大,直接分析代价高昂。本文关注一类特殊压缩形式——直线程序(SLP),它是恰好生成单条字符串(即被表示的轨迹)的上下文无关文法。作者研究两种经典的数据竞争检测方法:基于 happens-before 关系的方法与基于锁集(lockset)纪律的方法,并分别给出算法,其运行时间与压缩后的 SLP 表示规模呈线性关系,而非与解压后轨迹长度相关。由于真实程序执行几乎总会呈现可大幅压缩的模式,这些算法相比分析未压缩轨迹有望带来显著加速。作者在标准基准上进行了实验评估,结果证实了这一预期。

问题
如何在不解压的前提下,对以 SLP 形式压缩的程序轨迹高效地检测数据竞争,避免分析规模巨大的原始轨迹。
方法
针对 happens-before 关系与 lockset 纪律两种经典竞争检测方法,分别设计了时间复杂度与压缩后 SLP 表示规模成线性的算法。
评估
在标准基准上对两种新算法进行实验评估,验证了相对于分析未压缩轨迹的显著加速效果。
原文摘要(Abstract)

We consider the problem of detecting data races in program traces that have been compressed using straight line programs (SLP), which are special context-free grammars that generate exactly one string, namely the trace that they represent. We consider two classical approaches to race detection --- using the happens-before relation and the lockset discipline. We present algorithms for both these methods that run in time that is linear in the size of the compressed, SLP representation. Typical program executions almost always exhibit patterns that lead to significant compression. Thus, our algorithms are expected to result in large speedups when compared with analyzing the uncompressed trace. Our experimental evaluation of these new algorithms on standard benchmarks confirms this observation.

链接与引用

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

BibTeX
@inproceedings{paperbot4621,
  title = {Data race detection on compressed traces},
  author = {Dileep Kini and Umang Mathur and Mahesh Viswanathan},
  booktitle = {FSE},
  year = {2018},
  doi = {10.1145/3236024.3236025}
}