LIPIcs.FSTTCS.2014.611.pdf
- Filesize: 0.49 MB
- 13 pages
Document
On Bounded Reachability Analysis of Shared Memory Systems
Authors
-
Part of:
Volume:
34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2014-12-12
Cite As Get BibTex
Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, and Prakash Saivasan. On Bounded Reachability Analysis of Shared Memory Systems. In 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014). Leibniz International Proceedings in Informatics (LIPIcs), Volume 29, pp. 611-623, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2014)
https://doi.org/10.4230/LIPIcs.FSTTCS.2014.611
Abstract
This paper addresses the reachability problem for pushdown systems communicating via shared memory. It is already known that this problem is undecidable. It turns out that undecidability holds even if the shared memory consists of a single boolean variable. We propose a restriction on the behaviours of such systems, called stage bound, towards decidability. A k stage bounded run can be split into a k stages, such that in each stage there is at most one process writing to the shared memory while any number of processes may read from it. We consider several versions of stage-bounded systems and establish decidability and complexity results.
Subject Classification
Keywords
- Reachability problem
- Pushdown systems
- Counter systems
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Mohamed Faouzi Atig. Model-checking of ordered multi-pushdown automata. Logical Methods in Computer Science, 8(3), 2012.
-
Mohamed Faouzi Atig, Ahmed Bouajjani, and Tayssir Touili. On the reachability analysis of acyclic networks of pushdown systems. In CONCUR, volume 5201 of Lecture Notes in Computer Science, pages 356-371. Springer, 2008.
-
Mohamed Faouzi Atig and Tayssir Touili. Verifying parallel programs with dynamic communication structures. In CIAA, volume 5642 of Lecture Notes in Computer Science, pages 145-154. Springer, 2009.
-
Pierre Chambart and Ph. Schnoebelen. Post embedding problem is not primitive recursive, with applications to channel systems. In FSTTCS, volume 4855 of Lecture Notes in Computer Science, pages 265-276. Springer, 2007.
-
Bruno Courcelle. On constructing obstruction sets of words. Bulletin of the EATCS, 44:178-186, 1991.
-
Javier Esparza, Pierre Ganty, and Rupak Majumdar. Parameterized verification of asynchronous shared-memory systems. In CAV, volume 8044 of Lecture Notes in Computer Science, pages 124-140. Springer, 2013.
-
Matthew Hague. Parameterised pushdown systems with non-atomic writes. In FSTTCS, volume 13 of LIPIcs, pages 457-468. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2011.
-
Matthew Hague and Anthony Widjaja Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, volume 7358 of Lecture Notes in Computer Science, pages 260-276. Springer, 2012.
-
J. E. Hopcroft and J. D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley series in computer science. Addison-Wesley, 1979.
-
Rodney R. Howell and Louis E. Rosier. An analysis of the nonemptiness problem for classes of reversal-bounded multicounter machines. J. Comput. Syst. Sci., 34(1):55-74, 1987.
-
Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116-133, 1978.
-
Salvatore La Torre, Parthasarathy Madhusudan, and Gennaro Parlato. A robust class of context-sensitive languages. In LICS, pages 161-170. IEEE Computer Society, 2007.
-
Shaz Qadeer and Jakob Rehof. Context-bounded model checking of concurrent software. In TACAS, volume 3440 of Lecture Notes in Computer Science, pages 93-107. Springer, 2005.