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