Reachability Analysis of Multithreaded Software with Asynchronous Communication

We introduce asynchronous dynamic pushdown networks (ADPN), a new model for multithreaded programs in which pushdown systems communicate via shared memory. ADPN generalizes both CPS (concurrent pushdown systems) [QR05] and DPN (dynamic pushdown networks) [BMOT05]. We show that ADPN exhibit several advantages as a program model. Since the reachability problem for ADPN is undecidable even in the case without dynamic creation of processes, we address the bounded reachability problem [QR05], which considers only those computation sequences where the (index of the) thread accessing the shared memory is changed at most a fixed given number of times. We provide efficient algorithms for both forward and backward reachability analysis. The algorithms are based on automata techniques for symbolic representation of sets of configurations.

• Type: Conference
• Year: 2005
• Where: FSTTCS
• Authors: Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, Jan Strejcek
• Keywords: Asynchronous Dynamic Pushdown, Dynamic Pushdown Networks, FSTTCS 2005, Pushdown Systems