并发程序中数据竞争检测方法

针对数据竞争检测过程中的误报和漏报问题,提出一种静态数据竞争检测方法。首先,使用控制流分析自动构造线程内和线程间函数调用图;然后,收集线程内变量访问事件信息,定义竞争产生条件并分析检测出所有可能的竞争;其次,为了提高检测的准确率,进行别名变量和别名锁的分析降低漏报和误报;最后,通过控制流分析来抽象访问事件之间的时序关系,并结合程序切片技术对访问事件的发生序关系进行判断,以此避免因忽略线程交互带来的误报。依据该方法,使用Java语言在Soot软件分析框架下实现了一个数据竞争检测工具。在实验中,对JGF和IBM Contest基准测试套件中的raytracer和airline等程序进行数据竞争检测,并与目前已有的数据竞争检测算法和工具(HB算法和RVPredict)进行对比。实验结果表明,与HB算法和RVPredict工具相比,该方法检测到的数据竞争总数分别增加了81%和16%,数据竞争检测的准确率分别提升了约14%和19%,有效地避免了数据竞争检测中的漏报和误报现象。

Data race detection approach in concurrent programs

Aiming at the problems of false positive and false negatives in data race detection, a novel static data race detection approach was proposed. Firstly, intra-thread and inter-thread function call graphs were automatically constructed via control flow analysis. Secondly, the information of variable-access events within thread were collected, and possible races were detected based on the defined data race conditions. Then, in order to improve the detection accuracy, alias variables and alias locks were analyzed to reduce false negatives and false positives, respectively. Finally, the sequential relationship between access events was abstracted through control flow analysis, and program slicing was used to determine the happens-before relationship of access events, thereby reducing false positives caused by ignoring thread interactions. A data race detection tool was implemented by Java and Soot framework based on this approach. In the experimentation, several benchmarks from JGF and IBM Contest benchmark suites, such as raytracer and airline, were selected for evaluation, and the results were compared with existing data race detection algorithm and tool (HB (Happens-Before) and RVPredict). The experimental results show that, compared with algorithm HB and tool RVPredict, total number of data races detected by the proposed approach are increased by 81% and 16% respectively, the accuracy of this approach for data race detection are respectively increased by 14% and 19%, which effectively avoids false negatives and false positives.