一句话：证明线程池上下文限界布尔程序安全性验证为 EXPSPACE 完全，并给出基于向下闭包的紧致编码。
线程池是并发编程常见模式：固定数量的工作线程反复取任务并顺序执行，任务可递归并通过共享内存通信，还可派生子任务。本文研究线程池程序的安全性验证问题，以线程池大小和每个任务的上下文切换次数为参数；上下文限界对多线程递归程序的可判定性至关重要。作者证明，即使两个参数以二进制给出，线程池、上下文限界的布尔程序安全性验证仍是 EXPSPACE 完全的。其上界证明引入了一系列新的紧致编码技术，尤其是将 succinct pushdown automata 接受语言的向下闭包在多项式时间内构造为 doubly succinct nondeterministic finite automata，从而压缩了原本双指数下界的自动机表示。结果还表明线程池显著降低计算能力：若只有上下文限界为二进制且无线程池，问题变为 3EXPSPACE 完全。
Thread pooling is a common programming idiom in which a fixed set of worker threads are maintained to execute tasks concurrently. The workers repeatedly pick tasks and execute them to completion. Each task is sequential, with possibly recursive code, and tasks communicate over shared memory. Executing a task can lead to more new tasks being spawned. We consider the safety verification problem for thread-pooled programs. We parameterize the problem with two parameters: the size of the thread pool as well as the number of context switches for each task. The size of the thread pool determines the number of workers running concurrently. The number of context switches determines how many times a worker can be swapped out while executing a single task---like many verification problems for multithreaded recursive programs, the context bounding is important for decidability. We show that the safety verification problem for thread-pooled, context-bounded, Boolean programs is EXPSPACE-complete, even if the size of the thread pool and the context bound are given in binary. Our main result, the EXPSPACE upper bound, is derived using a sequence of new succinct encoding techniques of independent language-theoretic interest. In particular, we show a polynomial-time construction of downward closures of languages accepted by succinct pushdown automata as doubly succinct nondeterministic finite automata. While there are explicit doubly exponential lower bounds on the size of nondeterministic finite automata accepting the downward closure, our result shows these automata can be compressed. We show that thread pooling significantly reduces computational power: in contrast, if only the context bound is provided in binary, but there is no thread pooling, the safety verification problem becomes 3EXPSPACE-complete. Given the high complexity lower bounds of related problems involving binary parameters, the relatively low complexity of safety verification with thread-pooling comes as a surprise.
@article{paperbot1556,
title = {Context-bounded verification of thread pools},
author = {Pascal Baumann and Rupak Majumdar and Ramanathan S. Thinniyam and Georg Zetzsche},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {POPL},
year = {2022},
doi = {10.1145/3498678}
}