Skip to main content
SpringerLink
Log in

Hybrid Analysis for Partial Order Reduction of Programs with Arrays

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2016)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 9583))

Abstract

An important component of efficient approaches to software model checking and systematic concurrency testing is partial order reduction, which eliminates redundant non-deterministic thread scheduling choices during the state space traversal. Thread choices have to be created only at the execution of actions that access the global state visible by multiple threads, so the key challenge is to precisely determine the set of such globally-relevant actions. This includes accesses to object fields and array elements, and thread synchronization.

However, some tools completely disable thread choices at actions that access individual array elements in order to avoid state explosion. We show that they can miss concurrency errors in such a case. Then, as the main contribution, we present a new hybrid analysis that identifies globally-relevant actions that access arrays. Our hybrid analysis combines static analysis with dynamic analysis, usage of information from dynamic program states, and symbolic interpretation of program statements. Results of experiments with two popular approaches to partial order reduction show that usage of the hybrid analysis (1) eliminates many additional redundant thread choices and (2) improves the performance of software model checking on programs that use arrays.

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. Ball, T., Burckhardt, S., Coons, K.E., Musuvathi, M., Qadeer, S.: Preemption sealing for efficient concurrency testing. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010. LNCS, vol. 6015, pp. 420–434. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  2. Concurrency Tool Comparison repository. https://facwiki.cs.byu.edu/vv-lab/index.php/Concurrency_Tool_Comparison

  3. Dwyer, M., Hatcliff, J., Ranganath, V., Robby, : Exploiting object escape and locking information in partial-order reductions for concurrent object-oriented programs. Formal Meth. Syst. Des. 25, 199–240 (2004)

    Article  MATH  Google Scholar 

  4. Flanagan, C., Godefroid, P.: Dynamic partial-order reduction for model checking software. In: Proceedings of POPL 2005. ACM (2005)

    Google Scholar 

  5. Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996)

    MATH  Google Scholar 

  6. Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. In: Bošnački, D., Edelkamp, S. (eds.) SPIN 2007. LNCS, vol. 4595, pp. 95–112. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. The Java Grande Forum Benchmark Suite. https://www2.epcc.ed.ac.uk/computing/research_activities/java_grande/index_1.html

  8. Java Pathfinder: a system for verification of Java programs. http://babelfish.arc.nasa.gov/trac/jpf/

  9. Li, D., Srisa-an, W., Dwyer, M.B.: SOS: saving time in dynamic race detection with stationary analysis. In: Proceedings of OOPSLA 2011. ACM (2011)

    Google Scholar 

  10. Manson, J., Pugh, W., Adve, S.V.: The Java memory model. In: Proceedings of POPL 2005. ACM (2005)

    Google Scholar 

  11. Marron, M., Mendez-Lojo, M., Hermenegildo, M., Stefanovic, D., Kapur, D.: Sharing analysis of arrays, collections, and recursive structures. In: Proceedings of PASTE 2008. ACM (2008)

    Google Scholar 

  12. Noonan, E., Mercer, E., Rungta, N.: Vector-clock based partial order reduction for JPF. ACM SIGSOFT Softw. Eng. Notes 39(1), 1–5 (2014)

    Article  Google Scholar 

  13. pjbench: Parallel Java Benchmarks. https://bitbucket.org/pag-lab/pjbench

  14. Parizek, P., Jancik, P.: Approximating happens-before order: interplay between static analysis and state space traversal. In: Proceedings of SPIN 2014. ACM (2014)

    Google Scholar 

  15. Parizek, P., Lhotak, O.: Identifying future field accesses in exhaustive state space traversal. In: Proceedings of ASE 2011. IEEE CS (2011)

    Google Scholar 

  16. Parizek, P., Lhotak, O.: Model checking of concurrent programs with static analysis of field accesses. Sci. Comput. Program. 98, 735–763 (2015)

    Article  Google Scholar 

  17. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Trans. Program. Lang. Syst. 24(3), 217–298 (2002)

    Article  Google Scholar 

  18. Schaefer, M., Sridharan, M., Dolby, J., Tip, F.: Dynamic determinacy analysis. In: Proceedings of PLDI 2013. ACM (2013)

    Google Scholar 

  19. Sewell, P., Sarkar, S., Owens, S., Nardelli, F.Z., Myreen, M.: x86-TSO: a rigorous and usable programmer’s model for x86 multiprocessors. Comm. ACM 53(7), 89–97 (2010)

    Article  Google Scholar 

  20. Thomson, P., Donaldson, A., Betts, A.: Concurrency testing using schedule bounding: an empirical study. In: Proceedings of PPoPP 2014. ACM (2014)

    Google Scholar 

  21. Unkel, C., Lam, M.S.: Automatic inference of stationary fields: a generalization of Java’s final fields. In: Proceedings of POPL 2008. ACM (2008)

    Google Scholar 

  22. Visser, W., Havelund, K., Brat, G., Park, S., Lerda, F.: Model checking programs. Autom. Softw. Eng. 10(2), 203–232 (2003)

    Article  Google Scholar 

  23. Wala, T.J.: Watson Libraries for Analysis. http://wala.sourceforge.net/

  24. Yang, Y., Chen, X., Gopalakrishnan, G.C., Kirby, R.M.: Efficient stateful dynamic partial order reduction. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 288–305. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

Download references

Acknowledgments

This work was partially supported by the Grant Agency of the Czech Republic project 13-12121P.

Author information

Authors and Affiliations

  1. Department of Distributed and Dependable Systems, Faculty of Mathematics and Physics, Charles University in Prague, Prague, Czech Republic

    Pavel Parízek

Authors
  1. Pavel Parízek
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Pavel Parízek .

Editor information

Editors and Affiliations

  1. EPFL IC-DO, Lausanne, Switzerland

    Barbara Jobstmann

  2. Microsoft Research, Redmond, Washington, USA

    K. Rustan M. Leino

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Parízek, P. (2016). Hybrid Analysis for Partial Order Reduction of Programs with Arrays. In: Jobstmann, B., Leino, K. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2016. Lecture Notes in Computer Science(), vol 9583. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-49122-5_14

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-49122-5_14

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-49121-8

  • Online ISBN: 978-3-662-49122-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation