Skip to main content
SpringerLink
Log in

Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs

  • Conference paper
  • First Online:
Book cover Automated Technology for Verification and Analysis (ATVA 2016)

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

Abstract

Lazy sequentialization has emerged as one of the most promising approaches for concurrent program analysis but the only efficient implementation given so far works just for bounded programs. This restricts the approach to bug-finding purposes. In this paper, we describe and evaluate a new lazy sequentialization translation that does not unwind loops and thus allows to analyze unbounded computations, even with an unbounded number of context switches. In connection with an appropriate sequential backend verification tool it can thus also be used for the safety verification of concurrent programs, rather than just for bug-finding. The main technical novelty of our translation is the simulation of the thread resumption in a way that does not use gotos and thus does not require that each statement is executed at most once. We have implemented this translation in the UL-CSeq tool for C99 programs that use the pthreads API. We evaluate UL-CSeq on several benchmarks, using different sequential verification backends on the sequentialized program, and show that it is more effective than previous approaches in proving the correctness of the safe benchmarks, and still remains competitive with state-of-the-art approaches for finding bugs in the unsafe benchmarks.

Partially supported by EPSRC grant No. EP/M008991/1, and MIUR-FARB 2013-2016 grants.

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

Notes

  1. 1.

    http://users.ecs.soton.ac.uk/gp4/cseq/files/ul-cseq-0.2_64bit.tar.gz.

  2. 2.

    https://github.com/seahorn/seahorn/releases/download/v0.1.0/SeaHorn-0.1.0-Linu xx8664.tar.gz.

  3. 3.

    http://ultimate.informatik.uni-freiburg.de/downloads/svcomp2016/UltimateAutom izer.zip.

  4. 4.

    http://cpachecker.sosy-lab.org/CPAchecker-1.4-unix.tar.bz2.

  5. 5.

    http://www.cprover.org/concurrent-impact/impara-linux64-0.2.tgz.

  6. 6.

    http://www.cprover.org/satabs/download/satabs-3-2-linux-32.tgz.

  7. 7.

    http://www.cprover.org/cbmc/download/cbmc-5-4-linux-64.tgz.

  8. 8.

    http://users.ecs.soton.ac.uk/gp4/cseq/files/lazy-cseq-1.0.tar.gz.

  9. 9.

    http://vsl.cis.udel.edu/lib/sw/civl/1.5/svcomp16/CIVL-1.5_2739_svcomp16.tgz.

  10. 10.

    http://soarlab.org/smack/smack-1.5.2-64.tgz.

