Abstract
Dynamic Pushdown Networks (DPNs) are a model for parallel programs with (recursive) procedures and process creation. The goal of this paper is to develop generic techniques for more expressive reachability analysis of DPNs.
In the first part of the paper we introduce a new tree-based view on executions. Traditional interleaving semantics model executions by totally ordered sequences. Instead, we model an execution by a partially ordered set of rule applications, that only specifies the per-process ordering and the causality due to process creation, but no ordering between rule applications on processes that run in parallel. Tree-based executions allow us to compute predecessor sets of regular sets of DPN configurations relative to (tree-) regular constraints on executions. The corresponding problem for interleaved executions is not effective.
In the second part of the paper, we extend DPNs with (well-nested) locks. We generalize Kahlon and Gupta’s technique of acquisition histories to DPNs, and apply the results of the first part of this paper to compute lock-sensitive predecessor sets.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Bouajjani, A., Esparza, J., Schwoon, S., Strejcek, J.: Reachability analysis of multithreaded software with asynchronous communication. In: Ramanujam, R., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 348–359. Springer, Heidelberg (2005)
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)
Bruggemann-Klein, A., Murata, M., Wood, D.: Regular tree and regular hedge languages over unranked alphabets. Research report (2001)
Kahlon, V., Gupta, A.: An automata-theoretic approach for model checking threads for LTL properties. In: Proc. of LICS 2006, pp. 101–110. IEEE Computer Society, Los Alamitos (2006)
Kahlon, V., Ivancic, 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)
Kidd, N., Lal, A., Reps, T.: Language strength reduction. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 283–298. Springer, Heidelberg (2008)
Kidd, N., Lammich, P., Touili, T., Reps, T.: A decision procedure for detecting atomicity violations for communicating processes with locks (submitted for publication)
Kidd, N., Reps, T., Dolby, J., Vaziri, M.: Finding concurrency-related bugs using random isolation. In: Jones, N.D., Müller-Olm, M. (eds.) VMCAI 2009. LNCS, vol. 5403, pp. 198–213. Springer, Heidelberg (2009)
Lammich, P.: Isabelle formalization of hedge-constrained pre* and DPNs with locks. Technical Report, http://cs.uni-muenster.de/sev/publications/
Lammich, P., Müller-Olm, M.: Conflict analysis of programs with procedures, dynamic thread creation, and monitors. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 205–220. Springer, Heidelberg (2008)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Reps, T., Schwoon, S., Jha, S., Melski, D.: Weighted pushdown systems and their application to interprocedural dataflow analysis. Sci. Comput. Program. 58(1-2), 206–263 (2005)
Wenner, A.: Optimale Analyse gewichteter dynamischer Push-Down Netzwerke. Master’s thesis, University of Münster (August 2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Lammich, P., Müller-Olm, M., Wenner, A. (2009). Predecessor Sets of Dynamic Pushdown Networks with Tree-Regular Constraints. In: Bouajjani, A., Maler, O. (eds) Computer Aided Verification. CAV 2009. Lecture Notes in Computer Science, vol 5643. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-02658-4_39
Download citation
DOI: https://doi.org/10.1007/978-3-642-02658-4_39
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-02657-7
Online ISBN: 978-3-642-02658-4
eBook Packages: Computer ScienceComputer Science (R0)