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: |