Path-Sensitive Race Detection with Partial Order Reduced Symbolic Execution

Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8938)

Abstract

This paper presents a combination of symbolic execution and partial order reduction to achieve path-sensitive race detection. The presented approach limits the complexity of symbolic execution of multi-threaded code by applying it with a fixed scheduling algorithm only. Alternative thread interleavings are generated from fixed-scheduling ones with ample set partial order reduction on an abstraction level of thread interactions. Races are detected on the abstraction level. The proposed algorithm is implemented as plug-in extension of Eclipse CDT and evaluated by running it on the race condition test cases from the Juliet suite.

Notes

Acknowledgement

This work was funded by the German Ministry for Education and Research (BMBF) under grant 01IS13020.

References

  1. 1.
    King, J.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)CrossRefMATHGoogle Scholar
  2. 2.
    de Moura, L., Bjorner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)CrossRefGoogle Scholar
  3. 3.
    Cadar, C., et al.: Symbolic execution for software testing in practice - preliminary assessment. In: International Conference on Software Engineering (2011)Google Scholar
  4. 4.
    Pasareanu, C., Visser, W.: A survey of new trends in symbolic execution for software testing and analysis. Int. J. Softw. Tools Technol. Transfer 11, 339–353 (2009)CrossRefGoogle Scholar
  5. 5.
    Clarke, E., Grumberg, O., Minea, M., Peled, D.: State space reduction using partial order techniques. Softw. Tools Technol. Transfer 2(3), 279–287 (1999)CrossRefMATHGoogle Scholar
  6. 6.
    Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)CrossRefMATHGoogle Scholar
  7. 7.
    United States National Security Agency, Center for Assured Software: Juliet Test Suite v1.1 for C/C++, December 2011Google Scholar
  8. 8.
    Martin, R., Barnum, S., Christey, S.: Being explicit about security weaknesses. In: Blackhat DC (2007)Google Scholar
  9. 9.
    Ibing, A.: Parallel SMT-constrained symbolic execution for eclipse CDT/Codan. In: Yenigün, H., Yilmaz, C., Ulrich, A. (eds.) ICTSS 2013. LNCS, vol. 8254, pp. 196–206. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  10. 10.
    Parr, T.: Language Implementation Patterns. Pragmatic Bookshelf, Lewisville (2010)Google Scholar
  11. 11.
    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard Version 2.0., December 2010Google Scholar
  12. 12.
    Laskavaia, A.: Codan- C/C++ static analysis framework for CDT. In: EclipseCon (2011)Google Scholar
  13. 13.
    Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, New York (1994)Google Scholar
  14. 14.
    Peled, D.: Combining partial order reduction with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994)CrossRefGoogle Scholar
  15. 15.
    Savage, S., Burrows, M., Nelson, G., Sobalvarro, P., Anderson, T.: Eraser: a dynamic data race detector for multi-threaded programs. ACM Trans. Comput. Syst. 15(4), 391–411 (1997)CrossRefGoogle Scholar
  16. 16.
    Banerjee, U., Bliss, B., Ma, Z., Petersen, P.: A theory of data race detection. In: PADTAD (2006)Google Scholar
  17. 17.
    Flanagan, C., Freund, S.: FastTrack: efficient and precise dynamic race detection. In: PLDI (2009)Google Scholar
  18. 18.
    Abadi, M., Flanagan, C., Freund, S.: Types for safe locking: static race detection for Java. ACM Trans. Program. Lang. Syst. 28(2), 207–255 (2006)CrossRefGoogle Scholar
  19. 19.
    Voung, J., Jhala, R., Lerner, S.: RELAY: static race detection on millions of lines of code. In: ACM Symposium Foundations of Software Engineering (ESEC-FSE) (2007)Google Scholar
  20. 20.
    Naik, M.: Effective static race detection for Java. Ph.D. thesis, Stanford University (2008)Google Scholar
  21. 21.
    Kahlon, V., Wang, C., Gupta, A.: Monotonic partial order reduction: an optimal symbolic partial order reduction technique. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 398–413. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  22. 22.
    Qadeer, S., Rehof, J.: Context-bounded model checking of concurrent software. In: Halbwachs, N., Zuck, L.D. (eds.) TACAS 2005. LNCS, vol. 3440, pp. 93–107. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  23. 23.
    Rabinovitz, I., Grumberg, O.: Bounded model checking of concurrent programs. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 82–97. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  24. 24.
    Cordeiro, L.: SMT-based bounded model checking of multi-threaded software in embedded systems. Ph.D. thesis, University of Southampton (2011)Google Scholar
  25. 25.
    Lu, S., Jiang, W., Zhou, Y.: A study of interleaving coverage criteria. In: ECEC/FSE (2007)Google Scholar

Copyright information

© Springer International Publishing Switzerland 2015

Authors and Affiliations

  1. 1.Chair for IT SecurityTU MünchenGarchingGermany

Personalised recommendations