Context-Bounded Verification of Liveness for Multithreaded Shared-Memory Programs
summary
Shows that K‑context‑bounded fair termination for recursive multithreaded shared‑memory programs is decidable by reducing to reachability in Petri nets, introduces the intermediate model VASS with balloons whose balloons encode spawn vectors, and proves a decidability chain VASSB → VASS; basic nontermination is 2EXPSPACE‑complete; the proof uses a combinatorial token shifting argument to bound nonempty balloons and yields decidability of fair starvation while matching known non‑elementary lower bounds.
AI-written summary · about
chapters (23)
- 0:00Multithreaded Shared-Memory
- 1:47k-Context Bounded Analysis
- 2:32Example
- 4:34The Nontermination Problem
- 5:13The Fair Nontermination Problem
- 5:57Outline
- 6:29Generic Run of Program with k=2
- 7:16Language of a Thread
- 7:57Nontermination Preserved under Lost Spawns
- 8:28From Regular Threads to VASS
- 10:52Semilinear Representation of Language
- 11:47VASSB Definition
- 12:47VASSB from Programs
- 13:25Reducing Fairness in Programs to Fairness in VASSB
- 14:01Modelling programs with VASSB
- 18:04Self Covering Witness 1
- 19:04Infinitely often Appearing Colors in Infinite Runs
- 19:27Key Concept: Token Shifting in Infinite Runs Infinite Suffix
- 22:10After Token Shifting
- 23:10Reachability in VASSB to VASS
- 24:07Two Similar Balloons in a Finite Run
- 24:48New Token Shifting: Similar Balloons
- 26:00Conclusion
related talks
22mContext-Bounded Verification of Thread Pools
25mParametrised Verification of Intel-x86 Programs
24mTaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Pr
21mCommCSL: Proving Information Flow Security for Concurrent Programs using Abstract(…)
23mA Reachability Logic for a Weak Memory Model with Promises
23mStratified Commutativity in Verification Algorithms for Concurrent Programs
54mReasoning about Progress of Concurrent Objects
31mTermination in Concurrency, Revisited