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

• 全文链接
• 请求原文

作   者：

张晓东;  郑庆华;  刘烃;  俞乐晨;  刘沛;  杨子江; 

作者机构：

西安理工大学计算机科学与工程学院;  西安交通大学智能网络与网络安全教育部重点实验室; 

关键词：

多线程程序测试;  证据生成;  数据竞争;  约束求解; 

期刊名称：

计算机工程与科学

基金项目：

面向国家电子税务系统的可信软件试验环境与示范应用
可信网络交易软件系统试验环境与示范应用
大规模网络化系统的优化、安全与信息服务
基于物理-信息关联分析的智能电网安全检测方法

i s s n：

1007-130X

年卷期：

2014 年 36 卷 11 期

页   码：

2047-2053

摘   要：

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