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

J4 ›› 2014, Vol. 36 ›› Issue (11): 2047-2053.

• 论文 • 下一篇

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

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

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

收稿日期:2014-06-06 修回日期:2014-08-31 出版日期:2014-11-25 发布日期:2014-11-25
基金资助:
国家自然科学基金资助项目（91118005,91218301,61221063,61203174）；国家863计划资助项目（2012AA011003）；国家科技支撑计划（2012BAH16F02）；教育部创新团队资助项目（IRT13035）；中央高校基本科研业务费专项资金资助项目

A data race detection and witness generation
method for multithreaded programs

ZHANG Xiaodong1，ZHENG Qinghua1，LIU Ting1，YU Lechen1，LIU Pei1，YANG Zijiang2

(1.MOE Key Laboratory for Intelligent Networks and Network Security,Xi’an Jiaotong University,Xi’an 710049;
2.School of Computer Science and Engineering,Xi’an University of Technology,Xi’an 710049,China)

Received:2014-06-06 Revised:2014-08-31 Online:2014-11-25 Published:2014-11-25

摘要/Abstract

摘要：

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

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

Abstract:

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%.

Key words: multithreaded program testing;data race;constraint solving;witness generation

张晓东1，郑庆华1，刘烃1，俞乐晨1，刘沛1，杨子江2. 多线程程序数据竞争检测与证据生成方法[J]. J4, 2014, 36(11): 2047-2053.

ZHANG Xiaodong1，ZHENG Qinghua1，LIU Ting1，YU Lechen1，LIU Pei1，YANG Zijiang2. A data race detection and witness generation
method for multithreaded programs[J]. J4, 2014, 36(11): 2047-2053.

参考文献［20］

［1］	Savage S, Burrows M, Nelson G, et al. Eraser:A dynamic data race detector for multithreaded programs［J］. ACM Transactions on Computer Systems (TOCS),1997, 15(4):391411.
［2］	Erickson J, Musuvathi M, Burckhardt S, et al. Effective datarace detection for the Kernel［C］∥Proc of OSDI’10, 2010:116.
［3］	Voung J W, Jhala R, Lerner S. RELAY:Static race detection on millions of lines of code［C］∥Proc of the 6th Joint Meeting of the European Software Engineering Conference and the ACM SIGSOFT Symposium on the Foundations of Software Engineering, 2007:205214.
［4］	Kasikci B, Zamfir C, Candea G. RaceMob:Crowd sourced data race detection［C］∥Proc of SOSP’13, 2013:406422.
［5］	Wang L, Stoller S D. Runtime analysis of atomicity for multithreaded programs［J］. IEEE Transactions on Software Engineering, 2006, 32(2):93110.
［6］	Xie X, Xue J, Zhang J. Acculock:Accurate and efficient detection of data races［J］. Software:Practice and Experience, 2013,43(5):543576.
［7］	Wester B, Devecsery D, Chen P M, et al. Parallelizing data race detection［C］∥Proc of ASPLOS’13, 2013:2738.
［8］	Serebryany K, Iskhodzhanov T. ThreadSanitizer:Data race detection in practice［C］∥Proc of WBIA’09, 2009:6271.
［9］	Helgrind:A data race detector［EB/OL］.［20070101］.http://valgrind.org//docs/manual/hgmanual.html.
［10］	Marino D, Musuvathi M, Narayanasamy S. LiteRace:Effective sampling for lightweight datarace detection［C］∥Proc of PLDI’09, 2009:134143.
［11］	Flanagan C, Freund S N. FastTrack:Efficient and precise dynamic race detection［C］∥Proc of PLDI’09, 2009:121133.
［12］	Dutertre B, De Moura L. A fast lineararithmetic solver for DPLL(T)［M］∥Computer Aided Verification, Berlin Heidelberg: Springer,2006:8194.
［13］	Lattner C, Adve V. LLVM:A compilation framework for lifelong program analysis & transformation［C］∥Proc of TACAS’08, 2008:7586.
［14］	Cordeiro L,Fischer B.Verifying multithreaded software using SMTbased contextbounded model checking［C］∥Proc of ICSE’11, 2011:331340.
［15］	Gupta A,Popeea C,Rybalchenko A.Threader:A constraintbased verifier for multithreaded programs［M］∥Computer Aided Verification, Berlin Heidelberg:Springer, 2011:412417.
［16］	Engler D,Ashcraft K.RacerX:Effective,static detection of race conditions and deadlocks［C］∥Proc of SOSP’03, 2003:237252.
［17］	Von Praun C, Gross T R. Object race detection［C］∥Proc of OOPSLA’01, 2001:7082.
［18］	Wang C, Limaye R, Ganai M, et al. Tracebased symbolic analysis for atomicity violations［M］∥Tools and Algorithms for the Construction and Analysis of Systems, Berlin:Springer, 2010:328342.
［19］	Wang C, Kundu S, Limaye R, et al. Symbolic predictive analysis for concurrent programs［J］. Formal Aspects of Computing,2011,23(6):781805.
［20］	Said M, Wang C, Yang Z, et al. Generating data race witnesses by an SMTbased analysis［C］∥Proc of NASA Formal Methods, 2011:313327.

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

A data race detection and witness generation
method for multithreaded programs

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献［20］

相关文章 1

编辑推荐

Metrics

本文评价

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

A data race detection and witness generation method for multithreaded programs

PDF

可视化

摘要/Abstract

引用本文

使用本文

参考文献 ［20］

相关文章 1

编辑推荐

Metrics

本文评价

A data race detection and witness generation
method for multithreaded programs

参考文献［20］