Abstract
Undecidability is the scourge of verification for many program classes. We consider the class of shared-memory multithreaded programs in the interleaving semantics such that the number of threads is finite and constant throughout all executions, each thread has an unbounded stack, and the shared memory and the stack-frame memory are finite. Verifying that a given program state does not occur in executions of such a program is undecidable. We show that the complexity of verification drops to polynomial time under multithreaded-Cartesian abstraction. Furthermore, we demonstrate that multithreaded-Cartesian abstract interpretation generates an inductive invariant which is a regular language. Under logarithmic cost measure, both proving non-reachability and creating a finite automaton can be attained in \(\mathcal {O}(n\log _2n)\) time in the number of threads \(n\) and in polynomial time in all other quantities.
The author greatly acknowledges useful comments and suggestions from Neil Deaton Jones.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
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
Alur, R., Madhusudan, P.: Visibly pushdown languages. In: Symposium on Theory of Computing, pp. 202–211. ACM (2004)
Andersen, N., Jones, N.D.: Generalizing Cook’s transformation to imperative stack programs. In: Karhumäki, J., Rozenberg, G., Maurer, H.A. (eds.) Results and Trends in Theoretical Computer Science. LNCS, vol. 812, pp. 1–18. Springer, Heidelberg (1994)
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)
Bouajjani, A., Esparza, J., Touili, T.: A generic approach to the static analysis of concurrent programs with procedures. International Journal of Foundations of Computer Science 14(4), 551–582 (2003)
Bozzelli, L., La Torre, S., Peron, A.: Verification of well-formed communicating recursive state machines. Theoretical Computer Science 203(2-3), 382–405 (2008)
Büchi, J.R.: Regular canonical systems. Archiv für mathematische Logik und Grundlagenforschung 6, 91–111 (1962/1963)
Burkart, O., Steffen, B.: Pushdown processes: parallel composition and model checking. In: Jonsson, B., Parrow, J. (eds.) CONCUR 1994. LNCS, vol. 836, pp. 98–113. Springer, Heidelberg (1994)
Chaki, S., Clarke, E., Kidd, N., Reps, T., Touili, T.: Verifying Concurrent Message-Passing C Programs with Recursive Calls. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 334–349. Springer, Heidelberg (2006)
Cousot, R.: Fondements des méthodes de preuve d’invariance et de fatalité de programmes paralléles. Ph.D. thesis, Institut national polytechnique de Lorraine, pp. 4–118(4–119), pp. 4–120, 1985. §\(4.3.2.4.3\)
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)
Hansen, T.A., Nikolajsen, T., Träff, J.L., Jones, N.D.: Experiments with implementations of two theoretical constructions. In: Meyer, A.R., Taitslin, M.A. (eds.) Logic at Botik 1989. LNCS, vol. 363, pp. 119–133. Springer, Heidelberg (1989)
Jones, C. B.: Tentative steps toward a development method for interfering programs. ACM Trans. Program. Lang. Syst. 5(4), 596–619 (1983)
La Torre, S., Napoli, M., Parlato, G.: A Unifying Approach for Multistack Pushdown Automata. In: Csuhaj-Varjú, E., Dietzfelbinger, M., Ésik, Z. (eds.) MFCS 2014, Part I. LNCS, vol. 8634, pp. 377–389. Springer, Heidelberg (2014)
Malkis, A.: Cartesian abstraction and verification of multithreaded programs. Ph.D. thesis, Albert-Ludwigs-Universität Freiburg (2010)
Malkis, A.: Multithreaded-Cartesian abstract interpretation of multithreaded recursive programsis polynomial. Technical report (2015). http://www4.in.tum.de/ malkis/ Malkis-MultCartAbstIntOfMultRecProgIsPoly_techrep.pdf
Malkis, A., Podelski, A., Rybalchenko, A.: Thread-Modular Verification Is Cartesian Abstract Interpretation. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC 2006. LNCS, vol. 4281, pp. 183–197. Springer, Heidelberg (2006)
Mehlhorn, K.: Data structures and algorithms 1: sorting and searching. In: EATCS Monographs in Theoretical Computer Science, vol. 1. Springer (1984)
Mogensen, T.Æ.: WORM-2DPDAs: An extension to 2DPDAs that can be simulated in linear time. Inf. Process. Lett. 52(1), 15–22 (1994)
Nielson, F., Nielson, H.R., Seidl, H.: Normalizable Horn Clauses, Strongly Recognizable Relations, and Spi. In: Hermenegildo, M.V., Puebla, G. (eds.) SAS 2002. LNCS, vol. 2477, pp. 20–35. Springer, Heidelberg (2002)
Owicki, S.S.: Axiomatic proof techniques for parallel programs. Ph.D. thesis, Cornell University, department of computer science, TR 75–251, July 1975
Qadeer, S., Rajamani, S.K., Rehof, J.: Summarizing procedures in concurrent programs. In: Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 245–255. ACM, New York (2004)
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)
Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)
Schwoon, S.: Model-checking pushdown systems. Ph.D. thesis, Technische Universität München, June 2002
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer International Publishing Switzerland
About this paper
Cite this paper
Malkis, A. (2015). Multithreaded-Cartesian Abstract Interpretation of Multithreaded Recursive Programs Is Polynomial. In: Bojanczyk, M., Lasota, S., Potapov, I. (eds) Reachability Problems. RP 2015. Lecture Notes in Computer Science(), vol 9328. Springer, Cham. https://doi.org/10.1007/978-3-319-24537-9_11
Download citation
DOI: https://doi.org/10.1007/978-3-319-24537-9_11
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-24536-2
Online ISBN: 978-3-319-24537-9
eBook Packages: Computer ScienceComputer Science (R0)