# Context-Bounded Verification of Liveness Properties for Multithreaded
Shared-Memory Programs

Pascal Baumann  0000-0002-9371-0807 Max Planck Institute for Software Systems
(MPI-SWS)Paul-Ehrlich-Straße, Building G26Kaiserslautern67663Germany
<EMAIL_ADDRESS>,  Rupak Majumdar  0000-0003-2136-0542 Max Planck
Institute for Software Systems (MPI-SWS)Paul-Ehrlich-Straße, Building
G26Kaiserslautern67663Germany<EMAIL_ADDRESS>,  Ramanathan S. Thinniyam
0000-0002-9926-0931 Max Planck Institute for Software Systems (MPI-SWS)Paul-
Ehrlich-Straße, Building G26Kaiserslautern67663Germany<EMAIL_ADDRESS>and  Georg Zetzsche  0000-0002-6421-4388 Max Planck Institute for Software
Systems (MPI-SWS)Paul-Ehrlich-Straße, Building G26Kaiserslautern67663Germany
<EMAIL_ADDRESS>
###### Abstract.

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
${\mathsf{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.

††copyright: none

##  1\. Introduction

We study decision problems related to liveness verification of shared-memory
multithreaded programs. In a shared-memory multithreaded program, a number of
_threads_ execute concurrently. Each thread executes possibly recursive
sequential code, and can spawn new threads for concurrent execution. The
threads communicate through shared global variables that they can read and
write. The execution of the program is guided by a non-deterministic
_scheduler_ that picks one of the spawned threads to execute in each time
step. If the scheduler replaces the currently executing thread with a
different one, we say the current active thread is _context switched_.

Shared-memory multithreaded programming is ubiquitous and static verification
of safety or liveness properties of such programs is a cornerstone of formal
verification research. Indeed, there is a vast research literature on the
problem—from a foundational understanding of the computability and complexity
of (subclasses of) models, to program logics, and to efficient tools for
analysis of real systems.

In this paper, we focus on _decidability_ issues for _liveness_ verification
for multithreaded shared memory programs with the ability to spawn threads.
Liveness properties, intuitively, specify that “something good” happens when a
program executes. A simple example of a liveness property is _termination_ :
the property that a program eventually terminates. In fact, termination is a
“canonical” liveness property: for a very general class of liveness
properties, through monitor constructions, verifying liveness properties
reduces to verifying termination (Apt and Olderog, 1991; Vardi, 1991).

Unfortunately, under the usual notion of non-deterministic schedulers, some
programs may fail to terminate for uninteresting reasons. Consider the
following program:

⬇

1global bit := 1;

2main() { spawn foo; spawn bar; }

3foo() { if bit = 1 then spawn foo; }

4bar() { bit := 0; }

A main thread spawns two additional threads $\mathtt{foo}$ and $\mathtt{bar}$.
The thread $\mathtt{foo}$ checks if a global bit is set and, if so, re-spawns
itself. The thread $\mathtt{bar}$ resets the global bit. There is a non-
terminating execution of this program in which $\mathtt{bar}$ is never
scheduled. However, a scheduler that never schedules a thread that is ready to
run would be considered unfair. Instead, one formulates the problem of _fair
termination_ : termination under a _fair_ non-deterministic scheduler. We
abstract away from the exact mechanism of the scheduler, and only require that
every spawned thread that is infinitely often ready to run is eventually
scheduled. Then, every fair run of the above program is terminating:
eventually $\mathtt{bar}$ is scheduled, after which $\mathtt{foo}$ does not
spawn a new thread.

Fair termination of concurrent programs is highly undecidable. A celebrated
result by Harel (1986) shows that fair termination is $\Pi_{1}^{1}$-complete;
in fact, the problem is already $\Pi_{1}^{1}$-complete when the global state
is finite and there are a finite number of recursive threads.111 Recall that
the class $\Pi_{1}^{1}$ in the analytic hierarchy is the class of all
relations on ${\mathbb{N}}$ that can be defined by a universal _second-order_
number-theoretic formula.  In contrast, safety verification, modeled as state
reachability, is merely $\Sigma_{1}^{0}$-complete.

Since the high undecidability relies on an unbounded exchange of information
among threads, a recent and apposite approach to verifying concurrent
recursive programs is to explore only a representative subset of program
behaviors by limiting the number of inter-thread interactions (Qadeer and
Rehof, 2005; Musuvathi and Qadeer, 2007). This approach, called context
bounding by Qadeer and Rehof (2005), considers the verification problem as a
family of problems, one for each $K$. The $K$-context bounded instance, for
any fixed $K\geq 0$, considers only those executions where each thread is
context switched at most $K$ times by the scheduler. In the limit as
$K\rightarrow\infty$, the $K$-bounded approach explores all behaviors where
each thread runs a finite number of times. In practice, bounded explorations
with small values of $K$ have proved to be effective to uncover many safety
and liveness bugs in real systems.

In this paper, we prove the following results. We first show that $K$-context
bounded termination for multithreaded recursive programs with spawns is
decidable and ${\mathsf{2EXPSPACE}}$-complete when $K\geq 1$. Then, we show
that $K$-context bounded fair termination is decidable but non-elementary. Our
result implies fair termination is $\Pi_{1}^{0}$-complete when each thread is
context-switched a finite number of times. (Note that this does not contradict
the $\Pi_{1}^{1}$-completeness of the general problem, in which a thread can
be context switched infinitely often.) We also study a stronger notion of
fairness called _fair non-starvation_ , where threads are given unique
identities in order to distinguish threads with the same local configuration,
and show that fair non-starvation is also decidable.

Our results generalize the special case of $K=0$ studied by Ganty and Majumdar
(2012) as _asynchronous programs_. When $K=0$, each thread executes to
completion without being interrupted in the middle. Ganty and Majumdar show
the decidability of safety and liveness verification for this model. In
particular, they prove safety and termination are both
${\mathsf{EXPSPACE}}$-complete and fair termination and fair starvation are
decidable but non-elementary.222 Their result shows a polynomial-time
equivalence between fair termination and reachability in vector addition
systems with states (VASS, a.k.a. Petri nets). The complexity bounds follow
from our current knowledge of the complexity of VASS reachability (Czerwinski
et al., 2019).  Their proof depends on the observation that, since threads are
not interrupted, one can replace the pushdown automata for each thread by
finite automata that accept Parikh-equivalent languages. Unfortunately, their
technique does not generalize when context switches are allowed.

For $K\geq 1$, Atig et al. (2009) showed that the safety verification problem
is decidable in ${\mathsf{2EXPSPACE}}$. Ten years later, a matching lower
bound was shown by Baumann et al. (2020). The key observation in the decision
procedure is that safety is preserved under downward closures: one can analyze
a related program where some spawned threads are “forgotten.” Since the
downward closure of a context free language is effectively regular, one can
replace the pushdown automaton for each thread by a finite automaton accepting
the downward closure. In fact, our proof of termination also follows easily
from this observation, as termination is also preserved by downward closures.

Unfortunately, fair termination and fair non-starvation are not preserved
under downward closures. Thus, we cannot apply the preceding techniques to
replace pushdown automata by finite automata in our construction. Thus, our
proof is more intricate and requires several insights into the computational
model.

The key difficulty in our decision procedure is to maintain a finite
representation for _unboundedly_ many active threads, each with _unboundedly_
large local stacks and potentially spawning _unboundedly_ many new threads,
and to compose their context-switched executions into a global execution. In
order to maintain and compose such configurations, we introduce a new model,
called _VASS with balloons_ ($\mathsf{VASSB}$), that extends the usual model
of a vector addition systems with states (VASS) with “balloons”: a token in a
$\mathsf{VASSB}$ can be a usual VASS token or a balloon token that is itself a
vector. Intuitively, balloon tokens represent the possible new threads a
thread can spawn along one of its execution segments.

We show through a series of constructions that the fair termination problem
reduces to the fair termination problem for $\mathsf{VASSB}$, and thence to
the configuration reachability problem for $\mathsf{VASSB}$. Finally, we show
that configuration reachability for VASSB is decidable by a reduction to the
reachability problem for VASS. This puts $\mathsf{VASSB}$ in the rare class of
infinite-state systems which generalize VASS and yet maintain a decidable
reachability (not just coverability!) problem.

Finally, we show a reduction from the fair starvation problem to fair
termination. The reduction relies on two combinatorial insights. The first is
that if a program has an infinite fair run, then it has one in which there
exists a bound on the number of threads spawned by each thread. The second is
a novel pumping argument based on Ramsey’s theorem; it implies that it
suffices to track a finite amount of data about each thread to determine
whether some thread can be starved.

In conclusion, we prove decidability of liveness verification for
multithreaded shared memory programs with the ability to dynamically spawn
threads, an extremely expressive model of multithreaded programming. This
model sits at the boundary of decidability and subsumes many other models
studied before.

Related Work. Safety verification for concurrent recursive programs is already
undecidable with just two threads and finite global store (Ramalingam, 2000).
Many results on context-bounded safety verification consider a model with a
_fixed_ number of threads, without spawns. The complexity of safety
verification for this model is well understood at this point. The key idea
underlying the best algorithms reduce the problem to analyzing a sequential
pushdown system (Lal and Reps, 2009) by guessing the bounded sequences of
context switches for each thread and using the finite state to ensure the
sequential runs can be stitched together.

When the model allows _spawning_ of new threads, as ours does, existing
decision procedures are significantly more complex, both in their
technicalities and in computational cost. There are relatively few results on
decidability of liveness properties of infinite-state systems. Atig et al.
(2012a) show a sufficient condition for fair termination for context-bounded
executions of a fixed number of threads, where they look for ultimately
periodic executions, in which each thread is context switched at most $K$
times in the loop. They show that the search for such ultimately periodic
executions can be reduced to safety verification. In our model, fair infinite
runs may involve unboundedly many threads with unbounded stacks and need not
be periodic—for example, there can always be more and more newly spawned
threads.

Multi-pushdown systems model multithreaded programs with a fixed number of
threads. Many decision procedures are known when the executions of such
systems are restricted through different bounds such as context, scope, or
phase (Atig et al., 2012b; Torre et al., 2016; Atig et al., 2017), and also
through limitations on communication patterns (Lal et al., 2008). These
problems are orthogonal to us, either in the modeling capabilities or in the
properties verified.

Decidability of linear temporal logic is known for weaker models of
multithreaded recursive programs, such as symmetric parameterized programs
(Kahlon, 2008) or leader-follower programs with non-atomic reads and writes
(Durand-Gasselin et al., 2017; Fortin et al., 2017; Muscholl et al., 2017).
These programs cannot perform compare-and-swap operations, and therefore,
their computational power is quite limited (in fact, LTL model checking is
PSPACE-complete). A number of heuristic approaches to fair termination of
multithreaded programs provide sound but incomplete algorithms, but for a more
general class of programs involving infinite-state data variables (Cook et
al., 2011; Padon et al., 2018; Farzan et al., 2016; Cook et al., 2007; Kragl
et al., 2020). The goal there is to provide a sound proof rule for
verification but not to prove a decidability result.

In terms of fair termination problems for VASS, the theme of computational
hardness continues. For example, the classical notion of _fair runs_ , in
which an infinitely activated transition has to be fired infinitely often,
leads to undecidability (Carstensen, 1987) and even
$\Sigma_{1}^{1}$-completeness (Howell et al., 1991). However, _weakly fair_
termination, where only those transitions that are almost always activated
have to be fired infinitely often, is decidable (Jančar, 1990). A rich
taxonomy of fairness notions with corresponding decidability results can be
found in (Howell et al., 1991). However, all of these notions appear to be
incomparable with our fairness notion for VASSB.

Our model of $\mathsf{VASSB}$ treads the boundary of models that generalize
VASS for which reachability can be proved to be decidable. We note that there
are several closely related models, VASS with a stack (Leroux et al., 2015)
and branching VASS (Verma and Goubault-Larrecq, 2005), for which decidability
of reachability is a long-standing open problem, and others, nested Petri nets
(Lomazova and Schnoebelen, 1999), for which reachability is undecidable.

##  2\. Dynamic Networks of Concurrent Pushdown Systems ($\mathsf{DCPS}$)

###  2.1. Preliminary Definitions

#### Multisets

A _multiset_ $\mathbf{m}\colon S\rightarrow{\mathbb{N}}$ over a set $S$ maps
each element of $S$ to a natural number. Let ${\mathbb{M}[S]}$ be the set of
all multisets over $S$. We treat sets as a special case of multisets where
each element is mapped onto $0$ or $1$. We sometimes write
$\mathbf{m}={[\\![a_{1},a_{1},a_{3}]\\!]}$ for the multiset
$\mathbf{m}\in{\mathbb{M}[S]}$ such that $\mathbf{m}(a_{1})=2$,
$\mathbf{m}(a_{3})=1$, and $\mathbf{m}(a)=0$ for each $a\in
S\backslash{\\{a_{1},a_{3}\\}}$. The empty multiset is denoted $\emptyset$.
The size of a multiset $\mathbf{m}$, denoted $\lvert{\mathbf{m}}\rvert$, is
given by $\sum_{a\in S}\mathbf{m}(a)$. This definition applies to sets as
well.

Given two multisets $\mathbf{m},\mathbf{m}^{\prime}\in{\mathbb{M}[S]}$ we
define $\mathbf{m}+\mathbf{m}^{\prime}\in{\mathbb{M}[S]}$ to be a multiset
such that for all $a\in S$, we have
$(\mathbf{m}+\mathbf{m}^{\prime})(a)=\mathbf{m}(a)+\mathbf{m}^{\prime}(a)$.
For $c\in{\mathbb{N}}$, we define $c\mathbf{m}$ as the multiset that maps each
$a\in S$ to $c\cdot\mathbf{m}(a)$. We also define the natural order $\preceq$
on ${\mathbb{M}[S]}$ as follows: $\mathbf{m}\preceq\mathbf{m}^{\prime}$ iff
there exists $\mathbf{m}^{\Delta}\in{\mathbb{M}[S]}$ such that
$\mathbf{m}+\mathbf{m}^{\Delta}=\mathbf{m}^{\prime}$. We also define
$\mathbf{m}-\mathbf{m}^{\prime}$ for $\mathbf{m}^{\prime}\preceq\mathbf{m}$
analogously: for all $a\in S$, we have
$(\mathbf{m}-\mathbf{m}^{\prime})(a)=\mathbf{m}(a)-\mathbf{m}^{\prime}(a)$.

#### Pushdown Automata

A _pushdown automaton ( $\mathsf{PDA}$)_
$\mathcal{P}_{(g,\gamma)}=(Q,\Sigma,\Gamma,E,q_{0},\gamma_{0},Q_{F})$ consists
of a finite set of _states_ $Q$, a finite input alphabet $\Sigma$, a finite
alphabet of _stack symbols_ $\Gamma$, an _initial state_ $q_{0}\in Q$, an
_initial stack symbol_ $\gamma_{0}\in\Gamma$, a set of _final states_
$Q_{F}\subseteq Q$, and a transition relation
$E\subseteq(Q\times\Gamma)\times\Sigma_{\varepsilon}\times(Q\times\Gamma^{\leq
2})$, where $\Sigma_{\varepsilon}=\Sigma\cup\\{\varepsilon\\}$ and
$\Gamma^{\leq 2}=\\{\varepsilon\\}\cup\Gamma\cup\Gamma^{2}$. For
$((q,\gamma),a,(q^{\prime},w))\in E$ we also write
$q\xrightarrow{a|\gamma/w}q^{\prime}$.

The set of _configurations_ of $\mathcal{P}$ is $Q\times\Gamma^{*}$. The
_initial configuration_ is $(q_{0},\gamma_{0})$. The set of _final
configurations_ is $Q_{F}\times\Gamma^{*}$. For each
$a\in\Sigma\cup\\{\varepsilon\\}$, the relation $\xRightarrow{a}$ on
configurations of $\mathcal{P}$ is defined as follows: $(q,\gamma
w)\xRightarrow{a}(q^{\prime},w^{\prime}w)$ for all $w\in\Gamma^{*}$ iff (1)
there is a transition $q\xrightarrow{a|\gamma/w^{\prime}}q^{\prime}\in E$, or
(2) there is a transition $q\xrightarrow{a|\varepsilon}q^{\prime}\in E$ and
$\gamma=w^{\prime}=\varepsilon$.

For two configurations $c,c^{\prime}$ of $\mathcal{P}$, we write $c\Rightarrow
c^{\prime}$ if $c\xRightarrow{a}c^{\prime}$ for some $a$. Furthermore, we
write $c\xRightarrow{\smash{u}}^{*}c^{\prime}$ for some $u\in\Sigma^{*}$ if
there is a sequence of configurations $c_{0}$ to $c_{n}$ with

$c=c_{0}\xRightarrow{a_{1}}c_{1}\xRightarrow{a_{1}}c_{2}\cdots
c_{n-1}\xRightarrow{a_{n}}c_{n}=c^{\prime},$

such that $a_{1}\ldots a_{n}=u$. We then call this sequence a _run_ of
$\mathcal{P}$ over $u$. We also write $c\Rightarrow^{*}c^{\prime}$ if the word
$u$ does not matter. A run of $\mathcal{P}$ is _accepting_ if $c$ is initial
and $c^{\prime}$ is final. The _language_ accepted by $\mathcal{P}$, denoted
$L(\mathcal{P})$ is the set of words $\in\Sigma^{*}$, over which there is an
accepting run of $\mathcal{P}$.

Given two configurations $c,c^{\prime}$ of $\mathcal{P}$ with
$c\Rightarrow^{*}c^{\prime}$, we say that $c^{\prime}$ is _reachable_ from $c$
and that $c$ is _backwards-reachable_ from $c^{\prime}$. If $c$ is the initial
configuration, we simply say that $c^{\prime}$ is reachable.

#### Parikh Images and Semi-linear Sets

The Parikh image of a word $u\in\Sigma^{*}$ is a function
${\mathsf{Parikh}}(u):\Sigma\rightarrow{\mathbb{N}}$ such that, for every
$a\in\Sigma$, we have ${\mathsf{Parikh}}(u)(a)=|u|_{a}$, where $|u|_{a}$
denotes the number of occurrences of $a$ in $u$. We extend the definition to
the Parikh image of a language $L\subseteq\Sigma^{*}$:
${\mathsf{Parikh}}(L)={\\{{\mathsf{Parikh}}(u)\mid u\in L\\}}$. We associate
the natural isomorphism between ${\mathbb{N}}^{\Sigma}$ and
${\mathbb{N}}^{|\Sigma|}$ and consider the functions as vectors of natural
numbers.

A subset of ${\mathbb{M}[S]}$ is _linear_ if it is of the form
${\\{\mathbf{m}_{0}+t_{1}\mathbf{m}_{1}+\ldots+t_{n}\mathbf{m}_{n}\mid
t_{1},\ldots,t_{n}\in{\mathbb{N}}\\}}$ for some multisets
$\mathbf{m}_{0},\mathbf{m}_{1},\ldots,\mathbf{m}_{n}\in{\mathbb{M}[S]}$. We
call $\mathbf{m}_{0}$ the _base vector_ and
$\mathbf{m}_{1},\ldots,\mathbf{m}_{n}$ the _period vectors_. A linear set has
a finite representation based on its base and period vectors. A _semi-linear_
set is a finite union of linear sets.

###### Theorem 2.1 ((Parikh, 1966)).

For any context-free language $L$, the set ${\mathsf{Parikh}}(L)$ is semi-
linear. A representation of the semi-linear set ${\mathsf{Parikh}}(L)$ can be
effectively constructed from a $\mathsf{PDA}$ for $L$.

###  2.2. Dynamic Networks of Concurrent Pushdown Systems

A _Dynamic Network of Concurrent Pushdown Systems ( $\mathsf{DCPS}$)_
$\mathcal{A}=(G,\Gamma,\Delta,g_{0},\gamma_{0})$ consists of a finite set of
_(global) states_ $G$, a finite alphabet of _stack symbols_ $\Gamma$, an
_initial state_ $g_{0}\in G$, an _initial stack symbol_ $\gamma_{0}\in\Gamma$,
and a finite set of _transition rules_ $\Delta$. The set of transition rules
$\Delta$ is partitioned into four kinds of rules: _creation rules_
${\Delta_{\mathsf{c}}}$, _interruption rules_ ${\Delta_{\mathsf{i}}}$,
_resumption rules_ ${\Delta_{\mathsf{r}}}$, and _termination rules_
${\Delta_{\mathsf{t}}}$. Elements of ${\Delta_{\mathsf{c}}}$ have one of two
forms: (1) $g|\gamma\hookrightarrow g^{\prime}|w^{\prime}$, or (2)
$g|\gamma\hookrightarrow g^{\prime}|w^{\prime}\triangleright\gamma^{\prime}$,
where $g,g^{\prime}\in G$, $\gamma,\gamma^{\prime}\in\Gamma$,
$w^{\prime}\in\Gamma^{*}$, and $|w^{\prime}|\leq 2$. Rules of type (1) allow
the $\mathsf{DCPS}$ to take a single step in one of its threads. Rules of type
(2) additionally spawn a new thread with top of stack $\gamma^{\prime}$.
Elements of ${\Delta_{\mathsf{i}}}$ have the form $g|\gamma\mapsto
g^{\prime}|w^{\prime}$, where $g,g^{\prime}\in G$, $\gamma\in\Gamma$, and
$w^{\prime}\in\Gamma^{*}$ with $1\leq|w^{\prime}|\leq 2$. Elements of
${\Delta_{\mathsf{r}}}$ have the form $g\mapsto g^{\prime}\lhd\gamma$, where
$g,g^{\prime}\in G$ and $\gamma\in\Gamma$. Elements of ${\Delta_{\mathsf{t}}}$
have the form $g\mapsto g^{\prime}$, where $g,g^{\prime}\in G$.

The _size_ $|\mathcal{A}|$ of $\mathcal{A}$ is defined as
$|G|+|\Gamma|+|\Delta|$: the number of symbols needed to describe the global
states, the stack alphabet, and the transition rules.

The set of configurations of $\mathcal{A}$ is
$G\times\big{(}(\Gamma^{*}\times{\mathbb{N}})\cup{\\{\\#\\}}\big{)}\times{\mathbb{M}[\Gamma^{*}\times{\mathbb{N}}]}$.
Given a configuration $\langle g,(w,i),\mathbf{m}\rangle$, we call $g$ the
_(global) state_ , $(w,i)$ the _local configuration_ of the _active thread_ ,
and $\mathbf{m}$ the multiset of the _local configurations_ of the _inactive
threads_. In a configuration $\langle g,\\#,\mathbf{m}\rangle$, we call $\\#$
a _schedule point_.

The initial configuration of $\mathcal{A}$ is $\langle
g_{0},\\#,{[\\![(\gamma_{0},0)]\\!]}\rangle$. For a configuration $c$ of
$\mathcal{A}$, we will sometimes write $c.g$ for the state of $c$ and
$c.\mathbf{m}$ for the multiset of threads of $c$ (both active and inactive).
The _size_ of a configuration $c=\langle g,(w,i),\mathbf{m}\rangle$ is defined
as $|c|=|w|+\sum_{(w^{\prime},j)\in\mathbf{m}}|w^{\prime}|$.

Intuitively, a $\mathsf{DCPS}$ represents a multi-threaded, shared memory
program. The global states $G$ represent the shared memory. Each thread is
potentially recursive. It maintains its own stack $w$ over the stack alphabet
$\Gamma$ and uses the transition rules in ${\Delta_{\mathsf{c}}}$ to
manipulate the global state and its stack. It can additionally spawn new
threads using rules of type (2) in ${\Delta_{\mathsf{c}}}$. In a local
configuration, the natural number $i$ keeps track of how many times a thread
has already been context switched by the underlying scheduler. Any newly
spawned thread has its context switch number set to $0$.

The steps of a single thread defines the following _thread step_ relation
$\rightarrow$ on configurations of $\mathcal{A}$: we have $\langle g,(\gamma
w,i),\mathbf{m}\rangle\rightarrow\langle
g^{\prime},(w^{\prime}w,i),\mathbf{m}^{\prime}\rangle$ for all
$w\in\Gamma^{*}$ iff (1) there is a rule $g|\gamma\hookrightarrow
g^{\prime}|w^{\prime}$ in ${\Delta_{\mathsf{c}}}$ and
$\mathbf{m}^{\prime}=\mathbf{m}$ or (2) there is a rule
$g|\gamma\hookrightarrow g^{\prime}|w^{\prime}\triangleright\gamma^{\prime}$
in ${\Delta_{\mathsf{c}}}$ and
$\mathbf{m}^{\prime}=\mathbf{m}+{[\\![(\gamma^{\prime},0)]\\!]}$. We extend
the _thread step_ relation $\rightarrow^{+}$ to be the irreflexive-transitive
closure of $\rightarrow$; thus $c\rightarrow^{+}c^{\prime}$ if there is a
sequence $c\rightarrow c_{1}\rightarrow\ldots c_{k}\rightarrow c^{\prime}$ for
some $k\geq 0$.

A non-deterministic scheduler switches between concurrent threads. The active
thread is the one currently being executed and the multiset $\mathbf{m}$ keeps
all other partially executed threads in the system. Any spawned thread is put
in $\mathbf{m}$ for future execution with an initial context switch number
$0$. The scheduler may interrupt a thread based on the interruption rules and
non-deterministically resume a thread based on the resumption rules.

The actions of the scheduler define the _scheduler step_ relation $\mapsto$ on
configurations of $\mathcal{A}$:

$\small\inferrule[Swap]{g|\gamma\mapsto
g^{\prime}|w^{\prime}\in{\Delta_{\mathsf{i}}}}{{\langle g,(\gamma
w,i),\mathbf{m}\rangle}\mapsto{\langle
g^{\prime},\\#,\mathbf{m}+{[\\![w^{\prime}w,i+1]\\!]}\rangle}}\;\inferrule[Resume]{g\mapsto
g^{\prime}\lhd\gamma\in{\Delta_{\mathsf{r}}}}{{\langle
g,\\#,\mathbf{m}+{[\\![\gamma w,i]\\!]}\rangle}\mapsto{\langle
g^{\prime},(\gamma w,i),\mathbf{m}\rangle}}\;\inferrule[Term]{g\mapsto
g^{\prime}\in{\Delta_{\mathsf{t}}}}{{\langle
g,(\varepsilon,i),\mathbf{m}\rangle}\mapsto{\langle
g^{\prime},\\#,\mathbf{m}\rangle}}$

If a thread can be interrupted, then Swap swaps it out and increases the
context switch number of the thread. The rule Resume picks a thread that is
ready to run based on the current global state and its top of stack symbol and
makes it active. The rule Term removes a thread on termination (empty stack).

A _run_ of a $\mathsf{DCPS}$ is a finite or infinite sequence of alternating
thread execution and scheduler step relations

$c_{0}\rightarrow^{+}c_{0}^{\prime}\mapsto
c_{1}\rightarrow^{+}c_{1}^{\prime}\mapsto\ldots$

such that $c_{0}$ is the initial configuration. The run is _$K$ -context
switch bounded_ if, moreover, for each $j\geq 0$, the configuration
$c_{j}=(g,(w,i),\mathbf{m})$ satisfies $i\leq K$. In a $K$-context switch
bounded run, each thread is context switched at most $K$ times and the
scheduler never schedules a thread that has already been context switched
$K+1$ times. When the distinction between thread and scheduler steps is not
important, we write a run as a sequence $c_{0}\Rightarrow c_{1}\ldots$.

###  2.3. Identifiers and the Run of a Thread

Our definition of $\mathsf{DCPS}$ does not have thread identifiers associated
with a thread. However, it is convenient to be able to identify the run of a
single thread along the execution. This can be done by decorating local
configurations with unique identifiers and modifying the thread step for
$g|\gamma\hookrightarrow g^{\prime}|w\triangleright\gamma^{\prime}$ to add a
thread $(\ell,\gamma^{\prime},0)$ to the multiset of inactive threads, where
$\ell$ is a fresh identifier. By decorating any run with identifiers, we can
freely talk about the run of a single thread, the multiset of threads spawned
by a thread, etc.

Let us focus on the run of a specific thread, that starts executing from some
global state $g$ with an initial stack symbol $\gamma$. In the course of its
run, the thread updates its own local stack and spawns new threads, but it
also gets swapped out and swapped back in.

We show that the run of a thread corresponds to the run of an associated
$\mathsf{PDA}$ that can be extracted from $\mathcal{A}$. This $\mathsf{PDA}$
updates the global state and the stack based on the rules in
${\Delta_{\mathsf{c}}}$, but additionally (1) makes visible as the input
alphabet the initial symbols (from $\Gamma$) of the spawned threads, and (2)
non-deterministically guesses jumps between global states corresponding to the
effect of context switches. There are two kinds of jumps. A jump
$(g_{1},\gamma,g_{2})$ in the $\mathsf{PDA}$ corresponds to the thread being
switched out leading to global state $g_{1}$ and later resuming at global
state $g_{2}$ with $\gamma$ on top of its stack (without being active in the
interim). A jump $(g,\bot)$ corresponds to the last time the $\mathsf{PDA}$ is
swapped out (leading to global state $g$). We also make these guessed jumps
visible as part of the input alphabet. Thus, the input alphabet of the
$\mathsf{PDA}$ is $\Gamma\cup G\times\Gamma\times G\cup G\times{\\{\bot\\}}$.

For any $g\in G$ and $\gamma\in\Gamma$, we define the $\mathsf{PDA}$
$\mathcal{P}_{(g,\gamma)}=(Q,\Sigma,\Gamma_{\bot},E,\mathsf{init},\bot,{\\{\mathsf{init},\mathsf{end}\\}})$,
where $Q=G\cup G\times\Gamma\cup{\\{\mathsf{init},\mathsf{end}\\}}$,
$\Gamma_{\bot}$ = $\Gamma\cup{\\{\bot\\}}$, $\Sigma=\Gamma\cup
G\times\Gamma\times G\cup G\times{\\{\bot\\}}$, $E$ is the smallest transition
relation such that

  1. (1)

There is a transition
$\mathsf{init}\xrightarrow{\varepsilon|\bot/\gamma\bot}g$ in $E$,

  2. (2)

For every $g_{1}|\gamma_{1}\hookrightarrow g_{2}|w\in\Delta_{\mathsf{c}}$
there is a transition $g_{1}\xrightarrow{\varepsilon|\gamma_{1}/w}g_{2}$ in
$E$,

  3. (3)

For every $g_{1}|\gamma_{1}\hookrightarrow
g_{2}|w\triangleright\gamma_{2}\in\Delta_{\mathsf{c}}$ there is a transition
$g_{1}\xrightarrow{\gamma_{2}|\gamma_{1}/w}g_{2}$ in $E$,

  4. (4)

For every $g_{1}|\gamma_{1}\hookrightarrow g_{2}|w\in\Delta_{\mathsf{i}}$,
$g_{3}\in G$, and $\gamma_{2}\in\Gamma$ there is a transition
$g_{1}\xrightarrow{(g_{2},\gamma_{2},g_{3})|\gamma_{1}/w}(g_{3},\gamma_{2})$,
and a transition
$(g_{3},\gamma_{2})\xrightarrow{\varepsilon|\gamma_{2}/\gamma_{2}}g_{3}$ in
$E$,

  5. (5)

For every $g_{1}|\gamma_{1}\hookrightarrow g_{2}|w\in\Delta_{\mathsf{i}}$ and
every $\gamma_{2}\in\Gamma_{\bot}$ there is a transition
$g_{1}\xrightarrow{\varepsilon|\gamma_{1}/w}(g_{2},\bot)$, and a transition
$(g_{2},\bot)\xrightarrow{(g_{2},\bot)|\gamma_{2}/\gamma_{2}}\mathsf{end}$ in
$E$,

  6. (6)

For every $g_{1}\hookrightarrow g_{2}\in{\Delta_{\mathsf{t}}}$ there is a
transition $g_{1}\xrightarrow{(g_{2},\bot)|\bot/\bot}\mathsf{end}$ in $E$.

The set of behaviors of the $\mathsf{PDA}$ $\mathcal{P}_{(g,\gamma)}$ which
correspond to a thread execution with precisely $i$ ($i\leq K+1$) context
switches is given by the following language:

$L^{(i)}_{(g,\gamma)}=L(\mathcal{P}_{(g,\gamma)})\cap((\Gamma^{*}\cdot
G\times\Gamma\times G)^{i-1}(\Gamma^{*}\cdot G\times{\\{\bot\\}}))\ $

The language $L^{(i)}_{(g,\gamma)}$ is a context-free language. In the
definition, we use the end of stack symbol $\bot$ to recognize when the stack
is empty.

###  2.4. Decision Problems and Main Results

#### Previous Work: Safety

The _reachability problem_ for $\mathsf{DCPS}$ asks, given a global state $g$
of $\mathcal{A}$, if there is a run $c_{0}\Rightarrow c_{1}\ldots\Rightarrow
c_{n}$ such that $c_{n}.g=g$. It is well-known that reachability is
undecidable (e.g., one can reduce the emptiness problem for intersection of
context free languages). Therefore, it is customary to consider _context-
switch bounded_ decision questions. Given $K\in{\mathbb{N}}$, a state $g$ of
$\mathcal{A}$ is $K$-context switch bounded reachable if there is a
$K$-context switch bounded run $c_{0}\Rightarrow\ldots\Rightarrow c_{n}$ with
$c_{n}.g=g$. For a fixed $K$, the _$K$ -bounded state reachability problem_
($\mathsf{SRP}[K]$) for a $\mathsf{DCPS}$ is defined as follows:

Given:

A $\mathsf{DCPS}$ $\mathcal{A}$ and a global state $g$

Question:

Is $g$ $K$-context switch bounded reachable in $\mathcal{A}$?

This problem is known to be decidable; the ${\mathsf{2EXPSPACE}}$ upper bound
for each $K$ was proved by Atig et al. (2009) and a matching lower bound for
$K\geq 1$ by Baumann et al. (2020). In case $K=0$, the problem is known to be
${\mathsf{EXPSPACE}}$-complete (Ganty and Majumdar, 2012).

#### This Paper: Liveness

We now turn to context-bounded liveness specifications. The simplest liveness
specification is _(non-)termination_ : does a program halt? For a fixed
$K\in{\mathbb{N}}$, the _$K$ -bounded non-termination problem_
$\mathsf{NTERM}[K]$ is defined as follows:

Given:

A $\mathsf{DCPS}$ $\mathcal{A}$.

Question:

Is there an infinite $K$-context switch bounded run?

When $K=0$, the non-termination problem is known to be
${\mathsf{EXPSPACE}}$-complete (Ganty and Majumdar, 2012). We show the
following result.

###### Theorem 2.2 (Termination).

For each $K\geq 1$, the problem $\mathsf{NTERM}[K]$ is
${\mathsf{2EXPSPACE}}$-complete.

#### Fairness

An infinite run is _fair_ if, intuitively, any thread that can be executed is
eventually executed by the scheduler. Fairness is used as a way to rule out
non-termination due to uninteresting scheduler choices.

We say a thread $t=(\gamma w,i)$ is _ready_ at a configuration
$c=(g,\\#,\mathbf{m})$ if $t\in\mathbf{m}$ and there is some rule $g\mapsto
g^{\prime}\lhd\gamma$ in ${\Delta_{\mathsf{r}}}$. A thread $t$ is _scheduled_
at $c$ if the scheduler step makes $t$ the active thread. A run is unfair to
thread $t$ if it is ready infinitely often but never scheduled. A _fair_ run
$\rho$ is one which is not unfair to any thread. Restricting our attention to
$K$-context switch bounded runs gives us the corresponding notion of fair
$K$-context switch bounded runs.

For fixed $K\in{\mathbb{N}}$, the _$K$ -context bounded fair non-termination
problem_ $\mathsf{FNTERM}[K]$ asks:

Given:

A $\mathsf{DCPS}$ $\mathcal{A}$.

Question:

Is there an infinite, fair $K$-context switch bounded run?

Note that since our model does not have individual thread identifiers,
fairness is defined only over equivalence classes of threads that have the
same stack $w$ and the same context switch number $i$. The reason for our
taking into account stacks and context switch numbers is the following. It is
a simple observation that there exists an infinite fair run in our sense if
and only if there exists a run in the corresponding system _with thread
identifiers_ –that is fair to each individual thread. This is because an
angelic scheduler could always pick the earliest spawned thread among those
with the same stack and context switch number. Therefore, our results allow us
to reason about multi-threaded systems with identifiers.

This raises the question of whether there are runs that are fair in our sense,
but where a non-angelic scheduler would still yield unfairness for some thread
identity. In other words, is it possible that a fair run _starves_ a specific
thread. For example, consider a program in which the main thread spawns two
copies of a thread $\mathtt{foo}$. Each thread $\mathtt{foo}$, when scheduled,
simply spawns another copy of $\mathtt{foo}$ and terminates. Here is a fair
run of the program (we omit the global state as it is not relevant), where we
have decorated the threads with identifiers:

$\displaystyle(\\#,{[\\![(\mathtt{main},0)^{0}]\\!]})\xRightarrow{*}$
$\displaystyle((\mathtt{main},0)^{0},{[\\![]\\!]})\xRightarrow{*}(\\#,{[\\![(\mathtt{foo},0)^{1},(\mathtt{foo},0)^{2}]\\!]})\xRightarrow{*}((\mathtt{foo},0)^{2},{[\\![(\mathtt{foo},0)^{1}]\\!]})\xRightarrow{*}$
$\displaystyle(\\#,{[\\![(\mathtt{foo},0)^{1},(\mathtt{foo},0)^{3}]\\!]})\xRightarrow{*}((\mathtt{foo},0)^{3},{[\\![(\mathtt{foo},0)^{1}]\\!]})\xRightarrow{*}\ldots$

The run is fair, but a specific thread marked with identifier $1$ is never
picked.

Formally, a thread $t=(w,i)$ is _starved_ in an infinite fair run
$\rho=c_{0}\Rightarrow c_{1}\Rightarrow\ldots$ iff there is some $j$ such that
$c_{i}.\mathbf{m}(t)\geq 1$ for all $i\geq j$ and whenever $t$ is resumed at
$c_{k}$ for $k\geq j$, we have $c.\mathbf{m}(t)\geq 2$.

For fixed $K\in{\mathbb{N}}$, the _$K$ -bounded fair starvation problem_
$\mathsf{STARV}[K]$ is defined as follows:

Given:

A $\mathsf{DCPS}$ $\mathcal{A}$.

Question:

Is there an infinite, fair $K$-context switch bounded run that starves some
thread?

We show the following results.

###### Theorem 2.3 (Fair Non-Termination).

For each $K\in{\mathbb{N}}$, the problem $\mathsf{FNTERM}[K]$ is decidable.

###### Theorem 2.4 (Fair Starvation).

For each $K\in{\mathbb{N}}$, the problem $\mathsf{STARV}[K]$ is decidable.

Previously, decidability results were only known when $K=0$ (Ganty and
Majumdar, 2012). Recall that a decision problem is _nonelementary_ if it is
not in $\bigcup_{k\geq 0}k\mathchar 45\relax\mathsf{EXPTIME}$. Our algorithms
are nonelementary: they involve an (elementary) reduction to the reachability
problem for vector addition systems with states (VASS). This is unavoidable:
already for $K=0$, the fair non-termination and fair starvation problems are
non-elementary, because there is a reduction from the reachability problem for
VASS (Ganty and Majumdar, 2012), which is non-elementary (Czerwinski et al.,
2019).

In the rest of the paper, we prove Theorems 2.2, 2.3, and 2.4.

##  3\. Warm-Up: Non-termination

In this section, we prove Theorem 2.2. The theorem follows easily from
previous results for safety verification (Atig et al., 2011; Baumann et al.,
2020). We recall the main ideas as a step toward the more complex proof for
_fair_ termination.

### Downward Closures: From $\mathsf{DCPS}$ to $\mathsf{DCFS}$

A $\mathsf{DCPS}$ $\mathcal{A}=(G,\Gamma,\Delta,g_{0},\gamma_{0})$ is called a
dynamic network of concurrent _finite_ systems ($\mathsf{DCFS}$) if in each
transition rule in ${\Delta_{\mathsf{c}}}\cup{\Delta_{\mathsf{i}}}$, we have
$|w^{\prime}|\leq 1$. Intuitively, a $\mathsf{DCFS}$ corresponds to the
special case where each thread is a finite-state process (and each stack is
bounded by $1$).

We reduce the $K$-bounded non-termination problem for $\mathsf{DCPS}$ to the
non-termination problem for $\mathsf{DCFS}$. Fix $K\in{\mathbb{N}}$ and a
$\mathsf{DCPS}$ $\mathcal{A}=(G,\Gamma,\Delta,g_{0},\gamma_{0})$. The crucial
observation of Atig et al. (2011) is that answer to the $K$-bounded
reachability problem remains unchanged if we allow threads to “drop” some
spawned threads. That is, for every $g|\gamma\hookrightarrow
g^{\prime}|w^{\prime}\triangleright\gamma^{\prime}$, we also add the rule
$g|\gamma\hookrightarrow g^{\prime}|w^{\prime}$ to $\Delta_{\mathsf{c}}$.
Informally, the “forgotten” spawned thread $\gamma^{\prime}$ is never
scheduled. Clearly, a global state is reachable in the original
$\mathsf{DCPS}$ iff it is reachable in the new $\mathsf{DCPS}$.

We observe that this transformation also preserves non-termination: if there
is a ($K$-bounded) non-terminating run in the original $\mathsf{DCPS}$, there
is one in the new one.

The ability to forget spawned tasks allows us to transform the language
$L^{(i)}_{(g,\gamma)}$ of each thread into a _regular_ language by taking
_downward closures_.

We need some definitions. For any alphabet $\Sigma$, define the subword
relation $\sqsubseteq\subseteq\Sigma^{*}\times\Sigma^{*}$ as follows: for
every $u,v\in\Sigma^{*}$, we have $u\sqsubseteq v$ iff $u$ can be obtained
from $v$ by deleting some letters from $v$. For example, $acbba\sqsubseteq
bacbacbac$ but $abba\not\sqsubseteq baba$. The downward closure
$w\mathord{\downarrow}$ with respect to the subword order of a word
$w\in\Sigma^{*}$ is defined as
$w\mathord{\downarrow}:=\\{w^{\prime}\in\Sigma^{*}\mid w^{\prime}\sqsubseteq
w\\}$. The downward closure $L\mathord{\downarrow}$ of a language
$L\subseteq\Sigma^{*}$ is given by
$L\mathord{\downarrow}:=\\{w^{\prime}\in\Sigma^{*}\mid\exists w\in L\colon
w^{\prime}\sqsubseteq w\\}$. Recall that the downward closure
$L\mathord{\downarrow}$ of any language $L$ is a regular language (Haines,
1969). Moreover, a finite automaton accepting the downward closure of a
context-free language can be effectively constructed (Courcelle, 1991). The
size of the resulting automaton is at most exponential in the size of the
$\mathsf{PDA}$ for the context-free language (Bachmeier et al., 2015).

Now consider the following language:

$\hat{L}_{(g,\gamma)}=\bigcup_{i=1}^{K+1}\bigg{(}L^{(i)}_{(g,\gamma)}\mathord{\downarrow}\cap\Big{(}\big{(}\Gamma^{*}\cdot(G\times\Gamma\times
G)\big{)}^{i-1}(\Gamma^{*}\cdot G\times{\\{\bot\\}})\Big{)}\bigg{)}$

This language is regular and can be effectively constructed from the
$\mathsf{PDA}$ $\mathcal{P}_{(g,\gamma)}$. It accepts all behaviors of a
thread that is context switched at most $K+1$ times such that, by adding
additional spawned tasks, one gets back a run of the original thread in
$\mathcal{A}$.

The $\mathsf{DCFS}$ simulates the downward closure of the $\mathsf{DCPS}$ by
simulating the composition of the automata for each downward closure. The
construction is identical to (Atig et al., 2011, Lemma 5.3). Thus, we can
conclude with the following lemma.

###### Lemma 3.1.

The $K$-bounded non-termination problem for $\mathsf{DCPS}$ can be reduced in
exponential time to the non-termination problem for $\mathsf{DCFS}$. The
resulting $\mathsf{DCFS}$ is of size at most exponential in the size of the
$\mathsf{DCPS}$.

### From $\mathsf{DCFS}$ Non-Termination to $\mathsf{VASS}$ Non-Termination

A _vector addition system with states_ ($\mathsf{VASS}$) is a tuple
$V=(Q,P,E)$ where $Q$ is a finite set of _states_ , $P$ is a finite set of
_places_ , and $E$ is a finite set of edges of the form
$q\xrightarrow{\delta}q^{\prime}$ where $\delta\in{\mathbb{Z}}^{P}$. A
_configuration_ of the $\mathsf{VASS}$ is a pair $(q,u)\in
Q\times{\mathbb{M}[P]}$. The edges in $E$ induce a transition relation on
configurations: there is a transition
$(q,u)\xrightarrow{\delta}(q^{\prime},u^{\prime})$ if there is an edge
$q\xrightarrow{\delta}q^{\prime}$ in $E$ such that
$u^{\prime}(p)=u(p)+\delta(p)$ for all $p\in P$. A _run_ of the
$\mathsf{VASS}$ is a finite or infinite sequence of configurations
$c_{0}\xrightarrow{\delta_{0}}c_{1}\xrightarrow{\delta_{1}}\ldots$. The _non-
termination_ problem for $\mathsf{VASS}$ asks, given a $\mathsf{VASS}$ and an
initial configuration $c_{0}$, is there an infinite run starting from $c_{0}$.

###### Lemma 3.2.

The $K$-context bounded non-termination problem for $\mathsf{DCFS}$ can be
reduced in polynomial time to non-termination problem for $\mathsf{VASS}$.

###### Proof.

Let $\mathcal{A}=(G,\Gamma,\delta,g_{0},\gamma_{0})$ be a $\mathsf{DCFS}$. We
define a $\mathsf{VASS}$
$V(\mathcal{A})=(G\times(\Gamma\times{\\{0,\ldots,K\\}}\cup{\\{\\#\\}}),(\Gamma\cup{\\{\varepsilon\\}})\times{\\{0,\ldots,K+1\\}},E)$.
Intuitively, a configuration $((g,\gamma,i),u)$ of the $\mathsf{VASS}$
represents a configuration of the $\mathsf{DCFS}$ where the global state is
$g$, the active thread has stack $\gamma$ and has been previously context
switched $i$ times, and for each $\gamma^{\prime}\in\Gamma$ and
$i\in{\\{0,\ldots,K+1\\}}$, the value $u(\gamma^{\prime},i)$ represents the
number of pending threads with stack $\gamma^{\prime}$ which have each been
context switched $i$ times. A global state $(g,\\#)$ indicates a state where
the scheduler picks a new thread. The edges in $E$ update the configurations
to simulate the steps of the $\mathsf{DCFS}$.

For each transition $g|\gamma\hookrightarrow
g^{\prime}|\gamma^{\prime}\in{\Delta_{\mathsf{c}}}$ and for each
$i\in{\\{0,\ldots,K\\}}$, the $\mathsf{VASS}$ has a transition that changes
$(g,\gamma,i)$ to $(g^{\prime},\gamma^{\prime},i)$. For each transition
$g|\gamma\hookrightarrow
g^{\prime}|\gamma^{\prime}\triangleright\gamma^{\prime\prime}\in{\Delta_{\mathsf{c}}}$
and for each $i\in{\\{0,\ldots,K\\}}$, the $\mathsf{VASS}$ has a transition
that changes $(g,\gamma,i)$ to $(g^{\prime},\gamma^{\prime},i)$ and puts a
token in $(\gamma^{\prime\prime},0)$. For each transition $g|\gamma\mapsto
g^{\prime}|\gamma^{\prime}\in{\Delta_{\mathsf{i}}}$ and for each
$i\in{\\{0,\ldots,K\\}}$, the $\mathsf{VASS}$ has a transition that changes
$g$ to $(g^{\prime},\\#)$ while putting a token into $(\gamma^{\prime},i+1)$.
For each $g\mapsto g^{\prime}\lhd\gamma\in{\Delta_{\mathsf{r}}}$, there is a
transition $(g,\\#)$ to $(g^{\prime},\gamma,i)$ that takes a token from
$(\gamma,i)$. For each $g\mapsto g^{\prime}\in{\Delta_{\mathsf{t}}}$, there is
a transition $(g,\varepsilon,i)$ to $(g^{\prime},\\#)$.

Clearly, there is a bijection between the runs of $\mathcal{A}$ and the runs
of the $\mathsf{VASS}$ from $((g_{0},\\#),{[\\![\gamma_{0},0]\\!]})$. Thus,
there is an infinite run in $\mathcal{A}$ iff there is an infinite run in
$V(\mathcal{A})$ from $((g_{0},\\#),{[\\![\gamma_{0},0]\\!]})$.

### Proof of Theorem 2.2

The ${\mathsf{2EXPSPACE}}$ upper bound follows by combining Lemmas 3.1, 3.2,
and the ${\mathsf{EXPSPACE}}$ upper bound for the non-termination problem for
$\mathsf{VASS}$ (Rackoff, 1978).

The ${\mathsf{2EXPSPACE}}$ lower bound follows from the observation made
already in (Baumann et al., 2020) that the ${\mathsf{2EXPSPACE}}$-hardness of
$K$-bounded reachability already holds for _terminating_ $\mathsf{DCPS}$, in
which every run is terminating. It is now a simple reduction to take an
instance of the $K$-bounded state reachability problem for a terminating
$\mathsf{DCPS}$ and add a “gadget” that produces an infinite run whenever the
target global state is reached.

##  4\. Fair Non-Termination

We now turn to proving Theorem 2.3. Unfortunately, fair termination is not
preserved under downward closure. The example in Section 1 has no fair
infinite run, since eventually (under fairness), bit is set to $1$ by the
instance of bar and the program terminates. However, the downward closure that
omits bar has a fair infinite run. Thus, we cannot replace the $\mathsf{PDA}$s
for each thread with finite-state automata and there is no obvious reduction
to $\mathsf{VASS}$.

Our proof is more complicated. First, we introduce an extension, VASS with
_balloons_ ($\mathsf{VASSB}$), of $\mathsf{VASS}$ (Section 4.1). A
$\mathsf{VASSB}$ extends a $\mathsf{VASS}$ with balloon states and balloon
places, and allows keeping multisets of state-vector pairs over balloons. We
can use this additional power to store spawned threads. As we shall see
(Section 4.2), we can reduce $\mathsf{DCPS}$ to $\mathsf{VASSB}$. Later, we
shall show decidability of fair infinite behaviors for $\mathsf{VASSB}$,
completing the proof.

###  4.1. VASS with Balloons

A _VASS with balloons_ ($\mathsf{VASSB}$) is a tuple
$\mathcal{V}=(Q,P,\Omega,\Phi,E)$, where $Q$ is a finite set of _states_ , $P$
is a finite set of _places_ , $\Omega$ is a finite set of _balloon states_ ,
$\Phi$ is a finite set of _balloon places_ , and $E$ is a finite set of edges
of the form $q\xrightarrow{\mathit{op}}q^{\prime}$, where $\mathit{op}$ is one
of a finite set $\mathsf{OP}$ of operations of the following form:

  1. (1)

$\mathit{op}=\delta$ with $\delta\in{\mathbb{Z}}^{P}$,

  2. (2)

$\mathit{op}=\mathsf{inflate}(\sigma,S)$, where $\sigma\in\Omega$ and
$S\subseteq{\mathbb{N}}^{\Phi}$ is a semi-linear subset of
${\mathbb{N}}^{\Phi}$.

  3. (3)

$\mathit{op}=\mathsf{deflate}(\sigma,\sigma^{\prime},\pi,p)$, where
$\sigma,\sigma^{\prime}\in\Omega$, $\pi\in\Phi$, $p\in P$.

  4. (4)

$\mathit{op}=\mathsf{burst}(\sigma)$, where $\sigma\in\Omega$.

A _configuration_ of a $\mathsf{VASSB}$ is an element of
$Q\times{\mathbb{M}[P]}\times{\mathbb{M}[\Omega\times{\mathbb{M}[\Phi]}]}$.
That is, a configuration $c=(q,\mathbf{m},\mathbf{n})$ consists of a state
$q\in Q$, a multiset $\mathbf{m}\in{\mathbb{M}[P]}$, and a multiset
$\mathbf{n}\in{\mathbb{M}[\Omega\times{\mathbb{M}[\Phi]}]}$ of _balloons_. We
assume $\mathbf{n}$ has finite support. A _semiconfiguration_ is a
configuration $(q,\mathbf{m},\emptyset)$. For semiconfigurations, we simply
write $(q,\mathbf{m})\in Q\times{\mathbb{M}[P]}$. For a configuration $c$, we
write $c.q$, $c.\mathbf{m}$, and $c.\mathbf{n}$ to denote the components of
$c$. For a balloon $b\in\Omega\times{\mathbb{M}[\Phi]}$, we write $b.\sigma$
and $b.\mathbf{k}$ to indicate its balloon state and contents respectively and
write $c.\mathbf{n}(b)$ for the number of balloons $b$ in $c$.

The edges in $E$ define a transition relation on configurations. For an edge
$q\xrightarrow{\mathit{op}}q^{\prime}$, and configurations
$c=(q,\mathbf{m},\mathbf{n})$ and
$c^{\prime}=(q^{\prime},\mathbf{m}^{\prime},\mathbf{n}^{\prime})$, we define
$c\xrightarrow{\mathit{op}}c^{\prime}$ iff one of the following is true:

  1. (1)

If $\mathit{op}=\delta\in{\mathbb{Z}}^{P}$ and
$\mathbf{m}^{\prime}=\mathbf{m}+\delta$ and $\mathbf{n}^{\prime}=\mathbf{n}$.

  2. (2)

If $\mathit{op}=\mathsf{inflate}(\sigma,S)$ and
$\mathbf{m}^{\prime}=\mathbf{m}$ and
$\mathbf{n}^{\prime}=\mathbf{n}+{[\\![(\sigma,\mathbf{k})]\\!]}$ for some
$\mathbf{k}\in S$. That is, we create a new balloon with state $\sigma$ and
multiset $\mathbf{k}$ for some $\mathbf{k}\in S$.

  3. (3)

If $\mathit{op}=\mathsf{deflate}(\sigma,\sigma^{\prime},\pi,p)$ and there is a
balloon $b=(\sigma,\mathbf{k})\in\Omega\times{\mathbb{M}[\Phi]}$ with
$\mathbf{n}(b)\geq 1$ and
$\mathbf{m}^{\prime}=\mathbf{m}+\mathbf{k}(\pi)\cdot{[\\![p]\\!]}$ and
$\mathbf{n}^{\prime}=(\mathbf{n}-{[\\![b]\\!]})+{[\\![(\sigma^{\prime},\mathbf{k}^{\prime})]\\!]}$,
where $\mathbf{k}^{\prime}(\pi)=0$ and
$\mathbf{k}^{\prime}(\pi^{\prime})=\mathbf{k}(\pi^{\prime})$ for all
$\pi^{\prime}\in\Phi\setminus{\\{\pi\\}}$. That is, we pick a balloon
$(\sigma,\mathbf{k})$ from $\mathbf{n}$, transfer the contents in place $\pi$
from $\mathbf{k}$ to place $p$ in $\mathbf{m}$, and update the balloon state
$\sigma$ to $\sigma^{\prime}$. Here we say the balloon $(\sigma,\mathbf{k})$
was _deflated_.

  4. (4)

If $\mathit{op}=\mathsf{burst}(\sigma)$ and there is a balloon
$b=(\sigma,\mathbf{k})\in\Omega\times{\mathbb{M}[\Phi]}$ with
$\mathbf{n}(b)\geq 1$ and $\mathbf{m}^{\prime}=\mathbf{m}$ and
$\mathbf{n}^{\prime}=\mathbf{n}-{[\\![b]\\!]}$. This means we pick some
balloon $b$ with state $\sigma$ from our multiset $\mathbf{n}$ of balloons and
remove it, making any tokens still contained in its balloon places disappear
as well. Here we say the balloon $b$ is _burst_.

The edge set $E$ is the disjoint union of the sets $E_{p},E_{n},E_{d},E_{b}$
which stand for the edges with operations from (1),(2),(3),(4) respectively.
We write $c\xrightarrow{}c^{\prime}$ if $c\xrightarrow{\mathit{op}}c^{\prime}$
for some edge $q\xrightarrow{\mathit{op}}q^{\prime}$ in $E$. A _run_
$\rho=c_{0}\xrightarrow{\mathit{op}_{0}}c_{1}\xrightarrow{\mathit{op}_{1}}c_{2}\xrightarrow{\mathit{op}_{2}}\cdots$
is a finite or infinite sequence of configurations. The size of
$\mathcal{V}=(Q,P,\Omega,\Phi,E)$ is given by
$|\mathcal{V}|=|Q|+|P|+|\Omega|+|\Phi|+|E|$.

An infinite run $\rho$ is _progressive_ iff the following holds:

  1. (1)

For every configuration $c_{i}=(q_{i},\mathbf{m}_{i},\mathbf{n}_{i})$ and
every balloon $b=(\sigma,\mathbf{k})\in\Omega\times{\mathbb{M}[\Phi]}$ with
$\mathbf{n}_{i}(b)\geq 1$ there is a $c_{j}$, $j>i$, such that
$\mathit{op}_{j}$ either bursts or deflates $b$.

  2. (2)

Moreover, for every configuration
$c_{i}=(q_{i},\mathbf{m}_{i},\mathbf{n}_{i})$ and every place $p\in P$ with
$\mathbf{m}_{i}(p)\geq 1$ there is a $c_{j}$, $j>i$, such that a token is
removed from $p$; that is, $\mathit{op}_{j}\equiv\delta$ with $\delta(p)<0$.

We define the balloon-norm of a configuration $c=(q,\mathbf{m},\mathbf{n})$ as
${|\\!|c|\\!|}=\mathsf{max}{\\{\sum_{p\in\Phi}\mathbf{k}(p)\mid\exists\sigma\;\mathbf{n}(\sigma,\mathbf{k})>0\\}}$.
A progressive run is _shallow_ if there is a number $B\in{\mathbb{N}}$ such
that ${|\\!|c_{j}|\\!|}\leq B$ for all $j\geq 0$. In other words, shallowness
of a run means that each balloon in every configuration on the run contains at
most $B$ tokens in the balloon places. Note that this does not mean the size
of the configurations become bounded: the number of balloons and the number of
tokens in $P$ can still be unbounded.

The _progressive run problem for $\mathsf{VASSB}$_ is the following:

Given:

A $\mathsf{VASSB}$ $\mathcal{V}=(Q,P,\Omega,\Phi,E)$ and an initial
semiconfiguration $c_{0}$.

Question:

Does $\mathcal{V}$ have an infinite progressive run starting from $c_{0}$?

In Section 5, we shall prove the following theorems.

###### Theorem 4.1.

The progressive run problem for $\mathsf{VASSB}$ is decidable.

The following is a by-product of the proof of Theorem 4.1, which will be used
in Section 6.

###### Theorem 4.2.

A $\mathsf{VASSB}$ $\mathcal{V}$ has a progressive run iff it has a shallow
progressive run.

###  4.2. From $\mathsf{DCPS}$ to $\mathsf{VASSB}$

Instead of reducing fairness for $\mathsf{DCPS}$ to $\mathsf{VASSB}$, we would
like to use a stronger notion, which simplifies many of our proofs. To this
end, we introduce the notion of progressiveness that we already defined for
$\mathsf{VASSB}$ now for $\mathsf{DCPS}$ as well: given a bound
$K\in{\mathbb{N}}$, an infinite run $\rho$ of a $\mathsf{DCPS}$ is called
_progressive_ if the rule Term is only ever applied when the active thread is
at $K$ context switches, and for every local configuration $(w,i)$ of an
inactive thread in a configuration of $\rho$, there is a future point in
$\rho$ where the rule Resume is applied to $(w,i)$, making it the local
configuration of the active thread.

Intuitively, no type of thread can stay around infinitely long in a
progressive run without being resumed, and every thread that terminates does
so after exactly $K$ context switches. Note that progressiveness is a stronger
condition than fairness, because it does not allow threads to “get stuck” or
go above the context switch bound $K$. However, we can always transform a
$\mathsf{DCPS}$ where we want to consider fair runs into one where we can
consider progressive runs instead. The transformation is formalized by the
following lemma.

###### Lemma 4.3.

Given a bound $K\in{\mathbb{N}}$ and a $\mathsf{DCPS}$ $\mathcal{A}$, we can
construct a $\mathsf{DCPS}$ $\widetilde{\mathcal{A}}$ such that:

  * •

$\mathcal{A}$ has an infinite fair $K$-context switch bounded run iff
$\widetilde{\mathcal{A}}$ has an infinite progressive $K$-context switch
bounded run.

  * •

$\mathcal{A}$ has an infinite fair $K$-context switch bounded run that starves
a thread iff $\widetilde{\mathcal{A}}$ has an infinite progressive $K$-context
switch bounded run that starves a thread.

#### Idea

To prove Lemma 4.3 we modify the $\mathsf{DCPS}$ $\mathcal{A}$ by giving every
thread a bottom of stack symbol $\bot$ and saving its context switch number in
its top of stack symbol. We also save this number in the global state whenever
a thread is active. This way we can still swap a thread out and back in again
once it has emptied its stack, and we also can keep track of how often we need
to repeat that, before we reach $K$ context switches and allow it to
terminate.

Furthermore, we also keep a subset $G^{\prime}$ of the global states of
$\mathcal{A}$ in our new global states, which restricts the states that can
appear when no thread is active. This way we can guess that a thread will be
“stuck” in the future, upon which we terminate it instead (going up to $K$
context switches first) and also spawn a new thread keeping track of its top
of stack symbol in the bag. Then later we restrict the subset $G^{\prime}$ to
only those global states that do not have Resume rules for the top of stack
symbols we saved in the bag. This then verifies our guess of “being stuck”.
The second part of the lemma is used in Section 6, where we reason about
starvation.

We now state the main reduction to $\mathsf{VASSB}$.

###### Theorem 4.4.

Given a bound $K\in{\mathbb{N}}$ and a $\mathsf{DCPS}$ $\mathcal{A}$ we can
construct a $\mathsf{VASSB}$ $\mathcal{V}$ with a state $q_{0}$ such that
$\mathcal{A}$ has an infinite progressive $K$-context switch bounded run iff
$\mathcal{V}$ has an infinite progressive run from
$(q_{0},\emptyset,\emptyset)$.

#### Idea

One of the main insights regarding the behavior of $\mathsf{DCPS}$ is that the
order of the spawns of a thread during one round of being active does not
matter. None of the spawned threads during one such segment can influence the
run until the active thread changes. Thus we only need to look at the semi-
linear Parikh image of the language of spawns for each segment. One can then
identify a thread with the state changes and spawns it makes during segments
$0$ through $K$. The state changes can be stored in a balloon state and the
spawns for each segment in balloon places that correspond to $K+1$ copies of
the stack alphabet. The inflate operation then basically guesses the exact
multiset of spawns of the corresponding thread.

Representing threads by balloons in this way does not keep track of stack
contents, which was important for ensuring the progressiveness of a
$\mathsf{DCPS}$ run. However, starting from a progressive $\mathsf{DCPS}$ run
we can always construct a progressive run for the $\mathsf{VASSB}$ by always
continuing with the oldest thread in a configuration if given multiple
choices, and then building the balloons accordingly. Always picking the oldest
balloon also works for the reverse direction.

Now let us argue about the construction in more detail. Given a
$\mathsf{DCPS}$ with stack alphabet $\Gamma$ and a context switch bound $K$,
construct a $\mathsf{VASSB}$ whose configurations mirror the ones of the
$\mathsf{DCPS}$ in the following way. The set of places is $\Gamma$ and it is
used to capture threads that have not been scheduled yet and therefore only
carry a single stack symbol. Formally each thread with context switch number
$0$ and stack content $\gamma\in\Gamma$ is represented by a token on place
$\gamma$. The set of balloon places is $\Gamma\times\\{0,\ldots,K\\}$ and they
are supposed to carry the future spawns of any given thread during segments
$0$ to $K$. Every thread $t$ with context switch number $\geq 1$ is then
represented by a balloon where the number of tokens on balloon place
$(\gamma,i)$ is equal to the number of threads with stack content $\gamma$
that $t$ will spawn during its $i$th segment. The spawns for segment $0$ are
transferred to the place set $\Gamma$ immediately after such a balloon is
created, since the represented thread is now supposed to have made its first
context switch. Furthermore, each balloon state consists of the context switch
sequence and context switch number of its corresponding thread $t$. The set of
states of the $\mathsf{VASSB}$ mirrors the global states of the
$\mathsf{DCPS}$.

For this idea to work, we need to compute the semi-linear set of spawns that
each type of thread can make, so that we can correctly inflate the
corresponding balloon using this set. Here, the _type_ of a terminating thread
consists of the stack symbol $\gamma$ it spawns with, the global state $g$ in
which it first becomes active, the sequence of context switches it makes, and
the state in which it terminates. Given a $\mathsf{DCPS}$
$\mathcal{A}=(G,\Gamma,\Delta,g_{0},\gamma_{0})$ and a context switch bound
$K$, the formal definition of the set of thread types is

$\mathcal{T}(\mathcal{A},K)\coloneq G\times\Gamma\times(G\times\Gamma\times
G)^{K}\times G.$

Since we want to decide existence of an infinite progressive run of
$\mathcal{A}$, we can restrict ourselves to threads that make exactly $K$
context switches. Now let
$t=(g_{0}^{\prime},\gamma_{0}^{\prime},(g_{1},\gamma_{1},g_{1}^{\prime})\ldots(g_{K},\gamma_{K},g_{K}^{\prime}),g_{K+1})\in\mathcal{T}(\mathcal{A},K)$
be a thread type. We want to use
$\mathcal{P}_{(g_{0}^{\prime},\gamma_{0}^{\prime})}$, the PDA of a thread of
this type, to accept the language of spawns such a thread can make. However,
we have two requirements on this language, that the PDA does not yet fulfill.
Firstly, in the spirit of progressiveness, we only want to consider threads
that reach the empty stack and terminate. Secondly, we want the spawns during
each segment of the thread execution to be viewed separately from one another.

For the first requirement, we modify the transition relation of
$\mathcal{P}_{(g_{0}^{\prime},\gamma_{0}^{\prime})}$, such that transitions of
the form
$(g_{2},\bot)\xrightarrow{(g_{2},\bot)|\gamma_{2}/\gamma_{2}}\mathsf{end}$
defined in (5) are only kept in the relation for $\gamma_{2}=\bot$. This
ensures that the PDA no longer considers thread executions that do not reach
the empty stack.

Regarding the second requirement, we can simply introduce $K+1$ copies of
$\Gamma$ to the input alphabet of
$\mathcal{P}_{(g_{0}^{\prime},\gamma_{0}^{\prime})}$. It is then redefined as
$\Sigma=\Gamma\times\\{0,\ldots,K\\}\cup G\times\Gamma\times G\cup
G\times{\\{\bot\\}}$, while the stack alphabet and states stay the same. Any
transition previously defined on input $\gamma\in\Gamma$ is now copied for
inputs $(\gamma,0)$ to $(\gamma,k)$.

Let $\widetilde{\mathcal{P}}_{(g_{0}^{\prime},\gamma_{0}^{\prime})}$ be the
PDA these changes result in. Then the context-free language that characterizes
the possible spawns of a thread of type $t$ is given by the following:

$L_{t}\coloneq
L(\widetilde{\mathcal{P}}_{(g_{0}^{\prime},\gamma_{0}^{\prime})})\cap(\Gamma\times
0)^{*}\cdot(g_{1},\gamma_{1},g_{1}^{\prime})\cdot(\Gamma\times
1)^{*}\cdots(g_{K},\gamma_{K},g_{K}^{\prime})\cdot(\Gamma\times
K)^{*}\cdot(g_{K+1},\bot)$

Here we intersect the language of the PDA with a regular language, which
forces it to adhere to the type $t$ and groups the spawns correctly. If the
language $L_{t}$ is nonempty, using Parikh’s theorem (Theorem 2.1), we can
compute the semi-linear set characterizing the Parikh-image of this language
projected to $\Gamma\times\\{0,\ldots,K\\}$, which we denote $\mathsf{sl}(t)$.
We also define the set of all semi-linear sets that arise in this way as
$\mathsf{SL}(\mathcal{A},K)\coloneq\\{\mathsf{sl}(t)\mid
t\in\mathcal{T}(\mathcal{A},K),L_{t}\neq\emptyset\\}$.

Now we can construct a $\mathsf{VASSB}$ whose configurations correspond to the
ones of the $\mathsf{DCPS}$ in the way we mentioned earlier. From
$(q_{0},\emptyset,\emptyset)$ we put a token on $\gamma_{0}$ to simulate
spawning the initial thread and thus begin the simulation of the
$\mathsf{DCPS}$. We can then construct a progressive run of the
$\mathsf{VASSB}$ from a progressive run of the $\mathsf{DCPS}$ by constructing
the individual balloons as if the scheduler always picked the oldest thread
out of all choices with the same local configuration. The converse direction
works for similar reasons by always picking the oldest balloon to continue
with.

The proof also allows us to reason about _shallow_ progressive runs of
$\mathsf{DCPS}$. Following the same notion for $\mathsf{VASSB}$, we call a run
of a $\mathsf{DCPS}$ _shallow_ if there is a bound $B\in{\mathbb{N}}$ such
that each thread on that run spawns at most $B$ threads. Obverse that in the
$\mathsf{VASSB}$ construction of this section the spawns of $\mathsf{DCPS}$
threads are mapped to the contents of balloons, which is how the two notions
of shallowness correspond to each other. Thus we can go from progressive
$\mathsf{DCPS}$-run to progressive $\mathsf{VASSB}$-run by Theorem 4.4, to
shallow progressive $\mathsf{VASSB}$-run by Theorem 4.2, to shallow
progressive $\mathsf{DCPS}$ run by Theorem 4.4 combined with the observation
on the two notions of shallowness. This is formalized in the following:

###### Corollary 4.5.

A $\mathsf{DCPS}$ $\mathcal{A}$ has a progressive run iff it has a shallow
progressive run.

##  5\. From Progressive Runs for $\mathsf{VASSB}$ to Reachability

In this section, we prove Theorems 4.1 and 4.2. We outline the main ideas and
technical lemmas used to obtain the proofs. The formal proofs can be found in
the full version of the paper.

We first establish that finite witnesses exist for infinite progressive runs.
As a byproduct, this yields Theorem 4.2. Then, we show that finding finite
witnesses for progressive runs reduces to reachability in $\mathsf{VASSB}$.
Finally, we prove that reachability is decidable for $\mathsf{VASSB}$.

###  5.1. From Progressive Runs to Shallow Progressive Runs

Fix a $\mathsf{VASSB}$ $\mathcal{V}=(Q,P,\Omega,\Phi,E)$. A
_pseudoconfiguration_ $\mathsf{p}(c)=(q,\mathbf{m},\partial\mathbf{n})\in
Q\times{\mathbb{M}[P]}\times{\mathbb{M}[\Omega]}$ of a configuration
$c=(q,\mathbf{m},\mathbf{n})$ is given by
$\partial\mathbf{n}(\sigma)=\sum_{\mathbf{k}\in{\mathbb{M}[\Phi]}}\mathbf{n}(\sigma,\mathbf{k})$.
That is, a pseudoconfiguration is obtained by counting the number of balloons
in a given state $\sigma\in\Omega$ but ignoring the contents. The _support_
$\mathsf{supp}(\mathbf{m})$ of a multiset $\mathbf{m}$ is the set of places
${\\{p\mid\mathbf{m}(p)>0\\}}$ where $\mathbf{m}$ takes non-zero values.

For configurations $c=(q,\mathbf{m},\mathbf{n})$ and
$c^{\prime}=(q^{\prime},\mathbf{m}^{\prime},\mathbf{n}^{\prime})$, we write
$c\leq c^{\prime}$ if $q=q^{\prime}$, $\mathbf{m}\preceq\mathbf{m}^{\prime}$,
and $\mathbf{n}\preceq\mathbf{n}^{\prime}$. Moreover, we write
$\mathsf{p}(c)\leq_{\mathsf{p}}\mathsf{p}(c^{\prime})$ if $q=q^{\prime}$,
$\mathbf{m}\preceq\mathbf{m}^{\prime}$, and
$\partial\mathbf{n}\preceq\partial\mathbf{n}^{\prime}$. Both $\leq$ and
$\leq_{\mathsf{p}}$ are _well-quasi orders_ (wqo), that is, any infinite
sequence of configurations (resp. pseudoconfigurations) has an infinite
increasing subsequence with respect to $\leq$ (resp. $\leq_{\mathsf{p}}$)
(see, e.g., (Abdulla et al., 1996; Finkel and Schnoebelen, 2001) for details).
This follows because wqos are closed under multiset embeddings. Moreover,
$\mathcal{V}$ is _monotonic_ w.r.t. $\leq$: if $c_{1}\rightarrow
c_{1}^{\prime}$ and $c_{1}\leq c_{2}$, then there is some $c_{2}^{\prime}$
such that $c_{1}^{\prime}\leq c_{2}^{\prime}$ and $c_{2}\rightarrow
c_{2}^{\prime}$.

In analogy with algorithms for finding infinite runs in VASS (in particular
the procedure for checking fair termination in the case $K=0$ in (Ganty and
Majumdar, 2012)), one might try to find a self-covering run w.r.t. the
ordering $\leq$. However, checking for such a run would require comparing an
unbounded collection of pairs of balloons. In order to overcome this issue, we
use a _token-shifting surgery_ which moves tokens from one balloon to another.
The surgery is performed on the given progressive run $\rho$, converting it
into a progressive run $\rho^{\prime}$ with a special property: there exist
infinitely many configurations in $\rho^{\prime}$ which contain only empty
balloons. By restricting ourselves to such configurations, we are able to show
the existence of a special kind of self-covering run where the cover and the
original configuration only contain empty balloons and thus it suffices to
compare them using the ordering $\leq_{\mathsf{p}}$. First, we need the
following notion of a witness for progressiveness.

For $A\subseteq P,B\subseteq\Omega$, a run
$\rho_{A,B}=c_{0}\xrightarrow{*}c\xrightarrow{*}c^{\prime}$ is called an
_$A,B$ -witness_ for progressiveness if it satisfies the following properties:

  1. (1)

For any $c^{\prime\prime}$ occurring between $c$ and $c^{\prime}$, we have
$\mathsf{supp}(c^{\prime\prime}.\mathbf{m})\subseteq A$,

  2. (2)

for each $p\in A$, there exists $\mathit{op}$ between $c$ and $c^{\prime}$ in
$\rho_{A,B}$ such that $\mathit{op}=\delta$ where $\delta(p)<0$,

  3. (3)

for any balloon $b$, we have $c.\mathbf{n}(b)\geq 1$ iff
$c^{\prime}.\mathbf{n}(b)\geq 1$ iff ($b.\mathbf{k}=\emptyset$ and
$b.\sigma\in B$),

  4. (4)

for any $\sigma\in B$, there exists $\mathit{op}$ occurring between $c$ and
$c^{\prime}$ such that
$\mathit{op}=\mathsf{deflate}(\sigma,\cdot,\cdot,\cdot)$ or
$\mathit{op}=\mathsf{burst}(\sigma)$ is applied to an empty balloon with state
$\sigma$, and

  5. (5)

$\mathsf{p}(c)\leq_{\mathsf{p}}\mathsf{p}(c^{\prime})$ and
$\mathsf{supp}(c.\mathbf{m})=\mathsf{supp}(c^{\prime}.\mathbf{m})$.

In order to formalize the idea of a token-shifting surgery, we associate a
unique identity with each balloon. In particular, we may associate the unique
number $i\in{\mathbb{N}}$ with the balloon $b$ which is inflated by the
$i^{th}$ operation $\mathit{op}_{i}$ in a run
$\rho=c_{0}\xrightarrow{\mathit{op}_{1}}c_{1}\xrightarrow{\mathit{op}_{2}}c_{2}\cdots$,
giving us a _balloon-with-id_ $(b,i)$. The id of a balloon is preserved on
application of deflate and burst operations and thus we can speak of _the
balloon $i$_ and the sequence of operations $\mathsf{seq}_{i}$ that it
undergoes. Given a run $\rho$, we produce a corresponding _canonical run-with-
id_ $\tau$ inductively as follows: the balloon identities are assigned as
above and the balloon with least id is chosen for execution every time.
Extending the notion of a balloon-with-id to a configuration-with-id $d$
(where every balloon has an id) and a run-with-id $\tau$ (which consist of
sequences of configurations-with-id), we define the notion of a _progressive_
run-with-id $\tau$, which is one such that the sequence $\mathsf{seq}_{i}$
associated with any id $i$ in $\tau$ is either infinite, or $\mathsf{seq}_{i}$
is finite with the last operation being a burst. If every id $i$ undergoes a
burst operation in a run-with-id $\tau$, we say “$\tau$ bursts every balloon.”
We abuse terminology by saying “$\rho$ bursts every balloon” for a run $\rho$
to mean that there is a _corresponding_ run-with-id $\tau$ which bursts every
balloon. It is easy to see that the canonical run-with-id $\tau$ associated
with a progressive run $\rho$ is “almost” progressive. By always picking the
id which has been idle for the longest time, we can convert $\tau$ into a
progressive run-with-id. Thus there exists a progressive run if and only if
there exists a progressive run-with-id, but the latter retains more
information, allowing us to argue formally in proofs. With these notions in
hand, we prove the following lemma:

###### Lemma 5.1.

Given a $\mathsf{VASSB}$ $\mathcal{V}$ and a semiconfiguration $s$ of
$\mathcal{V}$, one can construct a $\mathsf{VASSB}$
$\mathcal{V}^{\prime}=(Q^{\prime},P^{\prime},\Omega^{\prime},\Phi^{\prime},E^{\prime})$
and a semiconfiguration $s^{\prime}$ of $\mathcal{V}^{\prime}$ such that the
following are equivalent:

  1. (1)

$\mathcal{V}$ has a progressive run from $s$,

  2. (2)

$\mathcal{V}^{\prime}$ has a progressive run from $s^{\prime}$ that bursts
every balloon, and

  3. (3)

$\mathcal{V}^{\prime}$ has an $A,B$-witness for some $A\subseteq P^{\prime}$
and $B\subseteq\Omega^{\prime}$.

The remainder of this subsection is devoted to the proof of Lemma 5.1. The
lemma is proved in two steps: first we show (1) $\iff$ (2), then we show (2)
$\iff$ (3). We do some preprocessing before (1) $\iff$ (2), by showing that
one can convert $\mathcal{V}$ into a $\mathsf{VASSB}$ $\mathcal{V}^{\prime}$
with two special properties: (i) the _zero-base_ property, by which every
linear set of $\mathcal{V}^{\prime}$ has base vector equal to $\mathbf{0}$,
and (ii) the property of being _typed_ , which means that we guess and verify
the sequence of deflates performed by a balloon $b$ that could potentially
transfer a non-zero number of tokens by including this information in its
balloon state $b.\sigma$. A deflate operation which transfers a non-zero
number of tokens is called a _non-trivial_ deflate. The _type_ $t=(L,S)$ of a
balloon $i$ consists of the linear set $L$ used during its inflation, along
with the sequence $S=(\pi_{1},p_{1}),(\pi_{2},p_{2}),\cdots,(\pi_{n},p_{n})$
of deflate operations on $i$, such that for each $j\in{\\{1,\cdots,n\\}}$, the
first deflate operation acting on the balloon place $\pi_{j}$ sends tokens to
the place $p_{j}$.

###### Lemma 5.2.

Given a $\mathsf{VASSB}$ $\mathcal{V}$ along with its semiconfigurations
$s_{0},s_{1}$, we can construct a zero-base, typed $\mathsf{VASSB}$
$\mathcal{V}^{\prime}$ and its semiconfigurations
$s^{\prime}_{0},s^{\prime}_{1}$ such that:

  1. (1)

There is a progressive run of $\mathcal{V}$ from $s_{0}$ iff there is a
progressive run of $\mathcal{V}^{\prime}$ from $s^{\prime}_{0}$.

  2. (2)

There is a run $s_{0}\xrightarrow{*}s_{1}$ in $\mathcal{V}$ iff there is a run
$s^{\prime}_{0}\xrightarrow{*}s^{\prime}_{1}$ in $\mathcal{V}^{\prime}$.

The zero-base property is easily obtained by making sure that the portion of
tokens transferred which correspond to the base vector are separately
transferred using $E_{p}$-edges. The addition of the types into the global
state can be done by expanding the set of balloon states exponentially. A
proof of the lemma is given in the full version.

We return to the proof of Lemma 5.1. The direction (1) $\Rightarrow$ (2)
requires us to show that $\mathcal{V}^{\prime}$ can be assumed to “burst every
balloon” in a progressive run-with-id. Consider a balloon $i$ occurring in an
arbitrary progressive run-with-id $\tau^{\prime\prime}$. In order to convert
the given $\tau^{\prime\prime}$ into a progressive $\tau^{\prime}$ in which
every balloon is burst, we need to burst those id’s $i$ such that
$\mathsf{seq}_{i}$ is infinite in $\tau^{\prime\prime}$. Since only a finite
number of non-trivial deflates can be performed by a given balloon $i$, this
implies that $\mathsf{seq}_{i}$ consists of a finite prefix in which non-
trivial deflates are performed, followed by an infinite suffix of trivial
deflates. Every such balloon $i$ can then be burst and replaced by a special
$\mathsf{VASS}$ token. The infinite trivial suffix is then simulated by using
addition and subtraction operations of these special tokens using additional
places, since any such balloon $i$ will not transfer any more tokens. The
converse direction (1) $\Leftarrow$ (2) is a reversal of the construction
where we replace the special $\mathsf{VASS}$ tokens with infinite sequences of
trivial deflate operations.

$\tau$$i_{0}$$i_{1}$$(\pi_{1},p_{1})$$i_{2}$$(\pi_{2},p_{2})$$i_{3}$$(\pi_{3},p_{3})$$j_{0}$$j_{1}$$(\pi_{1},p_{1})$$j_{2}$$(\pi_{2},p_{2})$$j^{\prime}_{2}$$(\pi_{2},p^{\prime}_{2})$$j_{3}$$(\pi_{3},p_{3})$$\tau^{\prime}$$i_{0}$$i_{1}$$(\pi_{1},p_{1})$$i_{2}$$(\pi_{2},p_{2})$$i_{3}$$(\pi_{3},p_{3})$$j_{0}$$j_{1}$$(\pi_{1},p_{1})$$j_{2}$$(\pi_{2},p_{2})$$j^{\prime}_{2}$$(\pi_{2},p^{\prime}_{2})$$j_{3}$$(\pi_{3},p_{3})$
Figure 1. Top: Initial run $\tau$ with two non-empty balloons which perform
the same sequence of three non-trivial deflates
$(\pi_{1},p_{1}),(\pi_{2},p_{2}),(\pi_{3},p_{3})$. Bottom: Modified run
$\tau^{\prime}$ after shifting tokens from the cyan balloon inflated at
$j_{0}$ to the red balloon inflated at $i_{0}$.

##### Token-Shifting

We move on to show (2) $\iff$ (3). The key idea is a token-shifting surgery. A
_token-shifting surgery_ creates a run $\tau^{\prime}$ from a run $\tau$ as
depicted in Figure 1. We start with the run-with-id
$\tau=d_{0}\xrightarrow{\mathit{op}_{1}}d_{1}\xrightarrow{\mathit{op}_{2}}d_{2}\cdots$
in which two balloons have the same type $t=(L,S)$ with
$S=(\pi_{1},p_{1}),(\pi_{2},p_{2}),(\pi_{3},p_{3})$ being the sequence of
(potentially) non-trivial deflates. Recall that an index $i$ relates to the
operation $\mathit{op}_{i}$ in $\tau$. The region of a balloon which is shaded
grey visualizes the total number of tokens contained in the balloon. This
number is seen to decrease after each non-trivial deflate operation. An empty
balloon is white in color. Balloons having the same identity have the same
outline color: red for the balloon $b_{1}$ inflated at $i_{0}$ and cyan for
the balloon $b_{2}$ inflated at $j_{0}$. At $i_{3}$ (resp. $j_{3}$) all tokens
have been transferred and the red balloon (resp. cyan balloon) is empty. The
crucial property satisfied is that $i_{k}<j_{k}$ for $k\in{\\{1,2,3\\}}$,
i.e., every deflate from $S$ of the red balloon occurs before the
corresponding deflate of the cyan balloon. In the modified run
$\tau^{\prime}$, we have the inflation of an empty cyan balloon and the
inflation of the red balloon with the sum of the tokens of both red and cyan
balloons in $\tau$. We require the zero-base property in order to be able to
shift the tokens in this manner: observe that a linear set with zero base
vector is closed under addition. Note that the cyan balloon undergoes a
trivial deflate at $j^{\prime}_{2}$ where no tokens are transferred: this
deflate is not part of $S$ and is not relevant for the token-shifting. Thus
the run-with-id $\tau$ may be modified to give a _valid_ run-with-id
$\tau^{\prime}$. Note that the configurations-with-id $d^{\prime}_{j}$ of
$\tau^{\prime}$ satisfy $d^{\prime}_{j}\geq d_{j}$ for each $j$ and so by
monotonicity every operation that is applied at $d_{j}$ can be applied at
$d^{\prime}_{j}$.

We now show how token-shifting is applied to prove (2) $\iff$ (3) in Lemma
5.1. First, from a progressive run $\tau$ of $\mathcal{V}^{\prime}$ such that
every balloon is burst, we produce a run $\tau^{\prime}$ of
$\mathcal{V}^{\prime}$ from which it will be easy to extract an $A,B$-witness.
Let $T_{\infty}$ be the set of types of balloons which occur infinitely often
in $\tau$. Since every balloon is eventually burst in $\tau$, there has to be
a configuration $d_{0}$ such that after $d_{0}$, every occurring balloon has a
type in $T_{\infty}$. We now inductively pick a sequence of configurations
$d_{1},d_{2},\cdots$ and a sequence of sets of balloons $I_{1},I_{2},\cdots$
with the following properties, for each $k\geq 1$:

  1. (1)

$I_{k}$ contains exactly one balloon inflated after $d_{k-1}$ for each type in
$T_{\infty}$ and

  2. (2)

every balloon in $I_{k}$ is burst before $d_{k}$.

For every balloon $i$ not in any of the sets $I_{1},I_{2},\cdots$, which is
inflated between $d_{k}$ and $d_{k+1}$ for $k\geq 1$, we shift its tokens to
the corresponding balloon $j$ in $I_{k}$ of the same type as $i$. Clearly this
is allowed since all of the deflate operations of $j$ occur before $i$ is
inflated. Thus we obtain the run
$\tau^{\prime}=d^{\prime\prime}_{0}\xrightarrow{*}d^{\prime}_{0}\xrightarrow{*}d^{\prime}_{1}\xrightarrow{*}d^{\prime}_{2}\ldots$
from $\tau$. The prefix $d^{\prime\prime}_{0}\xrightarrow{*}d^{\prime}_{0}$ of
the modified run $\tau^{\prime}$ may contain balloons of arbitrary type.
Between $d^{\prime}_{0}$ and $d^{\prime}_{1}$, there are only balloons in
$T_{\infty}$. After $d^{\prime}_{2}$, we have an infinite suffix where all
balloons are of a type from $T_{\infty}$ and the only non-empty balloons are
those belonging to $I_{k}$ for some $k\geq 2$. This means that the
configurations-with-id $d^{\prime}_{k}$ for each $k\geq 2$ only contain empty
balloons. Since $\leq_{\mathsf{p}}$ is a well-quasi-ordering, the sequence
$d^{\prime}_{2},d^{\prime}_{3},\ldots$ must contain configurations
$d^{\prime}_{l}$ and $d^{\prime}_{m}$ with
$d^{\prime}_{l}\leq_{\mathsf{p}}d^{\prime}_{m}$. We obtain an $A,B$-witness as
follows. We choose the set $P_{\infty}$ which is the set of places which are
non-empty infinitely often along $\tau^{\prime}$ for the set $A$. Since the
set of possible balloon states and places in a given configuration is finite,
by Pigeonhole Principle, we may assume that $d^{\prime}_{l}$ and
$d^{\prime}_{m}$ have the same set of non-empty places $A\subseteq P^{\prime}$
and balloon states $B\subseteq\Omega$. We may also assume that progressiveness
checks (2) and (4) corresponding to $A$ and $B$ occur between $d^{\prime}_{l}$
and $d^{\prime}_{m}$.

Conversely, an $(A,B)$-witness $\rho_{A,B}$ can be “unrolled” to give a
progressive run $\tau^{\prime\prime}$ of $\mathcal{V}^{\prime}$. Furthermore,
since the unrolling $\tau^{\prime\prime}$ only contains balloons with contents
present in the finite run $\rho_{A,B}$, giving us a shallow progressive run as
stated in Theorem 4.2.

###  5.2. Reduction to Reachability

The _reachability problem_ $\mathsf{REACH}$ for $\mathsf{VASSB}$ asks:

Given:

A $\mathsf{VASSB}$ $\mathcal{V}=(Q,P,{\Omega},{\Phi},E)$ and two
semiconfigurations $c_{0}$ and $c$.

Question:

Is there a run $c_{0}\xrightarrow{*}c$ ?

The more general version of the problem, where $c_{0}$ and $c$ can be
arbitrary configurations (i.e., with balloon contents), easily reduces to this
problem. However, the exposition is simpler if we restrict to
semiconfigurations here. In this subsection, we shall reduce the progressive
run problem for $\mathsf{VASSB}$ to the _reachability problem_ for
$\mathsf{VASSB}$. In the next subsection, we shall reduce the reachability
problem to the reachability problem for $\mathsf{VASS}$, which is known to be
decidable (Kosaraju, 1982; Mayr, 1981).

###### Lemma 5.3.

The progressive run problem for $\mathsf{VASSB}$ reduces to the problem
$\mathsf{REACH}$ for $\mathsf{VASSB}$.

Fix a $\mathsf{VASSB}$ $\mathcal{V}$. Using Lemma 5.1, we look for progressive
witnesses. Let $A\subseteq P$ and $B\subseteq\Omega$. We shall iterate over
the finitely many choices for $T=(A,B)$ and check that $\mathcal{V}$ has an
infinite progressive run with a $A,B$-witness by reducing to the configuration
reachability problem for an associated $\mathsf{VASSB}$ $\mathcal{V}(T)$.

The $\mathsf{VASSB}$ $\mathcal{V}(T)$ simulates $\mathcal{V}$ and guesses the
two configurations $c_{1}$ and $c_{2}$ such that
$c_{0}\xrightarrow{*}c_{1}\xrightarrow{*}c_{2}$ satisfies the conditions for a
progressive witness. It operates in five total stages, with three main stages
and two auxiliary ones sandwiched between the main stages. In the first main
stage, it simulates two identical copies of the run of $\mathcal{V}$ starting
from $c_{0}$. The global state is shared by the two copies while we have
separate sets of places. We cannot maintain separate sets of balloons for each
copy since the inflate operation is inherently non-deterministic and hence the
balloon contents may be different in the two balloons produced. The trick to
maintaining two copies of the same balloon is to in fact only inflate a single
instance of a “doubled” balloon which uses “doubled” vectors and two copies of
balloon places. Deflate operations are then performed twice on each doubled
balloon, moving tokens to the corresponding copies of places.

The $\mathsf{VASSB}$ $\mathcal{V}(T)$ also tracks the number of balloons in
each balloon state (independent of their contents), for each copy of the run.
At some point, it guesses that the current configuration is $c_{1}$ (in both
copies) and moves to the first auxiliary stage. The first auxiliary stage
checks whether all the balloons in $c_{1}$ are empty. Control is then passed
to the second main stage.

In the second main stage, the first copy of the run is frozen to preserve
$\mathsf{p}(c_{1})$ and $\mathcal{V}(T)$ continues to simulate $\mathcal{V}$
on the second copy. This is implemented by producing only “single” balloons
during this stage and only deflating the second copy of the places in the
“double” balloons which were produced in the first main stage. While
simulating $\mathcal{V}$ on the second copy, $\mathcal{V}(T)$ additionally
checks the progressiveness constraints (2) and (4) corresponding to an
$A,B$-witness in its global state. The second main stage non-deterministically
guesses when the second copy reaches $c_{2}$ (and ensures all progress
constraints have been met) and moves on to the second auxiliary stage. Here
the fact that all the balloons in $c_{2}$ are empty is checked and then
control passes to the third main stage. In the third main stage,
$\mathcal{V}(T)$ verifies that the two configurations $c_{1}$ and $c_{2}$ also
satisfy conditions (1), (3), and (5) for an $A,B$-witness. A successful
verification puts $\mathcal{V}(T)$ in a specific final semi-configuration.

###  5.3. From Reachability in $\mathsf{VASSB}$ to Reachability in
$\mathsf{VASS}$

In this subsection, we show that reachability for $\mathsf{VASSB}$ reduces to
reachability in ordinary $\mathsf{VASS}$. We write $\exp_{k}(x)$ for the
$k$-fold exponential function i.e. $\exp_{1}(x)$ is $2^{x}$, $\exp_{2}(x)$ is
$2^{2^{x}}$ etc.

A run $\rho=s_{1}\xrightarrow{*}s_{2}$ of a $\mathsf{VASSB}$ $\mathcal{V}$
between two semiconfigurations is said to be _$N$ -balloon-bounded_ for some
$N\in{\mathbb{N}}$ if there exist at most $N$ non-empty balloons which are
inflated in $\rho$. The following lemma is the crucial observation for our
reduction.

###### Lemma 5.4.

Given any $\mathsf{VASSB}$ $\mathcal{V}=(Q,P,{\Omega},{\Phi},E)$, there exists
$N\in{\mathbb{N}}$ with $N\leq O(\exp_{4}(|\mathcal{V}|))$ such that for any
two semiconfigurations $s_{1},s_{2}$, if
$(\mathcal{V},s_{1},s_{2})\in\mathsf{REACH}$, then there exists a run
$\rho=s_{1}\xrightarrow{*}s_{2}$ of $\mathcal{V}$ that is $N$-balloon-bounded.

Before we prove Lemma 5.4, let us see how it allows us to reduce reachability
in $\mathsf{VASSB}$ to reachability in $\mathsf{VASS}$.

###### Lemma 5.5.

The problem $\mathsf{REACH}$ for $\mathsf{VASSB}$ reduces to the problem
$\mathsf{REACH}$ for $\mathsf{VASS}$.

From a given $\mathsf{VASSB}$ $\mathcal{V}$, we construct a $\mathsf{VASS}$
$\mathcal{V}^{\prime}$ which has extra places
$\Omega\times{\\{1,\cdots,N\\}}\times\Phi$ for storing the contents of all the
non-empty balloons, as well as extra places $\Omega$ that store the number of
balloons which were created empty for each balloon state $\sigma$ of
$\mathcal{V}$. The global state of $\mathcal{V}^{\prime}$ is used to keep
track of the total number of non-empty balloons created as well as their state
changes. Deflate and burst operations are replaced by appropriate token
transfers such that there is only one opportunity for $\mathcal{V}^{\prime}$
to transfer tokens of any non-empty balloon by using the global state. This
results in a faithful simulation in the forward direction, as well as the easy
extraction of a run of $\mathcal{V}$ from a run of $\mathcal{V}^{\prime}$ in
the converse direction.

##### Proof of Lemma 5.4

We now prove Lemma 5.4, which will complete the proof of Theorem 4.1.

We observe that if, for every balloon state $\sigma$, the number of balloons
that are inflated in $\rho$ with state $\sigma$ is bounded by $N$, this
implies a bound of $|\Omega|N$ on the total number of balloons inflated in
$\rho$. Hence, we can equivalently show the former bound assuming a particular
balloon state. We assume that $\mathcal{V}$ is both zero-base and typed while
preserving reachability by Lemma 5.2. This implies that the type information
is contained in the state of a balloon. The lemma is then proved by showing
that if more than $N$ non-empty balloons of a particular state $\sigma$ are
inflated in a run $\rho=s_{1}\xrightarrow{*}s_{2}$, then it is possible to
perform an _id-switching_ surgery, resulting in a run
$\rho^{\prime}=s_{1}\xrightarrow{*}s_{2}$ which creates one less non-empty
balloon with state $\sigma$.

$\tau$$i_{0}$$j_{0}$$i_{1}$$j_{1}$$j_{2}$$i_{0}.\sigma.=j_{0}.\sigma$$i_{2}$$j_{3}$$i_{3}$$i_{0}.\sigma=j_{0}.\sigma$$i_{4}$$j_{4}$$i_{0}$$j_{0}$$i_{1}$$j_{1}$$i_{2}$$j_{2}$$i_{3}$$j_{3}$$i_{4}$$j_{4}$$\tau^{\prime}$$i_{0}$$j_{0}$$i_{1}$$j_{1}$$i_{2}$$j_{2}$$i_{3}$$j_{3}$$i_{4}$$j_{4}$
Figure 2. Top: Initial run $\tau$ with two non-empty balloons of the same
type: cyan balloon inflated at $i_{0}$ and orange balloon inflated at $j_{0}$.
Middle: Switching cyan and orange balloons in the part of $\tau$ between
$j_{2}$ and $i_{3}$. Bottom: Modified run $\tau^{\prime}$ obtained by shifting
token from orange balloon to cyan balloon.

The id-switching surgery is depicted in Figure 2 . The formal proof of
correctness uses runs-with-id. Fix a run-with-id
$\tau=d_{0}\xrightarrow{\mathit{op}_{1}}d_{1}\xrightarrow{\mathit{op}_{2}}d_{2}\cdots$.
Suppose the cyan and orange balloons are inflated at $i_{0}$ and $j_{0}$
respectively with the same balloon state. Since the type information is
included in the balloon state, this implies that they are also of the same
type $t=(L_{t},S_{t})$. The points marked with indices
$i_{1},i_{2},i_{3},i_{4}$ (resp. $j_{1},j_{2},j_{3},j_{4}$) are those at which
the cyan (resp. orange) balloon undergoes a deflate from $S_{t}$. While
$i_{1}<j_{1}$ and $i_{4}<j_{4}$, we have $j_{2}<i_{2}$ and $j_{3}<i_{3}$;
therefore token-shifting is not possible. However, let us assume that the
state of the cyan and orange balloons is the same at $d_{j_{2}-1}$ and
$d_{i_{3}}$ of $\tau$. This implies that the operations performed on the two
balloons in $\tau[j_{2},i_{3}]$ can be switched as shown in the middle of
Figure 2. Note that this need not be a valid run as the number of tokens
transferred by the orange at $j_{2}$ may exceed that transferred by the cyan
balloon at $i_{2}$ and the extra tokens may be required for the run
$\tau[j_{2},i_{2}]$ to be valid. However, the id-switching now enables a
token-shifting operation since $j_{k}<i_{k}$ for each
$k\in{\\{0,1,\ldots,4\\}}$. Thus, combining the switch with a token-shifting
operation which moves all tokens from orange to cyan results in the valid run
$\tau^{\prime}$ shown at the bottom of Figure 2, which contains one less non-
empty balloon of type $t$ than $\tau$. It remains to show that such an id-
switching surgery is always possible in a run $\tau$ when the number of non-
empty balloons of a type $t$ exceeds the bound $N$ given in the lemma.

##### Ramsey’s Theorem

To this end, we employ the well-known (finite) Ramsey’s theorem (Ramsey, 1930,
Theorem B), which we recall first. For a set $S$ and $k\in{\mathbb{N}}$, we
denote by $\mathbb{P}_{k}(S)$ the set of all $k$-element subsets of $S$. An
_$r$ -colored (complete) graph_ is a tuple $(V,E_{1},\ldots,E_{r})$, where $V$
is a finite set of _vertices_ and the sets $E_{1},\ldots,E_{r}$ form a
partition of all possible edges (i.e. two-element subsets), i.e.
$\mathbb{P}_{2}(V)=E_{1}\mathop{\dot{\cup}}\cdots\mathop{\dot{\cup}}E_{r}$. A
subset $U\subseteq V$ of vertices is _monochromatic_ if all edges between
members of $U$ have the same color, in other words, if
$\mathbb{P}_{2}(U)\subseteq E_{j}$ for some $j\in[1,r]$. Ramsey’s theorem says
that for each $r,n\in{\mathbb{N}}$, there is a number $R(r;n)$ such that any
$r$-colored graph with at least $R(r;n)$ vertices contains a monochromatic
subset of size $n$. It is a classical result by Erdős and Rado (Erdős and
Rado, 1952, Theorem 1) that $R(r;n)\leq r^{r(n-2)+1}$.

$\tau$$i_{0}$$j_{0}$$k_{0}$$l_{0}$$i_{1}$$j_{1}$$k_{1}$$l_{1}$$l_{2}$$i_{0}.\sigma.=j_{0}.\sigma$$k_{2}$$j_{2}$$i_{2}$$l_{3}$$k_{3}$$j_{3}$$i_{3}$$i_{0}.\sigma.=j_{0}.\sigma$$i_{4}$$j_{4}$$k_{4}$$l_{4}$

$i_{0}$$j_{0}$$k_{0}$$l_{0}$$G_{t}$$i_{0}$$j_{0}$$k_{0}$$l_{0}$$G^{\prime}_{t}$Ramsey$i_{0}$$j_{0}$Pigeonhole

Figure 3. Above:Four balloons inflated at $i_{0}<j_{0}<k_{0}<l_{0}$ of the
same type $t$ performing four deflate operations (subscripts denote deflate
operations of the same balloon). Note that the ordering relationship of
deflate operations between any pair of the four balloons is the same: between
balloons $i_{0}$ and $j_{0}$, their deflate sequences are related as
$i_{1}<j_{1},j_{2}<i_{2},j_{3}<i_{3},i_{4}<j_{4}$, which is represented by the
string $0110$. The edge-color red is used to represent $0110$ in the figure.
The balloons $i_{0}$ and $j_{0}$ share the same states at configurations
$d_{l_{2}}-1$ and $d_{i_{3}}$ of $\tau$.
Below: The same four balloons inflated at $i_{0}<j_{0}<k_{0}<l_{0}$ shown as
forming a monochromatic subgraph $G^{\prime}_{t}$ in the graph $G_{t}$. For
large enough $|G^{\prime}_{t}|$, by Pigeonhole Principle we find $i_{0},j_{0}$
which share the same states.

The application of Ramsey’s Theorem is shown in Figure 3. The bottom half of
the figure depicts the construction of a graph $G_{t}$ whose vertices are
balloons, on which Ramsey’s theorem is applied. This results in the
identification of a monochromatic clique with vertices
$i_{0},j_{0},k_{0},l_{0}$. The top half of the figure shows the deflate
operations on the balloons inflated at $i_{0},j_{0},k_{0},l_{0}$ in the run
$\tau$.

Formally, we construct a graph $G_{t}$ with vertex set $V_{t}$ of all id’s in
$\tau$ of a fixed type $t$. By assumption, $|V_{t}|\geq N$. For id’s $i,j\in
V_{t}$ with $i<j$ and $S=(\pi_{1},p_{1}),\cdots,(\pi_{n},p_{n})$, define a
sequence $s_{i,j}\in{\\{0,1\\}}^{|S|}$ by $s_{i,j}(k)=0$ if and only if $i$
undergoes the deflate transferring tokens from $\pi_{k}$ to $p_{k}$ before $j$
does.

In Figure 3, assuming that $|S|=4$, we have $s_{i_{0},j_{0}}=0110$.
Interpreting each word from ${\\{0,1\\}}^{|S|}$ as a color, we obtain a finite
coloring of the edges of $G_{t}$. Red colored edges in $G_{t}$ are to be
interpreted as the string $0110$, with other colors representing other
strings. For a large enough value of $N$, Ramsey’s Theorem gives us a
monochromatic subgraph $G^{\prime}_{t}$ of $G_{t}$ induced by a set of
vertices $V^{\prime}_{t}$. As shown in the figure, any pair of balloons chosen
from the cyan, orange, green and magenta balloons inflated at
$i_{0},j_{0},k_{0},l_{0}$ respectively, behave in the same way with respect to
their order of deflates and thus form a monochromatic subgraph
$G^{\prime}_{t}$ colored red.

Let a maximal contiguous sequence of $1$’s in $s_{i,j}$ be called a _$1$
-block_. Since the number of balloon states is finite, this implies that for a
large enough value of $|V^{\prime}_{t}|$, there will exist two id’s
$i_{0},j_{0}\in|V^{\prime}_{t}|$ (represented by the cyan and orange balloons
respectively) which share the same states at configurations at the beginning
and end of every $1$-block by the Pigeonhole Principle. The id-switching
surgery can be performed on the cyan and orange balloons, which are the ones
considered in the id-switching surgery of Figure 2. While Ramsey’s Theorem
gives a double-exponential bound on $N$ in order to obtain a large
monochromatic subgraph, the second condition requiring same states at the
beginning and end of $1$-blocks further increases our requirement to
$\exp_{4}$ for id-switching to be enabled.

This concludes the proof of Lemma 5.4 as well as Theorem 4.1.

##  6\. Starvation

We now prove Theorem 2.4. Let us first explain the additional difficulty of
the starvation problem. For deciding progressive termination, we observed that
each thread execution can be abstracted by its type and the threads it spawns.
(In other words, two executions that agree in these data are interchangeable
without affecting progressiveness of a run.) However, for starvation of a
thread, it is also important whether each thread visits some stack content $w$
after $i$ context switches. Here, $w$ is not known in advance and has to be
agreed upon by an infinite sequence of threads.

Very roughly speaking, we reduce starvation to progressive termination as
follows. For each thread, we track its spawned multiset up to some bound $B$.
Using Ramsey’s theorem (Ramsey, 1930, Theorem B), we show that if we choose
$B$ high enough, then this abstraction already determines whether a sequence
of thread executions can be replaced with different executions that actually
visit some agreed upon stack content $w$ after $i$ context switches. The
latter condition permitting replacement of threads will be called
“consistency.”

A further subtlety is that consistency of the abstractions up to $B$ only
guarantees consistency of the (unabstracted) executions if the run is shallow.
Here, Corollary 4.5 will yield a shallow run, so that we may conclude
consistency of the unabstracted executions.

### Terminology

In our terminology, a thread is a pair $(w,i)$, where $w$ is a stack content
and $i$ is a context switch number. To argue about starvation, it is
convenient to talk about how a thread evolves over time. By a _(thread)
execution_ we refer to the sequence of (pushdown and swap) instructions that
belong to a single thread, from its creation via spawn until its termination.
A thread execution can spawn new threads during each of its segments. We say
that a thread execution $e$ _produces_ the multiset
$\mathbf{m}\in{\mathbb{M}[\Lambda]}$, where
$\Lambda=\Gamma\times\\{0,\ldots,K\\}$ if the following holds: For each
$i\in\\{0,\ldots,K\\}$ and $\gamma\in\Gamma$, the thread execution $e$ spawns
$\mathbf{m}((\gamma,i))$ new threads with top of stack $\gamma$ in segment
$i$. In this case, we also call $\mathbf{m}$ the _production_ of $e$.

According to Lemma 4.3, in order to decide $\mathsf{STARV}[K]$, it suffices to
decide whether in a given $\mathsf{DCPS}$ $\mathcal{A}$, there exists a
_progressive_ run that starves some thread $(w,i)$. Therefore, we say that a
run $\rho$ is _starving_ if it is progressive and starves some thread $(w,i)$.
Let us first formulate starvation in terms of thread executions. We observe
that a progressive run $\rho$ starves a thread $(w,i)$ if and only if there
are configurations $c_{1},c_{2},\ldots$ and executions $e_{1},e_{2},\ldots$ in
$\rho$ such that:

  1. (1)

For each $j=1,2,\ldots$, in configuration $c_{j}$, both $e_{j}$ and $e_{j+1}$
are in state $(w,i)$,

  2. (2)

$e_{j}$ is switched to in the step after $c_{j}$, and

  3. (3)

$e_{j+1}$ is not switched to until $c_{j+1}$.

For the “if” direction, note that if a progressive run $\rho$ starves $(w,i)$,
then $(w,i)$ must be in the bag from some point on and whenever $(w,i)$
becomes active, there are at least two instances of $(w,i)$ in the bag. We
choose $c_{1},c_{2},\ldots$ as exactly those configurations in $\rho$ after
which $(w,i)$ becomes active. Moreover, $e_{j}$ is the thread execution that
is switched to after $c_{j}$. Furthermore, since in $c_{j}$, there must be
another instance of $(w,i)$ in the bag, there must be some execution
$e^{\prime}_{j}$ whose state $(w,i)$ is in the bag at $c_{j}$. However, since
$e_{j+1}$ will start from $(w,i)$ in $c_{j+1}$ and $e^{\prime}_{j}$ is in
$(w,i)$ at $c_{j}$, we may assume that $e_{j+1}=e^{\prime}_{j}$. With this
choice, we clearly satisfy (1)–(3) above.

For the “only if” direction, note that conditions (1)–(3) allow $(w,i)$ to
become active in between $c_{j}$ and $c_{j+1}$. However, since $e_{j+1}$ is
not switched to between $c_{j}$ and $c_{j+1}$, we know that any time $(w,i)$
becomes active, there must be another instance of $(w,i)$.

### Consistency

Our first step in deciding starvation is to find a reformulation that does not
explicitly mention the stack $w$. Instead, it states the existence of $w$ as a
consistency condition, which we will develop now.

Of course, it suffices to check whether a $\mathsf{DCPS}$ can starve some
thread $(w,i)$ when $i\in[1,K]$ is fixed. Therefore, from now on, we choose
some $i\in[1,K]$ and want to decide whether there is a stack $w\in\Gamma^{*}$
such that the thread $(w,i)$ can be starved by our $\mathsf{DCPS}$.

First, a note on notation. In the following, we will abbreviate the set
$\mathcal{T}(\mathcal{A},K)$ of thread types with $\mathcal{T}$. We will work
with families $(X_{t})_{t\in\mathcal{T}}$ of subsets $X_{t}\subseteq X$ of
some set $X$ indexed by types $t\in\mathcal{T}$. We identify the set of such
tuples indexed by $\mathcal{T}$ with $\mathbb{P}(X)^{\mathcal{T}}$. Sometimes,
it is more natural to treat them as tuples $(X_{1},\ldots,X_{k})$ with
$k=|\mathcal{T}|$. For simplicity, we will call both objects tuples.

For each type $t\in\mathcal{T}$, we consider the following set

$\displaystyle
S_{t}=\\{(w,\mathbf{m})\in\Gamma^{*}\times{\mathbb{M}[\Lambda]}\mid\text{there
is an execution of type $t$ that produces $\mathbf{m}$}$
$\displaystyle\text{and reaches stack $w$ after segment $i$}\\}$

The set $S_{t}$ encodes the following information: Is there a thread execution
of type $t$ that produces $\mathbf{m}\in{\mathbb{M}[\Lambda]}$ and at the same
time arrives in $w$ after $i$ segments? The tuple
$\mathfrak{S}_{\mathcal{A}}=(S_{t})_{t\in\mathcal{T}}$ encodes this
information for all types at once.

We will analyze $\mathfrak{S}_{\mathcal{A}}$ to show that if our decision
procedure claims that there exists a starving run, then we can construct one.
This construction will involve replacing one execution with another that (i)
has the same type, (ii) arrives in $w$ after $i$ segments, and (iii) spawns
more threads. Formally, the inserted execution must be larger w.r.t. the
following order: For $\mathbf{m},\mathbf{m}^{\prime}\in{\mathbb{M}[\Lambda]}$,
we have $\mathbf{m}\preceq_{1}\mathbf{m}^{\prime}$ if and only if
$\mathbf{m}\preceq\mathbf{m}^{\prime}$ and also
$\mathsf{supp}(\mathbf{m})=\mathsf{supp}(\mathbf{m}^{\prime})$. Recall that
$\mathsf{supp}(\mathbf{m})=\\{x\in\Lambda\mid\mathbf{m}(x)>0\\}$ is the
support of $\mathbf{m}\in{\mathbb{M}[\Lambda]}$. Here, the condition
$\mathsf{supp}(\mathbf{m})=\mathsf{supp}(\mathbf{m}^{\prime})$ makes sure that
the replacement does not introduce thread spawns with new stack symbols, as
this might destroy progressiveness of the run.

Let $S\subseteq\Gamma^{*}\times{\mathbb{M}[\Lambda]}$ be a set. For
$w\in\Gamma^{*}$, we define

$S\mathord{\downarrow}_{w}=\\{\mathbf{m}\in{\mathbb{M}[\Lambda]}\mid\exists\mathbf{m}^{\prime}\in{\mathbb{M}[\Lambda]}\colon\mathbf{m}\preceq_{1}\mathbf{m}^{\prime},~{}(w,\mathbf{m}^{\prime})\in
S\\}.$

Observe that $\mathbf{m}\in S_{t}\mathord{\downarrow}_{w}$ expresses that
there exists an execution of type $t$ that visits $w$ after segment $i$ and
produces a vector $\mathbf{m}^{\prime}\succeq_{1}\mathbf{m}$.

Our definition of consistency involves the tuple $\mathfrak{S}_{\mathcal{A}}$.
However, since some technical proofs will be more natural in a slightly more
abstract setting, we define consistency for a general tuple
$\mathfrak{S}=(S_{1},\ldots,S_{k})$ of subsets
$S_{l}\subseteq\Gamma^{*}\times{\mathbb{M}[\Lambda]}$. Hence, the following
definitions should be understood with the case
$\mathfrak{S}=\mathfrak{S}_{\mathcal{A}}$ in mind. Suppose we have a run with
thread executions $e_{1},e_{2},\ldots$ and for each type $t$, let $V_{t}$ be
the set of productions of all executions in $\\{e_{1},e_{2},\ldots\\}$ that
have type $t$. We want to formulate a condition expressing the existence of a
stack $w$ such that for any $t\in\mathcal{T}$ and any multiset $\mathbf{m}\in
V_{t}$, there exists an execution of type $t$ that visits $w$ (after $i$
context switches) and produces a multiset
$\mathbf{m}^{\prime}\succeq_{1}\mathbf{m}$. This would allow us to replace
each $e_{j}$ by an execution $e^{\prime}_{j}$ that actually visits $w$: Since
$\mathbf{m}^{\prime}\succeq_{1}\mathbf{m}$, we know that $e^{\prime}_{j}$
produces more threads of each stack symbol (and can thus still sustain the
run), but also does not introduce new kinds of threads (because
$\mathbf{m}^{\prime}$ and $\mathbf{m}$ have the same support), so that
progressiveness will not be affected by the replacement.

Let us make this formal. We say that a tuple
$\mathfrak{V}=(V_{1},\ldots,V_{k})$ with $V_{l}\subseteq{\mathbb{M}[\Lambda]}$
is _$\mathfrak{S}$ -consistent_ if there exists a $w\in\Gamma^{*}$ with
$V_{l}\subseteq S_{l}\mathord{\downarrow}_{w}$ for each $l\in[1,k]$. In this
case, we call $w$ an _$\mathfrak{S}$ -consistency witness_ for $\mathfrak{V}$.
For words $w,w^{\prime}\in\Gamma^{*}$, we write
$w\leq_{\mathfrak{S}}w^{\prime}$ if $S_{l}\mathord{\downarrow}_{w}\subseteq
S_{l}\mathord{\downarrow}_{w^{\prime}}$ for every $l\in[1,k]$.

### Starvation in Terms of Consistency

This allows us to state the following reformulation of starvation, where $w$
does not appear explicitly. A progressive run $\rho$ is said to be
_consistent_ if there are configurations $c_{1},c_{2},\ldots$ and thread
executions $e_{1},e_{2},\ldots$ that produce
$\mathbf{m}_{1},\mathbf{m}_{2},\ldots$ and such that:

  1. (1)

For each $j=1,2,\ldots$, in configuration $c_{j}$, the executions $e_{j}$ and
$e_{j+1}$ have completed $i$ segments,

  2. (2)

$e_{j}$ is switched to in the step after $c_{j}$,

  3. (3)

$e_{j+1}$ is not switched to until $c_{j+1}$, and:

  4. (4)

Let $V_{t}=\\{\mathbf{m}_{j}\mid\text{$j\in{\mathbb{N}}$, execution $e_{j}$
has type $t$}\\}$. Then the tuple $\mathfrak{V}=(V_{t})_{t\in\mathcal{T}}$ is
$\mathfrak{S}_{\mathcal{A}}$-consistent.

Note that the consistency condition in (4) expresses that there exists a stack
content $w$ such that we could, instead of each $e_{j}$, perform a thread
execution that actually visits $w$. It is thus straightforward to show:

###### Lemma 6.1.

A $\mathsf{DCPS}$ has a starving run if and only if it has a consistent run.

### Tracking Consistency

Our next step is to find some finite data that we can track about each of the
produced vectors $\mathbf{m}_{1},\mathbf{m}_{2},\ldots$ such that this data
determines whether the tuple $(V_{t})_{t\in\mathcal{T}}$ is
$\mathfrak{S}_{\mathcal{A}}$-consistent. We do this by abstracting vectors “up
to a bound.” Let $B\in{\mathbb{N}}$. We define the map
$\alpha_{B}\colon{\mathbb{M}[\Lambda]}\to{\mathbb{M}[\Lambda]}$ by
$\alpha_{B}(\mathbf{m})=\mathbf{m}^{\prime}$, where
$\mathbf{m}^{\prime}(x)=\mathsf{min}(\mathbf{m}(x),B)$ for $x\in\Lambda$. We
naturally extend $\alpha_{B}$ to subsets of ${\mathbb{M}[\Lambda]}$ (point-
wise) and to tuples of subsets of ${\mathbb{M}[\Lambda]}$ (component-wise).
Note that for a tuple $\mathfrak{V}=(V_{t})_{t\in\mathcal{T}}$ with
$V_{t}\subseteq{\mathbb{M}[\Lambda]}$ for $t\in\mathcal{T}$, the tuple
$\alpha_{B}(\mathfrak{V})$ belongs to the finite set
$\mathbb{P}([0,B]^{\Lambda})^{\mathcal{T}}$. The following Theorem tells us
that by abstracting w.r.t. some suitable $B$, we do not lose information about
$\mathfrak{S}_{\mathcal{A}}$-consistency.

###### Theorem 6.2.

Given a $\mathsf{DCPS}$ $\mathcal{A}$, there is an effectively computable
bound $B\in{\mathbb{N}}$ such that the following holds. If
$\mathfrak{V}=(V_{t})_{t\in\mathcal{T}}$ is a tuple of finite subsets
$V_{t}\subseteq{\mathbb{M}[\Lambda]}$, then $\mathfrak{V}$ is
$\mathfrak{S}_{\mathcal{A}}$-consistent if and only if
$\alpha_{B}(\mathfrak{V})$ is $\mathfrak{S}_{\mathcal{A}}$-consistent.

Roughly speaking, Theorem 6.2 allows us to check for the existence of a
consistent run by checking whether there is one with an
$\mathfrak{S}_{\mathcal{A}}$-consistent tuple $\alpha_{B}(\mathfrak{V})$.
However, we may only conclude consistency of $\mathfrak{V}$ (and hence of the
run) from consistency of $\alpha_{B}(\mathfrak{V})$ if $\mathfrak{V}$ is
finite. To remedy this, we shall employ the fact that a DCPS with a
progressive run also has a shallow progressive run (Corollary 4.5). We will
show that if our algorithm detects a run $\rho$ with consistent
$\alpha_{B}(\mathfrak{V})$, then there also exists a run $\rho^{\prime}$ with
finite $\mathfrak{V}$ such that $\alpha_{B}(\mathfrak{V})$ is consistent,
meaning by Theorem 6.2, $\rho^{\prime}$ has to be consistent.

Moreover, given a tuple of finite subsets, we can decide
$\mathfrak{S}_{\mathcal{A}}$-consistency:

###### Theorem 6.3.

Given a tuple $\mathfrak{V}=(V_{t})_{t\in\mathcal{T}}$ of finite subsets
$V_{t}\subseteq{\mathbb{M}[\Lambda]}$, it is decidable whether $\mathfrak{V}$
is $\mathfrak{S}_{\mathcal{A}}$-consistent.

### Deciding Starvation

We will prove Theorems 6.2 and 6.3 later in this section. Before we do that,
let us show how they are used to decide starvation. First, we use Theorem 6.2
to compute $B\in\mathbb{N}$. Let us fix $B$ for the decision procedure. Let
$\mathfrak{u}\in\mathbb{P}([0,B]^{\Lambda})^{\mathcal{T}}$ with
$\mathfrak{u}=(U_{t})_{t\in\mathcal{T}}$. We use a lower-case letter for this
tuple to emphasize that it is of bounded size. An infinite progressive run
$\rho$ of $\mathcal{A}$ is said to be _$(i,\mathfrak{u})$ -starving_ if it
contains configurations $c_{1},c_{2},\ldots$ and executions
$e_{1},e_{2},\ldots$ that produce $\mathbf{m}_{1},\mathbf{m}_{2},\ldots$ such
that:

  1. (1)

For each $j=1,2,\ldots$, in configuration $c_{j}$, the executions $e_{j}$ and
$e_{j+1}$ have completed $i$ segments,

  2. (2)

$e_{j}$ is switched to in the step after $c_{j}$,

  3. (3)

$e_{j+1}$ is not switched to until $c_{j+1}$, and:

  4. (4)

Let $V_{t}=\\{\mathbf{m}_{j}\mid\text{$j\in{\mathbb{N}}$, execution $e_{j}$
has type $t$}\\}$. Then $\alpha_{B}(V_{t})\subseteq U_{t}$ for each
$t\in\mathcal{T}$.

Now using the bound $B$ from Theorem 6.2, we can show the following.

###### Lemma 6.4.

If $\mathcal{A}$ has a starving run, then it has an
$(i,\mathfrak{u})$-starving run for some $i\in[1,K]$ and some
$\mathfrak{S}_{\mathcal{A}}$-consistent
$\mathfrak{u}\in\mathbb{P}([0,B]^{\Lambda})^{\mathcal{T}}$. Moreover, if
$\mathcal{A}$ has a shallow $(i,\mathfrak{u})$-starving run for some
$i\in[1,K]$ and some $\mathfrak{S}_{\mathcal{A}}$-consistent
$\mathfrak{u}\in\mathbb{P}([0,B]^{\Lambda})^{\mathcal{T}}$, then it has a
starving run.

Here, we need to assume shallowness for the converse direction because we need
finiteness of $\mathfrak{V}$ in the converse of Theorem 6.2.

Because of Lemma 6.4, we can proceed as follows to decide starvation. We first
guess a tuple $\mathfrak{u}\in\mathbb{P}([0,B]^{\Lambda})^{\mathcal{T}}$ and
check whether it is $\mathfrak{S}_{\mathcal{A}}$-consistent using Theorem 6.3.
Then, we construct a $\mathsf{DCPS}$ $\mathcal{A}_{(i,\mathfrak{u})}$ such
that $\mathcal{A}_{(i,\mathfrak{u})}$ has a progressive run if $\mathcal{A}$
has an $(i,\mathfrak{u})$-starving run. Moreover, we use the fact every
$\mathsf{DCPS}$ that has a progressive infinite run also has a shallow
infinite run (Corollary 4.5). This will allow us to turn a progressive run of
$\mathcal{A}_{(i,\mathfrak{u})}$ into a shallow $(i,\mathfrak{u})$-starving
run of $\mathcal{A}$, which must be starving by Lemma 6.4. Let us now see how
to construct $\mathcal{A}_{(i,\mathfrak{u})}$.

### Freezing $\mathsf{DCPS}$

For constructing $\mathcal{A}_{(i,\mathfrak{u})}$, it is convenient to have a
simple locking mechanism available, which we call “freezing.” It will be easy
to see that this can be implemented in $\mathsf{DCPS}$. In a freezing
$\mathsf{DCPS}$, there is one distinguished “frozen” thread in each
configuration. It cannot be resumed using the ordinary resume rules. It can
only be resumed using an unfreeze operation, which at the same time freezes
another thread. We use this to make sure that the $e_{j+1}$ stays inactive
between $c_{j}$ and $c_{j+1}$.

Syntactically, a _freezing $\mathsf{DCPS}$_ is a tuple
$\mathcal{A}=(G,\Gamma,\Delta,g_{0},\gamma_{0},\gamma_{f})$, where
$(G,\Gamma,\Delta,g_{0},\gamma_{0})$ is a $\mathsf{DCPS}$, except that the
rules $\Delta$ also contain a set ${\Delta_{\mathsf{u}}}$ of _unfreezing
rules_ of the form $g\mapsto g^{\prime}\lhd\gamma\mathbin{\text{{\tiny{\char
94\relax}}}}\gamma^{\prime}$ and $\gamma_{f}$ is the initial frozen thread
with a single stack symbol. The unfreezing rules allow the $\mathsf{DCPS}$ to
unfreeze and resume a thread with top of stack $\gamma$, while also freezing a
thread with top of stack $\gamma^{\prime}$. A _configuration_ is a tuple in
$G\times(\Gamma^{*}\times{\mathbb{N}}\cup\\{\\#\\})\times{\mathbb{M}[\hat{\Gamma}^{*}\times{\mathbb{N}}]}$,
where $\hat{\Gamma}=\Gamma\cup{\Gamma^{\text{{\tiny{\char 94\relax}}}}}$ and
${\Gamma^{\text{{\tiny{\char 94\relax}}}}}=\\{{\gamma^{\text{{\tiny{\char
94\relax}}}}}\mid\gamma\in\Gamma\\}$. A thread is _frozen_ if its top-of-stack
belongs to $\Gamma^{\text{{\tiny{\char 94\relax}}}}$. It will be clear from
the steps that in each reachable configuration, there is exactly one frozen
thread.

A freezing $\mathsf{DCPS}$ has the same steps as those of the corresponding
$\mathsf{DCPS}$. In particular, those apply only to top-of-stack symbols in
$\Gamma$. In addition, there is one more rule:

$\inferrule[Unfreeze]{g\mapsto g^{\prime}\lhd\gamma\mathbin{\text{{\tiny{\char
94\relax}}}}\gamma^{\prime}}{\langle
g,\\#,\mathbf{m}+{[\\![{\gamma^{\text{{\tiny{\char
94\relax}}}}}w,l]\\!]}+{[\\![\gamma^{\prime}w^{\prime},j]\\!]}\rangle\mapsto\langle
g^{\prime},(\gamma w,l),\mathbf{m}+{[\\![\gamma^{\prime\text{{\tiny{\char
94\relax}}}}w^{\prime},j]\\!]}\rangle}$

Hence, the frozen thread $({\gamma^{\text{{\tiny{\char 94\relax}}}}}w,l)$ is
unfrozen and resumes, while the thread $(\gamma^{\prime}w^{\prime},j)$ becomes
the new frozen thread. Moreover, the initial configuration is $\langle
g_{0},\\#,{[\\![(\gamma_{0},0)]\\!]}+{[\\![({\gamma_{f}^{\text{{\tiny{\char
94\relax}}}}},0)]\\!]}\rangle$.

Given these additional steps, progressive termination is defined as for
$\mathsf{DCPS}$. (In particular, the progressiveness condition also applies to
frozen threads.)

###### Lemma 6.5.

Given a freezing $\mathsf{DCPS}$ $\mathcal{A}$, it is decidable whether
$\mathcal{A}$ has a progressive run. Moreover, if $\mathcal{A}$ has a
progressive run, then it has a shallow progressive run.

Lemma 6.5 can be shown using a straightforward reduction to progressive
termination of ordinary $\mathsf{DCPS}$. The freezing is realized by
introducing stack symbols $\Gamma^{\text{{\tiny{\char
94\relax}}}}=\\{\gamma^{\text{{\tiny{\char
94\relax}}}}\mid\gamma\in\Gamma\\}$. An unfreeze rule $g\mapsto
g^{\prime}\lhd\gamma\mathbin{\text{{\tiny{\char 94\relax}}}}\gamma^{\prime}$
for a thread $(\gamma^{\text{{\tiny{\char 94\relax}}}}w,l)$ is then simulated
by a simple locking mechanism using a bounded number of context switches: It
turns a thread with stack $\gamma^{\prime}w^{\prime}$ into one with stack
$\gamma^{\prime\text{{\tiny{\char 94\relax}}}}w^{\prime}$ (using context
switches) and then resumes $(\gamma^{\text{{\tiny{\char 94\relax}}}}w,j)$,
where initially, $\gamma^{\text{{\tiny{\char 94\relax}}}}$ is replaced with
$\gamma$. Other than that, for threads with top of stack in
$\Gamma^{\text{{\tiny{\char 94\relax}}}}$, there are no resume rules. Since
each thread in a freeze $\mathsf{DCPS}$ can only be frozen and unfrozen at
most $K$ times, the constructed $\mathsf{DCPS}$ uses at most $2K+1$ context-
switches to simulate a run of the freeze $\mathsf{DCPS}$.

### Reduction to Progressive Runs in Freezing $\mathsf{DCPS}$

We now reduce starvation to progressive runs in freezing $\mathsf{DCPS}$. We
first guess a pair $(i,\mathfrak{u})$ with $i\in[1,K]$ and a
$\mathfrak{S}_{\mathcal{A}}$-consistent
$\mathfrak{u}\in\mathbb{P}([1,B]^{\Lambda})^{\mathcal{T}}$,
$\mathfrak{u}=(U_{t})_{t\in\mathcal{T}}$, and construct a freezing
$\mathsf{DCPS}$ $\mathcal{A}_{(i,\mathfrak{u})}$ so that $\mathcal{A}$ has an
$(i,\mathfrak{u})$-starving run if and only if
$\mathcal{A}_{(i,\mathfrak{u})}$ has a progressive run. Moreover, if
$\mathcal{A}_{(i,\mathfrak{u})}$ has a progressive run, then $\mathcal{A}$
even has a shallow $(i,\mathfrak{u})$-starving run. Therefore, $\mathcal{A}$
has a starving run if and only if for some choice of $(i,\mathfrak{u})$,
$\mathcal{A}_{(i,\mathfrak{u})}$ has a progressive run.

Intuitively, we do this by tracking for each thread execution the multiset
$\alpha_{B}(\mathbf{m})$, where $\mathbf{m}$ is its production. Using frozen
threads, we make sure that every progressive run in $\mathcal{A}$ contains
executions $e_{1},e_{2},\ldots$ to witness $(i,\mathfrak{u})$-starvation. To
verify the $(i,\mathfrak{u})$-starvation, we also track each thread’s type and
current context-switch number. Hence, we store a tuple
$(t,j,\bar{\mathbf{m}},\bar{\mathbf{n}})$, where (i) $t$ is the type, (ii) $j$
is the current context-switch number, (iii) $\bar{\mathbf{m}}$ is the guess
for $\alpha_{B}(\mathbf{m})$, where $\mathbf{m}\in{\mathbb{M}[\Lambda]}$ is
the entire production of the execution, and (iv) $\bar{\mathbf{n}}$ is
$\alpha_{B}(\mathbf{n})$, where $\mathbf{n}\in{\mathbb{M}[\Lambda]}$ is the
multiset spawned so far.

While a thread is inactive, the extra information is stored on the top of the
stack, resulting in stack symbols
$(\gamma,t,j,\bar{\mathbf{m}},\bar{\mathbf{n}})$. In particular, when we spawn
a new thread, we immediately guess its type $t$ and the abstraction
$\bar{\mathbf{m}}$, and we set $j=0$ and $\bar{\mathbf{n}}=\emptyset$. The
freezing and unfreezing works as follows. Initially, we have the frozen thread
$\gamma_{\dagger}$ (where $\gamma_{\dagger}$ is a fresh stack symbol). To
unfreeze it, we have to freeze a thread of some type $t$ where
$\bar{\mathbf{m}}$ belongs to $U_{t}$ (recall that this is a component of
$\mathfrak{u}$):

$g\mapsto g^{\prime}\lhd\gamma_{\dagger}\mathbin{\text{{\tiny{\char
94\relax}}}}(\gamma,t,i,\bar{\mathbf{m}},\bar{\mathbf{n}})$

for every $g,g^{\prime}\in G$, $t\in\mathcal{T}$, $\bar{\mathbf{m}}\in U_{t}$.
To unfreeze (and thus resume) a thread with top of stack
$(\gamma,t,i,\bar{\mathbf{m}},\bar{\mathbf{n}})$, we have to freeze a thread
$(\gamma^{\prime},t^{\prime},i,\bar{\mathbf{m}}^{\prime},\bar{\mathbf{n}}^{\prime})$
with $\bar{\mathbf{m}}^{\prime}\in U_{t^{\prime}}$. Unfreezing requires
context-switch number $i$, because the executions $e_{1},e_{2},\ldots$ must be
in segment $i$ in $c_{1},c_{2},\ldots$:

$g\mapsto\widehat{g^{\prime}}\lhd(\gamma,t,i,\bar{\mathbf{m}},\bar{\mathbf{n}})\mathbin{\text{{\tiny{\char
94\relax}}}}(\gamma^{\prime},t^{\prime},i,\bar{\mathbf{m}}^{\prime},\bar{\mathbf{n}}^{\prime})$

for each resume rule $g\mapsto g^{\prime}\lhd\gamma$, $t$, $\bar{\mathbf{m}}$,
and $\bar{\mathbf{n}}$, provided that $g$ is the state specified in $t$ to
enter from in the $i$th segment. Here, $\widehat{g^{\prime}}$ is a decorated
version of $g^{\prime}$, in which the thread can only transfer the extra
information related to $t,i,\bar{\mathbf{m}},\bar{\mathbf{n}}$ back to the
global state. Symmetrically, when interrupting a thread that information is
transferred back to the stack and the segment counter $j$ is incremented. To
resume an ordinary (i.e. unfrozen) inactive thread, we have a resume rule
$g\mapsto g^{\prime}\lhd(\gamma,t,j,\bar{\mathbf{m}},\bar{\mathbf{n}})$ for
each resume rule $g\mapsto g^{\prime}\lhd\gamma$ and each $t$, $j$,
$\bar{\mathbf{m}}$, and $\bar{\mathbf{n}}$ — if $g$ is specified as the
entering global state for segment $j$ in $t$. While a thread is active, it
keeps $\bar{\mathbf{n}}$ up to date by recording all spawns (and reducing via
$\alpha_{B}$). Finally, when a thread terminates, it checks that the
components $\bar{\mathbf{m}}$ and $\bar{\mathbf{n}}$ agree.

It is clear from the construction that $\mathcal{A}$ has a
$(i,\mathfrak{u})$-starving run if and only if
$\mathcal{A}_{(i,\mathfrak{u})}$ has a progressive run. Moreover, Lemma 6.5
tells us that if $\mathcal{A}_{(i,\mathfrak{u})}$ has a progressive run, then
it has a shallow progressive run. This shallow progressive run clearly yields
a shallow $(i,\mathfrak{u})$-starving run of $\mathcal{A}$. According to Lemma
6.4, this implies that $\mathcal{A}$ has a starving run. This establishes the
following lemma, which implies that starvation is decidable for
$\mathsf{DCPS}$.

###### Lemma 6.6.

$\mathcal{A}$ has a starving run if and only if for some $i\in[1,K]$ and some
$\mathfrak{S}_{\mathcal{A}}$-consistent
$\mathfrak{u}\in\mathbb{P}([0,B]^{\Lambda})^{\mathcal{T}}$, the freezing
$\mathsf{DCPS}$ $\mathcal{A}_{(i,\mathfrak{u})}$ has a progressive run.

### Proving Theorems 6.2 and 6.3

It remains to prove Theorems 6.2 and 6.3. We will use a structural description
of the sets $S_{t}$ (Lemma 6.7), which requires some terminology. An
_automaton over $\Gamma^{*}\times{\mathbb{M}[\Lambda]}$_ is a tuple
$\mathcal{M}=(Q,E,q_{0},q_{f})$, where $Q$ is a finite set of _states_ ,
$E\subseteq Q\times\Gamma^{*}\times{\mathbb{M}[\Lambda]}\times Q$ is a finite
set of _edges_ , $q_{0}\in Q$ is its _initial state_ , and $q_{f}\in Q$ is its
_final state_. We write $p\xrightarrow{u|\mathbf{m}}q$ if there is a sequence
$(p_{0},u_{1},\mathbf{m}_{1},p_{1}),(p_{1},u_{2},\mathbf{m}_{2},p_{2}),\ldots,(p_{n-1},u_{n},\mathbf{m}_{n},p_{n})$
of edges in $\mathcal{M}$ with $p=p_{0},q=p_{n}$, $u=u_{1}\cdots u_{n}$, and
$\mathbf{m}=\mathbf{m}_{1}+\cdots+\mathbf{m}_{n}$. The set _accepted by
$\mathcal{M}$_ is the set of all
$(w,\mathbf{m})\in\Gamma^{*}\times{\mathbb{M}[\Lambda]}$ with
$q_{0}\xrightarrow{w|\mathbf{m}}q_{f}$. A subset of
$\Gamma^{*}\times{\mathbb{M}[\Lambda]}$ is _rational_ if it is accepted by
some automaton over $\Gamma^{*}\times{\mathbb{M}[\Lambda]}$.

###### Lemma 6.7.

For every $t\in\mathcal{T}$, the set $S_{t}$ is effectively rational.

This can be deduced from (Zetzsche, 2013, Lemma 6.2). Since the latter would
require introducing a lot of machinery, we include a direct proof in the full
version. Both proofs are slight extensions of Büchi’s proof of regularity of
the set of reachable stacks in a pushdown automaton (Büchi, 1964, Theorem 1).
The only significant difference is the following: While (Büchi, 1964)
essentially introduces shortcut edges for runs that go from one stack $w$ back
to $w$, we glue in a finite automaton that produces the same output over
$\Lambda$ as such runs. This is possible since the set of the resulting
multisets is always semi-linear by Parikh’s theorem (Parikh, 1966, Theorem 2).

Because of Lemma 6.7, the following immediately implies Theorem 6.3:

###### Lemma 6.8.

Given a tuple $\mathfrak{S}=(S_{1},\ldots,S_{k})$ of rational subsets
$S_{j}\subseteq\Gamma^{*}\times{\mathbb{M}[\Lambda]}$ and a tuple
$\mathfrak{u}=(U_{1},\ldots,U_{k})$ of finite subsets
$U_{j}\subseteq{\mathbb{M}[\Lambda]}$, it is decidable whether $\mathfrak{u}$
is $\mathfrak{S}$-consistent.

###### Proof.

Since $S_{j}$ is rational, for each $\mathbf{m}\in{\mathbb{M}[\Lambda]}$ and
$j\in[1,k]$, we can compute a finite automaton for the language
$T_{j,\mathbf{m}}=\\{w\in\Gamma^{*}\mid\mathbf{m}\in
S_{j}\mathord{\downarrow}_{w}\\}$. Then $\mathfrak{u}$ is
$\mathfrak{S}$-consistent if and only if the intersection
$\bigcap_{j\in[1,k]}\bigcap_{\mathbf{m}\in U_{j}}T_{j,\mathbf{m}}$ of regular
languages is non-empty, which is clearly decidable.

Moreover, because of Lemma 6.7, Theorem 6.2 is a direct consequence of the
following.

###### Proposition 6.9.

Given rational subsets
$S_{1},\ldots,S_{k}\subseteq\Gamma^{*}\times{\mathbb{M}[\Lambda]}$, we can
compute a bound $B$ such that for the tuple
$\mathfrak{S}=(S_{1},\ldots,S_{k})$, the following holds: If
$\mathfrak{V}=(V_{1},\ldots,V_{k})$ is a tuple of finite subsets
$V_{j}\subseteq{\mathbb{M}[\Lambda]}$, then $\mathfrak{V}$ is
$\mathfrak{S}$-consistent if and only if $\alpha_{B}(\mathfrak{V})$ is
$\mathfrak{S}$-consistent.

Thus, it remains to prove Proposition 6.9, which is the purpose of the rest of
this section. Note that in Proposition 6.9, the requirement that the $V_{j}$
be _finite_ is crucial. For example, suppose $k=1$ and
$S=\\{(\mathtt{a}^{n},n\cdot{[\\![\mathtt{b}]\\!]})\mid n\in{\mathbb{N}}\\}$
and $\mathfrak{S}=(S)$. Then a set $V\subseteq{\mathbb{M}[\\{\mathtt{b}\\}]}$
is $\mathfrak{S}$-consistent if and only if $V$ is finite. Hence, there is no
bound $B$ such that $\alpha_{B}(V)$ reflects $\mathfrak{S}$-consistency of any
$V$. For Proposition 6.9, we use Ramsey’s theorem (see Section 5.3) to prove
the following pumping lemma.

###### Lemma 6.10.

Given a tuple $\mathfrak{S}=(S_{1},\ldots,S_{k})$ of rational subsets
$S_{j}\subseteq\Gamma^{*}\times{\mathbb{M}[\Lambda]}$, we can compute a bound
$M$ such that the following holds. In a word $w$ with $M$ marked positions, we
can pick two marked positions so that for the resulting decomposition $w=xyz$,
we have $xyz\leq_{\mathfrak{S}}xy^{\ell}z$ for every $\ell\geq 1$.

###### Proof.

Let $\mathcal{M}_{j}$ be an automaton for $S_{j}$ with state set $Q_{j}$ for
$j\in[1,k]$. We may assume that the sets $Q_{j}$ are pairwise disjoint and we
define $Q=\bigcup_{j=1}^{k}Q_{j}$ and $n=|Q|$. To each $u\in\Gamma^{*}$, we
assign a subset $\kappa(u)\subseteq Q\times\mathbb{P}(\Lambda)$, where
$(q,\Theta)\in Q_{j}\times\mathbb{P}(\Lambda)$ belongs to $\kappa(u)$ if there
is a cycle in $\mathcal{M}_{j}$ that starts (and ends) in $q$, reads $u$, and
reads a multiset with support $\Theta$. Hence, for $q\in Q_{j}$ and
$\Theta\subseteq\Lambda$, we have $(q,\Theta)\in\kappa(u)$ if and only if
$q\xrightarrow{u|\mathbf{m}}q$ in $\mathcal{M}_{j}$ for some
$\mathbf{m}\in{\mathbb{M}[\Lambda]}$ with $\mathsf{supp}(\mathbf{m})=\Theta$.

We specify $M$ later. Suppose $M$ positions $s_{1},\ldots,s_{M}$ are marked in
$w$. We build a colored graph on $M$ vertices and we label the edge from $j$
to $j^{\prime}$ by the set $\kappa(u)$, where $u$ is the infix of $w$ between
$s_{j}$ and $s_{j^{\prime}}$. Hence, the graph is $r$-colored, where
$r=2^{|Q|\cdot 2^{|\Lambda|}}$ is the number of subsets of
$Q\times\mathbb{P}(\Lambda)$. We now apply Ramsey’s theorem. We compute $M$ so
that $M\geq R(r;n+1)$, e.g. $M=r^{r(n-1)+1}$. Then our graph must contain a
monochromatic subset of size $n+1$. Let $t_{1},\ldots,t_{n+1}$ be the
corresponding positions in $w$. Moreover, let $w=xy_{1}\cdots y_{n}z$ be the
decomposition of $w$ such that $y_{j}$ is the infix between $t_{j}$ and
$t_{j+1}$. We claim that with $y=y_{1}\cdots y_{n}$, we have indeed
$xyz\leq_{\mathfrak{S}}xy^{\ell}z$ for every $\ell\geq 1$.

Consider a word $xy^{\ell}z$ and some multiset $\mathbf{m}\in
S_{j}\mathord{\downarrow}_{xyz}$. We have to show that $\mathbf{m}\in
S_{j}\mathord{\downarrow}_{xy^{\ell}z}$. Since $\mathbf{m}\in
S_{j}\mathord{\downarrow}_{xyz}$, there is a run of $\mathcal{M}_{j}$ reading
$(xyz,\mathbf{m}^{\prime})$ for some
$\mathbf{m}^{\prime}\succeq_{1}\mathbf{m}$. Since $\mathcal{M}_{j}$ has $\leq
n$ states, some state must repeat at two borders of the decomposition
$y=y_{1}\cdots y_{n}$. Suppose our run reads $(y_{f}\cdots
y_{g},\bar{\mathbf{m}})$ on a cycle on $q\in Q_{j}$ for some
$\bar{\mathbf{m}}$ in $\mathcal{M}_{j}$. By monochromaticity, we know that
$\kappa(y_{f}\cdots y_{g})=\kappa(y_{h})$ for every $h\in[1,n]$. Observe that
we can write

(1) $xy^{\ell}z=xy_{1}\cdots y_{f-1}(y_{f}\cdots y_{n}y_{1}\cdots
y_{f-1})^{\ell-1}y_{f}\cdots y_{n}z.$

For every $h\in[1,n]$, we have $\kappa(y_{f}\cdots y_{g})=\kappa(y_{h})$, and
hence $q\xrightarrow{y_{h}|\mathbf{m}_{h}}q$ in $\mathcal{M}_{j}$ for some
$\mathbf{m}_{h}\in{\mathbb{M}[\Lambda]}$ with
$\mathsf{supp}(\mathbf{m}_{h})=\mathsf{supp}(\bar{\mathbf{m}})$. Then, in
particular,
$\mathsf{supp}(\mathbf{m}_{h})\subseteq\mathsf{supp}(\mathbf{m}^{\prime})=\mathsf{supp}(\mathbf{m})$.
Therefore, Eq. 1 shows that $\mathcal{M}_{j}$ accepts
$(xy^{\ell}z,\mathbf{m}^{\prime}+(\ell-1)\sum_{h=1}^{n}\mathbf{m}_{h})$. Since
we now have
$\mathbf{m}\preceq_{1}\mathbf{m}^{\prime}+(\ell-1)\sum_{h=1}^{n}\mathbf{m}_{h}$,
this implies $\mathbf{m}\in S\mathord{\downarrow}_{xy^{\ell}z}$.

Using Lemma 6.10, we can obtain the final ingredient of Proposition 6.9:

###### Lemma 6.11.

Given a tuple $\mathfrak{S}=(S_{1},\ldots,S_{k})$ of rational subsets
$S_{j}\subseteq\Gamma^{*}\times{\mathbb{M}[\Lambda]}$, we can compute a bound
$B$ such that the following holds. Let $\mathfrak{V}=(V_{1},\ldots,V_{k})$ be
a $\mathfrak{S}$-consistent tuple and suppose $\alpha_{B}(\mathbf{m})\in
V_{j}$. Then adding $\mathbf{m}$ to $V_{j}$ preserves
$\mathfrak{S}$-consistency.

The idea is the following. Let
$\mathfrak{V}^{\prime}=(V^{\prime}_{1},\ldots,V^{\prime}_{k})$ be obtained
from $\mathfrak{V}$ by adding $\mathbf{m}$ to $V_{j}$. Let us say that
$w\in\Gamma^{*}$ _covers_ some $\mathbf{n}\in V^{\prime}_{j}$ if and only if