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

• 作者: 俞乐晨 刘沛 刘烃 张晓东 杨子江 郑庆华
• 来源期刊: 计算机工程与科学
• 学科: 工学
• 关键词: 多线程程序测试 数据竞争 约束求解 证据生成
• 年，卷（期）: 2014,（11）
• 所属期刊栏目: 高性能计算
• 页码范围: 2047-2053
• 页数: 7页
• 分类号: TP311
• 字数: 7376字
• 语种: 中文
• DOI: 10.3969/j.issn.1007-130X.2014.11.001

摘要

数据竞争是多线程程序最为常见的问题之一.由于线程交织导致状态空间爆炸,多线程程序数据竞争引起的错误检测难度大、成本高、精度低;此外,即使检测到数据竞争,由于线程调度难以控制、执行过程难以复现,错误难以复现和定位.提出了一种多线程程序数据竞争检测与证据生成方法,基于程序语义分析和执行过程监测,构建程序的执行路径约束模型和数据竞争条件,将多线程程序数据竞争检测问题转化为约束求解问题,降低检测难度,提高检测精度;利用SMT求解器计算可能的数据竞争,并生成触发该数据竞争的程序执行序列,协助程序员定位和验证错误.实验中对10个程序进行了测试,相比现有数据竞争检测工具threadsanitizer和helgrind,本方法检测出的数据竞争多出287.5％和264.7％,且没有误报,而其他方法平均误报率为10.5％和9.8％.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	郑庆华	西安交通大学智能网络与网络安全教育部重点实验室	118	1659	22.0	36.0
2	张晓东	西安交通大学智能网络与网络安全教育部重点实验室	48	216	8.0	12.0
3	刘烃	西安交通大学智能网络与网络安全教育部重点实验室	7	61	5.0	7.0
4	刘沛	西安交通大学智能网络与网络安全教育部重点实验室	3	16	3.0	3.0
5	俞乐晨	西安交通大学智能网络与网络安全教育部重点实验室	2	14	2.0	2.0
6	杨子江	西安理工大学计算机科学与工程学院	1	5	1.0	1.0