多线程程序数据竞争检测与证据生成方法  

A data race detection and witness generation method for multithreaded programs

作　　者：张晓东[1] 郑庆华[1] 刘烃[1] 俞乐晨 刘沛[1] 杨子江[2] 

机构地区：[1]西安交通大学智能网络与网络安全教育部重点实验室,陕西西安710049 [2]西安理工大学计算机科学与工程学院,陕西西安710049

出　　处：《计算机工程与科学》2014年第11期2047-2053,共7页Computer Engineering & Science

基　　金：国家自然科学基金资助项目(91118005;91218301;61221063;61203174);国家863计划资助项目(2012AA011003);国家科技支撑计划(2012BAH16F02);教育部创新团队资助项目(IRT13035);中央高校基本科研业务费专项资金资助项目

摘　　要：数据竞争是多线程程序最为常见的问题之一。由于线程交织导致状态空间爆炸,多线程程序数据竞争引起的错误检测难度大、成本高、精度低;此外,即使检测到数据竞争,由于线程调度难以控制、执行过程难以复现,错误难以复现和定位。提出了一种多线程程序数据竞争检测与证据生成方法,基于程序语义分析和执行过程监测,构建程序的执行路径约束模型和数据竞争条件,将多线程程序数据竞争检测问题转化为约束求解问题,降低检测难度,提高检测精度;利用SMT求解器计算可能的数据竞争,并生成触发该数据竞争的程序执行序列,协助程序员定位和验证错误。实验中对10个程序进行了测试,相比现有数据竞争检测工具threadsanitizer和helgrind,本方法检测出的数据竞争多出287.5%和264.7%,且没有误报,而其他方法平均误报率为10.5%和9.8%。Data race is a common problem in multithreaded programs.Due to the state explosion of thread interleaving,it is difficult to accurately detect bugs triggered by data races.Moreover,it is hard to replay and triage such bugs because of the facts that thread scheduling is difficult to control and the number of interleaving is astronomically large.A data race detection and witness generation method for multithreaded programs is proposed.A semantic model is designed to encode the execution path and the condition of data races as first-order logic formula.The satisfiability of the formula,solvable by constraint solvers,indicates the existence of data races under multiple thread interleavings without requiring repeated executions.The solutions produced by an SMT solver serve as witnesses to localize and verify data races.In the experiments,we compare existing tools threadsanitizer and helgrind with ours to detect the data races for 10 multithreaded programs.It is shown that our method can detect 287.5 ％ and 264.7％ more bugs respectively without false alarm,while the false alarm positive rate of threadsanitizer and helgrind are 10.5％ and 9.8％.

关 键 词：多线程程序测试 数据竞争 约束求解 证据生成 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]