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

( 1.西安交通大学智能网络与网络安全教育部重点实验室，陕西 西安 710049；2.西安理工大学计算机科学与工程学院，陕西 西安 710049)

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

张晓东1，郑庆华1，刘 烃1，俞乐晨1，刘 沛1，杨子江2

( 1.西安交通大学智能网络与网络安全教育部重点实验室，陕西 西安 710049；2.西安理工大学计算机科学与工程学院，陕西 西安 710049)

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

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

1 引言

随着处理器多核化的普及，多线程技术已经成为软件编程中提高CPU利用率不可或缺的技术。然而，由于线程之间交织的不确定性，多线程程序执行过程中可能会出现一些难以预料的行为导致程序出错，例如对临界区没有做好同步工作而导致的数据竞争问题。……