×

zbMATH — the first resource for mathematics

Automated deadlock detection in synchronized reentrant multithreaded call-graphs. (English) Zbl 1274.68084
van Leeuwen, Jan (ed.) et al., SOFSEM 2010: Theory and practice of computer science. 36th conference on current trends in theory and practice of computer science, Špindlerův Mlýn, Czech Republic, January 23–29, 2010. Proceedings. Berlin: Springer (ISBN 978-3-642-11265-2/pbk). Lecture Notes in Computer Science 5901, 200-211 (2010).
Summary: 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.
For the entire collection see [Zbl 1180.68007].

MSC:
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
68Q45 Formal languages and automata
68R10 Graph theory (including graph drawing) in computer science
Software:
ASF+SDF; MAGIC
PDF BibTeX XML Cite
Full Text: DOI