Advertisement

Modular Verification of Concurrent Programs via Sequential Model Checking

  • Dan RasinEmail author
  • Orna Grumberg
  • Sharon Shoham
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

Abstract

This work utilizes the plethora of work on verification of sequential programs for the purpose of verifying concurrent programs. We reduce the verification of a concurrent program to a series of verification tasks of sequential programs. Our approach is modular in the sense that each sequential verification task roughly corresponds to the verification of a single thread, with some additional information about the environment in which it operates. Information regarding the environment is gathered during the run of the algorithm, by need. While our approach is general, it specializes on concurrent programs where the threads are structured hierarchically. The idea is to exploit the hierarchy in order to minimize the amount of information that needs to be transferred between threads. To that end, we verify one of the threads, considered “main”, as a sequential program. Its verification process initiates queries to its “environment” (which may contain multiple threads). Those queries are answered by sequential verification, if the environment consists of a single thread, or, otherwise, by applying the same hierarchical algorithm on the environment. Our technique is fully automatic, and allows us to use any off-the-shelf sequential model checker. We implemented our technique in a tool called CoMuS and evaluated it against established tools for concurrent verification. Our experiments show that it works particularly well on hierarchically structured programs.

Notes

Acknowledgment

This publication is part of a project that has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No [759102-SVIS]). The research was partially supported by Len Blavatnik and the Blavatnik Family foundation, the Blavatnik Interdisciplinary Cyber Research Center, Tel Aviv University, and the United States-Israel Binational Science Foundation (BSF) grants No. 2016260 and 2012259.

