Advertisement

Bounded Model Checking of Multi-threaded C Programs via Lazy Sequentialization

  • Omar Inverso
  • Ermenegildo Tomasco
  • Bernd Fischer
  • Salvatore La Torre
  • Gennaro Parlato
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8559)

Abstract

Bounded model checking (BMC) has successfully been used for many practical program verification problems, but concurrency still poses a challenge. Here we describe a new approach to BMC of sequentially consistent C programs using POSIX threads. Our approach first translates a multi-threaded C program into a nondeterministic sequential C program that preserves reachability for all round-robin schedules with a given bound on the number of rounds. It then re-uses existing high-performance BMC tools as backends for the sequential verification problem. Our translation is carefully designed to introduce very small memory overheads and very few sources of nondeterminism, so that it produces tight SAT/SMT formulae, and is thus very effective in practice: our prototype won the concurrency category of SV-COMP14. It solved all verification tasks successfully and was 30x faster than the best tool with native concurrency handling.

Keywords

Model Check Concurrent Program Context Switch Input Program Symbolic Model Check 
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.

References

  1. 1.
    2013 28th IEEE/ACM International Conference on Automated Software Engineering, ASE 2013, Silicon Valley, CA, USA, November 11-15. IEEE (2013)Google Scholar
  2. 2.
    Ábrahám, E., Havelund, K. (eds.): TACAS 2014 (ETAPS). LNCS, vol. 8413. Springer, Heidelberg (2014)Google Scholar
  3. 3.
    Alglave, J., Kroening, D., Nimal, V., Tautschnig, M.: Software Verification for Weak Memory via Program Transformation. In: Felleisen, M., Gardner, P. (eds.) ESOP 2013. LNCS, vol. 7792, pp. 512–532. Springer, Heidelberg (2013)Google Scholar
  4. 4.
    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)CrossRefGoogle Scholar
  5. 5.
    Atig, M.F., Bouajjani, A., Parlato, G.: Getting Rid of Store-Buffers in TSO Analysis. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 99–115. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Ball, T., Sagiv, M. (eds.): Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28. ACM (2011)Google Scholar
  7. 7.
  8. 8.
    Beyer, D.: Second Competition on Software Verification - (Summary of SV-COMP 2013). In: Piterman, Smolka (eds.) [45], pp. 594–609Google Scholar
  9. 9.
    Beyer, D.: Status report on software verification - (competition summary sv-comp 2014). In: Ábrahám, Havelund (eds.) [2], pp. 373–388Google Scholar
  10. 10.
    Biere, A.: Bounded Model Checking. In: Biere, A., Heule, M., van Maaren, H., Walsh, T. (eds.) Handbook of Satisfiability. Frontiers in Artificial Intelligence and Applications, vol. 185, pp. 457–481. IOS Press (2009)Google Scholar
  11. 11.
    Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without bDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193–207. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  12. 12.
    Bouajjani, A., Emmi, M., Parlato, G.: On Sequentializing Concurrent Programs. In: Yahav, E. (ed.) Static Analysis. LNCS, vol. 6887, pp. 129–145. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  13. 13.
    Bouajjani, A., Maler, O. (eds.): CAV 2009. LNCS, vol. 5643. Springer, Heidelberg (2009)zbMATHGoogle Scholar
  14. 14.
    Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., Engler, D.R.: EXE: Automatically Generating Inputs of Death. In: Juels, A., Wright, R.N., di Vimercati, S.D.C. (eds.) ACM Conference on Computer and Communications Security, pp. 322–335. ACM (2006)Google Scholar
  15. 15.
    Chaki, S., Gurfinkel, A., Strichman, O.: Time-bounded Analysis of Real-time Systems. In: Bjesse, P., Slobodová, A. (eds.) FMCAD, pp. 72–80. FMCAD Inc. (2011)Google Scholar
  16. 16.
    Cho, C.Y., D’Silva, V., Song, D.: BLITZ: Compositional Bounded Model Checking for Real-world Programs. In: ASE [1], pp. 136–146Google Scholar
  17. 17.
    Clarke, E., Kroning, 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)CrossRefGoogle Scholar
  18. 18.
    Cordeiro, L., Fischer, B.: Verifying Multi-threaded Software using SMT-based Context-bounded Model Checking. In: Taylor, R.N., Gall, H., Medvidovic, N. (eds.) ICSE, pp. 331–340. ACM (2011)Google Scholar
  19. 19.
    Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-Based Bounded Model Checking for Embedded ANSI-C Software. IEEE Trans. Software Eng. 38(4), 957–974 (2012)CrossRefGoogle Scholar
  20. 20.
    Currie, D.W., Hu, A.J., Rajan, S.P.: Automatic Formal Verification of DSP software. In: DAC, pp. 130–135 (2000)Google Scholar
  21. 21.
    D’Silva, V., Kroening, D., Weissenbacher, G.: A Survey of Automated Techniques for Formal Software Verification. IEEE Trans. on CAD of Integrated Circuits and Systems 27(7), 1165–1178 (2008)CrossRefGoogle Scholar
  22. 22.
    Emmi, M., Qadeer, S., Rakamaric, Z.: Delay-bounded Scheduling. In: Ball, Sagiv (eds.) [6], pp. 411–422Google Scholar
  23. 23.
    Etessami, K., Rajamani, S.K. (eds.): CAV 2005. LNCS, vol. 3576. Springer, Heidelberg (2005)zbMATHGoogle Scholar
  24. 24.
    Falke, S., Merz, F., Sinz, C.: The Bounded Model Checker LLBMC. In: ASE [1], pp. 706–709Google Scholar
  25. 25.
    Fischer, B., Inverso, O., Parlato, G.: CSeq: A Concurrency Pre-processor for Sequential C Verification Tools. In: ASE [1], pp. 710–713Google Scholar
  26. 26.
    Fischer, B., Inverso, O., Parlato, G.: CSeq: A Sequentialization Tool for C - (Competition Contribution). In: Piterman, Smolka (eds.) [45], pp. 616–618Google Scholar
  27. 27.
    Forum, M.P.I.: MPI: A Message-Passing Interface Standard Version 3.0, 09, Chapter author for Collective Communication, Process Topologies, and One Sided Communications (2012)Google Scholar
  28. 28.
    Ganai, M.K., Gupta, A.: Efficient Modeling of Concurrent Systems in BMC. In: Havelund, K., Majumdar, R. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 114–133. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  29. 29.
    Ghafari, N., Hu, A.J., Rakamarić, Z.: Context-Bounded Translations for Concurrent Software: An Empirical Evaluation. In: van de Pol, J., Weber, M. (eds.) SPIN 2010. LNCS, vol. 6349, pp. 227–244. Springer, Heidelberg (2010)Google Scholar
  30. 30.
    Inverso, O., Tomasco, E., Fischer, B., La Torre, S., Parlato, G.: Lazy-CSeq: A Lazy Sequentialization Tool for C - (Competition Contribution). In: Ábrahám, Havelund (eds.) [2], pp. 398–401Google Scholar
  31. 31.
    ISO/IEC. Information technology—Portable Operating System Interface (POSIX) Base Specifications, Issue 7, ISO/IEC/IEEE 9945:2009 (2009)Google Scholar
  32. 32.
    Ivancic, F., Yang, Z., Ganai, M.K., Gupta, A., Shlyakhter, I., Ashar, P.: F-Soft: Software Verification Platform. In: Etessami, Rajamani (eds.) [23], pp. 301–306Google Scholar
  33. 33.
    Kahlon, V., Gupta, A., Sinha, N.: Symbolic Model Checking of Concurrent Programs Using Partial Orders and On-the-Fly Transactions. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 286–299. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  34. 34.
    La Torre, S., Madhusudan, P., Parlato, G.: Analyzing Recursive Programs Using a Fixed-point Calculus. In: Hind, M., Diwan, A. (eds.) PLDI, pp. 211–222. ACM (2009)Google Scholar
  35. 35.
    La Torre, S., Madhusudan, P., Parlato, G.: Reducing Context-Bounded Concurrent Reachability to Sequential Reachability. In: Bouajjani, Maler (eds.) [13], pp. 477–492Google Scholar
  36. 36.
    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)CrossRefGoogle Scholar
  37. 37.
    La Torre, S., Madhusudan, P., Parlato, G.: Sequentializing Parameterized Programs. In: Bauer, S.S., Raclet, J.-B. (eds.) FIT. EPTCS, vol. 87, pp. 34–47 (2012)Google Scholar
  38. 38.
    La Torre, S., Napoli, M., Parlato, G.: Scope-Bounded Pushdown Languages. In: Shur, A., Volkov, M. (eds.) DLT. LNCS. Springer (2014)Google Scholar
  39. 39.
    La Torre, S., Parlato, G.: Scope-bounded Multistack Pushdown Systems: Fixed-Point, Sequentialization, and Tree-Width. In: D’Souza, D., Kavitha, T., Radhakrishnan, J. (eds.) FSTTCS. LIPIcs, vol. 18, pp. 173–184. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2012)Google Scholar
  40. 40.
    Lahiri, S.K., Qadeer, S., Rakamaric, Z.: Static and Precise Detection of Concurrency Errors in Systems Code Using SMT Solvers. In: Bouajjani, Maler (eds.) [13], pp. 509–524Google Scholar
  41. 41.
    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)CrossRefGoogle Scholar
  42. 42.
    Lal, A., Reps, T.W.: Reducing Concurrent Analysis Under a Context Bound to Sequential Analysis. Formal Methods in System Design 35(1), 73–97 (2009)CrossRefzbMATHGoogle Scholar
  43. 43.
    Lamport, L.: A New Approach to Proving the Correctness of Multiprocess Programs. ACM Trans. Program. Lang. Syst. 1(1), 84–97 (1979)CrossRefzbMATHGoogle Scholar
  44. 44.
    Musuvathi, M., Qadeer, S.: Iterative Context Bounding for Systematic Testing of Multithreaded Programs. In: Ferrante, J., McKinley, K.S. (eds.) PLDI, pp. 446–455. ACM (2007)Google Scholar
  45. 45.
    Piterman, N., Smolka, S.A. (eds.): TACAS 2013 (ETAPS 2013). LNCS, vol. 7795. Springer, Heidelberg (2013)zbMATHGoogle Scholar
  46. 46.
    Popeea, C., Rybalchenko, A.: Threader: A Verifier for Multi-threaded Programs - (Competition Contribution). In: Piterman, Smolka (eds.) [45], pp. 633–636Google Scholar
  47. 47.
    Qadeer, S.: Poirot - A Concurrency Sleuth. In: Qin, S., Qiu, Z. (eds.) ICFEM 2011. LNCS, vol. 6991, pp. 15–15. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  48. 48.
    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
  49. 49.
    Qadeer, S., Wu, D.: KISS: Keep It Simple and Sequential. In: Pugh, W., Chambers, C. (eds.) PLDI, pp. 14–24. ACM (2004)Google Scholar
  50. 50.
    Rabinovitz, I., Grumberg, O.: Bounded Model Checking of Concurrent Programs. In: Etessami, Rajamani (eds.) [23], pp. 82–97Google Scholar
  51. 51.
    Sinha, N., Wang, C.: Staged Concurrent Program Analysis. In: Roman, G.-C., Sullivan, K.J. (eds.) SIGSOFT FSE, pp. 47–56. ACM (2010)Google Scholar
  52. 52.
    Sinha, N., Wang, C.: On Interference Abstractions. In: Ball, Sagiv (eds.) [6], pp. 423–434Google Scholar
  53. 53.
    Tomasco, E., Inverso, O., Fischer, B., La Torre, S., Parlato, G.: MU-CSeq: Sequentialization of C Programs by Shared Memory Unwindings - (Competition Contribution). In: Ábrahám, Havelund (eds.) [2], pp. 402–404Google Scholar
  54. 54.
    Wang, C., Chaudhuri, S., Gupta, A., Yang, Y.: Symbolic Pruning of Concurrent Program Executions. In: van Vliet, H., Issarny, V. (eds.) ESEC/SIGSOFT FSE, pp. 23–32. ACM (2009)Google Scholar
  55. 55.
    Xie, Y., Aiken, A.: Saturn: A SAT-Based Tool for Bug Detection. In: Etessami, Rajamani (eds.) [23], pp. 139–143Google Scholar

Copyright information

© Springer International Publishing Switzerland 2014

Authors and Affiliations

  • Omar Inverso
    • 1
  • Ermenegildo Tomasco
    • 1
  • Bernd Fischer
    • 2
  • Salvatore La Torre
    • 3
  • Gennaro Parlato
    • 1
  1. 1.Electronics and Computer ScienceUniversity of SouthamptonUK
  2. 2.Division of Computer ScienceStellenbosch UniversitySouth Africa
  3. 3.Università degli Studi di SalernoItaly

Personalised recommendations