  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.

Formal Languages and Automata Theory;Programming Languages