Advertisement

Decidable Models of Integer-Manipulating Programs with Recursive Parallelism

  • Matthew HagueEmail author
  • Anthony Widjaja LinEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 9899)

Abstract

We study safety verification for multithreaded programs with recursive parallelism (i.e. unbounded thread creation and recursion) as well as unbounded integer variables. Since the threads in each program configuration are structured in a hierarchical fashion, our model is state-extended ground-tree rewrite systems equipped with shared unbounded integer counters that can be incremented, decremented, and compared against an integer constant. Since the model is Turing-complete, we propose a decidable underapproximation. First, using a restriction similar to context-bounding, we underapproximate the global control by a weak global control (i.e. DAGs possibly with self-loops), thereby limiting the number of synchronisations between different threads. Second, we bound the number of reversals between non-decrementing and non-incrementing modes of the counters. Under this restriction, we show that reachability becomes NP-complete. In fact, it is poly-time reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our decidable approximation strictly generalises known decidable models including (i) weakly-synchronised ground-tree rewrite systems, and (ii) synchronisation/reversal-bounded concurrent pushdown systems with counters. Finally, we show that, when equipped with reversal-bounded counters, relaxing the weak control restriction by the notion of senescence results in undecidability.

Notes

Acknowledgments

We thank anonymous reviewers for their helpful feedback. This work was supported by the Engineering and Physical Sciences Research Council [EP/K009907/1] and Yale-NUS College Startup Grant.

