Advertisement

Dynamic Model Checking with Property Driven Pruning to Detect Race Conditions

  • Chao Wang
  • Yu Yang
  • Aarti Gupta
  • Ganesh Gopalakrishnan
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

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.

Keywords

Model Check Concurrent Program Execution Trace Data Race Partial Order Reduction 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: International Conference on Concurrency Theory. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)CrossRefGoogle Scholar
  2. 2.
    Chen, F., Rosu, G.: Parametric and sliced causality. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 240–253. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  3. 3.
    Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching time temporal logic. In: Proceedings Workshop on Logics of Programs. LNCS, vol. 131, pp. 52–71. Springer, Heidelberg (1981)CrossRefGoogle Scholar
  4. 4.
    Engler, D., Ashcraft, K.: RacerX: effective, static detection of race conditions and deadlocks. In: ACM Symposium on Operating Systems Principles, pp. 237–252. ACM, New York (2003)Google Scholar
  5. 5.
    Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Principles of programming languages, pp. 110–121 (2005)Google Scholar
  6. 6.
    Flanagan, C., Leino, K., Lillibridge, M., Nelson, G., Saxe, J., Stata, R.: Extended static checking for java. In: PLDI, pp. 234–245 (2002)Google Scholar
  7. 7.
    Ganai, M., Kundu, S., Gupta, R.: Partial order reduction for scalable testing of SystemC TLM designs. In: Design Automation Conference (2008)Google Scholar
  8. 8.
    Godefroid, P.: Partial-Order Methods for the Verification of Concurrent Systems - An Approach to the State-Explosion Problem. LNCS, vol. 1032. Springer, Heidelberg (1996)CrossRefzbMATHGoogle Scholar
  9. 9.
    Godefroid, P.: Software model checking: The VeriSoft approach. Formal Methods in System Design 26(2), 77–101 (2005)CrossRefGoogle Scholar
  10. 10.
    Holzmann, G., Najm, E., Serhrouchni, A.: SPIN model checking: An introduction. STTT 2(4), 321–327 (2000)CrossRefGoogle Scholar
  11. 11.
    Kahlon, V., Yang, Y., Sankaranarayanan, S., Gupta, A.: Fast and accurate static data-race detection for concurrent programs. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 226–239. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  12. 12.
    Leveson, N., Turner, C.: Investigation of the therac-25 accidents. IEEE Computer 26(7), 18–41 (1993)CrossRefGoogle Scholar
  13. 13.
    Mazurkiewicz, A.W.: Trace theory. In: Brauer, W., Reisig, W., Rozenberg, G. (eds.) APN 1986. LNCS, vol. 255, pp. 279–324. Springer, Heidelberg (1987)Google Scholar
  14. 14.
    Musuvathi, M., Qadeer, S.: CHESS: Systematic stress testing of concurrent software. In: Puebla, G. (ed.) LOPSTR 2006. LNCS, vol. 4407, pp. 15–16. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  15. 15.
    Necula, G., McPeak, S., Rahul, S., Weimer, W.: Cil: Intermediate language and tools for analysis and transformation of c programs. In: Horspool, R.N. (ed.) CC 2002. LNCS, vol. 2304, pp. 213–228. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  16. 16.
    Nethercote, N., Seward, J.: Valgrind: A program supervision framework. Electr. Notes Theor. Comput. Sci. 89(2) (2003)Google Scholar
  17. 17.
    Pratikakis, P., Foster, J., Hicks, M.: LOCKSMITH: context-sensitive correlation analysis for race detection. In: PLDI, pp. 320–331. ACM, New York (2006)Google Scholar
  18. 18.
    Quielle, J.P., Sifakis, J.: Specification and verification of concurrent systems in CESAR. In: Proceedings of the Fifth Annual Symposium on Programming (1981)Google Scholar
  19. 19.
    Salcianu, A., Rinard, M.: Pointer and escape analysis for multithreaded programs. In: Principles and Practices of Parallel Programming, pp. 12–23. ACM Press, New York (2001)Google Scholar
  20. 20.
    Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: A dynamic data race detector for multithreaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997)CrossRefGoogle Scholar
  21. 21.
    Sen, K., Rosu, G., Agha, G.: Detecting errors in multithreaded programs by generalized predictive analysis of executions. In: Steffen, M., Zavattaro, G. (eds.) FMOODS 2005. LNCS, vol. 3535, pp. 211–226. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  22. 22.
    Voung, J., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: Foundations of Software Engineering, pp. 205–214. ACM, New York (2007)Google Scholar
  23. 23.
    Yang, Y., Chen, X., Gopalakrishnan, G.: Inspect: A Runtime Model Checker for Multithreaded C Programs. Technical Report UUCS-08-004, University of Utah (2008)Google Scholar
  24. 24.
    Yang, Y., Chen, X., Gopalakrishnan, G., Kirby, R.: Efficient stateful dynamic partial order reduction. In: SPIN Workshop on Model Checking Software (2008)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Chao Wang
    • 1
  • Yu Yang
    • 2
  • Aarti Gupta
    • 1
  • Ganesh Gopalakrishnan
    • 2
  1. 1.NEC Laboratories AmericaPrincetonUSA
  2. 2.School of ComputingUniversity of UtahSalt Lake CityUSA

Personalised recommendations