Context-Bounded Verification of Liveness: Fair Non-Termination

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

4 FAIR NON-TERMINATION

We now turn to proving Theorem 2.3. Unfortunately, fair termination is not preserved under downward closure. The example in Section 1 has no fair infinite run, since eventually (under fairness), bit is set to 1 by the instance of bar and the program terminates. However, the downward closure that omits bar has a fair infinite run. Thus, we cannot replace the PDAs for each thread with finite-state automata and there is no obvious reduction to VASS.

Our proof is more complicated. First, we introduce an extension, VASS with balloons (VASSB), of VASS (Section 4.1). A VASSB extends a VASS with balloon states and balloon places, and allows keeping multisets of state-vector pairs over balloons. We can use this additional power to store spawned threads. As we shall see (Section 4.2), we can reduce DCPS to VASSB. Later, we shall show decidability of fair infinite behaviors for VASSB, completing the proof.

4.1 VASS with Balloons

4.2 From DCPS to VASSB

Instead of reducing fairness for DCPS to VASSB, we would like to use a stronger notion, which simplifies many of our proofs. To this end, we introduce the notion of progressiveness that we already defined for VASSB now for DCPS as well: given a bound K ∈ N, an infinite run p of a DCPS is called progressive if the rule Term is only ever applied when the active thread is at K context switches, and for every local configuration (w, i) of an inactive thread in a configuration of p, there is a future point in p where the rule Resume is applied to (w, i), making it the local configuration of the active thread.

Intuitively, no type of thread can stay around infinitely long in a progressive run without being resumed, and every thread that terminates does so after exactly K context switches. Note that progressiveness is a stronger condition than fairness, because it does not allow threads to “get stuck” or go above the context switch bound K. However, we can always transform a DCPS where we want to consider fair runs into one where we can consider progressive runs instead. The transformation is formalized by the following lemma.

Idea. One of the main insights regarding the behavior of DCPS is that the order of the spawns of a thread during one round of being active does not matter. None of the spawned threads during one such segment can influence the run until the active thread changes. Thus we only need to look at the semi-linear Parikh image of the language of spawns for each segment. One can then identify a thread with the state changes and spawns it makes during segments 0 through 퐾. The state changes can be stored in a balloon state and the spawns for each segment in balloon places that correspond to K + 1 copies of the stack alphabet. The inflate operation then basically guesses the exact multiset of spawns of the corresponding thread.

Representing threads by balloons in this way does not keep track of stack contents, which was important for ensuring the progressiveness of a DCPS run. However, starting from a progressive DCPS run we can always construct a progressive run for the VASSB by always continuing with the oldest thread in a configuration if given multiple choices, and then building the balloons accordingly. Always picking the oldest balloon also works for the reverse direction.

The proof also allows us to reason about shallow progressive runs of DCPS. Following the same notion for VASSB, we call a run of a DCPS shallow if there is a bound B ∈ N such that each thread on that run spawns at most B threads. Obverse that in the VASSB construction of this section the spawns of DCPS threads are mapped to the contents of balloons, which is how the two notions of shallowness correspond to each other. Thus we can go from progressive DCPS-run to progressive VASSB-run by Theorem 4.4, to shallow progressive VASSB-run by Theorem 4.2, to shallow progressive DCPS run by Theorem 4.4 combined with the observation on the two notions of shallowness. This is formalized in the following: