Document Open Access Logo

Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable

Authors Salvatore La Torre, Anca Muscholl, Igor Walukiewicz

PDF
Thumbnail PDF

File

LIPIcs.CONCUR.2015.72.pdf
  • Filesize: 0.7 MB
  • 13 pages

Document Identifiers

Author Details

Salvatore La Torre
Anca Muscholl
Igor Walukiewicz

Cite As Get BibTex

Salvatore La Torre, Anca Muscholl, and Igor Walukiewicz. Safety of Parametrized Asynchronous Shared-Memory Systems is Almost Always Decidable. In 26th International Conference on Concurrency Theory (CONCUR 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 42, pp. 72-84, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.CONCUR.2015.72

Abstract

Verification of concurrent systems is a difficult problem in general, and  this is the case even more in a parametrized setting where unboundedly many concurrent components are considered. Recently, Hague proposed an architecture with a leader process and unboundedly many copies of a contributor process interacting over a shared memory for which safety properties can be effectively verified. All processes in Hague's setting are pushdown automata. Here, we extend it by considering other formal models and, as a main contribution, find very liberal conditions on the individual processes under which the safety problem is decidable: the only substantial condition we require is the effective computability of the downward closure for the class of the leader processes. Furthermore, our result allows for a hierarchical approach to constructing models of concurrent systems with decidable safety problem: networks with tree-like architecture, where each process shares a register with its children processes (and another register with its parent). Nodes in such networks can be for instance pushdown automata, Petri nets, or multi-pushdown systems with decidable reachability problem.

Subject Classification

Keywords
  • Verification
  • parametrized systems
  • shared memory

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. P. A. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91-101, 1996. Google Scholar
  2. Parosh Aziz Abdulla, Luc Boasson, and Ahmed Bouajjani. Effective lossy queue languages. In ICALP'01, LNCS, pages 639-651. Springer, 2001. Google Scholar
  3. Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Holík. All for the price of few. In VMCAI'13, LNCS, pages 476-495. Springer, 2013. Google Scholar
  4. Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, Frédéric Haziza, and Ahmed Rezine. Parameterized tree systems. In FORTE'08, LNCS, pages 69-83. Springer, 2008. Google Scholar
  5. Benjamin Aminof, Tomer Kotek, Sasha Rubin, Francesco Spegni, and Helmut Veith2. Parameterized model checking of rendezvous systems. In CONCUR'14, LNCS, pages 109-124. Springer, 2014. Google Scholar
  6. Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. On bounded reachability analysis of shared memory systems. In FSTTCS'14, volume 29 of LIPIcs, pages 611-623. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. Google Scholar
  7. Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. Logical Methods in Computer Science, 7(4):1-48, 2011. Google Scholar
  8. Thomas Ball, Sagar Chaki, and Sriram K. Rajamani. Parameterized verification of multithreaded software libraries. In TACAS'01, LNCS, pages 158-173. Springer, 2001. Google Scholar
  9. Benedikt Bollig, Paul Gastin, and Jana Schubert. Parameterized verification of communicating automata under context bounds. In Reachability problems - International Workshop, LNCS, pages 45-57. Springer, 2014. Google Scholar
  10. Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejcek. Reachability analysis of multithreaded software with asynchronous communication. In FSTTCS'05, LNCS, pages 348-359. Springer, 2005. Google Scholar
  11. Edmund M. Clarke, Orna Grumberg, and Somesh Jha. Verifying parameterized networks. ACM Trans. Program. Lang. Syst., 19(5):726-750, 1997. Google Scholar
  12. Bruno Courcelle. On constructing obstruction sets of words. Bulletin of EATCS, 1991. Google Scholar
  13. Giorgio Delzanno. Parameterized verification and model checking for distributed broadcast protocols. In ICGT'14, LNCS, pages 1-16. Springer, 2014. Google Scholar
  14. Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification. In STACS'14, LIPIcs, pages 1-10. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. Google Scholar
  15. Javier Esparza, Alain Finkel, and Richard Mayr. On the verification of broadcast protocols. In LICS'99, pages 352-359. IEEE, 1999. Google Scholar
  16. Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV'13, LNCS, pages 124-140. Springer, 2013. Google Scholar
  17. S. A. German and P. A. Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675-735, 1992. Google Scholar
  18. Peter Habermehl, Roland Meyer, and Harro Wimmel. The downward-closure of Petri net languages. In ICALP'10, LNCS, pages 466-477. Springer, 2010. Google Scholar
  19. Matthew Hague. Parameterised pushdown systems with non-atomic writes. In FSTTCS'11, LIPIcs, pages 457-468. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2011. Google Scholar
  20. Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre. Collapsible pushdown automata and recursion schemes. In LICS'08, pages 452-461. IEEE, 2008. Google Scholar
  21. Vineet Kahlon. Parameterization as abstraction: A tractable approach to the dataflow analysis of concurrent programs. In LICS'08, pages 181-192. IEEE, 2008. Google Scholar
  22. Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV'10, LNCS, pages 645-659. Springer, 2010. Google Scholar
  23. Yonit Kesten, Amir Pnueli, Elad Shahar, and Lenore D. Zuck. Network invariants in action. In CONCUR'02, LNCS, pages 101-115. Springer, 2002. Google Scholar
  24. Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Model-checking parameterized concurrent programs using linear interfaces. In CAV'10, LNCS, pages 629-644. Springer, 2010. Google Scholar
  25. Salvatore La Torre, P. Madhusudan, and Gennaro Parlato. Sequentializing parameterized programs. In FIT'12, volume 87 of EPTCS, pages 34-47, 2012. Google Scholar
  26. Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. Scope-bounded pushdown languages. In DLT'14, LNCS, pages 116-128. Springer, 2014. Google Scholar
  27. Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. A unifying approach for multistack pushdown automata. In MFCS'14, LNCS, pages 377-389. Springer, 2014. Google Scholar
  28. Richard Mayr. Undecidable problems in unreliable computations. TCS, 1-3(297):337-354, 2003. Google Scholar
  29. Kedar S. Namjoshi and Richard J. Trefler. Analysis of dynamic process networks. In TACAS'15, LNCS, pages 164-178. Springer, 2015. Google Scholar
  30. Georg Zetzsche. An approach to computing downward closures. In ICALP'15, LNCS, pages 440-451. Springer, 2015. Google Scholar
  31. Georg Zetzsche. Computing downward closures for stacked counter automata. In STACS'15, LIPIcs, pages 743-756. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact