Decidable models of integer-manipulating programs with recursive parallelism (technical report)

Matthew Hague and Anthony Widjaja Lin

Royal Holloway, University of London, UK and Yale-NUS College, Singapore

Abstract: We study safety verification for multithreaded programs with recursive parallelism (i.e. unbounded thread creation and recursion) as well as unbounded integer variables. Since the threads in each program configuration are structured in a hierarchical fashion, our model is state-extended ground-tree rewrite systems equipped with shared unbounded integer counters that can be incremented, decremented, and compared against an integer constant. Since the model is Turing-complete, we propose a decidable underapproximation. First, using a restriction similar to context-bounding, we underapproximate the global control by a weak global control (i.e. DAGs possibly with self-loops), thereby limiting the number of synchronisations between different threads. Second, we bound the number of reversals between non-decrementing and non-incrementing modes of the counters. Under this restriction, we show that reachability becomes NP-complete. In fact, it is poly-time reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our decidable approximation strictly generalises known decidable models including (i) weakly-synchronised ground-tree rewrite systems, and (ii) synchronisation/reversal-bounded concurrent pushdown systems systems with counters. Finally, we show that, when equipped with reversal-bounded counters, relaxing the weak control restriction by the notion of senescence results in undecidability.

1  Introduction

Verification of multithreaded programs is well-known to be a challenging problem. One approach that has proven effective in addressing the problem is to bound the number of context switches [38, 36]. [Recall that a context switch occurs when the CPU switches from executing one thread to executing a different thread.] When the number of context switches is fixed, one may adopt pushdown systems as a model of a single thread and show that reachability for the concurrent extension of the abstraction (i.e. multi-pushdown systems) is NP-complete [38]. This result has paved the way for an efficient use of highly optimised SMT solvers in verifying concurrent programs (e.g. see [24, 1, 19]). Note that without bounding the number of context switches the model is undecidable [37].

In the past decade the work of Qadeer and Rehof [38] has spawned a lot of research in underapproximation techniques for verifying multithreaded programs, e.g., see [24, 1, 19, 40, 5, 28, 35, 31, 22, 42, 4, 2, 6, 20, 33, 27, 42, 14] among many others. Other than unbounded recursions, some of these results simultaneously address other sources of infinity, e.g., unbounded thread creation [31, 22, 5], unbounded integer variables [24], and unbounded FIFO queues [1, 2].

Contributions.

In this paper we generalise existing underapproximation techniques [23, 31] so as to handle both shared unbounded integer variables and recursive parallelism (unbounded thread creation and unbounded recursions). The paper also provides a cleaner proof of the result in [24]: an NP upper bound for synchronisation/reversal-bounded reachability analysis of concurrent pushdown systems with counters. We describe the details below.

We adopt state-extended ground-tree rewrite systems (sGTRS) [31] as a model for multithreaded programs with recursive parallelism (e.g. programming constructs including fork/join, parbegin/parend, and Parallel.For). Ground-tree rewrite systems (GTRS) are known (see [21]) to strictly subsume other well-known sequential and concurrent models like pushdown systems [11], PA-processes [18], and PAD-processes [34], which are known to be suitable for analysing concurrent programs. [One may think of GTRS as an extension of PA and PAD processes with return values to parent threads [21].] We then equip sGTRS with unbounded integer counters that can be incremented, decremented, and compared against an integer constant.

Since our model is Turing-powerful, we provide an underapproximation of the model for which safety verification becomes decidable. First, we underapproximate the global control by a weak global control [26, 31] (i.e. DAGs possibly with self-loops), thereby limiting the number of synchronisations between different threads. To this end, we may simply unfold the underlying control-state graph of the sGTRS (see Section 3) in the standard way, while preserving self-loops. This type of underapproximation is similar to loop acceleration in the symbolic acceleration framework of [8]. Second, we bound the number of reversals between non-decrementing and non-incrementing modes of the counters [25]. Under these two restrictions, reachability is shown to be NP-complete; in fact, it is poly-time reducible to satisfaction over existential Presburger formulas, which allows one to tap into highly optimised SMT solvers. Our result strictly generalises the decidability (in fact, NP-completeness) of reachability for (i) weakly-synchronised ground-tree rewrite systems [31, 41], and (ii) synchronisation/reversal-bounded concurrent pushdown systems with counters [24].

Finally, we show one negative result that delineates the boundary of decidability. If we relax the weak control underapproximation by the notion of senescence (with age restrictions associated with nodes in the trees) [22], then the resulting model becomes undecidable.

Related Work.

Recursively-parallel program analysis was analysed in detail by Bouajjani and Emmi [10]. However, in contrast to our systems, their model does not allow processes to communicate during execution. Instead, processes hold handles to other processes which allow them to wait on the completion of others, and obtain the return value. They show that when handles can be passed to child processes (during creation) then the state reachability problem is undecidable. When handles may only be returned from a child to its parent, state reachability is decidable, with the complexity depending on which of a number of restrictions are imposed.

The work of Bouajjani and Emmi is closely related to branching vector addition systems [43] which can model a stack of counter values which can be incremented and decremented (if they remain non-negative), but not tested. While it is currently unknown whether reachability of a configuration is decidable, control-state reachability and boundedness are both 2ExpTime-complete [17].

Another variant of vector addition systems with recursion are pushdown vector addition systems, where a single (sequential) stack and several global counters are permitted. As before, these counters can be incremented and decremented, but not compared with a value. Reachability of a configuration, and control-state reachability in these models remain open problems, but termination (all paths are finite) and boundedness are known to be decidable [30]. For reachability of a configuration, an under-approximation algorithm is proposed by Atig and Ganty where the stack behaviour is approximated by a finite index context-free language [7].

Lang and Löding study boundedness problems over sequential pushdown systems [29]. In this model, the pushdown system is equipped with a counter that can be incremented, reset, or recorded. Their model differs from ours first in the restriction to sequential systems, and second because the counter cannot effect execution or be decremented: it is a recording of resource usage. These kind of cost functions have also been considered over static trees [13, 9], however, to our knowledge, they have not been studied over tree rewrite systems.

2  Preliminaries

We write ℕ to denote the set of natural numbers and ℤ the set of integers.

Trees

A ranked alphabet is a finite set of characters Σ together with a rank function ρ : Σ ↦ ℕ. A tree domain D ⊂ ℕ is a non-empty finite subset of ℕ that is both prefix-closed and younger-sibling-closed. That is, if η iD, then we also have η ∈ D and, for all 1 ≤ ji, η jD (respectively). A tree over a ranked alphabet Σ is a pair t = (D, λ) where D is a tree domain and λ : D ↦ Σ such that for all η ∈ D, if λ(η) = a and ρ(a) = n then η has exactly n children (i.e. η nD and η (n + 1) ∉ D). Let TΣ denote the set of trees over Σ.

Context Trees

A context tree over the alphabet Σ with a set of context variables x1, …, xn is a tree C = (D, λ) over Σ ⊎ {x1, …, xn} such that for each 1 ≤ in we have ρ(xi) = 0 and there exists a unique context node ηi such that λ(ηi) = xi. By unique, we mean ηi ≠ ηj for all ij. We will denote such a tree C[x1, …, xn]. Given trees ti = (Di, λi) for each 1 ≤ in, we denote by C[t1, …, tn] the tree t′ obtained by filling each variable xi with ti. That is, t′ = (D′, λ′) where

D′ = D ⋃ η1 · D1 ⋃ ⋯ ⋃ ηn · Dn    and    λ′
η




λ
η
if  η ∈ D ∧ ∀ i . η ≠ ηi 
λi
η′
if  η = ηi η′  . 

Tree Automata

A bottom-up non-deterministic tree automaton (NTA) over a ranked alphabet Σ is a tuple T = (Q, Δ, F) where Q is a finite set of states, FQ is a set of final (accepting) states, and Δ is a finite set of rules of the form (q1, …, qn) –[a]→ q where q1, …, qn, qQ, a ∈ Σ and ρ(a) = n. A run of T on a tree t = (D, λ) is a mapping π : DQ such that for all η ∈ D labelled λ(η) = a with ρ(a) = n we have (π(η 1), …, π(η n)) –[a]→ π(η). It is accepting if π(ε) ∈ F. The language defined by a tree automaton T over alphabet Σ is a set L(T) ⊆ TΣ of trees over which there exists an accepting run of T.

Parikh images

Given an alphabet Σ = {γ1,…,γn} and a word w ∈ Σ*, we write P(w) to denote a mapping ρ: Σ → ℕ, where ρ(a) is defined to be the number of occurrences of a in w. Given a language L ⊆ Σ*, we write P(L) to denote the set {P(w) | wL}. We say that P(L) is the Parikh image of L.

Presburger Arithmetic

Presburger formulas are first-order formulas over integers with addition. Here, we use existential Presburger formulas ϕ(x,y) := ∃ x ϕ, where (i) x and y are sets of variables, and (ii) ϕ is a boolean combination of expressions ∑i=1m aizib for variables z1,…,zmxy, constants a1,…,am,b∈ ℤ, and ∼ ∈ {≤,≥,<,>,=} with constants represented in binary. A solution to ϕ is a valuation b: y ↦ ℤ to y such that ϕ(x,b) is true. The formula ϕ is satisfiable if it has a solution. Satisfiability of existential Presburger formulas is known to be NP-complete [39].

3  Formal Models

In this section, we will define our formal models, which are based on ground-tree rewrite systems. Ground-tree rewrite systems (GTRSs) [15] permit subtree rewriting where rules are given as a pair of ground-trees. In the sequel, we use the extension proposed by Löding [32] where NTA (instead of ground trees) appear in the rewrite rules. Hence, a single rule may correspond to an infinite number of concrete rules (i.e. containing concrete trees).

Ground Tree Rewrite Systems with State and Reversal Bounded Counters.

To capture synchronisations between different subthreads, we follow [31, 26, 41] and extend GTRS with state (a.k.a. global control). The resulting model is denoted by sGTRS (state-extended GTRS). To capture integer variables, we further extend the model with unbounded integer counters, which can be incremented, decremented, and compared against an integer constant. Since Minsky’s machines can easily be encoded in such a model, we apply a standard underapproximation technique: reversal-bounded analysis of the counters [23, 25]. This means that one only analyses executions of the machines whose number of reversals between nondecrementing and nonincrementing modes of the counters is bounded by a given constant r ∈ ℕ (represented in unary). The resulting model will be denoted by rbGTRS. We will now define this model in more detail.

An atomic counter constraint on counter variables C = {c1,…,ck} is an expression of the form civ, where v ∈ ℤ and ∼ ∈ {<,≤,=,≥,>}. A counter constraint θ on C is a boolean combination of atomic counter constraints on C. Given a valuation ν : C ↦ ℤ to the counter variables, we can determine whether θ[ν] is true or false by replacing a variable c by ν(c) and evaluating the resulting boolean expressions in the obvious way. Let ConsC denote the set of all counter constraints on C. Intuitively, these formulas will act as guards to determine whether certain transitions can be fired. Given two counter valuations ν and µ we define ν + µ as the pointwise addition of the valuations. That is, (ν + µ)(c) = ν(c) + µ(c).

Given a sequence of counter values, a reversal occurs when a counter switches from being incremented to being decremented or vice-versa. For example, if the values of a counter c along a run are 1,1,1,2,3,4,4,4,3,2,2,3, then the number of reversals of c is 2 (reversals occur in between the overlined positions). A sequence of valuations is reversal-bounded whenever the number of reversals is the sequence is bounded.

Definition 1 (r-Reversal-Bounded)   For a counter c from a set of counters C, a sequence ν1, …, νn of counter valuations over C is r-reversal-bounded for c whenever we can partition ν1, …, νn into (r+1) sequences A1, …, Ar+1 (with ν0, …, νn = A1, …, Ar+1) such that for all 1 ≤ ir there is some ∼ ∈ {≤, ≥} such that for all νj, νj+1 appearing together in Ai, we have νj(c) ∼cνj+1(c).

We define sGTRS with reversal-bounded counters.

Definition 2 (sGTRSs with r-Reversal-Bounded Counters (rbGTRS))   A state-extended ground tree rewrite system with r-reversal-bounded counters (rbGTRS) is a tuple G = (P, Σ, Γ, R, C, r) where P is a finite set of control-states, Σ is a finite ranked alphabet, Γ is a finite alphabet of output symbols (i.e. transition labels), C is a finite set of counters, R is a finite set of rules of the form (p1, T1, θ) –[γ]→ (p2, T2, µ) where p1, p2P, γ ∈ Γ, θ ∈ ConsC, µ ∈ C ↦ ℤ, and T1, T2 are NTAs over Σ.

In the sequel, we will omit mention of the number r in the tuple G if it is clear from the context.

A configuration of an sGTRS with counters is a tuple α = (p, t, ν) where p is a control-state, t a tree, and ν a valuation of the counters. We have a transition (p1, t1, ν1) –[γ]→ (p2, t2, ν2) whenever there is a rule (p1, T1, θ) –[γ]→ (p2, T2, µ) ∈ R such that: (i) (dynamics of counters) θ[ν1] is true and ν2 = ν1 + µ, and (ii) (dynamics of trees) t1 = C[t1] for some context C and tree t1L(T1) and t2 = C[t2] for some tree t2L(T2). A run π over γ1…γn−1 is a sequence

    
p1t1, ν1
–[γ1]→  ⋯ –[γn−1]→  
pntn, νn

such that for all 1 ≤ i < n we have (pi, ti, νi) –[γi]→ (pi+1, ti+1, νi+1) is a transition of G and for each cC the sequence ν1, …, νn is r-reversal-bounded for c. We say that γ1…γn−1 is the output string of π. We write (p, t, ν) –[γ1…γn]→ (p′, t′, ν′) (or simply (p, t, ν) →* (p′, t′, ν′)) whenever there is a run from (p, t, ν) to (p′, t′, ν′) over γ1…γn. Let ε denote the empty output symbol.

Whenever we wish to discuss sGTRSs without counters, we simply omit the counter components. That is, we have configurations of the form (p, t) and transitions of the form (p1, T1) –[γ]→ (p2, T2). The standard notion of GTRS (i.e. not state-extended) [32] is simply sGTRS without counters with only one state.

We next define the problems of (global) reachability. To this end, we use a tree automaton T (resp. an existential Presburger formula ϕ) to represent the tree (resp. counter) component of a configuration. More precisely, a symbolic config-set of an rbGTRS G = (P, Σ, Γ, R, C, r) is a tuple (p, T, ϕ), where pP, T is an NTA over Σ, and ϕ(x) is an existential Presburger formula with free variables x = {xc}cC (i.e. one free variable for each counter). Each symbolic config-set (c, T, ϕ) represents a set of configurations of G defined as follows: [[(p, T, ϕ) ]] := { (p, t, ν) : tL(T), ϕ(ν) is true }. Global Reachability

Input: an rbGTRS G and two symbolic config-sets (p1, T1, ϕ1) (p2, T2, ϕ2)

Problem: Decide whether (p1, t1, ν1) →* (p2, t2, ν2), for some (p1, t1, ν1) ∈ [[(p1, T1, ϕ1) ]] and (p2, t2, ν2) ∈ [[(p2, T2, ϕ2) ]] The problem of control-state reachability can be defined by restricting (i) the tree automata T1 and T2 to accept, respectively, a singleton tree and the set of all trees, and (ii) the solutions to the formulas ϕ1 and ϕ2 are, respectively, {ν0} (where ν0 is the valuation assigning 0 to all counters) and the set of all counter valuations.

Remark 1   When we measure the complexity of reachability for rbGTRS, the number r of reversals is represented in unary, while the numbers in counter constraints and valuations are represented in binary. This is consistent with the standard representation of numbers in previous work on reversal-bounded counter machines (e.g. see [23, 24]). The unary representation for r can be justified by the fact that bugs can often be discovered within a small number of reversals.

Weakly Synchronised Ground Tree Rewrite Systems

The control-state and global reachability problems for sGTRS are known to be undecidable [12, 21]. The problems become NP-complete for weakly-synchronised sGTRS [31, 41], where the underlying control-state graph (where there is an edge between p1 and p2 whenever there is a transition (p1, T1) –[γ]→ (p2, T2)) may only have cycles of length 1 (i.e. self-loops), i.e., a DAG (directed acyclic graph) possibly with self-loops. Underapproximation by a weak control is akin to loop acceleration in the symbolic acceleration framework of [8]. We extend the definition to rbGTRSs. The original definition can be easily obtained by omitting the counter components.

We define the underlying control graph of an rbGTRS G = (P, Σ, Γ, R, C) as a tuple (P, Δ) where Δ = {(p1, p2) | (p1, T1, θ) –[γ]→ (p1, T2, µ) ∈ R} .

Definition 3 (Weakly-Synchronised rbGTRS)   An rbGTRS is weakly synchronised if its underlying control graph (P, Δ) is a DAG possibly with self-loops.

4  Decidability

In this section we will prove the main result of the paper:

Theorem 1   Global reachability for weakly synchronised rbGTRS is NP-com-
plete. In fact, it is poly-time reducible to satisfiability over existential Presburger formulas.

To prove this theorem, we fix notation for the input to the problem: an rbGTRS G = (P, Σ, Γ, R, C, r) and two symbolic config-sets (p1, T1, ϕ1), (p2, T2, ϕ2) of G. Let C = {ci}i=1k. The gist of the proof is as follows. From G, we construct a new sGTRS G′ (without counters) by encoding the dynamics of the counters in the output symbols of G′. Of course, G′ has no way of comparing the values of counters with constants. [In this sense, G′ only overapproximates the behavior of G.] To deal with this problem, we use the result of [31] to compute an existential Presburger formula ψ capturing the Parikh images of the set of all output strings of G′ from (p1, T1, ϕ1) to (p2, T2, ϕ2). The final formula is ψ ∧ ψ′, where ψ is a constraint asserting that the desired counter comparisons are performed throughout runs of G′. We sketch the details of the construction below.

Modes of the counters.

The first notion that is crucial in our proof is that of mode of a counter [23, 25], which is an abstraction of the values of a counter in a run of an rbGTRS containing three pieces of information: (i) the region of the counter value (i.e. how it compares to constants occurring in counter constraints), (ii) the number of reversals that has been performed by each counter (between 0 and r), and (iii) whether a counter is currently non-decrementing (↑) or non-incrementing (↓). A mode vector is simply a k-tuple of modes, one mode for each of the k counters. We now formalise these notions.

Let d1 < … < dm be the integer constants appearing in the counter constraints in G. This sequence of constants gives rise to the set REG of regions defined as REG := { A0,…,Am, B1,…,Bm}, where Bi := {di} (where 1 ≤ im), Ai := { n ∈ ℤ: di < n < di+1 } (where 1 ≤ i < m), A0 := { n ∈ ℤ: n < d1 }, and Am := { n ∈ ℤ: n > dm }. A mode is simply a tuple in REG × [0,r] × {↑,↓}. A mode vector is simply a tuple in Modes := REGk × [0,r]k × {↑,↓}k.

Building the sGTRS G′.

We might be tempted to build G′ by first removing the counters from G and then embedding Modes into the control-states G′. This, however, causes two problems. First, the number of control-states becomes exponential in k. Second, the resulting system is no longer weakly synchronised even though G originally was weakly synchronised. To circumvent this problem, we adapt a technique from [23]. Every run π of G from (p1, T1, ϕ1) to (p2, T2, ϕ2) can be associated with a sequence σ of mode vectors recording the information (i)–(iii) for each counter. The crucial observation is that there are at most Nmax := 2mk(r+1) different mode vectors in σ. This is because a counter can only go through at most 2m regions without incurring a reversal. For this reason, we may use the control-states of G′ to store the number of mode vectors that G has gone through, while the actual mode vector guessed by G′ will be made “visible” in the output strings of G′. That way, we can use an additional existential Presburger formula ψ′ (see below) to enforce that the run of G′ faithfully simulates runs of G. In addition, the shape of the control-states (DAG with self-loops) of G′ is preserved. [The product graph of two DAGs with self-loops is also a DAG with self-loops.] We detail the construction below.

Define the weakly-synchronised sGTRS G′ = (P′, Σ, Γ′, R′) as follows. Let P′ := P × [0,Nmax]. The output alphabet Γ′ is defined as Γ × R × [0,Nmax] × {0,1}, where the boolean flag is used to denote whether the transition taken changes the mode. We define R′ as follows. For each rule τ = (p, T, θ) –[γ]→ (p′, T′, µ) in R, we add the rule ((p,i), T) –[(γ,τ,i,0)]→ ((p′,i), T′) for each i ∈ [0,Nmax], and ((p,i), T) –[(γ,τ,i,1)]→ ((p′,i+1), T′) for each i ∈ [0,Nmax). Since G is weakly-synchronised and the mode counter never decreases, it follows that G′ is weakly-synchronised too. Note also that this construction can be performed in polynomial-time.

Constructing the formula ψ ∧ ψ′.

As we mentioned, ψ is an existential Presburger formula encoding the Parikh image P(L) of the set L of all output strings of G′ from ((p1,0), T1) to (S, T2), where S = {p2} × [0,Nmax]. More precisely, the set z of free variables of ψ include za for each a ∈ Γ′. Furthermore, for each valuation µ ∈ z ↦ ℤ, it is the case that ψ(µ) is true iff µ ∈ P(L). Such a formula is known to be polynomial-time computable since G′ is a weakly-synchronised sGTRS [31].

Recall that ψ′ should assert that the desired counter comparisons are performed throughout runs of G′. To this end, the formula ψ′ will have extra variables for guessing the existence of a sequence of Nmax distinct mode vectors through runs of G′. More precisely, the formula ψ′ is the conjunction

ϕ1(x) ∧ ϕ2(y) ∧ Dom(m0,…,mNmax) ∧ Init(m0) ∧
GoodSeq(m0,…,mNmax) ∧ Respect(z,m0,…,mNmax) ∧ EndVal(x,y,z).

The set x consists of variables xi (1 ≤ ik) which contain the initial value of the ith counter. Similarly, the set y consists of variables yi (1 ≤ ik) which contain the final value of the ith counter. Each mi denotes a set of variables for the ith mode vector defined as follows:

We detail each subformula below.

The subformula Dom asserts that each variable in mi (for each i) has the right domain (i.e. range of integer values). More precisely, for each j ∈ [1,k], we add the conjuncts: (i) 0 ≤ regji ≤ 2m, (ii) 0 ≤ revjir, and (iii) 0 ≤ arrji ≤ 1. For the first constraint, we use an even number of the form 2i to represent the region Ai, and an odd number 2i−1 to represent the region Bi. The last constraint simply encodes non-decrementing (↑) as 1, and non-incrementing (↓) as 0.

The subformula Init asserts that m0 is an initial mode vector. More precisely, for each j ∈ [1,k], we add the conjuncts revj0 = 0.

The subformula GoodSeq asserts that m0,…,mNmax forms a valid sequence of mode vectors. More precisely, for each i ∈ [0,Nmax) and each j ∈ [1,k], we add the conjuncts: (i) arrjiarrji+1revji+1 = revji+1, (ii) arrji = arrji+1revji+1 = revji, (iii) regji < regji+1arrji+1 = 1, and (iv) regji > regji+1arrji+1 = 0. For example, the first constraint asserts that a change in the direction (non-incrementing or non-decrementing) of the counter incurs one reversal. The other constraints are similar.

The subformula Respect asserts that the Parikh image z of the run of G′ respects the sequence m0,…,mNmax of mode vectors. In effect, this subformula ensures that G′ faithfully simulates G. Firstly, we need to assert that the jth counter values at the start and at the end of the ith mode of G′ (which are encoded in z) are in the right regions regji. To state this more precisely, for each rule τ = (p, T, θ) –[γ]→ (p′, T′, µ) in R, we let µj(τ) denote the value µ(cj). For each i ∈ [0,Nmax] and j ∈ [1,k], we denote by the notation StartCounterji the term xj + ∑s=0i−1(γ,τ,s,l) µj(τ) × z(γ,τ,s,l), where γ, τ, and l, range over, respectively, Γ, R, and {0,1}. Similarly, we denote by EndCounterji the term StartCounterji + ∑(γ,τ,i,0) µj(τ) × z(γ,τ,i,0). We add the conjuncts: (i) regji = 2hEndCounterjiAh, for each h ∈ [0,m], and (ii) regji = 2h+1 ⇒ EndCounterjiBh, for each h ∈ [0,m). [Note that formulas of the form gA, for a Presburger term g and a set S ∈ {A0,…,Am,B1,…,Bm}, can be easily replaced by quantifier-free Presburger formulas, e.g., gA0 stands for g < d1.] To ensure that the initial condition is correct, for each j ∈ [1,k], we add the following conjuncts: (1) StartCounterj0Ahregj0 = 2h, and (2) StartCounterj0Bhregj0 = 2h+1. Secondly, we need to state that the transitions executed in each mode are valid (i.e. satisfy the counter constraints). More precisely, for each γ ∈ Γ, τ ∈ R, i ∈ [0,Nmax], and l ∈ {0,1}, if θ is the counter constraint in τ, we add the conjunct z(γ,τ,i,l) > 0 ⇒ θ(StartCounter1i,…,StartCounterki). Next we assert that, when the jth counter is non-incrementing (resp. non-decrementing), only non-negative (resp. non-positive) counter increments are permitted. More precisely, for each i ∈ [0,Nmax], j ∈ [1,k], l ∈ {0,1}, and τ ∈ R, if µj(τ) > 0, then add the conjunct arrji = 0 ⇒ z(γ,τ,i,l) = 0; if µj(τ) < 0, then add the conjunct arrji = 1 ⇒ z(γ,τ,i,l) = 0.

Finally, the subformula EndVal simply asserts that, starting from the initial counter value x and following the transitions z, the end counter values are y. To this end, we can simply add the conjunct yj = EndCounterjNmax for each j ∈ [1,k].

This concludes the formula construction. It is immediate that G′ faithfully simulates G iff ψ ∧ ψ′ is true. In addition, the formula construction runs in polynomial-time. Since satisfiability over existential Presburger formulas is NP-complete [39], the NP upper bound for Theorem 1 follows. NP-hardness already holds for the restricted model where the tree component is a stack [23].

5  Senescent Ground-Tree Rewrite Systems

A natural question arising from the result on weakly synchronised rbGTRS is whether the “weakly synchronised” restriction can be relaxed while maintaining decidability. It is known that allowing arbitrary underlying control-state graphs leads to undecidability of reachability even without reversal bounded counters. In this section we explore the notion of senescence [22], which is more general than the weakly synchronised restriction, but still permits a decidable reachability problem (without counters). After giving the formal definition of senescent GTRS, we show the following result.

Theorem 2 (Control-State Reachability of Senescent rbGTRS)   The control-state reachability problem for senescent rbGTRS is undecidable.

5.1  Model Definition

Senescence allows the underlying control-state graph to have arbitrary cycles (instead of only self-loops). For sGTRS, control-state reachability is decidable under an “age restriction” that is imposed on the nodes that can be rewritten. That is, when the control-state changes, the nodes in the tree age by one timestep. Once a node reaches an a priori fixed age r, it becomes fixed (i.e. cannot be rewritten by further transitions in the run).



Figure 1: A transition changing the control-state.

 

Figure 2: A transition that does not change the control-state.

Figure 3: Transitions of a senescent GTRS.

Before the formal definition, two example transitions of a senescent rbGTRS are shown in Figure 3. A configuration is written as its control-state and counter values ((p, ν) or (p′, ν′)) with the tree appearing below. In the tree, the label of each node appears in the centre of the node. The ages of each node is depicted as a subscript on the right. Dotted lines are used to indicate the part of the tree rewritten by a rule. In Figure 1 the transition changes the control-state, causing the age of the nodes that are not rewritten to increase by 1. The rewritten nodes are given the age 0 as they are new, fresh, nodes. The situation when the control-state does not change is shown in Figure 2. In this case, the nodes that are not rewritten maintain the same age. The senescence restriction disallows runs where nodes older than a fixed age are rewritten.

More formally, given a run

    
p1t1, ν1
–[γ1]→  ⋯ –[γn−1]→ 
pntn, νn

of an rbGTRS, let C1, …, Cn−1 be the sequence of tree contexts used in the transitions from which the run was constructed. That is, for all 1 ≤ i < n, we have ti = Ci[tiout] and ti+1 = Ci[ti+1in] where (pi, Ti, θi) –[γi]→ (pi+1, Ti, µi) was the rewrite rule used in the transition and tioutL(Ti), ti+1inL(Ti) were the trees that were used in the tree update.

For a given position (pi, ti, νi) in the run and a given node η in the domain of ti, the birthdate of the node is the largest 1 ≤ ji such that η is in the domain of Cj[tjin] and η is in the domain of Cj[x] only if its label is x. The age of a node is the cardinality of the set {i′ | ji′ < ipipi′+1}. That is, the age is the number of times the control-state changed between the jth and the ith configurations in the run.

A lifespan-restricted run with a lifespan of r is a run such that each transition (pi, Ci[tiout], νi) –[γi]→ (pi+1, Ci[ti+1in], νi+1) has the property that all nodes η in tiout have an age of at most r. That is, more precisely, that all nodes η in the domain of Ci[tiout] but only in the domain of Ci[x] if the label is x have an age of at most r.

Definition 4 (Senescent rbGTRS)   A senescent rbGTRS with lifespan r is an rbGTRS G = (P, Σ, R, C) where runs are lifespan-restricted with a lifespan of r.

Note that the senescence restriction is weaker than the weakly-synchronised restriction in that the number of times the finite control could change state is unbounded. In fact, a node could be affected by an unbounded number of control-state changes so long as it is always rewritten without becoming fixed (i.e. reaches age r).

5.2  Undecidability

We show control-state reachability for senescent rbGTRSs is undecidable in the appendix, and give the intuition here. In the following, we refer to nodes whose age is within the age bound as live. We refer to nodes that are not live as fixed. Note, each time a node is rewritten, its age is reset to zero. Thus, we can keep leaves of the tree live by allowing them to rewrite to themselves. That is, for all symbols a we wish to keep live and all control-states p, we have a transition (p, a, θ) –[γ]→ (p, a, µ) where θ is a formula that is always satisfied, and µ assigns 0 to all counters (i.e. the rule does not depend on, nor change the counter values). In addition, by omitting the above rules for certain control-states, we can prevent a node from keeping itself fresh in certain situations.

We follow the proof that reachability for reset Petri nets is undecidable [3]. We simulate a two-counter machine. Testing whether such a machine can reach a given control-state while having counters with value zero is undecidable.

Let the two counters be c1 and c2. In the tree, we track the value of a counter c ∈ {c1, c2} by the number of live leaves labelled with the counter name c. E.g. the tree •(c1, •(c2, ∗)) represents the situation where both counters have value 1, assuming these leaves are live. We will always use internal nodes labelled •. The node ∗ is for adding new leaves when required. To increment a counter we add a new leaf labelled c. To decrement a counter, we rewrite a leaf labelled c to a null label. Thus, we can easily increment and decrement counters. Zero tests, however, are more subtle. To help with this, we track, using reversal-bounded counters, the number of increments made to each counter, and in separate reversal-bounded counters, the number of decrements. That is, we have reversal bounded counters {c1+,c1,c2+,c2}. When we simulate an increment of c1 we add a leaf and increment c1+. When we simulate a decrement of c2 we rewrite a leaf to a null character and increment c1. Similarly for c2. We simulate zero tests as follows.

To simulate a zero test on a counter c we perform the following checks. First, we “reset” the counter to zero by forcing enough control-state changes to fix the nodes corresponding to the counter. That is, we move to a control-state p where all leaf labels may rewrite to themselves, except those labelled c. After the move to p all leaves will have age 1. Leaves not labelled c can refresh their age to 0 by rewriting themselves. Leaves labelled c will stay aged 1. Then, we move to the target control-state of the transition we are simulating. Thus, after these moves, all leaves labelled c will reach age 2, while all other nodes will only reach age 1. Thus, if our lifespan is 2, nodes labelled c will no longer be live. That is, the simulated value of c in the tree has been forced to 0.

After this reset operation, the counter value is definitely zero. However, we did not enforce that the counter value was zero before the transition. Recall, we track the number of increments and decrements to c in the reversal bounded counters. If the counter was not zero before the test, there will be a discrepancy with the reversal bounded counters: more increments will be recorded than decrements. E.g. for counter c1 we will have c1+ > c1. This cannot be corrected by the simulation. Thus, at the end of the run, we check whether the number of increments is equal to the number of decrements. If not, we know the run made a spurious transition. That is, it performed a zero test transition when the counter was not zero. If no spurious transitions were made, we know the two-counter machine has a corresponding run. This completes the gist of the simulation of a two-counter machine.

6  Extensions and Future Work

We proposed sGTRS with counters as a model of recursively parallel programs with unbounded recursion, thread creation, and integer variables. To obtain decidability, we gave an underapproximation in the form of weak sGTRS with reversal-bounded counters. We showed that the reachability problem for this model is NP-complete; in fact, polynomial-time reducible to satisfiability of linear integer arithmetic, for which highly optimised SMT solvers are available (e.g. Z3 [16]). Additionally, we explored the possibility of relaxing the weakly-synchronised constraint to that of senescence, and showed that the resulting model has an undecidable control-state reachability problem.

One possible avenue of future work is to investigate what happens when local integer values are permitted. That is, reversal-bounded counters can be stored on the nodes of the tree. We may also study techniques that allow nodes to contain multiple labels, permitting the modelling of multiple local variables without an immediate exponential blow up.

Acknowledgments

We thank anonymous reviewers for their helpful feedback. This work was supported by the Engineering and Physical Sciences Research Council [EP/K009907/1] and Yale-NUS College Startup Grant.

References

[1]
Parosh Aziz Abdulla, Mohamed Faouzi Atig, and Jonathan Cederberg. Analysis of message passing programs using SMT-solvers. In ATVA, pages 272–286, 2013.
[2]
C. Aiswarya, P. Gastin, and K. Narayan Kumar. Verifying communicating multi-pushdown systems via split-width. In ATVA, pages 1–17, 2014.
[3]
T. Araki and T. Kasami. Some Decision Problems Related to the Reachability Problem for Petri Nets. Theoretical Computer Science, 3(1):85–104, 1977.
[4]
M. F. Atig, B. Bollig, and P. Habermehl. Emptiness of multi-pushdown automata is 2etime-complete. In DLT, pages 121–133, 2008.
[5]
M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent programs with dynamic creation of threads. Logical Methods in Computer Science, 7(4), 2011.
[6]
M. F. Atig, K. Narayan Kumar, and P. Saivasan. Adjacent ordered multi-pushdown systems. Int. J. Found. Comput. Sci., 25(8):1083–1096, 2014.
[7]
Mohamed Faouzi Atig and Pierre Ganty. Approximating petri net reachability along context-free traces. In FSTTCS, pages 152–163, 2011.
[8]
S. Bardin, A. Finkel, J. Leroux, and P. Schnoebelen. Flat acceleration in symbolic model checking. In ATVA, pages 474–488, 2005.
[9]
Achim Blumensath, Thomas Colcombet, Denis Kuperberg, Pawel Parys, and Michael Vanden Boom. Two-way cost automata and cost logics over infinite trees. In CSL-LICS, pages 16:1–16:9, 2014.
[10]
A. Bouajjani and M. Emmi. Analysis of recursively parallel programs. ACM Trans. Program. Lang. Syst., 35(3):10, 2013.
[11]
Ahmed Bouajjani, Javier Esparza, and Oded Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, pages 135–150, 1997.
[12]
Laura Bozzelli, Mojmír Kretínský, Vojtech Rehák, and Jan Strejcek. On decidability of LTL model checking for process rewrite systems. Acta Inf., 46(1):1–28, 2009.
[13]
Thomas Colcombet and Christof Löding. Regular cost functions over finite trees. In LICS, pages 70–79, 2010.
[14]
Wojciech Czerwinski, Piotr Hofman, and Slawomir Lasota. Reachability problem for weak multi-pushdown automata. Logical Methods in Computer Science, 9(3), 2013.
[15]
M. Dauchet and S. Tison. The theory of ground rewrite systems is decidable. In LICS, pages 242–248, 1990.
[16]
L. Mendonça de Moura and N. Bjørner. Z3: An efficient smt solver. In TACAS, pages 337–340, 2008.
[17]
Stéphane Demri, Marcin Jurdzinski, Oded Lachish, and Ranko Lazic. The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci., 79(1):23–38, 2013.
[18]
J. Esparza and A. Podelski. Efficient algorithms for pre* and post* on interprocedural parallel flow graphs. In POPL, pages 1–11, 2000.
[19]
Javier Esparza, Pierre Ganty, and Tomás Poch. Pattern-based verification for multithreaded programs. ACM Trans. Program. Lang. Syst., 36(3):9:1–9:29, 2014.
[20]
P. Ganty, R. Majumdar, and M. Monmege. Bounded underapproximations. FMSD, 40(2), 2012.
[21]
Stefan Göller and Anthony Widjaja Lin. Refining the process rewrite systems hierarchy via ground tree rewrite systems. In CONCUR, pages 543–558, 2011.
[22]
M. Hague. Senescent ground tree rewrite systems. In CSL-LICS, pages 48:1–48:10, 2014.
[23]
M. Hague and A. W. Lin. Model checking recursive programs with numeric data types. In CAV, pages 743–759, 2011.
[24]
Matthew Hague and Anthony Widjaja Lin. Synchronisation- and reversal-bounded analysis of multithreaded programs with counters. In CAV, pages 260–276, 2012.
[25]
Oscar H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116–133, 1978.
[26]
Mojmír Kretínský, Vojtech Rehák, and Jan Strejcek. Extended process rewrite systems: Expressiveness and reachability. In CONCUR, pages 355–370, 2004.
[27]
Salvatore La Torre, Margherita Napoli, and Gennaro Parlato. Scope-bounded pushdown languages. In DLT, pages 116–128, 2014.
[28]
A. Lal, T. Touili, N. Kidd, and T. Reps. Interprocedural analysis of concurrent programs under a context bound. In TACAS, pages 282–298, Berlin, Heidelberg, 2008. Springer-Verlag.
[29]
Martin Lang and Christof Löding. Modeling and verification of infinite systems with resources. Logical Methods in Computer Science, 9(4), 2013.
[30]
Jérôme Leroux, M. Praveen, and Grégoire Sutre. Hyper-ackermannian bounds for pushdown vector addition systems. In CSL-LICS, pages 63:1–63:10, 2014.
[31]
A. W. Lin. Weakly-synchronized ground tree rewriting (with applications to verifying multithreaded programs). In MFCS, pages 630–642, 2012.
[32]
C. Löding. Reachability problems on regular ground tree rewriting graphs. Theory Coput. Syst., 39(2):347–383, 2006.
[33]
P. Madhusudan and Gennaro Parlato. The tree width of auxiliary storage. In POPL, pages 283–294, 2011.
[34]
R. Mayr. Decidability and Complexity of Model Checking Problems for Infinite-State Systems. PhD thesis, TU-Munich, 1998.
[35]
M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In PLDI, pages 446–455, 2007.
[36]
S. Qadeer. The case for context-bounded verification of concurrent programs. In SPIN, pages 3–6, 2008.
[37]
G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. Transactions on Programming Languages and Systems (TOPLAS), 2000.
[38]
S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software. In TACAS, pages 93–107, 2005.
[39]
Bruno Scarpellini. Complexity of subcases of Presburger arithmetic. Trans. of AMS, 284(1):203–218, 1984.
[40]
D. Suwimonteerabuth, J. Esparza, and S. Schwoon. Symbolic context-bounded analysis of multithreaded java programs. In SPIN, pages 270–287, 2008.
[41]
Anthony Widjaja To and Leonid Libkin. Algorithmic metatheorems for decidable LTL model checking over infinite systems. In FOSSACS, pages 221–236, 2010.
[42]
S. La Torre, P. Madhusudan, and G. Parlato. A robust class of context-sensitive languages. In In LICS, pages 161–170. IEEE Computer Society, 2007.
[43]
Kumar Neeraj Verma and Jean Goubault-Larrecq. Karp-Miller trees for a branching extension of VASS. Discrete Mathematics & Theoretical Computer Science, 7(1):217–230, 2005.

A  Proofs and Definitions for Senescent sGTRS

We show that the control-state reachability problem is undecidable via a reduction from the reachability problem for two-counter machines.

A two-counter machine is a tuple M = (S, Δ) where P is a finite set of control-states, Δ is a finite set of rules of the form p1 –[op, ]→ p2 where p1, p2S, and op ∈ {inc1, inc2, dec1, dec2, zero1, zero2}. A configuration of M is a tuple (p, v0, v1) ∈ S × ℕ × ℕ. We have a transition (p1, v01, v11) —→ (p2, v02, v12) if we have a rule p1 –[op, ]→ p2 and

Let ν0 be the valuation assigning 0 to all counters. For given two-counter machine M and control-states s0 and sf we define a senescent rbGTRS GM such that there is a run

    
s0T0, ν0
–[ε]→  ⋯ –[ε]→ 
sfT, ν

for some T and ν iff there is a run

    
p0, 0, 0
—→ ⋯ —→
pf, 0, 0

of M. Since this latter problem is well-known to be undecidable, we obtain undecidability of control-state reachability for senescent rbGTRS.

In the following definition we use the following 1-reversal-bounded counters: c0+, c1+, c0 and c1. We use Rfresh to keep leaf nodes within the lifespan, Rinc, Rdec, and Rzero to simulate the counter operations, and Rfin to check ci+ = ci for both i at the end of the run. Furthermore, let

    
µi+
c
=


1c = ci+ 
0otherwise, 
µi
c
=


1c = ci 
0otherwise, and 
µi=
c
=




−1
c ∈ 

ci+,ci

0otherwise. 
 

Recall ν0 maps all counters to zero.

Given a node η and trees t1, …, tn, we will often write η(t1, …, tn) to denote the tree with root node η and left-to-right child sub-trees t1, …, tn. When η is labelled a, we may also write a(t1, …, tn) to denote the same tree. We will often simply write a to denote the tree with a single node labelled a.

For a tree t, let Tt be an NTA accepting only t. For example, Ta(b) is the automaton accepting only the tree a(b), and Ta accepts only the tree containing a single node labelled a. Note, we do not use natural numbers as tree labels, hence T1, T2, … may range over all NTAs.

Definition 5 (GM)   Given a two-counter machine M = (S, Δ) and two control-states s0, sfS, we define a senescent rbGTRS with lifespan 1
        GM
P, Σ, Γ, RC
where
        
P =
S ⊎ 


si
 | 
s ∈ S ∧ i ∈ 

0,1



⊎ 

fp=

Σ =


•, ∗, ∘, 
1
2


Γ =


ε

C =


c1+c2+c1c2

R =Rfresh ⋃ Rinc ⋃ Rdec ⋃ Rzero ⋃ Rfin 
 
where
Rfresh =



sTη, ⊤
–[ε]→ 
sTη, ν0
 | 
s ∈ S ∧ η ∈ 

∗, 
1
2




 ⋃ 
  




si
Tη, ⊤
–[ε]→ 

si
Tη, ν0
 | 
s ∈ S ∧ η ∈ 

∗, 
1
2


∖ 

i




Rinc =



s1T, ⊤
–[ε]→ 

s2
T
 


i
, ∗

, µi+

 | p1 –[inci, ]→  p2 ∈ Δ

Rdec =




s1
T
 
i
, ⊤

–[ε]→ 
s2T, µi
 | p1 –[deci, ]→  p2 ∈ Δ

Rzero =




 

s1T, ⊤
–[ε]→ 

s2i
T, ν0


s2i
T, ⊤
–[ε]→ 
s2T, ν0
 
 |  p1 –[zeroi, ]→  p2 ∈ Δ 



Rfin =









sfT, ⊤
–[ε]→ 
p=T, ν0

p=T, ⊤
–[ε]→ 
p=T, µ0=

p=T, ⊤
–[ε]→ 
p=T, µ1=

p=Tc0+ = 0 ∧ c0 = 0 ∧ c1+ = 0 ∧ c1 = 0
–[ε]→ 
fT, ν0








 
Proposition 1 (Simulation of M)   For a given two-counter machine M and control-states s0 and sf there is a run
        
p0, 0, 0
—→ ⋯ —→
pf, 0, 0
of M iff there is a run
        
s0T0, ν0
–[ε]→  ⋯ –[ε]→ 
sfT, ν
for some T and ν of GM.

Proof. Let s1 = s0 and sn = sf and suppose we have a run

        
s1, 0, 0
—→ ⋯ —→
sn, 0, 0
 .

We build the required run of GM by induction such that for configuration (sj, v0j, v1j) along the run of M, we have a run to a configuration (sj, Tj, νj) of GM such that

In the base case the result holds trivially for the configuration (s1, ∗, ν0). Now take a transition (sj, op, sj+1) from the run of M. By induction we have a run to (sj, Tj, νj) as above. We show how to extend this run to (sj+1, Tj+1, νj+1). There are several cases depending on op. In each case we show how to reach a tree satisfying the induction hypothesis, except the age of the leaf nodes. After the case analysis we show how to satisfy the age requirement also.

Finally, to obtain the age restriction on all leaf nodes, we apply (sj+1, Tη, ⊤) –[ε]→ (sj+1, Tη, ν0) to each leaf labelled by some η ∈ {∗, 0, 1}.

Thus, by induction, we can reach a configuration (sf, T, ν) such that, for each i we have ν(ci+) = ν(ci). Thus, we can apply a sequence of rules from Rfin to reach (f, T, ν). In particular, we apply (sf, T, ⊤) –[ε]→ (p=, T, ν0) and then simultaneously reduce each reversal-bounded counter to zero using (p=, T, ⊤) –[ε]→ (p=, T, µi=) repeatedly for each i, and then finally apply

        
p=Tc0+ = 0 ∧ c0 = 0 ∧ c1+ = 0 ∧ c1 = 0
–[ε]→ 
fT, ν0

to complete this direction of the proof.

We prove the opposite direction via two inductions. First, take some run of GM, which necessarily has the form

        
p1T1, ν1
–[ε]→  ⋯ –[ε]→ 
pnTn, νn
–[ε]→ 
p=Tn, νn
–[ε]→  ⋯ –[ε]→ 
p=, 0, 0
–[ε]→ 
f, 0, 0

where the last sequence of transitions (from pn) are all from Rfin, p1 = s0, T1 = ∗, ν1 = ν0, and pn = sf. Let #i(T) be the number of leaves labelled i in T. We first prove by induction over the run that for all 1 ≤ jn and i ∈ {0,1} we have #i(Tj) = νj(ci+) − νj(ci). This is a straightforward induction that can be seen by observing

Given #i(Tj) = νj(ci+) − νj(ci) for all j and i, we construct, also by induction, a sequence

        
s1v01v11
, …,
snv0nv1n

of M such that for all j and i we have #i(Tj) = v0j and pj ∈ {sj, (sj, 0), (sj, 1)} and, either

In the base case we set (s1, v01, v01) = (s0, 0, 0). Next, take a transition

        
pjTj, νj
–[ε]→ 
pj+1Tj+1, νj+1

of GM. There are several cases depending on which rule τ was applied.

Thus, we have a sequence (s1, v01, v11), …, (sn, v0n, v1n) from which we can immediately extract a run of M from (s1, v01, v11) = (s0, 0, 0) to (sn, v0n, v1n) = (sf, v0n, v1n). That v0n = v1n = 0 follows since the final transitions from sn have the effect of asserting νn(ci+) − νn(ci) = 0 from which we conclude #i(Tn) = 0 and since vin = #i(Tn) we complete the proof as required.


Thus, via Property 1 (Simulation of M) we can reduce the reachability problem for two-counter machines to the control-state reachability problem for senescent rbGTRS. Thus, we show the control-state reachability problem is undecidable and complete the proof of Theorem 2.


This document was translated from LATEX by HEVEA.