  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.
