Advertisement

Compositional Reasoning for Shared-Variable Concurrent Programs

  • Fuyuan Zhang
  • Yongwang Zhao
  • David Sanán
  • Yang Liu
  • Alwen Tiu
  • Shang-Wei Lin
  • Jun Sun
Conference paper
First Online:
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10951)

Abstract

Scalable and automatic formal verification for concurrent systems is always demanding. In this paper, we propose a verification framework to support automated compositional reasoning for concurrent programs with shared variables. Our framework models concurrent programs as succinct automata and supports the verification of multiple important properties. Safety verification and simulations of succinct automata are parallel compositional, and safety properties of succinct automata are preserved under refinements. We generate succinct automata from infinite state concurrent programs in an automated manner. Furthermore, we propose the first automated approach to checking rely-guarantee based simulations between infinite state concurrent programs. We have prototyped our algorithms and applied our tool to the verification of multiple refinements.

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

Notes

Acknowledgement

This research is supported (in part) by the National Research Foundation, Prime Ministers Office, Singapore under its National Cybersecurity R&D Program (Award No. NRF2014NCR-NCR001-30) and administered by the National Cybersecurity R&D Directorate.

References

  1. 1.
    Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148(1), 1–70 (1999)MathSciNetCrossRefGoogle Scholar
  2. 2.
    Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, New York (2008)zbMATHGoogle Scholar
  3. 3.
    Brookes, S.D.: Full abstraction for a shared variable parallel language. In: Proceedings of the 8th Annual Symposium on Logic in Computer Science (LICS 1993), Montreal, Canada, pp. 98–109 (1993)Google Scholar
  4. 4.
    Burch, J.R., Clarke, E.M., McMillan, K.L., Dill, D.L., Hwang, L.J.: Symbolic model checking: 10\(\hat{~}\)20 states and beyond. Inf. Comput. 98(2), 142–170 (1992)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Burckhardt, S., Musuvathi, M., Singh, V.: Verifying local transformations on relaxed memory models. In: Gupta, R. (ed.) CC 2010. LNCS, vol. 6011, pp. 104–123. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-11970-5_7CrossRefGoogle Scholar
  6. 6.
    Chaki, S., Gurfinkel, A., Strichman, O.: Decision diagrams for linear arithmetic. In: Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD 2009), Austin, Texas, USA, pp. 53–60 (2009)Google Scholar
  7. 7.
    Clarke, E.M., Filkorn, T., Jha, S.: Exploiting symmetry in temporal logic model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 450–462. Springer, Heidelberg (1993).  https://doi.org/10.1007/3-540-56922-7_37CrossRefGoogle Scholar
  8. 8.
    Clarke, E.M., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J. ACM 50(5), 752–794 (2003)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Clarke, E.M., Grumberg, O., Long, D.E.: Model checking and abstraction. ACM Trans. Program. Lang. Syst. 16(5), 1512–1542 (1994)CrossRefGoogle Scholar
  10. 10.
    Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. Formal Methods Syst. Des. 34(2), 104–125 (2009)CrossRefGoogle Scholar
  11. 11.
    Cousot, P., Cousot, R.: Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proceedings of the 4th Symposium on Principles of Programming Languages (POPL 1977), Los Angeles, California, USA, pp. 238–252 (1977)Google Scholar
  12. 12.
    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
  13. 13.
    Emerson, E.A., Sistla, A.P.: Symmetry and model checking. In: Courcoubetis, C. (ed.) CAV 1993. LNCS, vol. 697, pp. 463–478. Springer, Heidelberg (1993).  https://doi.org/10.1007/3-540-56922-7_38CrossRefGoogle Scholar
  14. 14.
    Flanagan, C., Freund, S.N., Qadeer, S.: Thread-modular verification for shared-memory programs. In: Le Métayer, D. (ed.) ESOP 2002. LNCS, vol. 2305, pp. 262–277. Springer, Heidelberg (2002).  https://doi.org/10.1007/3-540-45927-8_19CrossRefGoogle Scholar
  15. 15.
    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
  16. 16.
    Godefroid, P.: Using partial orders to improve automatic verification methods. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 176–185. Springer, Heidelberg (1991).  https://doi.org/10.1007/BFb0023731CrossRefzbMATHGoogle Scholar
  17. 17.
    Graf, S., Saidi, H.: Construction of abstract state graphs with PVS. In: Grumberg, O. (ed.) CAV 1997. LNCS, vol. 1254, pp. 72–83. Springer, Heidelberg (1997).  https://doi.org/10.1007/3-540-63166-6_10CrossRefGoogle Scholar
  18. 18.
    Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843–871 (1994)CrossRefGoogle Scholar
  19. 19.
    Gupta, A., Popeea, C., Rybalchenko, A.: Predicate abstraction and refinement for verifying multi-threaded programs. In: Proceedings of the 38th Symposium on Principles of Programming Languages (POPL 2011), Austin, TX, USA, pp. 331–344 (2011)Google Scholar
  20. 20.
    Gurfinkel, A., Chaki, S.: Boxes: a symbolic abstract domain of boxes. In: Cousot, R., Martel, M. (eds.) SAS 2010. LNCS, vol. 6337, pp. 287–303. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-15769-1_18CrossRefGoogle Scholar
  21. 21.
    Hawblitzel, C., Petrank, E., Qadeer, S., Tasiran, S.: Automated and modular refinement reasoning for concurrent programs. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9207, pp. 449–465. Springer, Cham (2015).  https://doi.org/10.1007/978-3-319-21668-3_26CrossRefGoogle Scholar
  22. 22.
    Henzinger, T.A., Jhala, R., Majumdar, R.: Race checking by context inference. In: Proceedings of the 2004 Conference on Programming Language Design and Implementation (PLDI 2004), Washington, DC, USA, pp. 1–13 (2004)Google Scholar
  23. 23.
    Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt, W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 262–274. Springer, Heidelberg (2003).  https://doi.org/10.1007/978-3-540-45069-6_27CrossRefGoogle Scholar
  24. 24.
    Ip, C.N., Dill, D.L.: Better verification through symmetry. In: Proceedings of the 11th International Conference on Computer Hardware Description Languages and their Applications (CHDL 1993), Ontario, Canada, pp. 97–111 (1993)Google Scholar
  25. 25.
    Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)Google Scholar
  26. 26.
    Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)CrossRefGoogle Scholar
  27. 27.
    Kundu, S., Lerner, S., Gupta, R.: Automated refinement checking of concurrent systems. In: Proceedings of the 2007 International Conference on Computer-Aided Design (ICCAD 2007), San Jose, CA, USA, pp. 318–325 (2007)Google Scholar
  28. 28.
    Liang, H., Feng, X., Fu, M.: Rely-guarantee-based simulation for compositional verification of concurrent program transformations. ACM Trans. Program. Lang. Syst. 36(1), 3 (2014)CrossRefGoogle Scholar
  29. 29.
    Lochbihler, A.: Verifying a compiler for Java threads. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 427–447. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-11957-6_23CrossRefGoogle Scholar
  30. 30.
    Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
  31. 31.
    Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 7(4), 417–426 (1981)MathSciNetCrossRefGoogle Scholar
  32. 32.
    Peled, D.: Combining partial order reductions with on-the-fly model-checking. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 377–390. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58179-0_69CrossRefGoogle Scholar
  33. 33.
    Pnueli, A.: In transition from global to modular temporal reasoning about programs. In: Apt, K.R. (ed.) Logics and Models of Concurrent Systems, pp. 123–144. Springer, New York (1985).  https://doi.org/10.1007/978-3-642-82453-1_5CrossRefGoogle Scholar
  34. 34.
    Sangiorgi, D., Kobayashi, N., Sumii, E.: Environmental bisimulations for higher-order languages. In: Proceedings of the 22nd IEEE Symposium on Logic in Computer Science (LICS 2007), Wroclaw, Poland, pp. 293–302 (2007)Google Scholar
  35. 35.
    Valmari, A.: A stubborn attack on state explosion. In: Clarke, E.M., Kurshan, R.P. (eds.) CAV 1990. LNCS, vol. 531, pp. 156–165. Springer, Heidelberg (1991).  https://doi.org/10.1007/BFb0023729CrossRefGoogle Scholar
  36. 36.
    Xu, Q., de Roever, W.P., He, J.: The rely-guarantee method for verifying shared variable concurrent programs. Formal Asp. Comput. 9(2), 149–174 (1997)CrossRefGoogle Scholar
  37. 37.
    Zhang, F., Zhao, Y., Sanán, D., Liu, Y., Tiu, A., Lin, S.-W., Sun, J.: Compositional Reasoning for Shared-Variable Concurrent Programs. CoRR arXiv:1611.00574v2 (2018)

Copyright information

© Springer International Publishing AG, part of Springer Nature 2018

Authors and Affiliations

  • Fuyuan Zhang
    • 1
  • Yongwang Zhao
    • 3
  • David Sanán
    • 1
  • Yang Liu
    • 1
  • Alwen Tiu
    • 2
  • Shang-Wei Lin
    • 1
  • Jun Sun
    • 4
  1. 1.School of Computer Science and EngineeringNanyang Technological UniversitySingaporeSingapore
  2. 2.Research School of Computer ScienceAustralian National UniversityCanberraAustralia
  3. 3.School of Computer Science and EngineeringBeihang UniversityBeijingChina
  4. 4.Singapore University of Technology and DesignSingaporeSingapore

Personalised recommendations

Cite paper

Buy options