Skip to main content
SpringerLink
Log in

Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks

  • Conference paper
CONCUR 2013 – Concurrency Theory (CONCUR 2013)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 8052))

Included in the following conference series:

Abstract

In this paper, we study the program-point reachability problem of concurrent pushdown systems that communicate via unbounded and unordered message buffers. Our goal is to relax the common restriction that messages can only be retrieved by a pushdown process when its stack is empty. We use the notion of partially commutative context-free grammars to describe a new class of asynchronously communicating pushdown systems with a mild shape constraint on the stacks for which the program-point coverability problem remains decidable. Stacks that fit the shape constraint may reach arbitrary heights; further a process may execute any communication action (be it process creation, message send or retrieval) whether or not its stack is empty. This class extends previous computational models studied in the context of asynchronous programs, and enables the safety verification of a large class of message passing programs.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Babic, D., Rakamaric, Z.: Asynchronously communicating visibly pushdown systems. Technical Report UCB/EECS-2011-108, UC Berkeley (2011)

    Google Scholar 

  2. Bouajjani, A., Emmi, M.: Analysis of recursively parallel programs. In: POPL, pp. 203–214 (2012)

    Google Scholar 

  3. Bouajjani, A., Emmi, M.: Bounded phase analysis of message-passing programs. In: Flanagan, C., König, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 451–465. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  4. 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)

    Chapter  Google Scholar 

  5. Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)

    Article  MathSciNet  MATH  Google Scholar 

  6. Chadha, R., Viswanathan, M.: Decidability results for well-structured transition systems with auxiliary storage. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol. 4703, pp. 136–150. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  7. Czerwiński, W., Fröschle, S., Lasota, S.: Partially-commutative context-free processes. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 259–273. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  8. Czerwiński, W., Hofman, P., Lasota, S.: Reachability problem for weak multi-pushdown automata. In: Koutny, M., Ulidowski, I. (eds.) CONCUR 2012. LNCS, vol. 7454, pp. 53–68. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  9. D’Osualdo, E., Kochems, J., Ong, C.-H.L.: Soter: an automatic safety verifier for Erlang. In: AGERE! 2012, pp. 137–140 (2012)

    Google Scholar 

  10. D’Osualdo, E., Kochems, J., Ong, C.-H.L.: Automatic verification of Erlang-style concurrency. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 454–476. Springer, Heidelberg (2013)

    Google Scholar 

  11. Esparza, J.: Petri nets, commutative context-free grammars, and basic parallel processes. Fundam. Inform. 31(1), 13–25 (1997)

    MathSciNet  MATH  Google Scholar 

  12. Esparza, J., Ganty, P.: Complexity of pattern-based verification for multithreaded programs. In: POPL, pp. 499–510 (2011)

    Google Scholar 

  13. Esparza, J., Podelski, A.: Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In: POPL, pp. 1–11 (2000)

    Google Scholar 

  14. Esparza, J., Ganty, P., Kiefer, S., Luttenberger, M.: Parikh’s theorem: A simple and direct construction. CoRR, abs/1006.3825 (2010)

    Google Scholar 

  15. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1-2), 63–92 (2001)

    Article  MathSciNet  MATH  Google Scholar 

  16. 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)

    Chapter  Google Scholar 

  17. Ganty, P., Majumdar, R.: Algorithmic verification of asynchronous programs. ACM Trans. Program. Lang. Syst. 34(1), 6 (2012)

    Article  Google Scholar 

  18. Ganty, P., Majumdar, R., Rybalchenko, A.: Verifying liveness for asynchronous programs. In: POPL, pp. 102–113 (2009)

    Google Scholar 

  19. Geeraerts, G., Heußner, A., Raskin, J.-F.: Queue-dispatch asynchronous systems. CoRR, abs/1201.4871 (2012)

    Google Scholar 

  20. Henzinger, T.A., Jhala, R., Majumdar, R., Qadeer, S.: Thread-modular abstraction refinement. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 262–274. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  21. Heußner, A., Leroux, J., Muscholl, A., Sutre, G.: Reachability analysis of communicating pushdown systems. In: Ong, L. (ed.) FOSSACS 2010. LNCS, vol. 6014, pp. 267–281. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  22. Jhala, R., Majumdar, R.: Interprocedural analysis of asynchronous programs. In: POPL, pp. 339–350 (2007)

    Google Scholar 

  23. Kahlon, V.: Boundedness vs. unboundedness of lock chains: Characterizing decidability of pairwise CFL-reachability for threads communicating via locks. In: LICS, pp. 27–36 (2009)

    Google Scholar 

  24. Kochems, J., Ong, C.-H.L.: Safety verification of asynchronous pushdown systems with shaped stacks (long version) (2013), http://www.cs.ox.ac.uk/people/jonathan.kochems/apcps.pdf

  25. Lal, A., Reps, T.W.: Reducing concurrent analysis under a context bound to sequential analysis. Formal Methods in System Design 35(1), 73–97 (2009)

    Article  MATH  Google Scholar 

  26. Long, Z., Calin, G., Majumdar, R., Meyer, R.: Language-theoretic abstraction refinement. In: de Lara, J., Zisman, A. (eds.) FASE 2012. LNCS, vol. 7212, pp. 362–376. Springer, Heidelberg (2012)

    Google Scholar 

  27. Mukund, M., Narayan Kumar, K., Radhakrishnan, J., Sohoni, M.: Towards a characterisation of finite-state message-passing systems. In: Hsiang, J., Ohori, A. (eds.) ASIAN 1998. LNCS, vol. 1538, pp. 282–299. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  28. Mukund, M., Narayan Kumar, K., Radhakrishnan, J., Sohoni, M.: Robust asynchronous protocols are finite-state. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 188–199. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  29. Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)

    Article  Google Scholar 

  30. Sen, K., Viswanathan, M.: Model checking multithreaded programs with asynchronous atomic methods. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 300–314. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  31. La Torre, S., Napoli, M.: Reachability of multistack pushdown systems with scope-bounded matching relations. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 203–218. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  32. La Torre, S., Madhusudan, P., Parlato, G.: Reducing context-bounded concurrent reachability to sequential reachability. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 477–492. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  33. Wehrman, I.: Higman’s theorem and the multiset order (2006), http://www.cs.utexas.edu/~iwehrman/pub/ms-wqo.pdf

Download references

Author information

Authors and Affiliations

  1. University of Oxford, UK

    Jonathan Kochems & C. -H. Luke Ong

Authors
  1. Jonathan Kochems
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. C. -H. Luke Ong
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Facultad de Matemáticas, Astronomía y Física, Universidad Nacional de Córdoba – CONICET, Medina Allende s/n,, X5000HUA, Córdoba, Argentina

    Pedro R. D’Argenio

  2. Departamento de Computación,, Universidad de Buenos Aires - Conicet, Intendente Güirales 2160, C1428EGA, Ciudad Autónoma de Buenos Aires, Argentina

    Hernán Melgratti

Rights and permissions

Reprints and permissions

Copyright information

© 2013 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kochems, J., Ong, C.H.L. (2013). Safety Verification of Asynchronous Pushdown Systems with Shaped Stacks. In: D’Argenio, P.R., Melgratti, H. (eds) CONCUR 2013 – Concurrency Theory. CONCUR 2013. Lecture Notes in Computer Science, vol 8052. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-40184-8_21

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-40184-8_21

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-40183-1

  • Online ISBN: 978-3-642-40184-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation