TY - GEN
T1 - Dynamic model checking with property driven pruning to detect race conditions
AU - Wang, Chao
AU - Yang, Yu
AU - Gupta, Aarti
AU - Gopalakrishnan, Ganesh
N1 - Funding Information:
Yu Yang and Ganesh Gopalakrishnan were supported in part by NSF award CNS-0509379 and the Microsoft HPC Institutes program.
PY - 2008
Y1 - 2008
N2 - We present a new property driven pruning algorithm in dynamic model checking to efficiently detect race conditions in multithreaded programs. The main idea is to use a lockset based analysis of observed executions to help prune the search space to be explored by the dynamic search. We assume that a stateless search algorithm is used to systematically execute the program in a depth-first search order. If our conservative lockset analysis shows that a search subspace is race-free, it can be pruned away by avoiding backtracks to certain states in the depth-first search. The new dynamic race detection algorithm is both sound and complete (as precise as the dynamic partial order reduction algorithm by Flanagan and Godefroid). The algorithm is also more efficient in practice, allowing it to scale much better to real-world multithreaded C programs.
AB - We present a new property driven pruning algorithm in dynamic model checking to efficiently detect race conditions in multithreaded programs. The main idea is to use a lockset based analysis of observed executions to help prune the search space to be explored by the dynamic search. We assume that a stateless search algorithm is used to systematically execute the program in a depth-first search order. If our conservative lockset analysis shows that a search subspace is race-free, it can be pruned away by avoiding backtracks to certain states in the depth-first search. The new dynamic race detection algorithm is both sound and complete (as precise as the dynamic partial order reduction algorithm by Flanagan and Godefroid). The algorithm is also more efficient in practice, allowing it to scale much better to real-world multithreaded C programs.
UR - http://www.scopus.com/inward/record.url?scp=56749155800&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=56749155800&partnerID=8YFLogxK
U2 - 10.1007/978-3-540-88387-6_11
DO - 10.1007/978-3-540-88387-6_11
M3 - Conference contribution
AN - SCOPUS:56749155800
SN - 354088386X
SN - 9783540883869
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 126
EP - 140
BT - Automated Technology for Verification and Analysis - 6th International Symposium, ATVA 2008, Proceedings
PB - Springer Verlag
T2 - 6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008
Y2 - 20 October 2008 through 23 October 2008
ER -