Reference:

Ahmed Bouajjani, Javier Esparza, Stefan Schwoon, and Jan Strejček. Reachability analysis of multithreaded software with asynchronous communication. In Ramaswamy Ramanujam and Sandeep Sen, editors, Proceedings of FSTTCS 2005, volume 3821 of Lecture Notes in Computer Science, pages 348–359. Springer, December 2005.

Abstract:

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) and DPN (dynamic pushdown networks). 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 emphbounded reachability problem, 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.

Suggested BibTeX entry:

@inproceedings{BESS05b,
    author = {Ahmed Bouajjani and Javier Esparza and Stefan Schwoon and Jan Strej\v{c}ek},
    booktitle = {Proceedings of FSTTCS 2005},
    editor = {Ramaswamy Ramanujam and Sandeep Sen},
    month = {December},
    pages = {348--359},
    publisher = {Springer},
    series = {Lecture Notes in Computer Science},
    title = {Reachability analysis of multithreaded software with asynchronous communication},
    volume = {3821},
    year = {2005}
}