Skip to main content
SpringerLink
Log in

Path-Sensitive Race Detection with Partial Order Reduced Symbolic Execution

  • Conference paper
  • First Online:
Software Engineering and Formal Methods (SEFM 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8938))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. King, J.: Symbolic execution and program testing. Commun. ACM 19(7), 385–394 (1976)

    Article  MATH  Google Scholar 

  2. de Moura, L., Bjorner, N.: Satisfiability modulo theories: introduction and applications. Commun. ACM 54(9), 69–77 (2011)

    Article  Google Scholar 

  3. Cadar, C., et al.: Symbolic execution for software testing in practice - preliminary assessment. In: International Conference on Software Engineering (2011)

    Google Scholar 

  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)

    Article  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  6. Lamport, L.: Time, clocks, and the ordering of events in a distributed system. Commun. ACM 21(7), 558–565 (1978)

    Article  MATH  Google Scholar 

  7. United States National Security Agency, Center for Assured Software: Juliet Test Suite v1.1 for C/C++, December 2011

    Google Scholar 

  8. Martin, R., Barnum, S., Christey, S.: Being explicit about security weaknesses. In: Blackhat DC (2007)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  10. Parr, T.: Language Implementation Patterns. Pragmatic Bookshelf, Lewisville (2010)

    Google Scholar 

  11. Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB Standard Version 2.0., December 2010

    Google Scholar 

  12. Laskavaia, A.: Codan- C/C++ static analysis framework for CDT. In: EclipseCon (2011)

    Google Scholar 

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

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  16. Banerjee, U., Bliss, B., Ma, Z., Petersen, P.: A theory of data race detection. In: PADTAD (2006)

    Google Scholar 

  17. Flanagan, C., Freund, S.: FastTrack: efficient and precise dynamic race detection. In: PLDI (2009)

    Google Scholar 

  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)

    Article  Google Scholar 

  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. Naik, M.: Effective static race detection for Java. Ph.D. thesis, Stanford University (2008)

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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. Lu, S., Jiang, W., Zhou, Y.: A study of interleaving coverage criteria. In: ECEC/FSE (2007)

    Google Scholar 

Download references

Acknowledgement

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

Author information

Authors and Affiliations

  1. Chair for IT Security, TU München, Boltzmannstrasse 3, 85748, Garching, Germany

    Andreas Ibing

Authors
  1. Andreas Ibing
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andreas Ibing .

Editor information

Editors and Affiliations

  1. University of Malaga, Malaga, Spain

    Carlos Canal

  2. LIG Lab, Saint Martin d'Hères Cedex, France

    Akram Idani

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Ibing, A. (2015). Path-Sensitive Race Detection with Partial Order Reduced Symbolic Execution. In: Canal, C., Idani, A. (eds) Software Engineering and Formal Methods. SEFM 2014. Lecture Notes in Computer Science(), vol 8938. Springer, Cham. https://doi.org/10.1007/978-3-319-15201-1_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-15201-1_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-15200-4

  • Online ISBN: 978-3-319-15201-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation