一句话：提出 SeqCheck，可靠判定事件序列能否按指定顺序发生以预测并发缺陷，并在双线程轨迹上完备。
并发缺陷极难检测。近年动态技术可实现可靠分析，M2 甚至对双线程完备，但它只判定两个事件能否连续发生。真实缺陷常涉及更多事件与线程，且某些缺陷对应两个或多个事件顺序可交换、即使它们并非连续发生。为此，作者提出 SeqCheck，可靠判定一个事件序列能否按指定顺序发生；该有序序列表示潜在并发缺陷，多种已知缺陷形式可编码成事件序列。SeqCheck 显式分析分支事件，并配有一组高效算法。作者证明 SeqCheck 是可靠的，且在双线程轨迹上完备。
Concurrency bugs are extremely difficult to detect. Recently, several dynamic techniques achieve sound analysis. M2 is even complete for two threads. It is designed to decide whether two events can occur consecutively. However, real-world concurrency bugs can involve more events and threads. Some can occur when the order of two or more events can be exchanged even if they occur not consecutively. We propose a new technique SeqCheck to soundly decide whether a sequence of events can occur in a specified order. The ordered sequence represents a potential concurrency bug. And several known forms of concurrency bugs can be easily encoded into event sequences where each represents a way that the bug can occur. To achieve it, SeqCheck explicitly analyzes branch events and includes a set of efficient algorithms. We show that SeqCheck is sound; and it is also complete on traces of two threads.
DOI 原文 ·
@inproceedings{paperbot6451,
title = {Sound and efficient concurrency bug prediction},
author = {Yan Cai and Hao Yun and Jinqiu Wang and Lei Qiao and Jens Palsberg},
booktitle = {FSE},
year = {2021},
doi = {10.1145/3468264.3468549}
}