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

摘要：

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

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

所属期刊栏目：36

分类号：TP311(计算技术、计算机技术)

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

在线出版日期：2014-12-25（万方平台首次上网日期，不代表论文的发表时间）

页数：共7页

页码：2047-2053