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