Context-Bounded Verification of Liveness: B Proofs from Section 4.1

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

B PROOFS FROM SECTION 4.1

Intuitively, the edge in (1) spawns the initial thread, the edges in (2) remove a thread with csnumber 0 when it becomes active for the first time and the edges in (3) convert it to a balloon, the edges in (4) apply the spawns during the 푗th segment of a thread by transferring them from the balloon to the regular places, the edges in (5) and (6) finalize this application process with the edges in (6) handling the special case of the 퐾th segment of a thread, the edges in (7) burst balloons containing no more spawns, and the edges in (8) initialize the application of spawns for a thread with cs-number ≥ 1 that is already being represented by a balloon.

Lemma B.1. The DCPS A has an infinite, progressive, K-context switch bounded run iff the VASSB V has an infinite progressive run.

Proof. For the only if direction let p be an infinite, progressive, K-context switch bounded run of A. We want to decompose p into parts corresponding to a single thread each. To do this we look at the continuous segments of p where a thread is active, starting from the first configuration with an active thread and ending each segment at a configuration with no active thread, upon which a new segment begins at the very next configuration. We can now group segments together into executions of single threads:

• Start with the earliest not yet grouped segment where the active thread has context switch number 0. Note the local configuration that gets added to the bag at the end of this segment.

• Take the very next ungrouped segment in p where the active thread at the beginning matches the previously noted local configuration. Again, note the local configuration that gets added to the bag at the end of this segment.

• Repeat the previous step until an empty stack occurs.

The constructed run of V is also sound: For each segment of p it has a sequence of transitions that make the same state change as that segment, and also apply the same spawns. The latter is due to initially choosing the contents during the creation of a balloon correctly. A token representing the initial thread is also created in the beginning of the run. Since the transitions from one segment to the next require the same resumption rules Δr as in p (see edges (2) and (8)) these are also possible in V.

For the if direction we do a very similar construction, but backwards. Starting with an infinite progressive run of V from c0, we decompose it into segments that end in a state in G. Afterwards we group those segments together by matching the local balloon configurations in the same way we did for local thread configurations before. Then by construction of Lt we know that there is a thread execution of type t that makes the same spawns in each segment as the group of one balloon does. Those executions will all terminate after K context switches, guaranteeing progressiveness, and we can interleave them in the same way as the balloon segments to form an infinite progressive run of A.