Abstract
In this paper we investigate the synchronization of multithreaded call graphs with reentrance similar to call graphs in Java programs. We model the individual threads as Visibly Pushdown Automata (VPA) and analyse the reachability of a state in the product automaton by means of a Context Free Language (CFL) which captures the synchronized interleaving of threads. We apply this CFL-reachability analysis to detect deadlock.
This work has been supported by the EU-project IST-33826 Credo: Modelling and analysis of evolutionary structures for distributed services. For more information, see http://credo.cwi.nl
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alpuente, M., Vidal, G. (eds.): SAS 2008. LNCS, vol. 5079. Springer, Heidelberg (2008)
Alur, R., Madhusudan, P.: Visibly Pushdown Languages. In: Babai, L. (ed.) STOC, pp. 202–211. ACM, New York (2004)
Bouajjani, A., Esparza, J., Schwoon, S., Strejcek, J.: Reachability Analysis of Multithreaded Software with Asynchronous Communication. In: Sarukkai, S., Sen, S. (eds.) FSTTCS 2005. LNCS, vol. 3821, pp. 348–359. Springer, Heidelberg (2005)
Bouajjani, A., Esparza, J., Touili, T.: A Generic Approach to the Static Analysis of Concurrent Programs with Procedures. Int. J. Found. Comput. Sci. 14(4), 551 (2003)
Carotenuto, D., Murano, A., Peron, A.: 2-Visibly Pushdown Automata. In: Harju, T., Karhumäki, J., Lepistö, A. (eds.) DLT 2007. LNCS, vol. 4588, pp. 132–144. Springer, Heidelberg (2007)
Chaki, S., Clarke, E.M., Kidd, N., Reps, T.W., 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)
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.W.: Language Strength Reduction. In: Alpuente, Vidal [1], pp. 283–298
Lammich, P., Müller-Olm, M.: Conflict Analysis of Programs with Procedures, Dynamic Thread Creation, and Monitors. In: Alpuente, Vidal [1], pp. 205–220
Ramalingam, G.: Context-Sensitive Synchronization-Sensitive Analysis is Undecidable. ACM Transactions on Programming Languages and Systems 22 (2000)
Reps, T.W.: Program Analysis via Graph Reachability. Information & Software Technology 40(11-12), 701–726 (1998)
Rinard, M.C.: Analysis of Multithreaded Programs. In: Cousot, P. (ed.) SAS 2001. LNCS, vol. 2126, pp. 1–19. Springer, Heidelberg (2001)
van den Brand, M., van Deursen, A., Heering, J., de Jong, H., de Jonge, M., Kuipers, T., Klint, P., Moonen, L., Olivier, P., Scheerder, J., Vinju, J., Visser, E., Visser, J.: The asf+sdf Meta-Environment: A Component-Based Language Development Environment. Electronic Notes in Theoretical Computer Science 44(2), 3–8 (2001); LDTA 2001, First Workshop on Language Descriptions, Tools and Applications (a Satellite Event of ETAPS 2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
de Boer, F.S., Grabe, I. (2010). Automated Deadlock Detection in Synchronized Reentrant Multithreaded Call-Graphs. In: van Leeuwen, J., Muscholl, A., Peleg, D., Pokorný, J., Rumpe, B. (eds) SOFSEM 2010: Theory and Practice of Computer Science. SOFSEM 2010. Lecture Notes in Computer Science, vol 5901. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11266-9_17
Download citation
DOI: https://doi.org/10.1007/978-3-642-11266-9_17
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11265-2
Online ISBN: 978-3-642-11266-9
eBook Packages: Computer ScienceComputer Science (R0)