Reachability Analysis of Dynamic Pushdown Networks with Priorities

摘要

In this paper, we consider the reachability problem of multithreaded programs where threads have priorities and are scheduled by a priority based round-robin scheduler. For that, we introduce a new model, called Dynamic Pushdown Networks with Priorities (P-DPNs) that extends the well known DPN model with priorities. We represent potentially infinite sets of configurations of P-DPNs using finite state automata and show that the backward reachability sets of P-DPNs are regular and can be effectively computed.