Publication details
Reachability Analysis of Multithreaded Software with Asynchronous Communication
Authors | |
---|---|
Year of publication | 2005 |
Type | Article in Proceedings |
Conference | FSTTCS 2005: Foundations of Software Technology and Theoretical Computer Science, 25th International Conference |
MU Faculty or unit | |
Citation | |
Field | Informatics |
Keywords | bounded reachability; symbolic reachability; asynchronous dynamic pushdown network |
Description | 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. |
Related projects: |