References

  1. 1.
    Abdulla, P.A., Atig, M.F., Cederberg, J.: Analysis of message passing programs using SMT-solvers. In: Van Hung, D., Ogawa, M. (eds.) ATVA 2013. LNCS, vol. 8172, pp. 272–286. Springer, Heidelberg (2013)CrossRefGoogle Scholar
  2. 2.
    Aiswarya, C., Gastin, P., Narayan Kumar, K.: Verifying communicating multi-pushdown systems via split-width. In: Cassez, F., Raskin, J.-F. (eds.) ATVA 2014. LNCS, vol. 8837, pp. 1–17. Springer, Heidelberg (2014)Google Scholar
  3. 3.
    Araki, T., Kasami, T.: Some decision problems related to the reachability problem for petri nets. Theor. Comput. Sci. 3(1), 85–104 (1977)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Atig, M.F., Bollig, B., Habermehl, P.: Emptiness of multi-pushdown automata is 2ETIME-complete. In: Ito, M., Toyama, M. (eds.) DLT 2008. LNCS, vol. 5257, pp. 121–133. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  5. 5.
    Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Methods Comput. Sci. 7(4), 4:1–4:48 (2011)MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Atig, M.F., Ganty, P.: Approximating petri net reachability along context-free traces. In: FSTTCS, pp. 152–163 (2011)Google Scholar
  7. 7.
    Atig, M.F., Kumar, K.N., Saivasan, P.: Adjacent ordered multi-pushdown systems. Int. J. Found. Comput. Sci. 25(8), 1083–1096 (2014)MathSciNetCrossRefzbMATHGoogle Scholar
  8. 8.
    Bardin, S., Finkel, A., Leroux, J., Schnoebelen, P.: Flat acceleration in symbolic model checking. In: Peled, D.A., Tsay, Y.-K. (eds.) ATVA 2005. LNCS, vol. 3707, pp. 474–488. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Blumensath, A., Colcombet, T., Kuperberg, D., Parys, P., Vanden Boom, M.: Two-way cost automata, cost logics over infinite trees. In: CSL-LICS, pp. 16:1–16:9 (2014)Google Scholar
  10. 10.
    Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. ACM Trans. Program. Lang. Syst. 35(3), 10 (2013)CrossRefzbMATHGoogle Scholar
  11. 11.
    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)CrossRefGoogle Scholar
  12. 12.
    Bozzelli, L., Kretínský, M., Rehák, V., Strejcek, J.: On decidability of LTL model checking for process rewrite systems. Acta Inform. 46(1), 1–28 (2009)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Colcombet, T., Löding, C.: Regular cost functions over finite trees. In: LICS, pp. 70–79 (2010)Google Scholar
  14. 14.
    Czerwinski, W., Hofman, P., Lasota, S.: Reachability problem for weak multi-pushdown automata. Log. Methods Comput. Sci. 9(3), 1–29 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  15. 15.
    Dauchet, M., Tison, S.: The theory of ground rewrite systems is decidable. In: LICS, pp. 242–248 (1990)Google Scholar
  16. 16.
    de Moura, L., Bjørner, N.S.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  17. 17.
    Demri, S., Jurdzinski, M., Lachish, O., Lazic, R.: The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci. 79(1), 23–38 (2013)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Esparza, J., Ganty, P., Poch, T.: Pattern-based verification for multithreaded programs. ACM Trans. Program. Lang. Syst. 36(3), 9:1–9:29 (2014)CrossRefGoogle Scholar
  19. 19.
    Esparza, J., Podelski, A.: Efficient algorithms for pre\(^{*}\) and post\(^{*}\) on interprocedural parallel flow graphs. In: POPL, pp. 1–11 (2000)Google Scholar
  20. 20.
    Ganty, P., Majumdar, R., Monmege, M.: Bounded underapproximations. FMSD 40(2), 206–231 (2012)zbMATHGoogle Scholar
  21. 21.
    Göller, S., Lin, A.W.: Refining the process rewrite systems hierarchy via ground tree rewrite systems. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 543–558. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  22. 22.
    Hague, M.: Senescent ground tree rewrite systems. In: CSL-LICS, pp. 48:1–48:10 (2014)Google Scholar
  23. 23.
    Hague, M., Lin, A.W.: Model checking recursive programs with numeric data types. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 743–759. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  24. 24.
    Hague, M., Lin, A.W.: Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 260–276. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  25. 25.
    Ibarra, O.H.: Reversal-bounded multicounter machines and their decision problems. J. ACM 25(1), 116–133 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  26. 26.
    Křetínský, M., Řehák, V., Strejček, J.: Extended process rewrite systems: expressiveness and reachability. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004. LNCS, vol. 3170, pp. 355–370. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  27. 27.
    La Torre, S., Napoli, M., Parlato, G.: Scope-bounded pushdown languages. In: Shur, A.M., Volkov, M.V. (eds.) DLT 2014. LNCS, vol. 8633, pp. 116–128. Springer, Heidelberg (2014)Google Scholar
  28. 28.
    Lal, A., Touili, T., Kidd, N., Reps, T.: Interprocedural analysis of concurrent programs under a context bound. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 282–298. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  29. 29.
    Lang, M., Löding, C.: Modeling and verification of infinite systems with resources. Log. Methods Comput. Sci. 9(4), 1–39 (2013)MathSciNetzbMATHGoogle Scholar
  30. 30.
    Leroux, J., Praveen, M., Sutre, G.: Hyper-ackermannian bounds for pushdown vector addition systems. In: CSL-LICS, pp. 63:1–63:10 (2014)Google Scholar
  31. 31.
    Lin, A.W.: Weakly-synchronized ground tree rewriting. In: Rovan, B., Sassone, V., Widmayer, P. (eds.) MFCS 2012. LNCS, vol. 7464, pp. 630–642. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  32. 32.
    Löding, C.: Reachability problems on regular ground tree rewriting graphs. Theory Comput. Syst. 39(2), 347–383 (2006)MathSciNetCrossRefzbMATHGoogle Scholar
  33. 33.
    Madhusudan, P., Parlato, G.: The tree width of auxiliary storage. In: POPL, pp. 283–294 (2011)Google Scholar
  34. 34.
    Mayr, R.: Decidability and complexity of model checking problems for infinite-state systems. Ph.D. thesis, TU-Munich (1998)Google Scholar
  35. 35.
    Musuvathi, M., Qadeer, S.: Iterative context bounding for systematic testing of multithreaded programs. In: PLDI, pp. 446–455 (2007)Google Scholar
  36. 36.
    Qadeer, S.: The case for context-bounded verification of concurrent programs. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 3–6. Springer, Heidelberg (2008)Google Scholar
  37. 37.
    Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. Trans. Program. Lang. Syst. (TOPLAS) 22, 416–430 (2000)CrossRefGoogle Scholar
  38. 38.
    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
  39. 39.
    Scarpellini, B.: Complexity of subcases of Presburger arithmetic. Trans. AMS 284(1), 203–218 (1984)MathSciNetCrossRefzbMATHGoogle Scholar
  40. 40.
    Suwimonteerabuth, D., Esparza, J., Schwoon, S.: Symbolic context-bounded analysis of multithreaded Java programs. In: Havelund, K., Majumdar, R., Palsberg, J. (eds.) SPIN 2008. LNCS, vol. 5156, pp. 270–287. Springer, Heidelberg (2008)Google Scholar
  41. 41.
    To, A.W., Libkin, L.: Algorithmic metatheorems for decidable LTL model checking over infinite systems. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 221–236. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  42. 42.
    Torre, S.L., Madhusudan, P., Parlato, G.: A robust class of context-sensitive languages. In: LICS, pp. 161–170. IEEE Computer Society (2007)Google Scholar
  43. 43.
    Verma, K.N., Goubault-Larrecq, J.: Karp-Miller trees for a branching extension of VASS. Discret. Math. Theor. Comput. Sci. 7(1), 217–230 (2005)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer International Publishing Switzerland 2016

Authors and Affiliations

  1. 1.Royal HollowayUniversity of LondonLondonUK
  2. 2.Yale-NUS CollegeSingaporeSingapore

Personalised recommendations