References

  1. 1.
    Alglave, J., Kroening, D., Tautschnig, M.: Partial orders for efficient bounded model checking of concurrent software. In: Computer Aided Verification (CAV) (2013)Google Scholar
  2. 2.
  3. 3.
    Beyer, D., Keremoglu, M.E.: CPAchecker: a tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-22110-1_16CrossRefGoogle Scholar
  4. 4.
    Bradley, A.R.: SAT-based model checking without unrolling. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 70–87. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18275-4_7CrossRefGoogle Scholar
  5. 5.
    Cobleigh, J.M., Giannakopoulou, D., PĂsĂreanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-36577-X_24CrossRefzbMATHGoogle Scholar
  6. 6.
    Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 55–67. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73368-3_9CrossRefGoogle Scholar
  7. 7.
    de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008).  https://doi.org/10.1007/978-3-540-78800-3_24CrossRefGoogle Scholar
  8. 8.
    Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Upper Saddle River (1976)Google Scholar
  9. 9.
    Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: ESOP (2002)Google Scholar
  10. 10.
    Flanagan, C., Qadeer, S.: Thread-modular model checking. In: Ball, T., Rajamani, S.K. (eds.) SPIN 2003. LNCS, vol. 2648, pp. 213–224. Springer, Heidelberg (2003).  https://doi.org/10.1007/3-540-44829-2_14CrossRefzbMATHGoogle Scholar
  11. 11.
    Flanagan, C., Qadeer, S.: Transactions for software model checking. Electr. Notes Theor. Comput. Sci. 89(3), 518–539 (2003)CrossRefGoogle Scholar
  12. 12.
    Gavran, I., Niksic, F., Kanade, A., Majumdar, R., Vafeiadis, V.: Rely/guarantee reasoning for asynchronous programs. In: CONCUR (2015)Google Scholar
  13. 13.
    Godefroid, P. (ed.): Partial-Order Methods for the Verification of Concurrent Systems. LNCS, vol. 1032. Springer, Heidelberg (1996).  https://doi.org/10.1007/3-540-60761-7CrossRefzbMATHGoogle Scholar
  14. 14.
    Gueta, G., Flanagan, C., Yahav, E., Sagiv, M.: Cartesian partial-order reduction. SPIN’07Google Scholar
  15. 15.
    Günther, H., Laarman, A., Weissenbacher, G.: Vienna verification tool: IC3 for parallel software. In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 954–957. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_69CrossRefGoogle Scholar
  16. 16.
    Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: POPL (2011)CrossRefGoogle Scholar
  17. 17.
    Gupta, A., Popeea, C., Rybalchenko, A.: Threader: a constraint-based verifier for multi-threaded programs. In: Computer Aided Verification (CAV), pp. 412–417 (2011)CrossRefGoogle Scholar
  18. 18.
    Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The seahorn verification framework. In: Computer Aided Verification (CAV), pp. 343–361 (2015)CrossRefGoogle Scholar
  19. 19.
    Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. In: Computer Aided Verification (CAV), pp. 37–51 (2008)Google Scholar
  20. 20.
    Leino, K.R.M., Müller, P.: A Basis for Verifying Multi-threaded Programs. In: Castagna, G. (ed.) ESOP 2009. LNCS, vol. 5502, pp. 378–393. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-00590-9_27CrossRefGoogle Scholar
  21. 21.
    Malkis, A., Podelski, A., Rybalchenko, A.: Thread-modular verification is cartesian abstract interpretation. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 183–197. Springer, Heidelberg (2006).  https://doi.org/10.1007/11921240_13CrossRefGoogle Scholar
  22. 22.
    McMillan, K.L.: Lazy abstraction with interpolants. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 123–136. Springer, Heidelberg (2006).  https://doi.org/10.1007/11817963_14CrossRefGoogle Scholar
  23. 23.
    Nguyen, T.L., Fischer, B., La Torre, S., Parlato, G.: Unbounded lazy-cseq: a lazy sequentialization tool for c programs with unbounded context switches. In: Baier, C., Tinelli, C. (eds.) TACAS 2015. LNCS, vol. 9035, pp. 461–463. Springer, Heidelberg (2015).  https://doi.org/10.1007/978-3-662-46681-0_45CrossRefGoogle Scholar
  24. 24.
    Nguyen, T.L., Fischer, B., La Torre, S.: and G. Parlato. Lazy sequentialization for the safety verification of unbounded concurrent programs, In ATVA (2016)Google Scholar
  25. 25.
    Pasareanu, C.S., Giannakopoulou, D., Bobaru, M.G., Cobleigh, J.M., Barringer, H.: Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning. Form. Methods Syst. Des. 32(3), 175–205 (2008)CrossRefGoogle Scholar
  26. 26.
    Peterson, G.L.: Myths about the mutual exclusion problem. Inf. Process. Lett. 12(3), 115–116 (1981)CrossRefGoogle Scholar
  27. 27.
    Popeea, C., Rybalchenko, A.: Threader: a verifier for multi-threaded programs. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 633–636. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_51CrossRefGoogle Scholar
  28. 28.
    Popeea, C., Rybalchenko, A., Wilhelm, A.: Reduction for compositional verification of multi-threaded programs. In: FMCAD, pp. 187–194 (2014)Google Scholar
  29. 29.
    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).  https://doi.org/10.1007/11513988_9CrossRefGoogle Scholar
  30. 30.
    Rasin, D.: Modular verification of concurrent programs via sequential model checking. M.Sc. thesis, Technion – Israel Institute of Technology (2018)Google Scholar
  31. 31.
    Sinha, N., Clarke, E.: SAT-based compositional verification using lazy learning. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 39–54. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-73368-3_8CrossRefzbMATHGoogle Scholar
  32. 32.
    Tomasco, E., Inverso, O., Fischer, B., La 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).  https://doi.org/10.1007/978-3-662-46681-0_52CrossRefGoogle Scholar
  33. 33.
    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)Google Scholar
  34. 34.
    Wachter, B., Kroening, D., Ouaknine, J.: Verifying multi-threaded software with impact. In: Formal Methods in Computer-Aided Design, FMCAD, pp. 210–217 (2013)Google Scholar
  35. 35.
    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).  https://doi.org/10.1007/978-3-662-49674-9_57CrossRefGoogle Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.Technion – Israel Institute of TechnologyHaifaIsrael
  2. 2.Tel Aviv UniversityTel AvivIsrael

Personalised recommendations