References

  1. Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 141–157. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  2. Beyer, D.: Reliable and reproducible competition results with BenchExec and witnesses (report on SV-COMP 2016). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 887–904. Springer, Heidelberg (2016). doi:10.1007/978-3-662-49674-9_55

    Chapter  Google Scholar 

  3. Chaki, S., Gurfinkel, A., Strichman, O.: Time-bounded analysis of real-time systems. In: FMCAD, pp. 72–80 (2011)

    Google Scholar 

  4. Clarke, E., Kroening, D., Lerda, F.: A tool for checking ANSI-C programs. In: Jensen, K., Podelski, A. (eds.) TACAS 2004. LNCS, vol. 2988, pp. 168–176. Springer, Heidelberg (2004). doi:10.1007/978-3-540-24730-2_15

    Chapter  Google Scholar 

  5. Fischer, B., Inverso, O., Parlato, G.: CSeq: a concurrency pre-processor for sequential C verification tools. In: ASE, pp. 710–713 (2013)

    Google Scholar 

  6. Fischer, B., Inverso, O., Parlato, G.: CSeq: a sequentialization tool for C - (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013 (ETAPS 2013). LNCS, vol. 7795, pp. 616–618. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  7. Garg, P., Madhusudan, P.: Compositionality entails sequentializability. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 26–40. Springer, Heidelberg (2011). doi:10.1007/978-3-642-19835-9_4

    Chapter  Google Scholar 

  8. Ghafari, N., Hu, A.J., Rakamarić, Z.: Context-bounded translations for concurrent software: an empirical evaluation. In: Pol, J., Weber, M. (eds.) Model Checking Software. LNCS, vol. 6349, pp. 227–244. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  9. Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Heidelberg (2015). doi:10.1007/978-3-319-21690-4_20

    Chapter  Google Scholar 

  10. Heizmann, M., Christ, J., Dietsch, D., Ermis, E., Hoenicke, J., Lindenmann, M., Nutz, A., Schilling, C., Podelski, A.: Ultimate automizer with SMTInterpol - (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 641–643. Springer, Heidelberg (2013). doi:10.1007/978-3-642-36742-7_53

    Chapter  Google Scholar 

  11. Inverso, O., Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Lazy-CSeq: a context-bounded model checking tool for multi-threaded C-programs. In: ASE, pp. 807–812 (2015)

    Google Scholar 

  12. Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Bounded model checking of multi-threaded C programs via lazy sequentialization. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 585–602. Springer, Heidelberg (2014). doi:10.1007/978-3-319-08867-9_39

    Google Scholar 

  13. Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Lazy-CSeq: a lazy sequentialization tool for C - (competition contribution). In: Havelund, K., Ábrahám, E. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 398–401. Springer, Heidelberg (2014)

    Chapter  Google Scholar 

  14. La Torre, S., Madhusudan, P., Parlato, G.: Analyzing recursive programs using a fixed-point calculus. In: PLDI, pp. 211–222 (2009)

    Google Scholar 

  15. Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 477–492. Springer, Heidelberg (2009). doi:10.1007/978-3-642-02658-4_36

    Chapter  Google Scholar 

  16. La Torre, S., Madhusudan, P., Parlato, G.: Model-checking parameterized concurrent programs using linear interfaces. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 629–644. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  17. La Torre, S., Madhusudan, P., Parlato, G.: Sequentializing parameterized programs. In: FIT, pp. 34–47 (2012)

    Google Scholar 

  18. Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 427–443. Springer, Heidelberg (2012). doi:10.1007/978-3-642-31424-7_32

    Chapter  Google Scholar 

  19. Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods Syst. Des. 35(1), 73–97 (2009)

    Article  MATH  Google Scholar 

  20. Lamport, L.: A new approach to proving the correctness of multiprocess programs. ACM Trans. Program. Lang. Syst. 1(1), 84–97 (1979)

    Article  MATH  Google Scholar 

  21. Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO, pp. 75–86. IEEE (2004)

    Google Scholar 

  22. Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Unbounded Lazy-CSeq: a lazy sequentialization tool for C programs with unbounded context switches - (competition contribution). In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 461–463. Springer, Heidelberg (2015)

    Google Scholar 

  23. Qadeer, S., Wu, D.: KISS: keep it simple and sequential. In: PLDI, pp. 14–24 (2004)

    Google Scholar 

  24. Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106–113. Springer, Heidelberg (2014)

    Google Scholar 

  25. Tomasco, E., Inverso, O., Fischer, B., Torre, S., Parlato, G.: Verifying concurrent programs by memory unwinding. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 551–565. Springer, Heidelberg (2015). doi:10.1007/978-3-662-46681-0_52

    Google Scholar 

  26. Tomasco, E., Nguyen, T.L., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: Lazy sequentialization for TSO and PSO via shared memory abstractions. In: FMCAD (2016, to appear). http://eprints.soton.ac.uk/397759/

  27. Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with impact. In: FMCAD, pp. 210–217 (2013)

    Google Scholar 

  28. Zheng, M., Edenhofner, J.G., Luo, Z., Gerrard, M.J., Rogers, M.S., Dwyer, M.B., Siegel, S.F.: CIVL: applying a general concurrency verification framework to C/Pthreads programs (competition contribution). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 908–911. Springer, Heidelberg (2016)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Electronics and Computer Science, University of Southampton, Southampton, UK

    Truc L. Nguyen & Gennaro Parlato

  2. Computer Science, Stellenbosch University, Stellenbosch, South Africa

    Bernd Fischer

  3. Informatica, Università degli Studi di Salerno, Fisciano, Italy

    Salvatore La Torre

Authors
  1. Truc L. Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernd Fischer
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Salvatore La Torre
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Gennaro Parlato
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Truc L. Nguyen .

Editor information

Editors and Affiliations

  1. AIST , Osaka, Japan

    Cyrille Artho

  2. Inria Rennes , Rennes, France

    Axel Legay

  3. Bar Ilan University , Ramat Gan, Israel

    Doron Peled

Rights and permissions

Reprints and permissions

Copyright information

© 2016 Springer International Publishing AG

About this paper

Cite this paper

Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G. (2016). Lazy Sequentialization for the Safety Verification of Unbounded Concurrent Programs. In: Artho, C., Legay, A., Peled, D. (eds) Automated Technology for Verification and Analysis. ATVA 2016. Lecture Notes in Computer Science(), vol 9938. Springer, Cham. https://doi.org/10.1007/978-3-319-46520-3_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-46520-3_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-46519-7

  • Online ISBN: 978-3-319-46520-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation