Ahmed Bouajjani

Michael Emmi

Analysis of Recursively Parallel Programs

We propose a general formal model of isolated hierarchical parallel computations, and identify several fragments to match the concurrency constructs present in real-world programming languages such as Cilk and X10. By associating fundamental formal models (vector addition systems with recursive transitions) to each fragment, we provide a common platform for exposing the relative difficulties of algorithmic reasoning. For each case we measure the complexity of deciding state-reachability for finite-data recursive programs, and propose algorithms for the decidable cases. The complexities which include PTIME, NP, EXPSPACE, and 2EXPTIME contrast with undecidable state-reachability for recursive multi-threaded programs.

Introduction

Despite the ever-increasing importance of concurrent software (e.g., for designing reactive applications, or parallelizing computation across multiple processor cores), concurrent programming and concurrent program analysis remain challenging endeavors. The most widely available facility for designing concurrent applications is multithreading, where concurrently executing sequential threads nondeterministically interleave their accesses to shared memory. Such nondeterminism leads to rarely-occurring "Heisenbugs" which are notoriously difficult to reproduce and repair. To prevent such bugs programmers are faced with the difficult task of preventing undesirable interleavings, e.g., by employing lock-based synchronization, without preventing benign interleavings-otherwise the desired reactivity or parallelism is forfeited.

The complexity of multi-threaded program analysis seems to comply with the perceived difficulty of multi-threaded programming. The state-reachability problem for multi-threaded programs is PSPACE-complete [START_REF] Kozen | Lower bounds for natural proof systems[END_REF] with a finite number of finite-state threads, and undecidable [START_REF] Ramalingam | Context-sensitive synchronization-sensitive analysis is undecidable[END_REF] with recursive threads. Current analysis approaches either explore an underapproximate concurrent semantics by considering relatively few interleavings [START_REF] Esparza | Complexity of pattern-based verification for multithreaded programs[END_REF][START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF] or explore a coarse overapproximate semantics via abstraction [START_REF] Flanagan | Thread-modular model checking[END_REF][START_REF] Henzinger | Threadmodular abstraction refinement[END_REF].

Explicitly-parallel programming languages have been advocated to avoid the intricate interleavings implicit in program syntax [START_REF] Lee | The problem with threads[END_REF], and several such industrial-strength languages have been developed [START_REF] Allen | The Fortress language specification[END_REF][START_REF] Burckhardt | Concurrent programming with revisions and isolation types[END_REF][START_REF] Charles | X10: an object-oriented approach to non-uniform cluster computing[END_REF][START_REF] Halstead | Multilisp: A language for concurrent symbolic computation[END_REF][START_REF] Leijen | The design of a task parallel library[END_REF][START_REF] Randall | Cilk: Efficient Multithreaded Computing[END_REF][START_REF] Segulja | Synchronization-free and deterministic coarse-grain parallelism: Architectural support and programming model[END_REF]. Such systems introduce various mechanisms for creating (e.g., fork, spawn, post) and consuming (e.g., join, sync) concurrent computations, and either encourage (through recommended programming practices) or ensure (through static analyses or runtime systems) that parallel computations execute in isolation without interference from others, through datapartitioning [START_REF] Charles | X10: an object-oriented approach to non-uniform cluster computing[END_REF], data-replication [START_REF] Burckhardt | Concurrent programming with revisions and isolation types[END_REF], functional programming [START_REF] Halstead | Multilisp: A language for concurrent symbolic computation[END_REF], message passing [START_REF] Pratikakis | A programming model for deterministic task parallelism[END_REF], or version-based memory access models [START_REF] Segulja | Synchronization-free and deterministic coarse-grain parallelism: Architectural support and programming model[END_REF],

perhaps falling back on transactional mechanisms [START_REF] Larus | Transactional Memory[END_REF] when complete isolation is impractical. Although few of these systems behave deterministically, consuming one concurrent computation at a time, many are sensitive to the order in which multiple isolated computations are consumed. Furthermore, some allow computations creating an unbounded number of sub-computations, returning to their superiors an unbounded number of handles to unfinished computations. Even without multithreaded interleaving, nondeterminism in the order in which an unbounded number of computations are consumed has the potential to make program reasoning complex.

In this work we investigate key questions on the analysis of interleaving-free programming models. Specifically, we ask to what extent such models simplify program reasoning, how those models compare with each other, and how to design appropriate analysis algorithms. We attempt to answer these questions as follows:

• We introduce a general interleaving-free parallel programming model on which to express the features found in popular parallel programming languages (Section 2). • We discover a surprisingly-complex feature of some existing languages: even simple classes of programs with the ability to pass unfinished computations both to and from subordinate computations have undecidable state-reachability problems (Section 2.4). • We show that the concurrency features present in many realworld programming languages such as Cilk, X10, and Multilisp are captured precisely (modulo the possibility of interleaving) by various fragments of our model (Sections 4 and 6). • For fragments corresponding to real-world language features, we measure the complexity of computing state-reachability for finite-data programs, and provide, in most cases, asymptotically optimal state-reachability algorithms (Sections 5 and 7).

Our focus on finite-data programs without interleaving is a means to measuring complexity for the sake of comparison, required since state-reachability for infinite-data or multi-threaded programs is generally undecidable. Applying our algorithms in practice may rely on data abstraction [START_REF] Graf | Construction of abstract state graphs with PVS[END_REF], and separately ensuring isolation [START_REF] Larus | Transactional Memory[END_REF], or approximating possible interleavings [START_REF] Esparza | Complexity of pattern-based verification for multithreaded programs[END_REF][START_REF] Flanagan | Thread-modular model checking[END_REF][START_REF] Henzinger | Threadmodular abstraction refinement[END_REF][START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF]; still, our handling of computation-order non-determinism is precise. The major distinguishing language features are whether a single or an arbitrary number of subordinate computations are waited for at once, and whether the scope of subordinate computations is confined. Generally speaking, reasoning for the "single-wait" case of Section 4 is less difficult than for the "multi-wait" case of Section 6, and we demonstrate a range of complexities1 from PTIME, NP, EXPSPACE, and 2EXPTIME for various scoping restrictions in Sections 5 and 7. Despite these worst-case complexities, a promising line of work has already demonstrated effective algorithms for practically-occurring EXPSPACE-complete state-reachability problem instances based on simultaneously computing iterative under-and over-approximations, and rapidly converging to a fixed point [START_REF] Geeraerts | Expand, enlarge and check: New algorithms for the coverability problem of wsts[END_REF][START_REF] Jhala | Interprocedural analysis of asynchronous programs[END_REF].

We thus present a classification of concurrency constructs, connecting programming language features to fundamental formal models, which highlight the sources of concurrent complexity resulting from each feature, and provide a platform for comparing the difficulty of formal reasoning in each. We hope that these results may be used both to guide the design of impactful program analyses, as well as to guide the design and choice of languages appropriate for various programming problems.

Recursively Parallel Programs

We consider a simple concurrent programming model where computations are hierarchically divided into isolated parallely executing tasks. Each task executes sequentially while maintaining regions (i.e., containers) of handles to other tasks. The initial task begins without task handles. When a task t creates a subordinate (child) task u, t stores the handle to u in one of its regions, at which point t and u begin to execute in parallel. The task u may then recursively create additional parallel tasks, storing their handles in its own regions. At some later point when t requires the result computed by u, t must await the completion of u-i.e., blocking until u has finished-at which point t consumes its handle to u. When u does complete, the value it returns is combined with the current state of t via a programmer-supplied return-value handler. In addition to creating and consuming subordinate tasks, tasks can transfer ownership of their subordinate tasks to newly-created tasks-by initially passing to the child a subset of task handles-and to their superiors upon completion-by finally passing to the parent unconsumed tasks.

This model permits vastly concurrent executions. Each task along with all the tasks it has created execute completely in parallel. As tasks can create tasks recursively, the total number of concurrently executing tasks has no bound, even when the number of handles stored by each task is bounded.

Program Syntax

Let Procs be a set of procedure names, Vals a set of values, Exprs a set of expressions, Regs a finite set of region identifiers, and Rets ⊆ (Vals → Stmts) a set of return-value handlers. The grammar of Figure 1 describes our language of recursively parallel programs. We intentionally leave the syntax of expressions e unspecified, though we do insist Vals contains true and false, and Exprs contains Vals and the (nullary) choice operator . We refer to the class of programs restricted to a finite set of values as finite-value programs, and to the class of programs restricted to at most n ∈ N (resp., 1) region identifiers as n-region (resp., singleregion) programs. A sequential program is a program without post, ewait, and await statements.

Each program P declares a sequence of procedures named p0 . . . pi ∈ Procs * , each p having single type-T parameter l and a top-level statement denoted sp; as statements are built inductively by composition with control-flow statements, sp describes the entire body of p. The set of program statements s is denoted Stmts. Intuitively, a post r ← p e r d statement stores the handle to a newly-created task executing procedure p in the region r; besides the procedure argument e, the newly-created task is passed a subset of the parent's task handles in regions r, and a returnvalue handler d. The ewait r statement blocks execution until some task whose handle is stored in region r completes, at which point its return-value handler is executed. Similarly, the await r statement blocks execution until all tasks whose handles are stored in region r complete, at which point all of their return-value handlers are executed, in some order. We refer to the call, return, post, ewait and await as inter-procedural statements, and the others as intra-procedural statements, and insist that return-value handlers are comprised only of intra-procedural statements. The assume e statement proceeds only when e evaluates to true-we use this statement in subsequent sections to block undesired executions in our encodings of other parallel programming models.

Example 1. The Fibonacci function can be implemented as a singleregion recursively parallel program as follows.

proc fib (var n: N)

var sum: N if n < 2 then return 1 else post r ← fib (n-1) ε (λv. sum := sum + v); post r ← fib (n-2) ε (λv. sum := sum + v); await r; return sum
Alternate implementations are possible, e.g., by replacing the await statement by two ewait statements, or storing the handles to the recursive calls in separate regions. Note that in this implementation task-handles are not passed to child tasks (ε specifies the empty region sequence) nor to parent tasks (all handles are consumed by the await statement before returning).

The programming language we consider is simple yet expressive, since the syntax of types and expressions is left free, and we lose no generality by considering only a single variable per procedure.

Parallel Semantics with Task-Passing

Unlike recursive sequential programs, whose semantics is defined over stacks of procedure frames, the semantics of recursively parallel programs is defined over trees of procedure frames. Intuitively, the frame of each posted task becomes a child of the posting task's frame. Each step of execution proceeds either by making a single intra-procedural step of some frame in the tree, creating a new frame by posting a task, or removing a frame by consuming a completed task; unconsumed sub-task frames of a completed task are added as children to the completed task's parent.

A task , s, d is a valuation ∈ Vals to the procedure-local variable l, along with a statement s to be executed, and a returnvalue handler d ∈ Rets. (Here s describes the entire body of a procedure p that remains to be executed, and is initially set to p's top-level statement sp.) A tree configuration c is a finite unordered tree of task-labeled vertices and region-labeled edges, and the set of configurations is denoted Configs. Let M[Configs] denote the set of configuration multisets. We represent configurations inductively, writing t, m for the tree with t-labeled root whose child subtrees are given by a region valuation m : Regs → M[Configs]: for r ∈ Regs, the multiset m(r) specifies the collection of subtrees connected to the root of t, m by an r-edge. The initial region valuation m ∅ is defined by m ∅ (r) -as l is the only variable, the expression e[ /l] has no free variables.

To reduce clutter and focus on the relevant parts of transition rules in the program semantics, we introduce a notion of contexts. A configuration context C is a tree with a single -labeled leaf, task-labeled vertices and leaves otherwise, and region-labeled edges. We write C[c] for the configuration obtained by substituting a configuration c for the unique -labeled leaf of C. We use configuration contexts to isolate individual task transitions, writing, for instance

C[ t, m ] → C[ t , m ]
to indicate an intra-procedural transition of the task t. Similarly a statement context S = ; s1; . . . ; si is a -led sequence of statements, and we write S[s0] for the statement obtained by substituting a statement s0 for the unique occurrence of as the first symbol of S, indicating that s0 is the next-to-beexecuted statement. A task-statement context T = , S, d is a task with a statement context S in place of a statement, and we write T [s] to indicate that s is the next statement to be executed in the task , S[s] , d . Finally, we write

C[ T [s1] , m ] → C[ T [s2]
, m ] to denote a transition of a task executing a statement s1 and replacing s1 by s2-normally s2 is the skip statement. Since the current statement s of a task T [s] does not effect expression evaluation, we liberally write e(T ) to denote the evaluation e(T [s]).

We say a task t = , S[s] , d is completed when its next-tobe-executed statement s is return e, in which case we define rvh(t) def = {d(v) : v ∈ e( )} as the set of possible return-value handler statements for t; rvh(t) is undefined when t is not completed.

Figure 2 and Figure 3 define the transition relation → rpp/p of recursively parallel programs as a set of operational steps on configurations. The intra-procedural transitions → seq of individual tasks in Figure 2 The POST-T rule creates a procedure frame to execute in parallel, and links it to the current frame by the given region, passing ownership of tasks in the specified region sequence to the newlycreated frame. The ∃WAIT-T rule consumes the result of a single child frame in the given region, and applies the return-value handler to update the parent frame's local valuation. Similarly, the ∀WAIT-NEXT-T and ∀WAIT-DONE-T rules consume the results of every child frame in the given region, applying their return handlers in the order they are consumed. The semantics of call statements reduces to that of post and ewait: supposing an unused region identifier r call , we translate each statement call l := p e into the sequence post r call ← p e ε d call ; ewait r call , where d call (v) def = l := v is the return-value handler which simply writes the entire return value v into the local variable l, and ε denotes an empty sequence of region identifiers.

A parallel execution of a program P (from c0 to cj) is a configuration sequence c0c1 . . . cj where ci → rpp/p P ci+1 for 0 ≤ i < j. An initial condition ι = p0, 0 is a procedure p0 ∈ Procs along with a value 0 ∈ Vals. A configuration 0, s, d , m ∅ is called p0, 0 -initial when s is the top-level statement of p0. A configuration c f is called f -final when there exists a context C such that c f = C[ t, m ] and l(t) = f . We say a valuation is reachable in P from ι when there exists an execution of P from some c0 to c f , where c0 is ι-initial and c f is -final.

POST-T v ∈ e(T ) m = m \ m | r ∪ r → v, sp, d , m | r C[ T [post r ← p e r d] , m ] rpp/p ----→ P C T [skip] , m ∃WAIT-T m 1 = (r → t 2 , m 2 ) ∪ m 1 s ∈ rvh(t 2 ) C[ T 1 [ewait r] , m 1 ] rpp/p ----→ P C T 1 [s] , m 1 ∪ m 2 ∀WAIT-NEXT-T m 1 = (r → t 2 , m 2 ) ∪ m 1 s ∈ rvh(t 2 ) C[ T 1 [await r] , m 1 ] rpp/p ----→ P C T 1 [s; await r] , m 1 ∪ m 2 ∀WAIT-DONE-T m(r) = ∅ C[ T [await r] , m ] rpp/p ----→ P C[ T [skip] , m ]
Problem 1 (State-Reachability). The state-reachability problem is to determine, given an initial condition ι of a program P and a valuation , whether is reachable in P from ι.

Sequential Semantics with Task-Passing

Since tasks only exchange values at creation and completion-time, the order in which concurrently-executing tasks make execution steps does not affect computed program values. In this section we leverage this fact and focus on a particular execution order in which at any moment only a single task is enabled. When the currently enabled task encounters and ewait/await statement, suspending execution to wait for a subordinate task t, t becomes the currentlyenabled task; when t completes, control returns to its waiting parent. At any moment only the tasks along one path ρ in the configuration tree have ever been enabled, and all but the last task in ρ are waiting for their child in ρ to complete. We encode this execution order into an equivalent stack-based operational semantics, which essentially transforms recursively parallel programs into sequential programs with an unbounded auxiliary storage device used to store subordinate tasks. We interpret the ewait and await statements as procedure calls which compute the values returned by previously-posted tasks. We define a frame to be a configuration in the sense of the tree-based semantics of Section 2.2, i.e., a finite unordered tree of task-labeled vertices and region-labeled edges. (Here all non-root nodes in the tree are posted tasks that have yet to take a single step of execution.) In our stack-based semantics, a stack configuration c is a sequence of frames, representing a procedure activation stack.

Figures 2 and4 define the sequential transition relation → rpp/s of recursively parallel programs as a set of operational steps on configurations. The inter-procedural transitions of Figure 4 implicitly include a transition t1, m c → rpp/s P t2, m c whenever t1 → seq P t2. Interesting here are the rules for ewait and await. The ∃WAIT-S rule blocks the currently executing frame to obtain the result for a single, nondeterministically chosen, frame c0 in the given region, by pushing c0 onto the activation stack. Similarly, the ∀WAIT-NEXT-S and ∀WAIT-DONE-S rules block the currently executing frame to obtain the results for every task in the given region, in a nondeterministically-chosen order. Finally, the RETURN-S applies a completed task's return-value handler to update the parent frame's POST local valuation. The definitions of sequential execution, initial, and reachable are nearly identical to their parallel counterparts.

-S v ∈ e(T ) m = m \ m | r ∪ r → v, sp, d , m | r T [post r ← p e r d] , m c rpp/s ----→ P T [skip] , m c ∃WAIT-S m = (r → c 0 ) ∪ m T [ewait r] , m c rpp/s ----→ P c 0 T [skip] , m c ∀WAIT-NEXT-S m = (r → c 0 ) ∪ m T [await r] , m c rpp/s ----→ P c 0 T [skip; await r] , m c ∀WAIT-DONE-S m(r) = ∅ T [await r] , m c rpp/s ----→ P T [skip] , m c RETURN-S s ∈ rvh(t 1 ) t 1 , m 1 T 2 [skip] , m 2 c rpp/s ----→ P T 2 [s] , m 1 ∪ m 2 c
Lemma 1. The parallel semantics and the sequential semantics are indistinguishable w.r.t. state reachability, i.e., for all initial conditions ι of a program P , the valuation is reachable in P from ι by a parallel execution if and only if is reachable in P from ι by a sequential execution.

Undecidability of State-Reachability with Task-Passing

Recursively parallel programs allow pending tasks to be passed bidirectionally: both from completed tasks and to newly-created tasks. This capability makes the state-reachability problem undecidableeven for the very simple cases recursive programs with at least one region, and for non-recursive programs with at least two regions. Essentially, when pending tasks can be passed to newly-created tasks, it becomes possible to construct and manipulate unbounded task-chains by keeping a handle to most-recently created task, after having passed the handle of the previously-most-recently created task to the most-recently created task. We can then show that such unbounded chains of pending tasks can be used to simulate an arbitrary unbounded and ordered storage device.

Definition 1 (Task passing). A program which contains a statement post r ← p e r d, such that | r| > 0 is called task-passing.

The task-depth of a program P is the maximum length of a sequence p1 . . . pi of procedures in P such that each pj contains a statement post r ← pi+j e r d, for 0 < j < i, and some r ∈ Regs, e ∈ Exprs, r ∈ Regs * , and d ∈ Rets. Programs with unbounded task-depth are recursive, and are otherwise non-recrusive.

Theorem 1. The state-reachability problem for n-region finitevalue task-passing parallel programs is undecidable for (a) non-recursive programs with n > 1, and (b) recursive programs with n > 0.

The proof of Theorem 1 is given by two separate reductions from the emptiness problem for Turing machines to "single-wait" programs, i.e., those using ewait statements but not await statements. In essence, as each task-handle can point to an unbounded chain of task-handles, we can construct an unbounded Turing machine tape by using one task-chain to store the contents of cells to the left of the tape head, and another chain to store the contents of cells to the right of the tape head. If only one region is granted but recursion is allowed (i.e., as in (b)), we can still construct the tape using the task-chain for the cells right of the tape head, while using the (unbounded) procedure-stack to store the cells left of the head. When only one region is granted and recursion is not allowed, neither of these reductions work. Without recursion we can bound the procedure stack, and then we can show that single-stack machine suffices to encode the single unbounded chain of tasks.

Programs without Task Passing

Due to the undecidability result of Theorem 1 and our desire to compare the analysis complexities of parallel programming models, we consider, henceforth, unless otherwise specified, only nontask-passing programs, simplifying program syntax by writing post r ← p e d. When task-passing is not allowed, region valuations need not store an entire configuration for each newly-posted task, since the posted task's initial region valuation is empty. As this represents a significant simplification on which our subsequent analysis results rely, we redefine here a few key notions.

Sequential Semantics without Task-Passing

A region valuation is a (non-nested) mapping m : Regs → M[Tasks] from regions to multisets of tasks, a frame t, m is a task t ∈ Tasks paired with a region valuation m, and a configuration c is a sequence of frames representing a procedure activation stack. The transition relation → rpp of Figures 2 and5 implicitly include a transition t1, m c → rpp P t2, m c whenever t1 → seq P t2. The definitions of sequential execution, initial, and reachable are nearly identical to their task-passing parallel and sequential counterparts. Since pending tasks need not store initial region-valuations in nontask-passing programs, this simpler semantics is equivalent to the previous stack-based semantics.

Lemma 2. For all initial conditions ι non-task-passing programs P , the valuation is reachable in P from ι by a sequential execution with task-passing if and only if is reachable in P from ι by a sequential execution without task-passing.

POST v ∈ e(T ) m = m ∪ (r → v, sp, d ) T [post r ← p e d] , m c rpp --→ P T [skip] , m c ∃WAIT m = (r → t 2 ) ∪ m T 1 [ewait r] , m c rpp --→ P t 2 , ∅ T 1 [skip] , m c ∀WAIT-NEXT m = (r → t 2 ) ∪ m T 1 [await r] , m c rpp --→ P t 2 , ∅ T 1 [skip; await r] , m c ∀WAIT-DONE m(r) = ∅ T [await r] , m c rpp --→ P T [skip] , m c RETURN s ∈ rvh(t 1 ) t 1 , m 1 T 2 [skip] , m 2 c rpp --→ P T 2 [s] , m 1 ∪ m 2 c
Even with this simplification, we do not presently know whether the state-reachability problem for (finite-value) recursively parallel programs is decidable in general. In the following sections, we identify several decidable, and in some cases tractable, restrictions to the program model which correspond to the concurrency mechanisms found in real-world parallel programming languages.

Recursive Vector Addition Systems with Zero-Test Edges

Fix k ∈ N. A recursive vector addition system (RVASS) A = Q, δ of dimension k is a finite set Q of states, along with a finite set δ = δ1 δ2 δ3 of transitions partitioned into additive transitions

δ1 ⊂ Q × N k × N k × Q, recursive transitions δ2 ⊆ Q × Q × Q × Q, and zero-test transitions δ3 ⊆ Q × Q. We write q n 1 n 2 -→ q
when q, n1, n2, q ∈ δ1, and q q 1 q 2 -→q when q, q1, q2, q ∈ δ2.

q →q when q, q ∈ δ3.

A (non-recursive) vector addition system (with states) (VASS) is a recursive vector addition system Q, δ such that δ contains only additive transitions. An (RVASS) frame q, n is a state q ∈ Q along with a vector n ∈ N k , and an (RVASS) configuration c ∈ (Q × N k ) + is a nonempty sequence of frames representing a stack of non-recursive sub-computations. The transition relation → rvas for recursive vector addition systems is defined in Figure 6. The ADDITIVE rule updates the top frame q, n by subtracting the vector n1 from n, adding the vector n2 to the result, and updating the control state to q . The CALL rule pushes on the frame-stack a new frame q1, 0 from which the RETURN rule will eventually pop at some point when the control state is q2; when this happens, the vector n1 of the popped frame is added to the vector n2 of the frame below. We describe an application of the CALL (resp., RETURN) rule as a call (resp., return) transition. Finally, the ZERO rule proceeds only when the top-most frame's vector equals 0.

An execution of a RVASS A (from c0 to cj) is a configuration sequence c0c1 . . . cj where ci → rvas ci+1 for 0 ≤ i < j. A configuration q, n is called q0-initial when q = q0 and n = 0, and a configuration c f is called q f -final when c f = q f , n c for some configuration c and n ∈ N k . We say a state q f is reachable in A from q0 when there exists an execution of A from some q0-initial configuration c0 to some q f -final configuration c f . The state-reachability problem for recursive vector addition systems is to determine whether a given state q is reachable from some q0.

Recently Demri et al. [START_REF] Demri | The covering and boundedness problems for branching vector addition systems[END_REF] have proved that state-reachability in branching vector addition systems (BVAS)-a very similar formal model to which RVASS reduces-is in 2EXPTIME. This immediately gives us an upper-bound on computing state-reachability in RVASS without zero-test edges. Though state-reachability in nonrecursive systems is EXPSPACE-complete [START_REF] Lipton | The reachability problem requires exponential space[END_REF][START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], for the moment, we do not know matching upper and lower bounds for RVASS.

Lemma 3. The state-reachability problem for recursive (resp., nonrecursive) vector addition systems without zero-test edges is EXPSPACE-hard, and in 2EXPTIME (resp., EXPSPACE).

Encoding Recursively Parallel Programs as RVASSs

When the value set Vals of a given program P is taken to be finite, the set Tasks also becomes finite since there are finitely many statements and return-value handlers occurring in P . As finitedomain multisets are equivalently encoded with a finite number of counters (i.e., one counter per element), we can encode each region valuation m ∈ Regs → M[Tasks] by a vector n ∈ N k of counters, where k = |Regs × Tasks|. To clarify the correspondence, we fix an enumeration cn : Regs × Tasks → {1, . . . , k}, and associate each region valuation m with a vector n such that for all r ∈ Regs and t ∈ Tasks, m(r)(t) = n(cn(r, t)). Let ni denote the unit vector of dimension i, i.e., ni(i) = 1 and ni(j) = 0 for j = i.

Given a finite-data recursively parallel program P without taskpassing, we associate a corresponding recursive vector addition system AP = Q, δ . We define Q def = Tasks ∪ Tasks 3 , and define δ formally in Figure 7. Intra-procedural transitions translate directly to additive transitions. The call statements are handled by recursive transitions between entry and exit points t0 and t f of the called procedure. The post statements are handled by additive transitions that increment the counter corresponding to a region-task pair. The ewait statements are handled in two steps: first an additive transition decrements the counter corresponding to region-task pair r, t0 , then a recursive transition between entry and exit points t0 and t f of the corresponding procedure is made, applying the returnvalue handler of t f upon the return. (Here we use an intermediate state T [skip] , t0, t f ∈ Q to connect the two transitions, in order to differentiate the intermediate steps of other ewait transitions.)

The await statements are handled similarly, except the await statement must be repeated again upon the return. Finally, a zero-test transition allows AP to eventually step past each await statement. Notice that ignoring intermediate states t1, t2, t3 ∈ Q, the frames t, n of AP correspond directly to frames t, m of the given program P , given the correspondence between vectors and region valuations. This correspondence between frames indeed extends to configurations, and ultimately to the state-reachability problems between AP and P . Lemma 4. For all programs P without task-passing, procedures p0 ∈ Procs, and values 0, ∈ Vals, is reachable from 0, p0 in P if and only if there exist s ∈ Stmts and d0, d ∈ Rets such that , s, d is reachable from 0, sp 0 , d0 in AP .

Our analysis algorithms in the following sections use Lemma 4 to compute state-reachability of a program P without task-passing by computing state-reachability on the corresponding RVASS AP .

ADDITIVE q n 1 n 2 -→ q n ≥ n 1 q, n c rvas ---→ q , n n 1 ⊕ n 2 c CALL q q 1 q 2 -→q q, n c rvas ---→ q 1 , 0 q, n c RETURN q q 1 q 2 -→q q 2 , n 1 q, n 2 c rvas ---→ q , n 1 ⊕ n 2 c ZERO q →q q, 0 c rvas ---→ q , 0 c Figure 6.
The transition relation for recursive vector addition systems. To simplify presentation, we assume that there is at most one recursive transition originating from each state, i.e., for all q ∈ Q, δ2 ∩ ({q} × Q 3 ) ≤ 1. We denote by 0 the vector 0, 0, . . . , 0 , and by ⊕ and the usual vector addition and subtraction operators. In general, our algorithms compute sets of region valuation vectors

v 0 ∈ e(T ) i = cn(r, v 0 , sp, d ) T [post r ← p e d] 0 n i -→T [skip] T [await r] -→T [skip] v 0 ∈ e(T ) t 0 = v 0 , sp, d call (l := v f ) ∈ rvh(t f ) T [call l := p e] t 0 t f -→T l := v f t 1 seq --→ P t 2 t 1 00 -→t 2 i = cn(r, t 0 ) s ∈ rvh(t f ) T [ewait r] n i 0 -→ T [skip] , t 0 , t f t 0 t f -→T [s] i = cn(r, t 0 ) s ∈ rvh(t f ) T [await r] n i 0 -→ T [skip] , t 0 , t f t 0 t f -→T [s; await r]
sms(t0, t f , P ) def = { n : t0, 0 rvas --→ A P * t f , n },
summarizing the execution of a procedure between an entry point t0 and exit point t f , where we write → rvas A P * to denote zero or more applications of → rvas A P . Given an effective way to compute such a function, we could systematically replace inter-procedural program steps (i.e., of the call, ewait, and await statements) with intraprocedural edges performing their net effect. Note however that even if the set of tasks is finite, the set sms(t0, t f , AP ) of summaries between t0 and t f need not be finite; the ability to compute this set is thus the key to our summarization-based algorithms in the following sections.

Single-Wait Programs

Definition 2 (Single wait). A single-wait program is a program which does not contain the await statement.

Single-wait programs can wait only for a single pending task at any program point. Many parallel programming constructs can be modeled as single-wait programs.

Parallel Programming with Futures

The future annotation of Multilisp [START_REF] Halstead | Multilisp: A language for concurrent symbolic computation[END_REF] has become a widely adopted parallel programming construct, included, for example, in X10 [START_REF] Charles | X10: an object-oriented approach to non-uniform cluster computing[END_REF] and in Leijen et al. [START_REF] Leijen | The design of a task parallel library[END_REF]'s task parallel library. Flanagan and Felleisen [START_REF] Flanagan | The semantics of future and an application[END_REF] provide a principled description of its semantics. The future construct leverages the procedural program structure for parallelism, essentially adding a "lazy" procedure call which immediately returns control to the caller with a placeholder for a value that may not yet have been computed, along with an operation for ensuring that a given placeholder has been filled in with a computed value. Syntactically, futures add two statements,

future x := p e touch x,
where x ranges over program variables, p ∈ Procs, and e ∈ Exprs.

Though it is not necessarily present in the syntax of a source language with futures, we assume every use of a variable assigned by a future statement is explicitly preceded by a touch statement. Semantically, the future statement creates a new process in which to execute the given procedure, which proceeds to execute in parallel with the caller-and all other processes created in this way. The touch statement on a variable x blocks execution of the current procedure until the future procedure call which assigned to x completes, returning a value with which is copied into x. Even though each procedure can only spawn a bounded number of parallel processes-i.e., one per program variable-there is in general no bound on the total number of parallelly-executing processes, since procedure calls-even parallel ones-are recursive.

Example 2. The Fibonacci function can be implemented as a parallel algorithm using futures as follows.

proc fib (var n: N) var x, y: N if n < 2 then return 1 else future x := fib (n-1); future y := fib (n-2); touch x; touch y; return x + y

As opposed to the usual (naïve) sequential implementation operating in time O(n 2 ), this parallel implementation runs in time O(n).

The semantics of futures is readily expressed with task-passing programs using the post and ewait statements. Assuming a region identifier rx and return handler dx for each program variable x, we encode future x := p e as post rx ← p e r dx touch x as ewait rx

where dx(v) def = x := v simply assigns the return value v to the variable x, and the vector r contains each ry such that the variable y appears in e.

Parallel Programming with Revisions

Burckhardt et al. [START_REF] Burckhardt | Concurrent programming with revisions and isolation types[END_REF]'s revisions model of concurrent programming proposes a mechanism analogous to (software) version control systems such as CVS and subversion, which promises to naturally and easily parallize sequential code in order to take advantage of multiple computing cores. There, each sequentially executing process is referred to as a revision. A revision can branch into two revisions, each continuing to execute in parallel on their own separate copies of data, or merge a previously-created revision, provided a programmer-defined merge function to mitigate the updates to data which each have performed. Syntactically, revisions add two statements,

x := rfork s join x,
where x ranges over program variables, and s ∈ Stmts. Semantically, the rfork statement creates a new process to execute the given statement, which proceeds to execute in parallel with the invoker-and all other processes created in this way. The assignment stores a handle to the newly-created revision in a revision variable x. The join statement on a revision variable x blocks execution of the current revision until the revision whose handle is stored in x completes; at that point the current revision's data is updated according to a programmer-supplied merge function m : (Vals × Vals × Vals) → Vals: when v0, v1 are, resp., the initial and final data values of the merged revision, and v2 is the current data value of the current revision, the current revisions data value is updated to m(v0, v1, v2).

The semantics of revisions is readily expressed with task-passing programs using the post and ewait statements. Assuming a region identifier rx for each program variable x, and a programmersupplied merge function m, we encode

x := rfork s as post rx ← ps l r d join x as ewait rx
where ps is a procedure declared as proc ps (var l: T ) var l 0 := l s; return (l 0 ,l)

and d( v0, v1 ) def = l := m(v0,l,v1) updates the current local valuation based on the joined revision's initial and final valuations v0, v1 ∈ Vals, and the joining revision's current local valuation stored in l. The vector r contains each ry for which the revision variable y is accessed in s. 2

Programming with Asynchronous Procedures

Asynchronous programs [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF][START_REF] Jhala | Interprocedural analysis of asynchronous programs[END_REF][START_REF] Sen | Model checking multithreaded programs with asynchronous atomic methods[END_REF] are becoming widely-used to build reactive systems, such as device drivers, web servers, and graphical user interfaces, with low-latency requirements. Essentially, a program is made up of a collection of short-lived tasks running oneby-one and accessing a global store, which post other tasks to be run at some later time. Tasks are initially posted by an initial procedure, and may also be generated by external system events. An event loop repeatedly chooses a pending task from its collection to execute to completion, adding the tasks it posts back to the task collection. Syntactically, asynchronous programs add two statements, async p e eventloop such that eventloop is invoked only once as the last statement of the initial procedure. Semantically, the async statement initializes a procedure call and returns control immediately, without waiting for the call to return. The eventloop statement repeatedly dispatches pending-i.e., called but not yet returned-procedures, and executing them to completion; each procedure executes atomically making both synchronous calls, as well as an unbounded number of additional asynchronous procedure calls. The order in which procedure calls are dispatched is chosen non-deterministically. We encode asynchronous programs as (non-deterministic) recursively parallel programs using the post and ewait statements. Assuming a single region identifier r0, we encode async p e as post r0 ← p e d eventloop as while true do ewait r0.

Supposing p has top-level statement s accessing a shared global variable g (besides the procedure parameter l), we declare p as proc p (var l: T ) var g 0 := var g := g 0 s; return (g 0 ,g).

Finally d( v0, v1 ) def = assume l = v0; l := v1 models the atomic update p performs from an initial (guessed) shared global valuation v0. Guessing allows us to simulate the communication of a shared global state g, which is later ensured to have begun with v0, which the previously-executed asynchronous task had written.

Single-Wait Analysis

The absence of await edges in a program P implies the absence of zero-test transitions in the corresponding recursive vector addition system AP . To compute state-reachability in P via procedure summarization, we must summarize the recursive transitions of AP by additive transitions (in a non-recursive system) accounting for the left-over pending tasks returned by reach procedure. This is not trivial in general, since the space of possibly returned region valuations is infinite. In increasing difficulty, we isolate three special cases of single-wait programs, whose analysis problems are simpler than the general case. In the simplest "non-aliasing" case where the number of tasks stored in each region of a procedure frame is limited to one, the execution of ewait statements are deterministic. When the number of tasks stored in each region is not limited to one, non-determinism arises from the choice of which completed task to pick at each ewait statement (see the ∃WAIT rule of Figure 5). This added power makes the state-reachability problem at least as hard as state-reachability in vector addition systems-i.e., EXPSPACEhard, though the precise complexity depends on the scope of pending tasks. After examining the PTIME-complete non-aliasing case, we examine two EXPSPACE-complete cases by restricting the scope of task handles, before moving to the general case.

Single-Wait Analysis without Aliasing

Many parallel programming languages consume only the computations of precisely-addressed tasks. In futures, for example, the touch x statement applies to the return value of a particular procedure-the last one whose future result was assigned to x. Similarly, in revisions, the join x statement applies to the last revision whose handle was stored in x. Indeed in the single-wait program semantics of each case, we are guaranteed that the corresponding region, rx, contains at most one task handle. Thus the non-determinism arising (from choosing between tasks in a given region) in the ∃WAIT rule of Figure 3 disappears. Though both futures and revisions allow task-passing, the following results apply to futures-and revisions-based programs which only pass pending tasks from child to parent. Definition 3 (Non aliasing). We say a region r ∈ Regs is aliased in a region valuation m :

Regs → M[Tasks] when |m(r)| > 1.
We say r is aliasing in a program P if there exists a reachable configuration C[ t, m ] of P in which r is aliased in m. A nonaliasing program is a program in which no region is aliasing.

Note that the set of non-aliasing region valuations is finite when the number of program values is. The non-aliasing restriction thus allow us immediately to reduce the state-reachability problem for single-wait programs to reachability in a recursive finite-data sequential program. To compute state-reachability we consider a sequence A0A1 . . . of finite-state systems iteratively under-approximating the recursive system AP given from a single-wait program P . Initially, A0 has only the transitions of AP corresponding to intra-procedural and post transitions of P . At each step i > 0, we add to Ai an additive edge summarizing an ewait transition

T [ewait r] n j n -→T [s] ,
for some t0, t f ∈ Tasks such that j = cn(r, t0), s ∈ rvh(t f ), and n is reachable at t f from t0 in Ai-1, i.e., n ∈ sms(t0, t f , Ai-1). This A0A1 . . . sequence is guaranteed to reach a fixed-point A k , since the set of non-aliasing region valuation vectors, and thus the number of possibly added edges, is finite. Furthermore, as each Ai is finite-state, only finite-state reachability queries are needed to determine the reachable states of A k , which are precisely the same reachable states of AP . Note that the number of region valuations grows exponentially in the number of regions.

Theorem 2. The state-reachability problem for non-aliasing singlewait finite-value programs is PTIME-complete for a fixed number of regions, and EXPTIME-complete in the number of regions. To solve state-reachability in local-scope single-wait programs, we compute a sequence A0A1 . . . of non-recursive vector addition systems iteratively under-approximating the recursive system AP arising from a program P . The initial system A0 has only the transitions of AP corresponding to intra-procedural and post transitions of P . At each step i > 0, we add to Ai an additive edge summarizing an ewait transition

T [ewait r] n j 0 -→T [s]
for some t0, t f ∈ Tasks such that j = cn(r, t0), s ∈ rvh(t f ), and n ∈ sms(t0, t f , Ai-1); since P is local-scope, every such n must equal 0. Since the number of possibly added edges is polynomial in P , the A0A1 sequence is guaranteed to reach in a polynomial number of steps a fixed-point A k whose reachable states are exactly those of AP . The entire procedure is EXPSPACE-complete, since each procedure-summarization reachability query is equivalent to computing state-reachability in vector addition systems.

Theorem 3. The state-reachability problem for local-scope singlewait finite-value programs is EXPSPACE-complete.

Global-Scope Single-Wait Analysis

Another relatively simple case of interest is when pending tasks are allowed to leave the scope in which they are posted, but can only be consumed by a particular, statically declared, task in an enclosing scope. This is the case, for example, in asynchronous programs [START_REF] Sen | Model checking multithreaded programs with asynchronous atomic methods[END_REF], though here we allow for slightly more generality, since tasks can be posted to multiple regions, and arbitrary control in the initial procedure frame is allowed.

Definition 5 (Global scope). A global-scope programs is a program in which the ewait (and await) statements are used only in the initial procedure frame.

Since each non-initial procedure p of a global-scope program cannot consume tasks, the set of tasks posted by p and recursively-called procedures along any execution from t0 to t f is a semi-linear set, described by the Parikh-image3 of a context-free language. Following Ganty and Majumdar [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF]'s approach, for each t0, t f ∈ Tasks we construct a polynomial-sized vector addition system A(t0, t f ) characterizing this semi-linear set of tasks (recursively) posted between t0 and t f . Then, we use each A(t0, t f ) as a component of a non-recursive vector addition system A P representing execution of the initial frame. In particular, A P contains transitions to and from the component A(t0, t f ) for each t0, t f ∈ Tasks,

T [ewait r] n j 0 -→ q0, T [skip] q f , T [skip] 00 -→T [s] ,
for all r ∈ Regs such that j = cn(r, t0), s ∈ rvh(t f ), and q0 and q f are the initial and final states of A(t0, t f ). We assume each A(t0, t f ) has unique initial and final states, distinct from the states of other components A(t 0 , t f ). In order to transition to the correct state T [s] upon completion, A(t0, t f ) carries an auxiliary statecomponent T [skip]. In this way, for each task t posted to region r in an execution between t0 and t f , the component A(t0, t f ) does the incrementing of the cn(r , t )-component of the region-valuation vector. As each of the polynomially-many components A(t0, t f ) are constructed in polynomial time [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF], this method constructs A P in polynomial time. Thus state-reachability in P is computed by state-reachability in the non-recursive vector addition system A P , in exponential space. The complexity is asymptotically optimal since global-scope single-wait programs are powerful enough to capture state-reachability in vector addition systems.

Theorem 4. The state-reachability problem for global-scope singlewait finite-value programs is EXPSPACE-complete.

The General Case of Single-Wait Analysis

In general, the state-reachability problem for finite-value single-wait programs is as hard as state-reachability in recursive vector addition systems without zero-test edges.

Theorem 5. The state-reachability problem for single-wait finitevalue programs is EXPSPACE-hard, and in 2EXPTIME.

Demri et al. [START_REF] Demri | The covering and boundedness problems for branching vector addition systems[END_REF]'s proof of membership in 2EXPTIME relies on a non-deterministically chosen reachability witness without materializing a practical algorithm for the search of said witness.

Here we give a summarization-based algorithm.

To compute state-reachability we consider again a sequence A0A1 . . . of non-recursive vector addition systems successively under-approximating the recursive system AP of a single-wait program P . Initially A0 has only the transitions of AP corresponding to intra-procedural and post transitions of P . At each step i > 0, we add to Ai an additive edge summarizing an ewait transition

T [ewait r] n j n -→T [s] ,
for some t0, t f ∈ Tasks such that j = cn(r, t0), s ∈ rvh(t f ), and n ∈ sms(t0, t f , Ai-1). Even though the set of possible added additive edges summarizing recursive transitions is infinite, with careful analysis we can show that this very simple algorithm terminates, provided we can bound the edge-labels n needed to compute state-reachability in AP . It turns out we can bound these edge labels, by realizing that the minimal vectors required to reach a target state from any given program location are bounded.

We adopt an approach based on iteratively applying backward reachability analyses in order to determine for each task t the set of vectors η(t) needed to reach the target state in AP . Let us first recall some useful basic facts. Vector addition systems are monotonic w.r.t. the natural ordering on vectors of integers, i.e., if a transition is possible from a vector v, it is also possible from any u greater than v. The ordering on vectors of integers is a well quasi-ordering (WQO), i.e., in every sequence of vectors v0, v1, . . ., there are two indices i < j such that vi is less or equal than vj . Thus, every infinite set of vectors has a finite number of minimals. A set of vectors is upward closed if whenever it contains v it also contains all vectors greater than v. Such a set can be characterized by its minimals. Moreover, the set of all predecessors in a vector addition system of an upward closed set of vectors is also upward closed; and therefore backward reachability analysis in these systems always terminates starting from an upward closed set [START_REF] Abdulla | General decidability theorems for infinite-state systems[END_REF][START_REF] Finkel | Well-structured transition systems everywhere![END_REF].

We observe that for every task t, the set η(t) is upward closed (by monotonicity), and therefore we need only determine its minimals. However, since our model is recursive vector addition systems, we must solve several state-reachability queries on a sequence of vector addition systems with increasingly more transitions, which necessarily stabilizes. We elaborate below.

First, in order to reason backward about executions to the target state, consider the non-recursive system A i obtained by adding "return" transitions t f 00 →T [s] from every procedure exit point t f = T f [return e] and procedure return point T [ewait e] occurring in P such that s ∈ rvh(t f ). These extra transitions in A i simulate a return from t f to t, transferring all of the pending tasks from a frame at t f to a frame at T [s], without any contribution from the T [s]'s intra-procedural predecessor T [ewait e].

Then define a sequence of functions η0, η1, . . . : Tasks → ℘(N k ), each ηi mapping each t ∈ Tasks to the (possibly empty, upward-closed) set of vectors ηi(t) such that for any n ∈ ηi(t), a configuration t, n is guaranteed to reach the target reachable state in A i -and thus t, n c is guaranteed to reach the target reachable state in AP for any c; each ηi can be computed in by backward reachability in the non-recursive vector addition system as explained above. Since each Ai contains at least the transitions of Ai-1, the ηi-sequence is non-decreasing w.r.t. set inclusion; i.e., more and more configurations can reach the target state; i.e., for all t ∈ Tasks we have ηi-1(t) ⊆ ηi(t). Since there can be no ever-increasing sequence of upward-closed sets of vectors over natural numbers (by the fact that the ordering on vectors of natural numbers if a WQO), the ηi sequence must stabilize after a finite number of steps.

Furthermore, since any n ∈ ηi(t) is guaranteed to reach the target state, it suffices to consider only vectors n bounded by the minimals of the upward-closed set ηi(t). To see why, notice that if some n ∈ ηi(t) labels an edge between t0 and t, then every configuration at t0 is guaranteed to reach the target state, since this edge adds the vector guaranteed to reach the target from t. Additionally, any vector greater than a minimal of ηi(t) is already guaranteed to be present in ηi(t), since ηi(t) is upward closed. Thus we need only consider edge-labels bounded by the decreasing η0η1 . . . sequence, which shows that the A0A1 . . . sequence stabilizes after a finite number of steps.

Multi-Wait Programs

Though single-wait programs capture many parallel programming constructs, they can not express waiting for each and every of an unbounded number of tasks to complete. Some programming languages require this dual notion, expressed here with await. Definition 6 (Multi wait). A multi-wait program is a program which does not contain the ewait statement. Thus, multi-wait programs can wait only on every pending task (in a given region) at any program point. Many parallel programming constructs can be modeled as multi-wait programs.

Parallel Programming in Cilk

The Cilk parallel programming language [START_REF] Randall | Cilk: Efficient Multithreaded Computing[END_REF] is an industrialstrength language with an accompanying runtime system which is used in a spectrum of environments, from modest multi-core computations to massively parallel computations with supercomputers. Similarly to futures (see Section 4.1), Cilk adds a form of procedure call which immediately returns control to the caller. Instead of an operation to synchronize with a particular previously-called pro-cedure, Cilk only provides an operation to synchronize with every previously-called procedure. At such a point, the previously-called procedures communicate their results back to the caller one-by-one with atomically-executing procedure in-lined in scope of the caller. Syntactically, Cilk adds two statements spawn p e p sync,

where p ranges over procedures, e over expressions, and p over procedures declared by inlet p (var rv: T ) s.

Here s ranges over intra-procedural program statements containing two variables: rv, corresponding to the value returned from a spawned procedure, and l, corresponding to the local variable of the spawning procedure. Semantically, the spawn statement creates a new process in which to execute the given procedure, which proceeds to execute in parallel with the caller-and all other processes created in this way. The sync statement blocks execution of the current procedure until each spawned procedure completes, and executes its associated inlet. The inlets of each procedure execute atomically. Each procedure can spawn an unbounded number of parallel processes, and the order in which the inlets of procedures execute is chosen non-deterministically.

Example 3. The Fibonacci function can be implemented as a parallel algorithm using Cilk as follows.

Parallel Programming with Asynchronous Statements

The async/finish pair of constructs in X10 [START_REF] Charles | X10: an object-oriented approach to non-uniform cluster computing[END_REF] introduces parallelism through asynchronously executing statements and synchronization blocks. Essentially, an asynchronous statement immediately passes control to a following statement, executing itself in parallel. A synchronization block executes as any other program block, but does not pass control to the following statements/block until every asynchronous statement within has completed. Syntactically, this mechanism is expressed with two statements, async s finish s where s ranges over program statements. Semantically, the async statement creates a new process to execute the given statement, which proceeds to execute in parallel with the invoker-and all other processes created in this way. The finish statement executes the given statement s, then blocks execution until every process created within s has completed.

Example 4. The Fibonacci function can be implemented as a parallel algorithm using asynchronous statements as follows.

proc fib (var n: N) var x, y: N if n < 2 then return 1 else finish async call x := fib (n-1); async call y := fib (n-2); return x + y

As opposed to the usual (naïve) sequential implementation operating in time O(n 2 ), this parallel implementation runs in time O(n).

Asynchronous statements are readily expressed with (nondeterministic) recursively parallel programs using the post and await statements. Let N be the maximum depth of nested finish statements. Assuming region identifiers r1, . . . , rN , we encode async s as post ri ← ps d finish s as await ri

where i -1 is number of enclosing finish statements, and ps is a procedure declared as proc ps (var l: T ) var l 0 := l s; return (l 0 ,l)

and d( v0, v1 ) def = assume l = v0; l := v1 models the update p performs from an initial (guessed) local valuation v0. Using the same trick we have used to model asynchronous programs in Section 4.3, we model the sequencing of asynchronous tasks by initially guessing the value v0 which the previously-executed asynchronous tasks had written, and validating that value when the return-value handler of a given task is finally run. Note that although X10 allows, in general, asynchronous tasks to interleave their memory accesses, our model captures only non-interfering tasks, by assuming either data-parallelism (i.e., disjoint accesses to data), or by assuming tasks are properly synchronized to ensure atomicity.

Structured Parallel Programming

So-called structured parallel constructs are becoming a standard parallel programming feature, adopted, for instance, in X10 [START_REF] Charles | X10: an object-oriented approach to non-uniform cluster computing[END_REF] and in Leijen et al. [START_REF] Leijen | The design of a task parallel library[END_REF]'s task parallel library. These constructs leverage normally sequential control structures to express parallelism. A typical syntactic instance of this is the parallel for-each loop: foreach x in e do s where x ranges over program variables, e over expressions, and s over statements. Semantically, the foreach statement creates a collection of new processes in which to execute the given statementone for each valuation of the loop variable. After creating these processes, the foreach statement then block execution, waiting for each to complete.

The semantics of the for-each loop is readily expressed with recursively parallel programs using the post and await statements. With a region identifier r0, we encode foreach x in e do s as for x in e do post r0 ← ps (x, ) d; await r0 and given that both x and l are free variables in s, ps is a procedure declared as proc ps (var x: T , l: T ) var l 0 := l s; return (l 0 ,l) and d( v0, v1 ) def = assume l = v0; l := v1 models the update p performs from an initial (guessed) local valuation v0.

Multi-Wait Analysis

The presence of await edges implies the presence of zero-test transitions in the recursive vector addition system AP corresponding to a multi-wait program P . As we have done for single-wait programs, we first examine the easier sub-case of local-scope programs, which in the multi-wait setting corresponds concurrency in the Cilk [START_REF] Randall | Cilk: Efficient Multithreaded Computing[END_REF] language (modulo task interleaving), as well as structured parallel programming constructs such as the foreach parallel loop in X10 [START_REF] Charles | X10: an object-oriented approach to non-uniform cluster computing[END_REF] and in Leijen et al. [START_REF] Leijen | The design of a task parallel library[END_REF]'s task parallel library (see Section 6.3). The concurrent behavior of the asynchronous statements (Section 6.2) in X10 [START_REF] Charles | X10: an object-oriented approach to non-uniform cluster computing[END_REF] does not satisfy the localscope restriction, since async statements can include recursive procedure calls which are nested without interpolating finish statements. There computing state-reachability is equivalent to determining whether a particular vector is reachable in a nonrecursive vector addition system-a decidable problem which is known to be EXPSPACE-hard, but for which the only known algorithms are non-primitive recursive. Since all multi-wait parallel languages we have encountered use only a single-region, we restrict our attention at present to single-region multi-wait programs.

Local-Scope Single-Region Multi-Wait Analysis

With the local-scoping restriction, executions of each procedure p ∈ Procs between entry point t0 ∈ Tasks and exit point t f ∈ Tasks are completely summarized by a Boolean indicating whether or not t f is reachable from t0. However, as executions of p may encounter await statements, modeled by zero-test edges in the recursive vector addition system AP , computing this Boolean requires determining the reachable program valuations between each pair of consecutive "synchronization points" (i.e., occurrences of the await statement), which in principle requires deciding whether the vector 0 is reachable in a vector addition system describing execution from the program point just after the first await statement to the point just after the second; i.e., when T1[await r] and T2[await r] are consecutively-occurring synchronization points, we must determine whether T1[skip] , 0 can reach T2[skip] , 0 .

A careful analysis of our reachability problem reveals it does not have the EXPSPACE-hard complexity of determining vectorreachability in general, due to the special structure of our reachability query. We notice that between two synchronization points t1 and t2 of p, execution proceeds in two phases. In the first, post statements made by p only increment the vector valuations. In the second phase, starting when the second await statement is encountered, the await statement repeatedly consumes tasks, only decrementing the vector valuations-the vector valuations can not be re-incremented again because of the local-scope restriction: each consumed task is forbidden from returning addition tasks. Due to this special structure, deciding reachability between t1 and t2 reduces to deciding if a particular integer linear program I(t1, t2) has a solution.

Since consuming tasks in the await-loop requires using the summaries computed for other procedures, we consider a sequence A0A1 . . . of non-recursive vector addition systems iteratively underapproximating the recursive system AP . Initially A0 has only the transitions of AP corresponding to intra-procedural and post transitions of P . At each step i > 0, we add to Ai one of two edges types. One type is an additive procedure-summary edge, used to describe a single task-consumption step of an await transition,

T [await r] n j 0 -→T [s; await r] ,
for some t0, t f ∈ Tasks such that j = cn(r, t0), s ∈ rvh(t f ), and sms(t0, t f , Ai-1) = ∅. The second possibility is an additive synchronization-point summary edge, summarizing an entire of sequence of program transitions between two synchronization points,

T1[skip] 00 -→T2[skip] ,
where T1[await r] , T2[await r] ∈ Tasks are consecutive synchronization points occurring P , and 0 ∈ sms(T1[skip] , T2[skip] , AP ). The procedure-summary edges are computed using only finite-state reachability between program states, using the synchronizationpoint summary edges, while the synchronization-point summary edges are computed by reduction to integer linear programming. As the number of possible edges is bounded polynomially in the program size, the A0A1 sequence is guaranteed to reach a fixed-point A k in a polynomial number of steps, though each step may take nondeterministic-polynomial time, in the worst case, to compute solutions to integer linear programs. The reachable states of A k are precisely the same reachable states of AP . Theorem 6. The state-reachability problem for local-scope multiwait single-region finite-value programs is NP-complete.

Single-Region Multi-Wait Analysis

Without the local-scoping restriction, each execution of each procedure p ∈ Procs between entry point t0 ∈ Tasks and exit point t f ∈ Tasks is summarized by the tasks posted between the last-encountered await statement, at a "synchronization point" ts ∈ Tasks (note that ts = t0 if no await statements are encountered), and a return statement, at the exit point t f . Since p can make recursive procedure calls between ts and t f , and each called procedure can again return pending tasks, the possible sets of pending tasks upon p's return at t f is described by the Parikh-image 3 of a context-free language L(t0, t f ). It turns out we can describe this image as the set of vectors computed by a polynomially-sized vector addition system A L (t0, t f ) without recursion and zero-test edges [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF]. We use thus computations of A L (t0, t f ) to summarize the set of possible region-valuations reached in an execution from t0 to t f . However, computing A L (t0, t f ) is not immediate, since between t0 and the last-encountered synchronization point ts, execution of the given procedure p may encounter await statements (necessarily so when t0 = ts). Since we use zero-test edges to express await statements, we also need to summarize execution between synchronization points (i.e., between the procedure entry point and among await statements) using only additive edges. To further complicate matters, each such summarization requires, in turn, the summaries A L (t 0 , t f ) computed for other procedures!

We break the circular dependence between procedure summaries and synchronization-point summaries by iteratively computing both. In particular, we compute a sequence A L 0 A L 1 . . . of procedure summary vector addition systems along with a sequence A0A1 . . . of vector addition systems such that each A L i , for i > 0, is computed using the transitions of Ai-1, and Ai, for i ≥ 0 is computed using the procedure summaries of A L i . Initially A L 0 contains only the pending-task sets reachable without taking await transitions, and A0 contains only the transitions of AP corresponding to intraprocedural and post transitions of P , along with transitions to components A L 0 . For i ≥ 0, Ai contains transitions to and from the components

A L i (t0, t f ) T [await r] n j 0 -→ q 0 , T [skip] q f , T [skip] 00 -→T [s; await r]
for each t0, t f ∈ Tasks such that j = cn(r, t0), s ∈ rvh(t f ), and q0 and q f are the unique initial and final states of A L i (t0, t f ). (We assume each component A L i (t0, t f ) has unique initial and final states, distinct from the states of other components. Additionally, we equip each A L (t0, t f ) with auxiliary state to carry the identity T [skip] of the invoking task to ensure the proper return of control when A L (t0, t f ) completes.)

At each step i > 0, we add to Ai an additive edge summarizing the execution between two synchronization points T1[await r] and T2[await r] occurring in P :

T1[skip] 00 -→T2[skip] such that T2[skip] is reachable in Ai-1 from T1[skip], i.e., 0 ∈ sms(T1[skip] , T2[skip] ,
Ai-1). Note that when T [await r] is a synchronization point occurring in P , T [skip] refers to the program point immediately after the await statement. Since there are only polynomially-many such edges that can possibly be added, we are guaranteed to reach a fixed-point A k of A0A1 . . . in a polynomial number of steps. Furthermore, the reachable states of A k are precisely the same reachable states of AP . However, computing 0 ∈ sms(t1, t2, Ai-1) at each step is difficult due to the zerotest edge in the await statement immediately preceding t2; this is computationally equivalent to computing reachability of a particular vector in non-recursive vector addition systems.

Theorem 7. The state-reachability problem for multi-wait singleregion finite-value programs is decidable.

Since practical algorithms to compute vector-reachability is a difficult open problem, we remark that it is possible to obtain algorithms to approximate our state-reachability problem. Consider, for instance, the over-approximate semantics given by transforming each await r statement into while do ewait r. Though many more behaviors are present in the resulting program, since not every task is necessarily consumed during the while loop, practical algorithmic solutions are more probable (see Section 5.4).

Related Work

Formal modeling and verification of multi-threaded programs has been heavily studied, including but not limited to identifying decidable sub-classes [START_REF] Kahlon | Boundedness vs. unboundedness of lock chains: Characterizing decidability of pairwise CFL-reachability for threads communicating via locks[END_REF], and effective over-approximate [START_REF] Flanagan | Thread-modular model checking[END_REF][START_REF] Henzinger | Threadmodular abstraction refinement[END_REF] and under-approximate [START_REF] Esparza | Complexity of pattern-based verification for multithreaded programs[END_REF][START_REF] Lal | Reducing concurrent analysis under a context bound to sequential analysis[END_REF] analyses.

To our knowledge little work has been done in formal modeling and verification of programs written in explicitly-parallel languages which are free of thread interleaving. Sen and Viswanathan [START_REF] Sen | Model checking multithreaded programs with asynchronous atomic methods[END_REF]'s asynchronous programs, which falls out as a special case of our single-wait programs, is perhaps most similar to our work in this regard. Practical verification algorithms by combining iterative over-and under-approximation [START_REF] Jhala | Interprocedural analysis of asynchronous programs[END_REF], and in-depth complexity analysis [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF] of asynchronous programs have been studied.

Though decidability results of abstract parallel models have been reported [START_REF] Bouajjani | Regular symbolic analysis of dynamic networks of pushdown systems[END_REF][START_REF] Esparza | Efficient algorithms for pre * and post * on interprocedural parallel flow graphs[END_REF] (Bouajjani and Esparza [START_REF] Bouajjani | Rewriting models of boolean programs[END_REF] survey of this line of work), these works target abstract computation models, and do not identify precise complexities and optimal algorithms for real-world parallel programming languages, nor do they handle the case where procedures can return unbounded sets of unfinished computations to their callers.

Conclusion

We have proposed a general model of recursively parallel programs which captures the concurrency constructs in a variety of popular programming languages. By isolating the fragments corresponding to various language features, we are able to associate corresponding formal models, measure the complexity of state-reachability, and provide precise analysis algorithms. We hope our complexity measurements may be used to guide the design and choice of con-

A. Proofs of Theorems

To begin with we introduce notation and simplifying assumptions in order to simplify the proof arguments in the following subsections. Finite-State Automata A finite-state automaton (FSA) A = Q, Σ, → over an alphabet Σ is a finite set Q of states, along with a set → ⊆ Q × Σ × Q of transitions. Given initial and accepting states q0, q f ∈ Q, the language A(q0, q f ) is the set of Σ-words labeling runs of A which begin in the initial state q0 and terminate in the accepting state q f . The language-emptiness problem for finite-state automata is to decide, given an automaton A and states q0, q f ∈ Q, whether A(q0, q f ) = ∅.

Notation and Simplifying Assumptions

Context-Free Grammars A context-free grammar (CFG) G = V, Σ, → over an alphabet Σ is a finite set V of variables, along with a finite set → ⊆ V × (V ∪ Σ) * of productions. Given an initial variable v0 ∈ V , the language G(v0) is the set of Σ-words derived by G from the initial variable v0.

Pushdown Automata A pushdown automaton (PDA) A = Q, Σ, Γ, → over an alphabet Σ is a finite set Q of states, along with a stack alphabet Γ, and a finite set → ⊆ Q×Γ×Σ×Γ * ×Q of transitions. A configuration qw is a state q ∈ Q paired with a stack-symbol sequence w ∈ Γ * . Given initial and accepting states q0, q f ∈ Q, the language A(q0, q f ) is the set of Σ-words labeling runs of A which begin in the initial configuration q0ε and terminate in an accepting configuration q f w, for some w ∈ Γ * . The language-emptiness problem for pushdown automata is to decide, given an automaton A and states q0, q f ∈ Q, whether A(q0, q f ) = ∅.

Vector Addition Systems A vector addition system (VAS)

A = Q, → of dimension k ∈ N is a finite set Q of states, along with a finite set → ⊂ Q × N k × N k × Q of transitions.
A configuration q n is a state q ∈ Q paired with a vector n ∈ N k . Given initial and accepting states q0, q f ∈ Q, the language A(q0, q f ) is the set of vectors N f ⊆ N k such that A has a run which begins in q00 and terminates in q f n f , for some n f ∈ N f . The statereachability problem (resp., the configuration-reachability problem) for vector addition systems is to decide, given a system A and states q0, q f ∈ Q (resp., and a vector n f ∈ N k ), whether A(q0, q f ) = ∅ (resp., whether n f ∈ A(q0, q f )).

Turing Machines A Turing machine (TM) A = Q, Σ, → over an alphabet Σ is a finite set Q of states, along with a finite set → ⊆ Q×Σ×{L, R}×Σ×Q of transitions. A configuration q, w1, w2 is a state q ∈ Q along with two words w1, w2 ∈ Σ * . Given initial and accepting states q0, q f ∈ Q, the language A(q0, q f ) is the set of Σ-words w such that A has a run which begins in an initial configuration q0, ε, w and terminates in an accepting configuration q f , w1, w2 , for some and w1, w2 ∈ Σ * . The language-emptiness problem for Turing machines is to decide, given a machine A and states q0, q f ∈ Q, whether A(q0, q f ) = ∅.

A.1 Proof of Theorem 1 Theorem 1. The state-reachability problem for n-region finitevalue task-passing parallel programs is undecidable for (a) non-recursive programs with n > 1, and (b) recursive programs with n > 0.

We prove (a) and (b) separately, both by reduction from the language emptiness problem for Turing machines.

Proof (a). By reduction from the language emptiness problem for Turing machines, let A = Q, Σ, → be a Turing machine with → = {d1, . . . , dj}, and let q0, q f ∈ Q. We assume, without loss of generality, that upon entering the accepting state q f , A performs a sequence of left-moves until reaching the end of the tape; i.e., q f , a, L, a, q f ∈ → for all a ∈ Σ. We define a task-passing program PA with two regions rL and rR, and one return-value handler d, along with an initial procedure given by proc main () where each transition di ∈ → gives rise to a corresponding statement si defined as follows. For right-moving transitions di = q a/b,R -→ q , we define si as assume state = q; assume sym = a; post rL ← p b d; state := q ; ewait rR // overwrites sym For left-moving transitions di = q a/b,L -→ q , we define si as assume state = q; assume sym = a; post rR ← p b d; state := q ; ewait rL // overwrites sym where the return-value handler d(a) def = sym := a assigns a to sym. By connecting the configurations of q, w1, w2 of A to the chain of tasks in region rL-corresponding to the cells of w1-and the chain of tasks in region rR-corresponding to the cells of w2-it is routine to show that PA faithfully simulates precisely the runs of A. As we assume A moves to the left upon encountering the accepting state q f , we need only check reachability of a valuation q f to state at the end of the main procedure to know whether or not A has an accepting run.

var
Proposition A.1.I. A(q0, q f ) = ∅ if and only if state = q f and done = true is reachable in PA.

Thus state-reachability in PA solves language emptiness for A.

Using only a single region, it will not be possible to create two independent, unbounded task chains. However, if the program is allowed to be recursive, we can leverage the unbounded procedure stack as an additional, independent, unbounded data structure.

Proof (b). By reduction from the language emptiness problem for Turing machines, let A = Q, Σ, → be a Turing machine with → = {d1, . . . , dj}, and let q0, q f ∈ Q. We assume, without loss of generality, that upon entering the accepting state q f , A performs a sequence of left-moves until reaching the end of the tape; i.e., q f , a, L, a, q f ∈ → for all a ∈ Σ. We define a single-region task-passing program PA with a single return-value handler d, along with an initial procedure given by where each transition di ∈ δ gives rise to a corresponding statement si defined as follows. For the right-moving transitions di = q a/b,R -→ q , we define si as assume q_cur = q; assume sym = a; sym := b; ewait r; // At this point q_R, q_cur, and sym_R // have been overwritten by the initial-// and current-state valuations, and the // symbol stored in the right-neighbor // who has just moved left. assume q_R = q ; post r ← p sym_R d where d(q, q , a) assigns q to q_R, q to q_cur, and a to sym_R.

Our program thus simulates right moves by awaiting a pending task representing the right neighbor of the current task. For left-moving transitions di = q a/b,L -→ q , we define si as assume q_cur = q; assume sym = a; return (q_init, q , b);

Our program thus simulates left moves by returning to the awaiting task, who promptly recreates its right-neighbor by posting a new task to replace it. By connecting the configurations of q, w1, w2 of A to the chain of awaiting tasks-corresponding to the cells of w1-and the chain of posted tasks-corresponding to the cells of w2-it is routine to show that PA faithfully simulates precisely the runs of A. As we assume A moves to the left upon encountering the accepting state q f , we need only check reachability of a valuation q f to q_cur at the end of the main procedure to know whether or not A has an accepting run.

Proposition A.1.II. A(q0, q f ) = ∅ if and only if q cur = q f and done = true is reachable in PA.

Thus state-reachability of PA solves language emptiness for A.

Theorem A.1.I. The state-reachability problem for single-region non-recursive finite-value task-passing parallel programs is PTIMEcomplete for fixed task-depth, and EXPTIME in the task-depth.

Proof. Let P be a non-aliasing single-wait finite-value single-region non-recursive task-passing parallel program with finite sets of procedures Procs, values Vals, regions Regs, and return-value handlers Rets, and let ∈ Vals be a target reachable value. Furthermore, we assume P is non-recursive, which implies there is a maximum task-depth N ∈ N-i.e., N is the maximum length of a sequence p0p1 . . . ∈ Procs * such that each pi contains a post to pi+1. Without loss of generality, suppose is only reachable in procedure frames where the current statement is s f . We construct a pushdown automaton AP = Q, Σ, Γ, → along with initial and accepting states q0, q f ∈ Q. We define the states of AP to be N -bounded sequences of tasks

Q def = Tasks ≤N
In this way a state t0t1 . . . ti ∈ Q represents a computation of P in which each tj-1 (0 < j ≤ i) is a task posted by tj. Note that this finite representation is only possible since we know the task-depth is bounded by N . Given this state-representation, we define the transition relation → of AP as follows:

Intra-task transitions For each intra-task transition t1 → seq ∃WAIT For each statement ewait r occurring in P , we add a transition which simply pops the pair v, d from the top of the pushdown stack, and applies the return-value handler,

T [ewait r] • t pop v,d ----→ T [s] • t, where s ∈ d(v).
RETURN For each statement return e occurring in P , we add a transition which pushes the return value and return-value handler for the current task onto the pushdown stack, to be later consumed by a subsequent ewait statement,

, S[return e] , d • t0 • t push v,d ----→ t0 • t.
where v ∈ e( ) Finally, given an initial condition ι = p0, 0 and target value f of P , we let q0 = 0, sp 0 , d , and q f = f , s f , d , for some d ∈ Rets. (See above for the definition of s f .) Proposition A.1.III. AP (q0, q f ) = ∅ if and only if is reachable in P from ι.

As |Q| is O((|Locs| • |Rets|) N ) and |Γ| is O(|Vals| • |Rets|),
the size of AP is polynomial in P . Since language emptiness is decidable in polynomial time for pushdown automata, our procedure gives a polynomial-time algorithm for state-reachability when N is fixed, though exponential in N . def = Tasks. We model task-posting by labeling the transitions of the automata by tasks, and define the alphabet Σ def = Tasks∪ {ε}. The initial task-summary automaton is A t 0 = Q, {ε}, ∅ with states Q, alphabet {ε}, and the empty set ∅ of transitions.

Construction of A s i

For i > 0, we define the i th sync-point summary automaton, characterizing state-reachability between syncpoint pairs, as

A s i = Q ∪ Q, Σ, δ s i ,
where the states Q and Q def = {q : q ∈ Q} correspond, resp., to control locations of the first (task-posting) and second (task-consuming) phases, and the transitions δ s i = δ + δ δ - i are partitioned into first-phase transitions δ + ⊆ Q × Σ × Q, phase-change transitions δ = { q, ε, q : q ∈ Q}, and second-phase transitions

δ - i ⊆ Q × Σ × Q.
The relation δ + is given directly by the sequential and taskposting transitions of the input program. The relation δ - i contains a transition T [await r] , t0, T [s; await r] summarizing the computation of the task t0 if and only if there exists t f ∈ Tasks such that A t i-1 (t0, t f ) is non-empty, and s ∈ rvh(t f ). In other words, q, t, q summarizes the effect of consuming task t, based on A t i-1 's summarization of t, including the local-variable update due to its return-value handler. In this way, the possible behaviors between sync-points are computed using the thus-far computed (entire) behaviors of each posted task.

Note that not every word of A s i (q0, qf ) represents a valid computation between two consecutive sync points q0 and q f , since A s i cannot ensure that each task posted in the first phase is consumed in the second. For q0, q f ∈ Q, we say a word w1w2 ∈ A s i (q0, qf ) is balanced if and only if Π(w1) = Π(w2) and there exists q ∈ Q such that w1 ∈ A s i (q0, q) and w2 ∈ A s i (q, qf ). We say A s i (q0, qf ) has a balanced run if some word of A s i (q0, qf ) is balanced. For each sync-point pair q0, q f , we can decide whether A s i (q0, qf ) has a balanced run by integer linear programming. In particular, given A s i and q0, q f , we construct a integer linear program Φ s i (q0, q f ) which has a positive integer solution exactly when A s i (q0, qf ) has a balanced run.

Construction of Φ s i

Given the sync-point summary automaton A s i and sync-point pair q0, q f ∈ Q, we construct an ILP, denoted Φ s i (q0, q f ). Fix (finite) enumerations q1q2 . . ., a1a2 . . ., and d1d2 . . . of the states, symbols, and transitions, resp., of A s i ; i.e., Q = {q1, q2, . . .}, Σ = {a1, a2, . . .}, and δ = {d1, d2, . . .}. Additionally, assume that dj = qj, ε, qj ∈ δ for each qj ∈ Q. We define Φ s i (q0, q f ) as an integer linear program with |δ s i | transition occurrence variables, one dj for each transition dj ∈ δ s i , and

|Σ| -1 task counter variables, one aj for each aj ∈ Σ \ {ε}. Then Φ s i (q0, q f ) contains the following constraints: for each q k ∈ Q,   d k + d j ∈δ + (q k ,•,•) dj -

d j ∈δ + (•,•,q k ) dj   =
0 when q k = q0 1 when q k = q0

ensures each state in the first phase is exited once per entry (except q0, which is exited one extra time); for each qk ∈ Q,   dk +

d j ∈δ - i (•,•,q k ) dj - d j ∈δ - i (q k ,•,•) dj    =
0 when q k = q f 1 when q k = q f ensures each state in the second phase is exited once per entry (except q f , which is entered one extra time);   ensures that the number of occurrences of each a k in the first phase is equal to the number of occurrence in the second phase. (Note that the aj variables are not strictly necessary; they are added only for clarity.) Supposing dj 1 dj 2 . . . is a connected sequence of transitions through A s i , a corresponding solution to the given set of constraints would set the variables dj 1 , dj 2 , . . . to positive (non-zero) values corresponding to the number of times each transition is taken in A s i . However, supposing there are loops in A s i which are not connected to any of the selected transitions, the given constraints do not prohibit solutions which take each transition of these loops an arbitrary number of times. This is a standard issue with encoding automaton traces which can be addressed by adding a polynomial number of constraints to Φ s i (q0, q f ). Proposition A.6.I. A s i (q0, qf ) has a balanced run if and only if Φ s i (q0, q f ) has a positive integer solution.

Note that |Φ

Construction of A t i

For i > 0 we define the i th task-summary automaton, characterizing state-reachability among synchronization points, as

A t i = Q, {ε}, δ t i
such that q, ε, q ∈ δ t i if and only if q, q is a sync-point pair, and A s i (q, q ) has a balanced run. Note that there are only finitely-many transitions which can be added over the entire A s i and A t i sequence. It follows that there exists a fixed-point m ∈ N of this sequence, and it is not hard to see that A s m and A t m capture every behavior of the input program P . Proposition A.6.II. A synchronization point q f of the initial task is reachable from an initial control location q0 if and only if A t m (q0, q f ) is non-empty.

Though we consider here only state-reachability to a synchronization point contained in the initial task for simplicity, Proposition A.6.II can indeed be extended to arbitrary control locations of arbitrary tasks. As the set of possible added transitions is bounded We demonstrate this equivalence by a polynomial-time reduction in each direction. Though VASS configuration-reachability has been shown decidable [START_REF] Rackoff | The covering and boundedness problems for vector addition systems[END_REF], only non-primitive recursive algorithms are known; VASS state-reachability gives an EXPSPACE lower-bound.

Lemma A.7.I. The state-reachability problem for multi-wait finitevalue programs is reducible to the configuration-reachability problem for vector addition systems.

Proof sketch. Without the local-scoping restriction, each execution of each procedure p ∈ Procs between entry point t0 ∈ Tasks and exit point t f ∈ Tasks is summarized by the tasks posted between the last-encountered await statement, at a "synchronization point" ts ∈ Tasks (note that ts = t0 if no await statements are encountered), and a return statement, at the exit point t f . Since p can make recursive procedure calls between ts and t f , and each called procedure can again return pending tasks, the possible sets of pending tasks upon p's return at t f is described by the Parikh-image 3 of a context-free language L(t0, t f ). It turns out we can describe this image as the set of vectors computed by a polynomially-sized vector addition system A L (t0, t f ) without recursion and zero-test edges [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF]. We use thus computations of A L (t0, t f ) to summarize the set of possible region-valuations reached in an execution from t0 to t f . However, computing A L (t0, t f ) is not immediate, since between t0 and the last-encountered synchronization point ts, execution of the given procedure p may encounter await statements (necessarily so when t0 = ts). Since we use zero-test edges to express await statements, we also need to summarize execution between synchronization points (i.e., between the procedure entry point and among await statements) using only additive edges. To further complicate matters, each such summarization requires, in turn, the summaries A L (t 0 , t f ) computed for other procedures!

We break the circular dependence between procedure summaries and synchronization-point summaries by iteratively computing both. In particular, we compute a sequence A L 0 A L 1 . . . of procedure summary vector addition systems along with a sequence A0A1 . . . of vector addition systems such that each A L i , for i > 0, is computed using the transitions of Ai-1, and Ai, for i ≥ 0 is computed using the procedure summaries of A L i . Initially A L 0 contains only the pending-task sets reachable without taking await transitions, and A0 contains only the transitions of AP corresponding to intraprocedural and post transitions of P , along with transitions to components A L 0 . For i ≥ 0, Ai contains transitions to and from the components A L i (t0, t f )

T [await r] n j 0 -→ q 0 , T [skip] q f , T [skip] 00 -→T [s; await r]
for each t0, t f ∈ Tasks such that j = cn(r, t0), s ∈ rvh(t f ), and q0 and q f are the unique initial and final states of A L i (t0, t f ). (We assume each component A L i (t0, t f ) has unique initial and final states, distinct from the states of other components. Additionally, we equip each A L (t0, t f ) with auxiliary state to carry the identity T [skip] of the invoking task to ensure the proper return of control when A L (t0, t f ) completes.)

At each step i > 0, we add to Ai an additive edge summarizing the execution between two synchronization points T1[await r] and T2[await r] occurring in P :

T1[skip]

PFigure 1 .

 1 Figure 1. The grammar of recursively parallel programs. Here T is an unspecified type, p ranges over procedure names, e over expressions, r over regions, and d over return-value handlers.

def=

  ∅ for all r ∈ Regs. The singleton region valuation (r → c) maps r to {c}, and r ∈ Regs \ {r} to ∅, and the union m1 ∪ m2 of region valuations is defined by the multiset union of each valuation: (m1 ∪ m2)(r) def = m1(r) ∪ m2(r) for all r ∈ Regs. The projection m | r of a region valuation m to a region sequence r is defined by m | r (r ) = m(r ) when r occurs in r, and m | r (r ) = ∅ otherwise. For expressions without program variables, we assume the existence of an evaluation function • e : Exprs → ℘(Vals) such that e = Vals. For convenience, we define e( , s, d ) def = e( ) def = e[ /l] e

  are standard. More interesting are the interprocedural transitions of Figure 3, which implicitly include a transition C[ t1, m ] → rpp/p P C[ t2, m ] whenever t1 → seq P t2.

Figure 3 .

 3 Figure 3. The tree-based transition relation for parallely-executing recursively parallel programs with task-passing.

T [if e then s 1 else s 2 T [if e then s 1 else s 2 T

 22 [s; while e do s] LOOP-END false ∈ e(T ) T [while e do s]

Figure 2 .

 2 Figure 2. The intra-procedural transition relation for recursively parallel programs.

Figure 4 .

 4 Figure 4. The stack-based transition relation for sequentiallyexecuting recursively parallel programs with task-passing.

Figure 5 .

 5 Figure 5. The stack-based transition relation for sequentiallyexecuting recursively parallel programs without task-passing.

Figure 7 .

 7 Figure 7. The transitions of the RVASS AP encoding the behavior of a finite-data recursively parallel program P .

5. 2

 2 Local-Scope Single-Wait Analysis Definition 4 (Local scope). A local-scope program is a program in which tasks only return with empty region valuations; i.e., for all reachable configurations C[ t[return e] , m ] we have m = m ∅ .

  Words & Languages A Σ-word is a finite sequence w ∈ Σ * of symbols from an alphabet Σ; the symbol ε denotes the empty word, and a language L ⊆ Σ * is a set of words. The Parikh-image Π(w) of a word w ∈ Σ * is the multiset m ∈ M[Σ] (equivalently, the vector n ∈ N |Σ| ) such that for each a ∈ Σ, m(a) (resp., , n(a)) is the number of occurrences of a in w; the Parikh-image of a language L ⊆ Σ * is the set of Parikh-images of each constituent word: Π(L) = {Π(w) : w ∈ L}. Two languages L1 and L2 are Parikh-equivalent when Π(L1) = Π(L2).

  proc main () var q_cur, q_R: Q var sym_R: Σ var done: B = false while do post r ← p d; post r ← p w(k) d; post r ← p w(k -1) d; ...; post r ← p w(1) d; ewait r; assume q_R = q0; // check: is q_cur = q f reachable here? done := true; return and an auxiliary recursive procedure p given by proc p (var sym: Σ) var q_cur, q_init, q_R: Q var sym_R: Σ q_init := ; q_cur := q_init;

P t2 of Figure 2 ,

 2 we add the transition t1 • t -→t2 • t. POST For each statement post r ← p e d occurring in P , we add a transition which transfers control directly to procedure p, T [post r ← p e d] -→t • T [skip] , where t = v, sp, d , for each v ∈ e(T ).

  inter-phase transition is taken; and for each a k ∈ Σ,  d j ∈δ + (•,a k ,•) dj   = a k =    d j ∈δ - i (•,a k ,•)

  s i | is bounded by O(|P | 5 •|Vals| 5 •|Rets|), since each of O(|Q| 2 )-many programs Φ s i (q, q ) contains O(|δ s i |) = O(|Q| 2 • |Σ|)variables and O(|Q| + |Σ|) constraints, where O(|Q|) = O(|P | • |Vals|) and O(|Σ|) = O(|P | • |Vals| • |Rets|).

7 Theorem 7 .

 77 by O(|Q| 2 • |Σ|) = O(|P | 3 • |Vals| 3 • |Rets|), our procedure is guaranteed to terminate in polynomial-time.A.7 Proof of Theorem The state-reachability problem for multi-wait finitevalue programs is polynomial-time equivalent to the configurationreachability problem for vector addition systems.

In order to isolate concurrent complexity from the exponential factor in the number of program variables, we consider a fixed number of variables in each procedure frame; this allows us a PTIME point-of-reference for state-reachability in recursive sequential programs[START_REF] Reps | Precise interprocedural dataflow analysis via graph reachability[END_REF].

Actually r must in general be chosen non-deterministically, as each revision handle may be joined either by the parent revision or its branch.

The Parikh-image of a word w over an alphabet Σ is the |Σ|-dimension vector of integers counting the number of occurrences of each symbol of Σ in w. The image of a language is the set of images of its elements.

Acknowledgments

We greatly appreciate formative discussions with Arnaud Sangnier and Peter Habermehl, and the feedback of Pierre Ganty, Giorgio Delzanno, Rupak Majumdar, Tom Ball, Sebastian Burckhardt, and the anonymous POPL reviewers.

* Partially supported by the project ANR-09-SEGI-016 Veridyc. † Supported by a post-doctoral fellowship from the Fondation Sciences Mathématiques de Paris. 0 Proofs to technical results are contained in the appendices.

A.2 Proof of Theorem 2 Theorem 2. The state-reachability problem for non-aliasing singlewait finite-value programs is PTIME-complete for a fixed number of regions, and EXPTIME-complete in the number of regions.

Though our proof only handles local-scope programs, the extension to generally-scoped programs is possibly by allowing the values of the region-container variables rg below to be returned to waiting procedures.

Proof. Let P be a non-aliasing local-scope single-wait finite-value program with regions r1, . . . , rn. We define a sequential finitevalue program Ps by a code-to-code translation of P . We extend each procedure declaration proc p (var l: T ) s with additional procedure-local variables rg, rg', and rv, where we assume each d ∈ Rets is given by an expression in which rv is a free variable. Note that for local-scope programs, the rg' array will always be equal to [ ⊥; ..; ⊥ ] and can be safely omitted from the translation. Since regions do not alias, it is not hard to show that the state-reachability problem for the resulting sequential program Ps is equivalent to the state-reachability problem for P . (Though technically we must check for reachability for a complete local valuation in Ps, including l, rg, rg', and rv, we may assume without loss of generality reachability to certain values, by adding if then rg := ; rg' := ; rv := ; assume false between every statement of Ps. Since the assume false statement cannot continue execution, this extra conditional statement has no effect on program behavior, besides making any valuation with l = reachable, if there is some reachable valuation with l = .) Proposition A.2.I. The value is reachable in P from ι if and only if is reachable in Ps from ι.

The size of Ps is polynomial in P , while the number of variables in Ps increases by n . Thus our state-reachability problem is PTIMEcomplete for fixed n since the state-reachability for sequential programs is [START_REF] Chaudhuri | Subcubic algorithms for recursive state machines[END_REF][START_REF] Reps | Precise interprocedural dataflow analysis via graph reachability[END_REF]. When the number n of regions is not fixed, this state-reachability problem becomes EXPTIME-complete, due to the logarithmic encoding of the program values into the n extra variables.

A.3 Proof of Theorem 3

Theorem 3. The state-reachability problem for local-scope singlewait finite-value programs is EXPSPACE-complete.

We show an equivalence between the state-reachability problems of local-scope single-wait recursively parallel programs and vector addition systems (VASS)-i.e., we show the problems are polynomial-time reducible to each other. EXPSPACE-completeness follows since state-reachability in VASS is known to be EXPSPACEcomplete.

Lemma A.3.I. The state-reachability problem for local-scope single-wait finite-value programs is polynomial-time reducible to the state-reachability problem for vector addition systems (VASS).

Proof sketch. To solve state-reachability in local-scope single-wait programs, we compute a sequence A0A1 . . . of non-recursive vector addition systems iteratively under-approximating the recursive system AP arising from a program P . The initial system A0 has only the transitions of AP corresponding to intra-procedural and post transitions of P . At each step i > 0, we add to Ai an additive edge summarizing an ewait transition

for some t0, t f ∈ Tasks such that j = cn(r, t0), s ∈ rvh(t f ), and n ∈ sms(t0, t f , Ai-1); since P is local-scope, every such n must equal 0. Since the number of possibly added edges is polynomial in P , the A0A1 sequence is guaranteed to reach in a polynomial number of steps a fixed-point A k whose reachable states are exactly those of AP . Thus by solving a polynomial-sized sequence of statereachability queries in polynomial-sized VASSs, we compute statereachability in local-scope single-wait programs.

Lemma A.3.II. The state-reachability problem for vector addition systems (VASS) is polynomial-time reducible to the state-reachability problem for local-scope single-wait finite-value programs.

Proof. Let k ∈ N, and let A = Q, → be a k-dimension VASS, and let q0, q f ∈ Q. We construct a single-wait program PA with an initial condition ι and target valuation f such that A(q0, q f ) = ∅ if and only if f is reachable in PA from ι.

The program PA contains only two procedures: an initial procedure main and a dummy procedure p which will be posted (resp., awaited) for each addition (resp., subtraction) performed in A. Accordingly, the region-set Regs = {r1, . . . , r k } of PA contains a region ri per vector component. The program's local variable l is used to store the control-state of A, and we set Vals = Q. Finally, let Rets = {dconst}, where dconst(v) def = l; i.e., dconst is the return-value handler which ignores the return value, keeping the local valuation intact.

We simulate the transitions of A by awaiting a task from each region ri once per decrement to the ith vector component, and subsequently posting a task to each region ri once per increment to the i th vector component. Thus for each transition dj = q n 1 n 2 -→ q , we define the statement sj given by assume l = q ewait r1; . . . ; ewait r1 Finally, the initial procedure is given by

Note the correspondence between configurations of A and PA. Each configuration q, n of A maps directly to a configuration q, s, dconst , m of PA, where s is the loop statement of the initial procedure, and |m(ri)| = n(i). Given this correspondence, it follows easily that the state q f is reachable in A from q0 if and only if the valuation f = q f is reachable in PA from ι = p main , q0 . As there are O(|A|) statements in PA per transition of A, the size of PA is O(|A| 2 ).

A.4 Proof of Theorem 4

Theorem 4. The state-reachability problem for global-scope singlewait finite-value programs is EXPSPACE-complete.

To proceed we show an equivalence between the state-reachability problems of global-scope single-wait recursively parallel programs and vector addition systems (VASS)-i.e., we show the problems are polynomial-time reducible to each other. EXPSPACE-completeness follows since state-reachability in VASS is known to be EXPSPACEcomplete.

Lemma A.4.I. The state-reachability problem for global-scope single-wait finite-value programs is polynomial-time reducible to the state-reachability problem for vector addition systems (VASS).

Proof sketch. Since each non-initial procedure p of a global-scope program cannot consume tasks, the set of tasks posted by p and recursively-called procedures along any execution from t0 to t f is a semi-linear set, described by the Parikh-image of a contextfree language. Following Ganty and Majumdar [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF]'s approach, for each t0, t f ∈ Tasks we construct a polynomial-sized vector addition system A(t0, t f ) characterizing this semi-linear set of tasks (recursively) posted between t0 and t f . Proposition A.4.I ( [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF]). For every pair t0, t f ∈ Tasks, region valuation m, and p ∈ Procs, there exists an execution of p from t0, m ∅ to t f , m if and only if there exists n ∈ N k such that n ∈ AP (t0, t f ), and m and n represent the same Parikh-image.

We use each A(t0, t f ) as a component of a non-recursive vector addition system A P representing execution of the initial frame. In particular, A P contains transitions to and from the component A(t0, t f ) for each t0, t f ∈ Tasks,

for all r ∈ Regs such that j = cn(r, t0), s ∈ rvh(t f ), and q0 and q f are the initial and final states of A(t0, t f ). We assume each A(t0, t f ) has unique initial and final states, distinct from the states of other components A(t 0 , t f ). In order to transition to the correct state T [s] upon completion, A(t0, t f ) carries an auxiliary statecomponent T [skip]. In this way, for each task t posted to region r in an execution between t0 and t f , the component A(t0, t f ) does the incrementing of the cn(r , t )-component of the region-valuation vector. As each of the polynomially-many components A(t0, t f ) are constructed in polynomial time [START_REF] Ganty | Algorithmic verification of asynchronous programs[END_REF] To proceed we show an equivalence between the state-reachability problems of single-wait recursively parallel programs and recursive vector addition systems without zero-test edges-i.e., we show the problems are polynomial-time reducible to each other. EXPSPACEhardness follows from that of non-recursive vector addition systems, and membership in 2EXPTIME follows from Demri et al. [START_REF] Demri | The covering and boundedness problems for branching vector addition systems[END_REF]'s result on branching vector addition systems (BVAS). Proof. The RVASS of AP corresponding to a program P is given by Lemma 4 of Section 3.3; since P does not contain await statements, AP does not contain zero-test edges.

Lemma A.5.II. The state-reachability problem for recursive vector addition systems A is reducible to the state-reachability problem for single-wait finite-value programs in time O(|A| 2 ).

Proof. Let k ∈ N, and let A = Q, → be a RVASS over klength vectors with additive transitions δ1 and recursive transitions δ2 (where → = δ1 δ2), and let q0, q f ∈ Q. We construct a singlewait program PA with initial condition ι and target valuation f such that A(q0, q f ) = ∅ if and only if f is reachable in PA from ι.

The program PA contains two types of procedures: a set of recursive procedure {pq : q ∈ Q} whose invocations will correspond to recursive transitions in A, and a dummy procedure pD which will be posted (resp., awaited) for each addition (resp., subtraction) performed in A. Accordingly, the region-set Regs = {r1, . . . , r k , r call } of P contains a region ri per vector component, and a call region r call . As the program's local variable l is used to store the control-state of A, we set Vals = Q. Finally, let Rets = {dconst}, where dconst(v) def = ; i.e., dconst is the returnvalue handler which ignores the return value, keeping the local valuation intact.

The top-level statement for the dummy procedure p0 is simply return ; the top-level statement for the other procedures pq for q ∈ Q will simulate all transitions of A and return only when the control-state reaches q. Let → = {d1, . . . , dn}. We define si for each di ∈ → as follows. We simulate recursive transitions by calling a procedure which may only return upon reaching q2. For each transition di = q q 1 q 2 -→q , si is given by assume l = q; call l := pq 2 q1; l := q .

We simulate the additive transitions by awaiting a task from each region ri once per decrement to the ith vector component, and subsequently posting a task to each region ri once per increment to the ith vector component. For each transition di = q n 1 n 2 -→ q , si is given by assume l = q ewait r1; . . . ; ewait r1 Finally, the top-level statement for procedure pq is while do if l = q and then return else if then s1 else if then s2 ... else if then sn else skip.

Note the correspondence between configurations of A and PA. Each frame q, n of A maps directly to a frame q, s, dconst , m of PA, where s is the top-level statement of some procedure p q , and |m(ri)| = n(i) for all i ∈ {1, . . . , k}; this correspondence extends directly to the configurations of A and PA. It follows that the state q f is reachable in A if and only if the valuation q f is reachable in PA. As there are O(|Q|) statements in PA per transition of A, the size of PA is O(|A| 2 ).

A.6 Proof of Theorem 6 Theorem 6. The state-reachability problem for local-scope multiwait single-region finite-value programs is NP-complete.

We show NP-hardness in Lemma A.6.I by a reduction from circuit satisfiability [START_REF] Papadimitriou | Computational Complexity[END_REF], and membership in NP in Lemma A.6.II by a procedure which solves a polynomial number of polynomialsized integer linear programs.

Lemma A.6.I. The circuit satisfiability problem [START_REF] Papadimitriou | Computational Complexity[END_REF] is polynomialtime reducible to the state-reachability problem for local-scope multi-wait single-region finite-value programs.

Proof. Let C be a Boolean circuit with wires W , gates G, inputs I, and an output wire w0 ∈ W . Without loss of generality, assume that each gate g ∈ G is connected to exactly two input wires and two output wires, and that each input h ∈ I is connected to exactly two wires. The circuit satisfiability problem asks if there exists a valuation to the inputs I which makes the value of write w0 true.

We construct a multi-wait single-region finite-value program PC as follows. Let Wire be the type defined as Finally, the initial procedure posts two instances of set per input h ∈ I, and two instances of set per gate g ∈ G, along with one instance of pg, then waits until every task is consumed in some sequence, where w h i ,j (resp., wg i ,j ) denotes the jth wire of input hi (resp., gate gi). The return handler dw(f,s) assigns f to fst and s to snd, and drw(f0,s0,f,s) ensures f0 = fst and s0 = snd 4 , and assigns f to fst and s to snd.

The program PC simulates C by evaluating each gate g ∈ G one-by-one at the await statement, based on an ordering such that g's input wires are active exactly when the task of procedure pg is consumed. This is possible since the setting of each input wire w ∈ W of g is also a pending task (of procedure set), which in turn can be scheduled immediately before pg. Such an execution is guaranteed to be explored since every possible ordering of pending task consumption is considered at the await statement.

We then ask if there is a reachable state in which fst.id = w0 and fst.val = true and done = true 4 We can block executions by allowing return handlers to be partial functions.

and if so, it must be the case that C is satisfiable. Inversely, if C is satisfiable then there must exist a corresponding execution of PC since every possible circuit evaluation order is considered.

Lemma A. Proof. Let A = Q, → be a k-dimension vector addition system with → = {d1, . . . , dn}, and let q0, q f ∈ Q. Instead of checking reachability of a vector n f from 0 in A, we will instead solve an equally-hard problem of checking whether 0 is reachable from an initial vector n0. To do this we construct a multi-wait program PA and a local valuation which is reachable in PA if and only if the configuration q0 is reachable from q n0 in A.

We will construct PA such that the number of pending tasks in a configuration is equal to the sum of vector components in a corresponding configuration of A. We then simulate each step of A, which subtracts n1 ∈ N k and adds n2 ∈ N k , by consuming i n1(i) tasks and posting i n2(i) tasks, while ensuring each task consumed (resp., posted) corresponds to a subtraction (resp., addition) to the correct vector-component.

For each transition di = q, n1, n2, q we define the sequence σi ∈ We assume, without loss of generality, that each transition has a non-zero decrement vector, i.e., n1 = 0 and thus |σi| > 0. We will use return-value handlers to ensure that a |σi|-length sequence of consecutively-consumed tasks corresponds the decrement of transition di. For each j ∈ {1, . . . , |σi|}, let di,j(v) be the returnvalue handler defined by assume cur_tx = i; assume cur_pos = j; if cur_pos = |σi| then assume v = true; cur_tx := ; cur_pos := 1 else assume v = false; cur_pos := cur_pos + 1, which checks that consuming a given task corresponds to a decrement (by one) of the σi(j) th component of the decrement vector of di ∈ δ. For each increment vector n (i.e., q, n1, n, q ∈ δ for some n1 ∈ N k ), or initial vector n = n0, we declare the procedure proc inc n () for var idx := 1 to k do for var cnt := 1 to n(idx) do let tx = and pos = in assume σtx(pos) = idx; post r ← p tx dtx,pos.

which posts n(m) tasks for each m ∈ {1, . . . , k}, to be consumed later by arbitrary positions j of the decrement sequences σi (since pos is assigned ) of arbitrary transitions di (since tx is assigned ) such that σi(j) = m-this ensures that the subsequent consumption of a task with handler di,j corresponds to decrementing the m th component of n. To perform the increment of transition di ∈ δ by vector n2, we declare the procedure p i , which non-deterministically calls inc n 2 , as proc p i () if then call inc n 2 (); return true else return false.

Note that the Boolean return value is used by the attached returnvalue handler di,j (for some j ∈ {1, . . . , |σi|}) to ensure that the increment is only performed once per transition di, by the lastconsumed task in the |σi|-length sequence. Finally, the initial procedure main simply adds tasks corresponding to the initial vector n0 to an initially-empty region container, then loops until every task has been consumed: proc main () var cur_tx := ; var cur_pos = 1; var empty := false; call inc n 0 (); await r; // check: is this point reachable? empty := true; return.

Checking that PA faithfully simulates A is easily done by noticing the correspondence between configurations q n of A and configurations of PA with i n pending tasks. Since empty = true is only reachable when there are no pending tasks, reachability to empty = true implies 0 is reachable in A. Furthermore, if 0 is reachable in A, a run of PA will eventually proceed past the await statement without pending tasks, setting empty = true. Proposition A.7.I. The configuration q0 is reachable in A from q n0 if and only if empty = true is reachable in PA.

Since the size of PA is polynomial in A, we have a polynomialtime reduction for deciding configuration-reachability in A.