Context-Bounded Verification of Liveness: Starvation

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

6 STARVATION

We now prove Theorem 2.4. Let us first explain the additional difficulty of the starvation problem. For deciding progressive termination, we observed that each thread execution can be abstracted by its type and the threads it spawns. (In other words, two executions that agree in these data are interchangeable without affecting progressiveness of a run.) However, for starvation of a thread, it is also important whether each thread visits some stack content w after i context switches. Here, w is not known in advance and has to be agreed upon by an infinite sequence of threads.

Very roughly speaking, we reduce starvation to progressive termination as follows. For each thread, we track its spawned multiset up to some bound B. Using Ramsey’s theorem [Ramsey 1930, Theorem B], we show that if we choose B high enough, then this abstraction already determines whether a sequence of thread executions can be replaced with different executions that actually visit some agreed upon stack content w after i context switches. The latter condition permitting replacement of threads will be called “consistency.”

A further subtlety is that consistency of the abstractions up to B only guarantees consistency of the (unabstracted) executions if the run is shallow. Here, Corollary 4.5 will yield a shallow run, so that we may conclude consistency of the unabstracted executions.

Terminology

Consistency

Our first step in deciding starvation is to find a reformulation that does not explicitly mention the stack w. Instead, it states the existence of 푤 as a consistency condition, which we will develop now.

Starvation in Terms of Consistency

Tracking Consistency

Deciding Starvation

Freezing DCPS

Reduction to Progressive Runs in Freezing DCPS

Proving Theorems 6.2 and 6.3