CHESS: A Systematic Testing Tool for Concurrent Software

作者: Shaz Qadeer , Madanlal Musuvathi

DOI:

关键词:

摘要: Concurrency is used pervasively in the development of large systems programs. However, concurrent programming difficult because possibility unexpected interference among concurrently executing tasks. Such often results “Heisenbugs” that appear rarely and are extremely to reproduce debug. Stress testing, which system run under heavy load for a long time, method commonly employed flush out such concurrency bugs. This form testing provides inadequate coverage has unpredictable results. paper proposes an alternative called scenario relies on systematic exhaustive We have implemented tool CHESS performing uses model checking techniques systematically generate all interleaving given scenario. scales programs found numerous previously unknown bugs had been stress tested many months prior being by CHESS. For each bug, able consistently erroneous execution manifesting thereby making it significantly easier debug problem. integrated into test frameworks code bases inside Microsoft testers daily basis.

参考文章(37)
Amin Vahdat, Ranjit Jhala, Charles Edwin Killian, James W. Anderson, Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code (Awarded Best Paper). networked systems design and implementation. ,(2007)
M. Robby, Bogor : An Extensible and Highly Modular Model Checking Framework Proc. 9th ESEC/11th FSE, 2003. ,(2003)
Scott D. Stoller, Ernie Cohen, Optimistic synchronization-based state-space reduction tools and algorithms for construction and analysis of systems. pp. 489- 504 ,(2003) , 10.1007/3-540-36577-X_36
Xuezheng Liu, Zheng Zhang, Wei Lin, Aimin Pan, WiDS checker: combating bugs in distributed systems networked systems design and implementation. pp. 19- 19 ,(2007)
J. Hartmanis, Pierre Wolper, G. Goos, J. van Leeuwen, Patrice Godefroid, Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem ,(1996)
Amin Vahdat, Ranjit Jhala, Charles Killian, James W. Anderson, Life, death, and the critical transition: finding liveness bugs in systems code networked systems design and implementation. pp. 18- 18 ,(2007)
Edmund M. Clarke, E. Allen Emerson, Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic Logic of Programs, Workshop. pp. 52- 71 ,(1981) , 10.1007/BFB0025774
J. P. Queille, J. Sifakis, Specification and verification of concurrent systems in CESAR Proceedings of the 5th Colloquium on International Symposium on Programming. pp. 337- 351 ,(1982) , 10.1007/3-540-11494-7_22
Leblanc, Mellor-Crummey, Debugging Parallel Programs with Instant Replay IEEE Transactions on Computers. ,vol. 36, pp. 471- 482 ,(1987) , 10.1109/TC.1987.1676929
Bob Boothe, Efficient algorithms for bidirectional debugging Proceedings of the ACM SIGPLAN 2000 conference on Programming language design and implementation - PLDI '00. ,vol. 35, pp. 299- 310 ,(2000) , 10.1145/349299.349339