Advertisement

Model Checking Dynamic Pushdown Networks with Locks and Priorities

  • Marcio Diaz
  • Tayssir Touili
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11028)

Abstract

A dynamic pushdown network (DPN) is a set of pushdown systems (PDSs) where each process can dynamically create new instances of PDSs. DPNs are a natural model of multi-threaded programs with (possibly recursive) procedure calls and thread creation. A PL-DPN is an extension of DPNs that allows threads to synchronize using locks and priorities. Transitions in a PL-DPN can have different priorities and acquire/release locks. We consider in this work model checking PL-DPNs against single-indexed LTL properties. We show that this model checking problem is decidable. We propose automata-based approaches for computing the set of configurations of a PL-DPN that satisfy the corresponding single-indexed LTL formula.

References

  1. 1.
    Bouajjani, A., Müller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 473–487. Springer, Heidelberg (2005).  https://doi.org/10.1007/11539452_36CrossRefGoogle Scholar
  2. 2.
    Song, F., Touili, T.: Model checking dynamic pushdown networks. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 33–49. Springer, Cham (2013).  https://doi.org/10.1007/978-3-319-03542-0_3CrossRefGoogle Scholar
  3. 3.
    Wenner, A.: Weighted dynamic pushdown networks. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 590–609. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-11957-6_31CrossRefGoogle Scholar
  4. 4.
    Lammich, P., Müller-Olm, M.: Precise fixpoint-based analysis of programs with thread-creation and procedures. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 287–302. Springer, Heidelberg (2007).  https://doi.org/10.1007/978-3-540-74407-8_20CrossRefGoogle Scholar
  5. 5.
    Gawlitza, T.M., Lammich, P., Müller-Olm, M., Seidl, H., Wenner, A.: Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 199–213. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18275-4_15CrossRefGoogle Scholar
  6. 6.
    Lammich, P., Müller-Olm, M., Seidl, H., Wenner, A.: Contextual locking for dynamic pushdown networks. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 477–498. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-38856-9_25CrossRefGoogle Scholar
  7. 7.
    Lammich, P., Müller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 525–539. Springer, Heidelberg (2009).  https://doi.org/10.1007/978-3-642-02658-4_39CrossRefGoogle Scholar
  8. 8.
    Diaz, M., Touili, T.: Reachability analysis of dynamic pushdown networks with priorities. In: El Abbadi, A., Garbinato, B. (eds.) NETYS 2017. LNCS, vol. 10299, pp. 288–303. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-59647-1_22CrossRefGoogle Scholar
  9. 9.
    Diaz, M., Touili, T.: Dealing with priorities and locks for concurrent programs. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 208–224. Springer, Cham (2017).  https://doi.org/10.1007/978-3-319-68167-2_15CrossRefGoogle Scholar
  10. 10.
    Kahlon, V., Gupta, A.: An automata-theoretic approach for model checking threads for LTL properties. In: LICS, pp. 101–110 (2006)Google Scholar
  11. 11.
    Kahlon, V., Ivančić, F., Gupta, A.: Reasoning about threads communicating via locks. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 505–518. Springer, Heidelberg (2005).  https://doi.org/10.1007/11513988_49CrossRefGoogle Scholar
  12. 12.
    Gawlitza, T.M., Lammich, P., Müller-Olm, M., Seidl, H., Wenner, A.: Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. In: Jhala, R., Schmidt, D. (eds.) VMCAI 2011. LNCS, vol. 6538, pp. 199–213. Springer, Heidelberg (2011).  https://doi.org/10.1007/978-3-642-18275-4_15CrossRefGoogle Scholar
  13. 13.
    Wenner, A.: Weighted dynamic pushdown networks. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol. 6012, pp. 590–609. Springer, Heidelberg (2010).  https://doi.org/10.1007/978-3-642-11957-6_31CrossRefGoogle Scholar
  14. 14.
    Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997).  https://doi.org/10.1007/3-540-63141-0_10CrossRefGoogle Scholar
  15. 15.
    Vardi, M.Y., Wolper, P.: Automata-theoretic techniques for modal logics of programs. J. Comput. Syst. Sci. 32(2), 183–221 (1986)MathSciNetCrossRefGoogle Scholar
  16. 16.

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.LIPN and University Paris DiderotParisFrance
  2. 2.LIPN, CNRS and University Paris 13VilletaneuseFrance

Personalised recommendations