Compositional Reasoning for Shared-Variable Concurrent Programs
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.
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.Abadi, M., Gordon, A.D.: A calculus for cryptographic protocols: the spi calculus. Inf. Comput. 148(1), 1–70 (1999)MathSciNetCrossRefGoogle Scholar
- 2.Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, New York (2008)zbMATHGoogle Scholar
- 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.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.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.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.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.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.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.Cohen, A., Namjoshi, K.S.: Local proofs for global safety properties. Formal Methods Syst. Des. 34(2), 104–125 (2009)CrossRefGoogle Scholar
- 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.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.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.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.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.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.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.Grumberg, O., Long, D.E.: Model checking and modular verification. ACM Trans. Program. Lang. Syst. 16(3), 843–871 (1994)CrossRefGoogle Scholar
- 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.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.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.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.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.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.Jones, C.B.: Specification and design of (parallel) programs. In: IFIP Congress, pp. 321–332 (1983)Google Scholar
- 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.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.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.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.Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Upper Saddle River (1989)zbMATHGoogle Scholar
- 31.Misra, J., Chandy, K.M.: Proofs of networks of processes. IEEE Trans. Softw. Eng. 7(4), 417–426 (1981)MathSciNetCrossRefGoogle Scholar
- 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.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.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.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.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.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)