Context-Bounded Verification of Liveness: Dynamic Networks of Concurret Pushdown Systems (DCPS)

Table of Links

• Introduction
• Dynamic Networks of Concurret Pushdown Systems (DCPS)
• Warm-up: Non-Termination
• Fair Non-Termination
• From Progressive Runs for VASSB to Reachability
• Starvation
• Conclusion, Acknowledgment & References
• A. Strengthening Fairness to Progressive Runs
• B. Proofs from Section 4.1
• C. Proofs for Section 5
• D. Proofs for Section 5.3
• E. Proofs for Section 6

2 DYNAMIC NETWORKS OF CONCURRENT PUSHDOWN SYSTEMS (DCPS)

2.1 Preliminary Definitions

2.2 Dynamic Networks of Concurrent Pushdown Systems

2.3 Identifiers and the Run of a Thread

2.4 Decision Problems and Main Results

Note that since our model does not have individual thread identifiers, fairness is defined only over equivalence classes of threads that have the same stack 푤 and the same context switch number i. The reason for our taking into account stacks and context switch numbers is the following. It is a simple observation that there exists an infinite fair run in our sense if and only if there exists a run in the corresponding system with thread identifiers–that is fair to each individual thread. This is because an angelic scheduler could always pick the earliest spawned thread among those with the same stack and context switch number. Therefore, our results allow us to reason about multi-threaded systems with identifiers.

This raises the question of whether there are runs that are fair in our sense, but where a nonangelic scheduler would still yield unfairness for some thread identity. In other words, is it possible that a fair run starves a specific thread. For example, consider a program in which the main thread spawns two copies of a thread foo. Each thread foo, when scheduled, simply spawns another copy of foo and terminates. Here is a fair run of the program (we omit the global state as it is not relevant), where we have decorated the threads with identifiers:

Question Is there an infinite, fair K-context switch bounded run that starves some thread?

We show the following results.

Theorem 2.3 (Fair Non-Termination). For each K ∈ N, the problem FNTERM[K] is decidable

Theorem 2.4 (Fair Starvation). For each K ∈ N, the problem STARV[K] is decidable.