一句话：证明上下文限定下多线程共享内存程序（线程可动态生成）的公平终止等活性性质可判定。
论文研究多线程共享内存程序（线程可动态生成子线程）活性性质的上下文限定验证，每个新生成线程只能被上下文切换固定常数次。作者证明公平终止可判定：由于公平终止需推理无界多线程与无界栈的组合，既有把下推线程替换为有限状态线程的技术失效。为此引入带气球 VASS（VASSB），其令牌本身是标记（气球）。论文将上下文限定公平终止归约到 VASSB 公平终止，再经配置可达性归约到 VASS 可达性。下界方面，公平终止即使无线程切换也已非初等；上下文限定终止是 2EXPSPACE-完全的；公平饥饿在上下文限定下同样可判定且非初等。
We study context-bounded verification of liveness properties of multi-threaded, shared-memory programs, where each thread can spawn additional threads. Our main result shows that context-bounded fair termination is decidable for the model; context-bounded implies that each spawned thread can be context switched a fixed constant number of times. Our proof is technical, since fair termination requires reasoning about the composition of unboundedly many threads each with unboundedly large stacks. In fact, techniques for related problems, which depend crucially on replacing the pushdown threads with finite-state threads, are not applicable. Instead, we introduce an extension of vector addition systems with states (VASS), called VASS with balloons (VASSB), as an intermediate model; it is an infinite-state model of independent interest. A VASSB allows tokens that are themselves markings (balloons). We show that context bounded fair termination reduces to fair termination for VASSB. We show the latter problem is decidable by showing a series of reductions: from fair termination to configuration reachability for VASSB and thence to the reachability problem for VASS. For a lower bound, fair termination is known to be non-elementary already in the special case where threads run to completion (no context switches). We also show that the simpler problem of context-bounded termination is 2EXPSPACE-complete, matching the complexity bound---and indeed the techniques---for safety verification. Additionally, we show the related problem of fair starvation, which checks if some thread can be starved along a fair run, is also decidable in the context-bounded case. The decidability employs an intricate reduction from fair starvation to fair termination. Like fair termination, this problem is also non-elementary.
@article{paperbot1201,
title = {Context-bounded verification of liveness properties for multithreaded shared-memory programs},
author = {Pascal Baumann and Rupak Majumdar and Ramanathan S. Thinniyam and Georg Zetzsche},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434325}
}