Synchronisation- and Reversal-Bounded Analysisof Multithreaded Programs with Counters
Matthew Hague1,2 and Anthony W. Lin2
1

LIGM (Université Paris-Est), LIAFA (Université Paris Diderot) & CNRS
2
Oxford University, Department of Computer Science

Abstract. We study a class of concurrent pushdown systems communicating by both global synchronisations and reversal-bounded counters,
providing a natural model for multithreaded programs with procedure
calls and numeric data types. We show that the synchronisation-boundedreachability problem can be efficiently reduced to the satisfaction of an
existential Presburger formula. Hence, the problem is NP-complete andcan be tackled with efficient SMT solvers such as Z3. In addition, we
present optimisations to make our reduction practical, e.g., heuristics forremoving or merging transitions in our models. We provide optimised algorithms and a prototypical implementation of our results and perform
preliminary experiments on examples derived from real-world problems.

1

Introduction

Pushdown systems (PDS) are a popular abstraction of sequential programs withrecursive procedure calls. Verification problems for these models have been extensively studied (e.g. [7, 17]) and they have been successfully used in the model
checking of sequential software (e.g. [3, 5, 37]).
However, given the ubiquity and growing importance of concurrent software(e.g. in web-servers, operating systems and multi-core machines), coupled with
the inherent non-determinism and difficulties in anticipating all concurrent interactions, the verification of concurrent programs is a pressing problem. In the caseof concurrent pushdown systems, verification problems quickly become undecidable [33]. Because of this, much research has attempted to address the undecidability, proposing many different approximations, and restrictions on topology
and communication behaviour (e.g. [29, 8–10, 35, 34, 21, 25]). A technique thathas proved popular in the literature is that of bounded context-switches [34].
Bounded context-switching uses the observation that many real-world bugs
require only a small number of inter-thread communications. It is known that, if
the number of communications is bounded to a fixed k, reachability checking of
pushdown systems becomes NP-complete [26]. The utility of this approach has
been demonstrated by several successful implementations (e.g. [4, 30, 36]).
In addition to recursive procedure calls, numeric data types are an importantfeature of programs. By adding counters to pushdown systems one can accurately model integer variables and, furthermore, abstract certain data structures

– such as lists – by tracking their size. It is well known that finite-state machines
augmented even with only two counters leads to undecidability of the simplest
verification problems. One way to retain decidability of reachability is to impose an upper bound r on the number of reversals between incrementing anddecrementing modes for each counter (cf. [12, 23]).
This restriction can be viewed in at least two ways (cf. [12, 24]). First, inthe spirit of bounded-context switches, it provides a generalisation of boundedmodel checking – a successful verification technique which exploits the fact thatmany bugs occurring in practice are “shallow” (cf. [14]). Secondly, many counting
properties — such as checking the existence of a computation where the numberof calls to the functions f1 , f2 , f3 , and f4 are the same — require no reversals(e.g. the number of memory allocations equals the number of frees). Similarcounting properties (and their model checking problems) have been studied inmany other contexts (cf. [27] and references therein).
In this paper, we study the problem of verifying reachability over a program model incorporating concurrency, numeric data types, and recursions. Ourcontributions are as follows:
1. We propose a concurrent extension of pushdown systems with reversalbounded counters that communicate through shared counters and global
synchronisations, and prove that the notion of global synchronisations subsumes context-bounded model checking.
2. We show that reachability checking for these systems is in NP, by reduction
to existential Presburger, handled by efficient SMT solvers such as Z3 [13].
3. We provide several new optimisation techniques, including a minimisation
routine for pushdown systems, that are crucial in making our reductions
feasible in practice. These techniques keep the size of the computation objects
small throughout reduction, while also producing smaller output formulas.
4. Finally, we provide two optimised, prototypical tools using these techniques.
The first translates a simple programming language into our model, while
the second performs our reduction to existential Presburger. We demonstrate
the efficacy of our tools on several real-world problems.
The tool implementations and benchmarks can be obtained from the authors’
homepages.
Related Work. In recent work [20], we showed that reachability analysis for
pushdown systems with reversal-bounded counters is NP-complete. We provided
a prototypical implementation of our algorithm and obtained encouraging results
on examples derived from Linux device drivers.
Over reversal-bounded counter systems (without stack), reachability is NPcomplete but becomes NEXP-complete when the number of reversals is given
in binary [22]. On the other hand, when the numbers of reversals and counters
are fixed, the problem is solvable in P [19]. The techniques developed by [19,22], which reason about the maximal counter values, are very different to ourtechniques, which exploit the connection to Parikh images of pushdown automata(first explicated in Ibarra’s original paper [23] though not in a way that gives
optimal complexity or a practical algorithm).
2

Context-bounded model checking was introduced in 2005 by Qadeer andRehof [34, 8, 32]. It has then been used in many different settings and manydifferent generalisations have been proposed. For example, one may consider
phase-bounds [38], ordered multi-stack machines [1], bounded languages [18],dynamic thread creation [2] and more general approaches [28].
In recent, independent work, Esparza et al. used a reduction to existential
Presburger to tackle a generalisation of context-bounded reachability checking
for multithreaded programs without counters [15]. Their work, however, does notallow the use of counters and it is not clear whether our global synchronisation
conditions can be simulated succinctly in their framework.
Organisation. In S2, we define the models that we study. We prove decidability of the synchronisation-bounded reachability problem in S3. In S4 we showthat synchronisation-bounded model checking subsumes context-bounded model
checking. Our optimisations are presented in S5. In S6 we describe our implementation and experimental results. Finally, we conclude in S7.

2Model Definition

In this section, we define the models that we study. For a vector v = (v1 , . . . , vn ),we write v (i) to access vi . For a formula θ over variables (x1 , . . . , xn ) we writeθ(v1 , . . . , vn ) to substitute the values v1 , . . . , vn for the variables x1 , . . . , xn respectively. Given an alphabet Γ = {γ1 , . . . , γm } and a word w ∈ Γ ∗ , we write
P(w) to denote a tuple with |Γ | entries where the ith entry counts the numberof occurrences of γi in w. Given a language L ⊆ Γ ∗ , we write P(L) to denotethe set { P(w) | w ∈ L }. We say that P(L) is the Parikh image of L.
Pushdown Automata. A pushdown automaton P is a tuple (Q, Σ, Γ, ∆, q0 , F )where Q is a finite set of control states, Σ is a finite stack alphabet with a special
bottom-of-stack symbol ⊥, Γ is a finite output alphabet, q0 ∈ Q is an initialstate, F ⊆ Q is a set of final states, and ∆ ⊆ (Q × Σ) × Γ ∗ × (Q × Σ ∗ ) is a
finite set of transition rules. We will denote a transition rule ((q, a), γ, (q ′ , w′ ))γusing the notation (q, a) ֒−→ (q ′ , w′ ). Note that γ ∈ Γ ∗ is a sequence of output
characters. This is for convenience, and optimisation. We can reduce this tosingle output characters using intermediate control states or stack characters.
Note, a pushdown system is a pushdown automaton without a set of final states.
A configuration of P is a tuple (q, w), where q ∈ Q and w ∈ Σ ∗ are the control
state and stack contents. We say that a configuration (q, aw) has a head q, a.
γγThere exists a transition (q, aw) −→ (q ′ , w′ w) of P whenever (q, a) ֒−→ (q ′ , w′ ) ∈γmγ2γ1∆. We call a sequence c0 −→ c1 −→ · · · −−→ cm a run of P. It is accepting if
c0 = (q0 , ⊥) and cm = (q, w) with q ∈ F . Let L(P) be the set of words labelling
accepting runs. Finally, we write c →∗ c′ if there is a run from c to c′ .
Pushdown Systems with Counters. A pushdown system with counters is a
pushdown system which, in addition to the control states and the stack, has anumber of counter variables. These counters may be incremented, decremented
and compared against constants (given in binary).
3

An atomic counter constraint on counter variable X = {x1 , . . . , xn } is an expression of the form xi ∼ c, where c ∈ Z and ∼∈ {<, >, =}. A counter constraint
θ(x1 , . . . , xn ) on X is a boolean combination of atomic counter constraints on
X. Let ConstX denote the set of counter constraints on X.
A pushdown system with n counters (n-PDS) P is a tuple (Q, Σ, Γ, ∆, X)
where Q is a finite set of control states, Σ is a finite stack alphabet, Γ is a
finite output alphabet, X = {x1 , . . . , xn } is a set of n counter variables, and∆ ⊆ (Q × Σ × ConstX ) × Γ ∗ × (Q × Σ ∗ × Zn ) is a finite set of transition rules.
γ
We will denote a rule ((q, a, θ), γ, (q ′ , w′ , u)) using (q, a, θ) ֒−→ (q ′ , w′ , u).
A configuration of P is a tuple (q, w, v), where q ∈ Q is the current control
state, w ∈ Σ ∗ is the current stack contents, and v = (v1 , . . . , vn ) ∈ Nn gives thecurrent valuation of the counter variables x1 , . . . , xn respectively. There exists aγtransition (q, aw, v) −→ (q ′ , w′ w, v ′ ) of P wheneverγ

1. (q, a, θ) ֒−→ (q ′ , w′ , u) ∈ ∆, and2. θ(v (1) , . . . , v (n)) is true, and3. v ′ (i) = v (i) + u (i) ≥ 0 for all 1 ≤ i ≤ n.
Communicating Pushdown Systems with Counters. Given Q1 , . . . , Qm ,′let Y = {y1 , . . . , ym , y1′ , . . . , ym
} be a set of control state variables such that,′for each i, yi , yi range over Qi . Then, an atomic state constraint is of the form
yi = q for some yi ∈ Y and q ∈ Qi . A synchronisation constraint, written′), is a boolean combination of atomic state constraints.
δ(y1 , . . . , ym , y1′ , . . . , ym
For example, let n = 3 and consider the constraint(y1 = q1 ∧ (y1′ = q1 ∧ y2′ = q2 ∧ y3′ = q3 )) ∨(y1 = r1 ∧ (y1′ = r1 ∧ y2′ = r2 ∧ y3′ = r3 )) .
This allows synchronisations where, whenever the first process has control state
q1 , the other processes can simultaneously move to qi (for all 1 ≤ i ≤ 3), whereas,
if process one has control state r1 , the processes move to states ri instead. Let
StateConsQ1 ,...,Qm be the set of synchronisation constraints for Q1 , . . . , Qm .
Definition 1 (n-SyncPDSr). Given a finite output alphabet Γ and set of ncounter variables X, a system of communicating pushdown systems with n counters C is a tuple (P1 , . . . , Pm , ∆g , X, r) where, for all 1 ≤ i ≤ m, Pi is a pushdown system (Qi , Σi , Γ, ∆i , X) with n counters, and ∆g ⊆ StateConsQ1 ,...,Qm ×
ConstX ×Zn is a finite set of synchronisation constraints, and r ∈ N is a natural
number given in unary.
Notice that a system of communicating pushdown systems share a set ofcounters. A configuration of such a system is a tuple (q1 , w1 , . . . , qm , wm , v)γ
where each (qi , wi , v) is a configuration of Pi . We have (q1 , w1 , . . . , qm , wm , v) =⇒′′, v ′ ) whenever,, wm(q1′ , w1′ , . . . , qm
γ

1. for some 1 ≤ i ≤ m, we have (qi , wi , v) −→ (qi′ , wi′ , v ′ ) is a transition of Pi′′
and qj = qj and wj = wj for all j 6= i, or
4

2. γ = ε and wi = wi′ for all 1 ≤ i ≤ m and (δ, θ, u) ∈ ∆g with′(a) δ(q1 , . . . , qm , q1′ , . . . , qm
) is true, and(b) θ(v (1) , . . . , v (n)) is true, and(c) v ′ (i) = v (i) + u (i) ≥ 0 for all 1 ≤ i ≤ n.
We refer to these two types of transition as internal and synchronising respecγ2
γ1γmtively. A run of C is a run c0 =⇒ c1 =⇒ · · · ==⇒ cm .
Bounding Runs. During a run, the counter is in a non-decrementing mode if
the last value-changing operation on that counter was an increment. Similarly, acounter may be in a non-incrementing mode. The number of reversals of a counter
during a run is the number of times the counter changes from an incrementing
to a decrementing mode, and vice versa. For example, if the values of a counterx in a path are 1, 1, 1, 2, 3, 4, 4, 4, 3, 2, 2, 3, then the number of reversals of x is
2 (reversals occur in between the overlined positions). This sequence has threephases (i.e. subpaths interleaved by consecutive reversals or end points): nondecrementing, non-incrementing, and finally non-decrementing.
γ1

γ2

γm

Definition 2 (r-Reversal-Bounded). A run c0 =⇒ c1 =⇒ · · · ==⇒ cm is rreversal-bounded whenever we can partition c0 c1 . . . cm into C1 . . . Cr such thatfor all 1 ≤ p ≤ r, there is some ∼∈ {≤, ≥} such that for all cj cj+1 appearing
together in Cp , we have cj = (. . ., v j ), cj+1 = (. . ., v j+1 ), and for all 1 ≤ i ≤ n,v j (i) ∼ v j+1 (i).
Finally, we define the notion of synchronisation-bounded. We show in Section 4 that this notion subsumes context-bounded model checking.
Definition 3 (k-Synchronisation-Bounded). A run π is k-synchronisationbounded whenever π uses k or fewer synchronising transitions.

3

Synchronisation-Bounded Reachability

The r-reversal and k-synchronisation-bounded reachability problem for a given
C, bound r and k asks, for given configurations c and c′ of C, is there a ksynchronisation-bounded run of C from c to c′ using up to r reversals. We prove:
Theorem 1. For two bounds r and k given in unary, the r-reversal and ksynchronisation-bounded reachability problem for n-SyncPDS is NP-complete.
The proof extends the analogous theorem for r-reversal-bounded n-PDS [20].
We will construct, for each Pi in C, an over-approximating pushdown automaton
Pi′ and use Verma et al. [40]3 to obtain an existential Presburger formula Imagei
giving the Parikh image of Pi′ . Finally, we add additional constraints such thata solution exists iff the reachability problem has a positive answer.
3

It is well known that [40] contains a small bug, fixed by Barner [6]. See the appendix
for more details.

5

The encoding presented here is one of two encodings that we developed.
This encoding is both simpler to explain and seems to be handled better by Z3
for almost all of our examples than the second encoding. However, the second
encoding results in a smaller formula. Hence, we include both reductions as
contributions, and present the second reduction in the appendix.
The key difference between the encodings is where we store the number ofsynchronisations performed so far. In the first encoding, we keep a component g
in each control state; thus, from each P we build P ′ with |Q| × Nmax × (k + 1)
control states, where Q is set of control states of P and Nmax is the number ofmode vectors (where modes are defined below).
In the alternative encoding we put the number of synchronisations in themodes, resulting in |Q| × (Nmax + k + 1) control states. This is important since
our reduction is quadratic in the number of controls. Hence, if k = 2, the alternative results in pushdown automata a third of the size of the encoding presented
here. However, the resulting formulas seem experimentally more ′difficult to solve.
0, v f ). By hardLet c = q10 , w1 , . . . , qm
, wm , v 0 and c′ = (f1 , w1′ , . . . , fm , wm
coding the initial and final stack contents, we can assume that all wi = wi′ =⊥.
Unfortunately, we cannot use the reduction for r-reversal-bounded n-PDS as
a completely black box; hence, we will recall the relevant details and highlightthe new techniques required. We refer the reader to the article [20] for further
details. The correctness of the reduction is given in the appendix.
The final formula HasRun will take the shape
Init(m1 ) ∧ GoodSeq(m1 , . . . , mNmax )VImagei (z i )
∧


1≤i≤m




P



∧ Respectz i , m1 , . . . , mNmax∃m1 , . . . , mNmax ∃z 1 . . . z m 
1≤i≤m




P




∧ OneChange
z
i
1≤i≤m

P

P

∧ EndVal1≤i≤m z i ∧ Syncs
1≤i≤m z i




P
P
are theandSyncszwhere the formulas OneChange
z
i
i
1≤i≤m
1≤i≤m
main differences with the single thread case. In addition, further adaptations
need to be made within other aspects of the formula. We remark at this pointthat the user may add to HasRun an additional constraint on the Parikh imagesof runs — such as restricting to runs where the number of characters γ output
is greater than the number of γ ′ .
The Mode Vectors. We begin with the vectors m1 , . . . , mNmax , which areunchanged from the case of r-reversal-bounded n-PDS. Let d1 < . . . < dh denote
all the numeric constants appearing in an atomic counter constraint as a part ofthe constraints in the Pi . Without loss of generality, we assume that d1 = 0 for
convenience. Let REG = {ϕ1 , . . . , ϕh , ψ1 , . . . , ψh } be a set of formulas defined asfollows. Note that these formulas partition N into 2h pairwise disjoint regions.
ϕi (x) ≡ x = di ,ψi (x) ≡ di < x < di+1 (1 ≤ i < h),6ψh (x) ≡ dh < x .

We call a vector in REGn × [0, r]n × {↑, ↓}n a mode vector. Given a path πfrom configurations c to c′ , we may associate a mode vector to each configurationin π. This vector records for each counter, which region its value is in, howmany reversals it’s used, and whether its phase is non-decrementing (↑) or nonincrementing (↓). Consider a sequence of mode vectors. A crucial observation is,once a change occurs to the mode information of a counter, the same information
will not recur for that counter. For example, returning to the same region will
incur an increase in the number of reversals. Thus, there are at most Nmax :=|REG| × (r + 1) × n = 2hn(r + 1) distinct mode vectors in any sequence.
Constructing Pi′ . We define the pushdown automataPi′ = Q′i , Σi , Γ ′ , ∆′i , qi0 , 1, 1 , {fi } × [1, Nmax ] × [1, k + 1]

for each Pi in C. Note that each Pi′ has the same output alphabet Γ ′ . We assume
that all Qi are pairwise disjoint. There are two main aspects to each Pi′ . First, weremove the counters. To replace them, we have Pi′ output any counter changes
or tests that would have been performed. E.g. where Pi would increment a
counter, Pi′ will output a symbol (ctrj , 1, . . .) indicating (amongst other things)
that counter ctrj should be increased by 1. Furthermore, Pi′ guesses when, andkeeps track of when, mode changes would have occurred. Secondly, we allow Pi′
to non-deterministically make synchronisations (instead of communicating, theeffect of external threads is guessed). In this case, the control state change, alongwith the number of synchronisations performed thus far, will be output. In thisway, Pi′ makes “visible” the counter tests, counter updates and synchronisations
that would have been performed by Pi on the same run. Constraints describedlater in HasRun ensure these operations are valid.
More formally, let Q′i = Qi × [1, Nmax] × [1, k + 1] (that is, we add to Qi thecurrent mode and synchronisation number). We define Γ ′ implicitly from thetransition relation. In fact, Γ ′ is a (finite) subset of∪Γ ∪ { (ctrj , u, e, l) | j ∈ [1, n], u ∈ Z, e ∈ [1, Nmax ], l ∈ {0, 1} }∪ (ConstX × [1, Nmax ])S(StateConsQ1 ,...,Qm × Qi × Qi × [1, Nmax ] × [1, k + 1] × {0, 1}) .

1≤i≤mCharacters (ctrj , u, e, l) mean to add u to ctrj , in mode e, where l indicates
whether the counter action changes the mode vector. Characters (θ, e) indicate
a counter test in mode e. Finally, characters (δ, q, q ′ , e, g, l) indicate a use ofsynchronisation rule δ, changing Pi from control state q to q ′ , in mode e with gsynchronisations performed so far.
γ
We define ∆′i to be the smallest set such that, if (q, a, θ) ֒−→ (q ′ , w, u) ∈ ∆i
where u = (u1 , . . . , un ) then for each e ∈ [1, Nmax ] and g ∈ [1, k + 1], ∆′i contains
γ(θ,e)(ctr1 ,u1 ,e,l)...(ctrn ,un ,e,l)((q, e, g), a) ֒−−−−−−−−−−−−−−−−−−−−−→ ((q ′ , e + l, g), w)
for all l ∈ {0, 1} if e ∈ [1, Nmax) and l = 0 otherwise. Thus, l = 1 signifies amode changing transition.
7

These rules are the rules required in the single thread case. We need additional rules to reflect the multi-threaded environment. In particular, an external
thread may change the mode, or a synchronising transition may occur. To account for this ∆′i also has for each q ∈ Qi , a ∈ Σi , e ∈ [1, Nmax ), and g ∈ [1, k+1],ε((q, e, g), a) ֒−→ ((q, e + 1, g), a)(∗)

and, to model synchronisations, we have for all q, q ′ ∈ Qi , e ∈ [1, Nmax ], g ∈[1, k + 1) and (δ, θ, u) ∈ ∆g , when i > 1,
(δ,q,q′ ,e,g,l)((q, e, g), a) ֒−−−−−−−→ ((q ′ , e + l, g + 1), a)and when i = 1 and u = (u1 , . . . , un ),(δ,q,q′ ,e,g,l)(θ,e)(ctr1 ,u1 ,e,l)...(ctrn ,un ,e,l)((q, e, g), a) ֒−−−−−−−−−−−−−−−−−−−−−−−−−−−−→ ((q ′ , e + l, g + 1), a)
for all l ∈ {0, 1} when e ∈ [1, Nmax) and l = 0 otherwise. That is, Pi′ guesses
the effect of non-internal transitions and P1′ is responsible for performing therequired counter updates. Note that the information in the output character(δ, q, q ′ , e, g, l) allows us to check that synchronising transitions take place in thesame order and in the same modes across all threads.
Constructing The Formula. Fix an ordering γ1 < . . . < γl on Γ ′ . By f wedenote a function mapping γi to i for each i ∈ [1, l]. Let z denote a vector ofl variables. The formula is HasRun given above, where Init, GoodSeq, Respect,
and EndVal are defined as in the single thread case (using only variables which
are unchanged from [20]); therefore, we describe them informally here, referring
the reader to the appendix for the full definitions. We convert each Pi′ to acontext-free grammar (of cubic size) and use [40] to obtain Imagei such that foreach n ∈ Nl we have n ∈ P(L(Pi′ )) iff Imagei (n) holds. Informally,– Init ensures the initial mode vector m1 respects the initial configuration c;– GoodSeq ensures that the sequence of mode vectors m1 , . . . , mNmax is valid.
For example, if the direction of a counter changes, then an extra reversal isincurred on that counter;– Respect requires that the counter tests and actions fired within a mode areallowed. For example, a subtraction may not occur on a counter in a nondecreasing phase, only one mode change action may occur per mode, andthat counter tests only occur in sympathetic regions; and– EndVal checks that the counter operations applied during the run leave eachcounter in the correct value, as given in the final configuration c′ .
It remains for us to define OneChange and Syncs. We use OneChange to assertthat only one thread may be responsible for firing the transition that changes agiven mode of the counters to the next. That is,^
zf (ctrj ,u,e,1) = 1
zf (ctrj ,u,e,1) > 0 ⇒.
OneChange (z) ≡∧ zf (ctrj ,u′ ,e,1) = 0(ctrj ,u,e,1)(ctrj ,u′ ,e,1)u′ 6=u8

The role of Syncs is to ensure that the synchronising transitions taken by′
P1′ , . . . , Pm
are valid. Note that, by design, each Pi′ will only output at most one
character of the form (δ, q, q ′ , e, g, l) for each g ∈ [1, k]. We assert, if one threaduses a global transition with condition δ, all do, and δ is satisfied. That is,
!
^
_
Fired
 (δ,e,g,l) (z) ⇒Syncs (z) ≡Sync(δ,e,g,l) (z) ∧ AllFired(δ,e,g,l) (z)1≤g≤k 1≤e≤Nmax(δ,θ,u)∈∆gl∈{0,1}

where Sync(δ,e,g,l) (z) is δ (z) with each atomic state constraints replaced as
below.
__
zf (δ,q,q′ ,e,g,l) > 0 .
zf (δ,q,q′ ,e,g,l) > 0 and (yi = q ′ ) ≡(yi = q) ≡(δ,q,q′ ,e,g,l)(δ,q,q′ ,e,g,l)Finally, Fired(δ,e,g,l) (z) ≡W

zf (δ,q,q′ ,e,g,l) > 0, and(δ,q,q′ ,e,g,l)

AllFired(δ,e,g,l) (z) ≡^_zf (δ,q,q′ ,e,g,l) > 0 .

1≤i≤m q,q′ ∈Qi

We remark upon a pleasant corollary of our main result. Consider a system of pushdown systems communicating only via reversal-bounded counters.
Since such a system cannot use any synchronising transitions, all runs are 0synchronisation-bounded; hence, their reachability problem is in NP.

4

Comparison with Context-Bounded Model Checking

Global synchronisations can be used to model classical context-bounded model
checking. We present a simple encoding here. We begin with the definition.
Definition 4 (n-ClPDS). A classical system of communicating pushdown
systems with n counters C is a tuple (P1 , . . . , Pm , G, X) where, for all 1 ≤ i ≤ m,
Pi is a PDA with n counters (Qi , Σi , Γ, ∆i , X), X is a finite set of counter variables and Qi = G × Q′i for some finite set Q′i .
A configuration of a n-ClPDS is a tuple (g, q1 , w1 . . . , qm , wm , v) where g ∈ Gγand (g, qi ) ∈ Qi for all i. We have a transition (g, q1 , w1 , . . . , qm , wm , v) =⇒γ′′
, v ′ ) when, for some 1 ≤ i ≤ m, we have ((g, qi ), wi , v) −→, wm
(g ′ , q1′ , w1′ , . . . , qm
′
′
′
′
′ ′
((g , qi ), wi , v ) is a transition of Pi and qj = qj and wj = wj for all j 6= i.
γ1

γ2

γm

A run of C is a sequence c0 =⇒ c1 =⇒ · · · ==⇒ cm . A k-context-bounded run isγ2
γ1γma run c0 =⇒ c1 =⇒ · · · ==⇒ cm that can be divided into k phases C1 , . . . , Ck suchthat during each Ci only transitions from a unique Pj are used. By convention,
the first phase contains only transitions from P1 .
We define an n-SyncPDS simulating any given n-ClPDS. It uses the synchronisations to pass the global component g of the n-ClPDS between configurationsof the n-SyncPDS, acting like a token enabling one process to run. Since there
are k global synchronisations, the run will be k-context-bounded.
9Definition 5. Given a n-ClPDS C = (P1 , . . . , Pm , G, X). Let # be a symbol
not in G. We define from each Pi = (Qi , Σi , Γ, ∆i , X) with Qi = G × Q′i thepushdown system PiS = QSi ∪ {fi } , Σi , Γ, ∆Si , X where QSi = Qi × (G ∪ {#})εand ∆Si is the smallest set containing ∆i and ((g, q), a, tt) ֒−→ (fi , w, 0) for allq, a appearing as a head in the final configuration with g = # or with g also in
the final configuration.
S
Finally, let CS = P1S , . . . , Pm
, ∆g , X , where ∆g = {(δ, tt, 0)} such thatthe formula δ(q11 , . . . , qn1 , q12 , . . . , qn2 ) holds only when there is some g ∈ G and
1 ≤ i 6= j ≤ n such that
1. qi1 = (g, q) and qi2 = (#, q) for some q, and2. qj1 = (#, q) and qj2 = (g, q) for some q, and3. for all i′ 6= i and i′ 6= j, qi1′ = (#, q) and qi2′ = (#, q) for some q.

We show in the appendix that an optimised version of this simulation — discussed in Section 5 — is correct. That is, there is a run of C to the final configuration (g, q1 , w1 , . . . , qm , wm , v) iff there is a run of CS to (f1 , w1 , . . . , fm , wm , v)
using the same number of reversals.

5

Optimisations

Our experiments suggest that without further optimisations our reduction from
Section 3 is rather impractical. In this section, we provide several optimisations
which considerably improve the practical aspect of our reduction. We discuss
improving the encoding of the context-bounded model checking, identifying andeliminating “removable” heads from our models, and minimising the size of the
CFG produced during the reduction using reachability information. The gist
behind our optimisation strategies is to keep the size of the models (pushdown
automata, CFG, etc.) as small as possible throughout our reduction, which canbe achieved by removing redundant objects as early as possible. For the rest of
this section, we fix an initial and a final configuration.
Context-Bounded Model Checking. The encoding context-bounded model
checking encoding given in Section 4 allows context-switches to occur at any
moment. However, we can observe that context-switches only need to occur when
global information needs to be up-to-date. This restriction led to improvements
in our experiments. We describe the positions where context-switches may occur
informally here, and give a formal definition and proof in the appendix.
In our restricted encoding, context-switches may occur when an update to
global component g occurs; the value of g is tested; an update to the countersoccurs; the values of the counters are tested; or the control state of the active
thread appears in the final configuration. Intuitively, we delay context-switches
as long as possible without removing behaviours — that is, until the status of
the global information affects, or may be affected by, the next transition.
Minimising Communicating Pushdown Systems with Counters. We describe a minimisation technique to reduce the size of the pushdown systems. It
10

identifies heads q, a of the pushdown systems that are removable. We collapse
pairs of rules passing through the head q, a into a single combined rule. Thus,
we build a pushdown system with fewer heads, but the same behaviours. In thefollowing definition, sink states will be defined later. Intuitively it means whenq is reached, q cannot be changed in one local or global transition.
Definition 6. A head q, a is removable whenever
1. q, a is not the head of the initial or final configuration, andγ
2. it is not a return location, i.e. there is no rule (q1 , b1 , θ) ֒−→ (q2 , b2 w′ , u) witha appearing in w′ and a does not appear below the top of the stack in theinitial configuration, andγ
3. it is not a loop, i.e. there is no rule (q, a, θ) ֒−→ (q, aw′ , u), andγ
4. it is not a synchronisation location, i.e. for all (q2 , b, θ) ֒−→ (q1 , aw′ , u) or initial configuration containing q1 and a, we have either, (i) for all (δ, θ′ , u′ ) ∈12
12∆g and q11 , . . . , qm
, q12 , . . . , qm
such that δ(q11 , . . . , qm
, q12 , . . . , qm
) holds wejhave qi 6= q1 for all i, j, or (ii) q1 is a sink state, andγ
5. it is not a counter access location, i.e. there is no rule (q, a, θ) ֒−→ (q ′ , w′ , u)such that θ depends on a counter or u contains a non-zero entry, and thereγ
is no rule (q ′ , b, θ) ֒−→ (q, aw′ , u) such that u contains a non-zero entry.
γDefinition 7. A state q is a sink state when for all rules (q, a, θ) ֒−→ (q ′ , w′ , u)
2
2
1
′
′
′
1
we have q = q and for all (δ, θ , u ) ∈ ∆g and q1 , . . . , qm , q1 , . . . , qm with qi1 = q
1
2
for some i such that δ(q11 , . . . , qm
, q12 , . . . , qm
) holds we have qi2 = q.
Removable heads can be eliminated by merging rules passing through them.
In general, this may increase the number of rules, but in practice it leads tosignificant reductions (see Table 1). We show, in the appendix, that this optimisation preserves behaviours of the systems.
Definition 8. Given a n-SyncPDS with global rules ∆g and a pushdown system
P with n counters (Q, Σ, Γ, ∆, X) and a removable head q, a, we define Pq,a tobe (Q, Σ, Γ, ∆′ , X) where ∆′ = ∆ if ∆1 is empty and ∆′ = ∆1 ∪ ∆2 otherwise,
where


γ1

(q1 , b, θ1 ) ֒−→ (q, aw1 , u1 ) ∈ ∆ ∧ 
γ 1 ,γ 22∆1 =(q1 , b, θ) ֒−−−→ (q2 , w, u1 + u2 ) (q, a, θ2 ) ֒−γ→
(q
,
w
,
u
)
∈
∆
∧
2
2
2




θ = (θ1 ∧ θ2 ) ∧ w = w2 w1noγ(q1 , b, θ) ֒−→ (q2 , w′ , u) | q1 , b = q, a ∪o .
and ∆2 = ∆ \  nγ(q1 , b1 , θ) ֒−→ (q2 , b2 w′ , u) | q2 , b2 = q, aMinimising CFG size via pushdown reachability table. Recall that our
reduction to existential Presburger formulas from an n-SyncPDS makes use ofa standard language-preserving reduction from pushdown automata to contextfree grammars (CFGs). Unfortunately, the standard translations from PDAs
11

to CFGs incur a cubic blow-up. More precisely, if the input PDA is P =Q, Σ, Γ, ∆, q 0 , F , the output CFG has size O(|∆| × |Q|2 ). Our experimentssuggest that this cubic blow-up is impractical without further optimisation, i.e.,
the naive translation failed to terminate within a couple of hours for most of
our examples. Note that the complexity of translating from PDA to CFG is verymuch related to the reachability problem for pushdown systems, for which the
optimal complexity is a long-standing open problem (the fastest algorithm [11]to date has complexity O(n3 / log n) under certain assumptions).
We will now describe two optimisations to improve the size of the CFG that is
produced by our reduction in the previous section, the second optimisation gives
better performance (asymptotically and empirically) than the first. Without lossof generality, we assume that: (A1) the PDA empties the stack as it accepts anγ
input word, (A2) the transitions of the input PDA are of the form (p, a) ֒−→ (q, w)where p, q ∈ Q, γ ∈ Γ ∗ , a ∈ Σ, and w ∈ Σ ∗ with |w| ≤ 2. [It is well-known
that any input PDA can be translated into a PDA in this “normal form” thatrecognises the same language while incuring only a linear blow-up.] The gist
behind both optimisations is to refrain from producing redundant CFG rules bylooking at the reachability table for the PDA. Keeping the CFG size low in thefirst place results in algorithms that are more efficient than removing redundant
rules after the CFG is produced.
Let us first briefly recall a standard language-preserving
translation from
PDA to CFG. Given a PDA P = Q, Σ, Γ, ∆, q 0 , F , we construct the following
CFG with nonterminals N = {S} ∪ {Ap,a,q : p, q ∈ Q, a ∈ Σ}, terminals Γ ,starting nonterminal S, and the following transitions:γ(1) For each (p, a) ֒−→ (q, ǫ) ∈ ∆, the CFG has Ap,a,q → γ.
γ(2) For each (p, a) ֒−→ (p′ , b) ∈ ∆ and q ∈ Q, the CFG has Ap,a,q → γAp′ ,b,q .
γ(3) For each (p, a) ֒−→ (p′ , cb) ∈ ∆ and r, q ∈ Q, the CFG has Ap,a,q →γAp′ ,c,r Ar,b,q .
(4) Add S → Aq0 ,⊥,qF for each qF ∈ F .
Note that Ap,a,q generates all words that can be output by P from configuration(p, a) ending in configuration (q, ǫ). Both of our optimisations refrain from generating: (i) CFG rules of type (2) above in the case when (p′ , b) 6→∗ (q, ǫ), and(ii) CFG rules of type (3) in the case when (p′ , c) 6→∗ (r, ǫ) or (r, b) 6→∗ (q, ǫ),and (iii) CFG rules of type (4) in the case when q 0 , ⊥ 6→∗ (qF , ǫ).
It remains to describe how to build the reachability lookup table for P withentries of the form (p, a, q) witnessing whether (p, a) →∗ (q, ǫ). The first optimisation achieves this by directly applying the pre∗ algorithm for pushdown
systems described in [16], which takes O(|Q|2 × |∆|) time. This optimisation
holds for any input PDA and, hence, does not exploit the structure of the PDA
that we generated in the previous section. Our second optimisation improves
the pre∗ algorithm for pushdown systems from [16] by exploiting the structureof the PDA generated in the previous section, for which each control state is of
the form (p, i, j), where i, j ∈ Z>0 . The crucial observation is that, due to the12

PDA rules of type (*) generated from the previous section, the PDA that we areconcerned with satisfy the following two properties:(P0) ((p, i, j), v) →∗ ((q, i′ , j ′ ), w) implies i′ ≥ i and j ′ ≥ j.
(P1) ((p, i, j), v) →∗ ((q, i′ , j ′ ), w)) implies for each d1 , d2 ∈ N that we have((p, i + d1 , j + d2 ), v) →∗ ((q, i′ + d1 , j ′ + d2 ), w) .
(P2) for each nonempty v ∈ Σ ∗ : ((p, i, j), av) →∗ ((q, i′ , j ′ ), v) implies we have((p, i, j), av) →∗ ((q, i′′ , j ′ ), v) for each i′′ ≥ i′ .
Properties (P0) and (P1) imply it suffices to keep track of the differences in
the mode indices and context indices in the reachability lookup table, i.e., instead of keeping track of all values ((p, i, j), a) →∗ ((q, i′ , j ′ ), ǫ), each entry is of
the form (p, a, q, d, d′ ) meaning that ((p, i, j), a) →∗ ((q, i + d, j + d′ ), ǫ) for eachi, j ∈ Z>0 . Property (P2) implies that if (p, a, q, d, d′ ) is an entry in the table,
then so is (p, a, q, d+ i, d′ ) for each i ∈ N. Therefore, whenever p, a, q, d′ are fixed,
it suffices to only keep track of the minimum value d such that (p, a, q, d, d′ ) is anentry in the table. We describe the adaptation of the pre∗ algorithm for pushdown systems from [16] for computing the specialised reachability lookup tablein the appendix. The resulting time complexity for computing the specialised
reachability lookup table becomes linear in the number of mode indices.

6

Implementation and Experimental Results

We implemented two tools: Pushdown Translator and SynPCo2Z3.
Pushdown Translator The Pushdown Translator tool, implemented in C++,takes a program in a simple input language and produces an n-SyncPDS. The
language supports threads, boolean variables (shared between threads, global toa thread, or local), shared counters, method calls, assignment to boolean variables, counter increment and decrement, branching and assertions with counterand boolean variable tests, non-deterministic branching, goto statements, locks,
output, and while loops. The user can specify the number of reversals andcontext-switches and specify a constraint on the output performed (e.g. findruns where the number of γ characters output equals the number of γ ′ s). The
full syntax is given in the appendix. The translation uses the context-switch
technique presented in Definition 5 and the minimisation technique of Definition 8. Furthermore, the constructed pushdown systems only contain transitions
for reachable states of each thread (assuming counter tests always pass, andsynchronising transition can always be fired).
SynPCo2Z3 Our second tool SynPCo2Z3 is implemented in SWI-Prolog. The
input is an n-SyncPDS, reversal bound r, and synchronisation-bound k. Dueto the declarative nature of Prolog, the syntax is kept close to the n-SyncPDS
definition. The output is an existential Presburger formulas in SMT-LIB format,
supported by Z3. Moreover, the tool implements all the different translations
that have been described in this paper (including appendix) with and without
the optimisations described in the previous section. The user may also specify aconstraint on the output performed by the input n-SyncPDS.
13

Experiments We tested our implementation on several realistic benchmarks.
One benchmark concerns the producer-consumer examples (with one producer
and one consumer) from [31]. We took two examples from [31]: one uses one
counter and is erroneous, wherein both producer and consumer might be bothasleep (a deadlock), and the other uses two counters and is correct. The nSyncPDS models of these examples were hand-coded since they use synchronisations rather than the context-switches of Pushdown Translator.
The remaining benchmarks were adapted from modules found in Linux kernel 3.2.1, which contained list- and memory-management, as well as locks forconcurrent access. These modules often provided “register” and “unregister”
functions in their API. We tested that, when register was called as many times
as unregister, the number of calls to malloc was equal to the number of calls to
free. Furthermore, we checked that the module did not attempt to remove an
item from an empty list. In all cases, memory and list management was correct.
We then introduced bugs by either removing a call to free, or a lock statement. Note the translation from C to our input language was by hand, and an
automatic translation is an interesting avenue of future work.
The results are shown in Table 1. All tests were run on a 2.8GHz Intel machinewith 32GB of RAM. Each benchmark had two threads, two context-switches,
one counter and one reversal. The size fields give the total number of pushdown
rules in the n-SyncPDS, both before and after removable heads minimisation.
Tran. Time gives the time it took to produce the SMT formula, Solve Time isthe time taken by Z3 (v. 3.2, Linux build). Each cell contains two entries: thefirst is for the instance with a bug, the second for the correct instance.
File
prod-cons.c
api.c (rtl8192u)
af alg.chid-quirks.cdm-target.c

Size
22/13
654/660
506/528
557/559416/436

Min. Size-/202/208
174/204
303/303254/278

Tran. Time
0.8s/1.8s
28s/28s
18s/21s
47s/47s
27s/29s

Solve Time
4.2s/6.8s
4m19s/4m32s
10m2s/4m47s
18m41s/12m5s
36m43s/10m1s

Table 1. Results of experimental runs.

7

Conclusions and Future Work

We have studied the synchronisation-bounded reachability problem for a classof pushdown systems communicating by shared reversal-bounded counters andglobal synchronisations. This problem was shown to be NP-complete via anefficient reduction to existential Presburger arithmetic, which can be analysedusing fast SMT solvers such as Z3. We have provided optimisation techniques forthe models and algorithms and a prototypical implementation of this reductionand experimented on a number of realistic examples, obtaining positive results.
14

There are several open problems. For instance, one weakness we would like toaddress is that we cannot represent data symbolically (using BDDs, for example).
This prevents us from being competitive with tools such as Getafix [39] forcontext-bounded model-checking of pushdown systems without counters.
Furthermore, although we can obtain from the SMT solver a satisfying assignment to the Presburger formula, we would like to be able to construct a complete trace witnessing reachability. Additionally, the construction of a counterexample guided abstraction-refinement loop will require the development of newtechniques not previously considered. In particular, heuristics will be needed todecide when to introduce new counters to the abstraction.
We may also consider generalisations of context-bounded analysis such asphase-bounds and ordered multi-stack automata. A further challenge will be toadapt our techniques to dynamic thread creation, where each thread has its own
context-bound, rather than the system as a whole.
Acknowledgments. We thank EPSRC (EP/F036361 & EP/H026878/1), AMIS(ANR 2010 JCJC 0203 01 AMIS) and VAPF (Fondation de Coopération Scientifique du Campus Paris Saclay) for their support.

References
1. M. F. Atig, B. Bollig, and P. Habermehl. Emptiness of multi-pushdown automata
is 2etime-complete. In Developments in Language Theory, pages 121–133, 2008.
2. M. F. Atig, A. Bouajjani, and S. Qadeer. Context-bounded analysis for concurrent
programs with dynamic creation of threads. In LMCS, 7(4), 2011.
3. T. Ball, B. Cook, V. Levin, and S. K. Rajamani. Slam and static driver verifier:Technology transfer of formal methods inside microsoft. In IFM, pages 1–20, 2004.
4. T. Ball, V. Levin, and S. K. Rajamani. A decade of software model checking withslam. Commun. ACM, 54:68–76, July 2011.
5. T. Ball and S. K. Rajamani. Bebop: A symbolic model checker for boolean programs. In SPIN, pages 113–130, 2000.
6. S. Barner. H3 mit gleichheitstheorien. Diploma thesis, TUM, 2006.
7. A. Bouajjani, J. Esparza, and O. Maler. Reachability analysis of pushdown automata: Application to model-checking. In CONCUR, pages 135–150, 1997.
8. A. Bouajjani, J. Esparza, S. Schwoon, and J. Strejcek. Reachability analysis ofmultithreaded software with asynchronous communication. In FSTTCS, pages
348–359, 2005.
9. A. Bouajjani, J. Esparza, and T. Touili. A generic approach to the static analysis
of concurrent programs with procedures. SIGPLAN Not., 38(1):62–73, 2003.
10. A. Bouajjani, M. Müller-Olm, and T. Touili. Regular symbolic analysis of dynamic
networks of pushdown systems. In CONCUR, pages 473–487, 2005.
11. Swarat Chaudhuri. Subcubic algorithms for recursive state machines. In POPL,
pages 159–169, 2008.
12. Z. Dang, O. H. Ibarra, T. Bultan, R. A. Kemmerer, and J. Su. Binary reachability
analysis of discrete pushdown timed automata. In CAV, pages 69–84, 2000.
13. L. Mendonça de Moura and N. Bjørner. Z3: An efficient smt solver. In TACAS,
pages 337–340, 2008.
14. V. D’Silva, D. Kroening, and G. Weissenbacher. A survey of automated techniques
for formal software verification. IEEE Trans. on CAD of Integrated Circuits andSystems, 27(7):1165–1178, 2008.
15. J. Esparza and P. Ganty. Complexity of pattern-based verification for multithreaded programs. In POPL, pages 499–510, 2011.

15

16. J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms formodel checking pushdown systems. In CAV, pages 232–247, 2000.
17. J. Esparza, A. Kucera, and S. Schwoon. Model checking ltl with regular valuations
for pushdown systems. Inf. Comput., 186(2):355–376, 2003.
18. P. Ganty, R. Majumdar, and B. Monmege. Bounded underapproximations. In
CAV, pages 600–614, 2010.
19. E. M. Gurari and O. H. Ibarra. The complexity of decision problems for finite-turnmulticounter machines. J. Comput. Syst. Sci., 22(2):220–229, 1981.
20. M. Hague and A. W. Lin. Model checking recursive programs with numeric datatypes. In CAV, pages 743–759, 2011.
21. A. Heußner, J. Leroux, A. Muscholl, and G. Sutre. Reachability analysis of communicating pushdown systems. In FOSSACS’10, pages 267–281, 2010.
22. R. R. Howell and L. E. Rosier. An analysis of the nonemptiness problem for classesof reversal-bounded multicounter machines. J. Comput. Syst. Sci., 34(1):55–74,
1987.
23. O. H. Ibarra. Reversal-bounded multicounter machines and their decision problems. J. ACM, 25(1):116–133, 1978.
24. O. H. Ibarra, J. Su, Z. Dang, T. Bultan, and R. A. Kemmerer. Counter machinesand verification problems. Theor. Comput. Sci., 289(1):165–189, 2002.
25. V. Kahlon. Parameterization as abstraction: A tractable approach to the dataflow
analysis of concurrent programs. In LICS, pages 181–192, 2008.
26. A. Lal, T. Touili, N. Kidd, and T. Reps. Interprocedural analysis of concurrent
programs under a context bound. In TACAS, pages 282–298, 2008.
27. F. Laroussinie, A. Meyer, and E. Petonnet. Counting CTL. In FOSSACS, pages
206–220, 2010.
28. P. Madhusudan and G. Parlato. The tree width of auxiliary storage. In POPL,
pages 283–294, 2011.
29. R. Mayr. Decidability and Complexity of Model Checking Problems for InfiniteState Systems. PhD thesis, TU-München, 1998.
30. M. Musuvathi and S. Qadeer. Iterative context bounding for systematic testing ofmultithreaded programs. In PLDI, pages 446–455, 2007.
31. Wikipedia. http://en.wikipedia.org/wiki/Producer-consumer_problem.
32. S. Qadeer. The case for context-bounded verification of concurrent programs. In
SPIN, pages 3–6, 2008.
33. G. Ramalingam. Context-sensitive synchronization-sensitive analysis is undecidable. In TOPLAS, 2000.
34. S. Qadeer and J. Rehof. Context-bounded model checking of concurrent software.
In TACAS, pages 93–107, 2005.
35. K. Sen and M. Viswanathan. Model checking multithreaded programs with asynchronous atomic methods. In CAV, pages 300–314, 2006.
36. D. Suwimonteerabuth, J. Esparza, and S. Schwoon. Symbolic context-bounded
analysis of multithreaded java programs. In SPIN, pages 270–287, 2008.
37. D. Suwimonteerabuth, S. Schwoon, and J. Esparza. jmoped: A java bytecodechecker based on moped. In TACAS, pages 541–545, 2005.
38. 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.
39. S. La Torre, P. Madhusudan, and G. Parlato. Analyzing recursive programs using
a fixed-point calculus. In PLDI, pages 211–222, 2009.
40. K. N. Verma, H. Seidl, and T. Schwentick. On the complexity of equational hornclauses. In CADE, pages 337–352, 2005.

16

A

Fix for Verma et al. [40]It is well known that the reduction of encoding of the Parikh image of a given
CFG as an existential Presburger formula given by Verma et al. [40] contains
a small mistake, resulting in a formula that is under-constrained. This bug has
been fixed by Barner in a 2006 Master’s thesis [6]. We describe briefly here thebug and the fix that we implemented in our work (which is logically equivalent
to Barner’s).
The formula uses a number of variables which correspond to a derivation treeof the CFG and are summarised below.
– Variables xA for each terminal A denote the number of occurrences of theterminal A.
– Variables yp for each production rule p denotes the number of times the
production rule p is used in the derivation.
There are two parts to the formula. The first part expresses the fact that the
number of production rules fired and terminals generated are consistent. E.g., if
a rule p = B → A is fired i times, and is the only rule generating the terminal A,
then xA must equal yp . Similarly, the number of times p is used cannot exceed
the number of B non-terminals generated by other production rules (and theinitial non-terminal).
The second part of the formula contains the mistake. It’s role is to ensurethat production rules don’t appear “out of thin air”. E.g., a rule p = B → AB
(where A is a terminal and B a non-terminal) could be self-supporting under theconditions in the first part of the formula. E.g., if p is the only rule using andgenerating B, we can assign any value to yp since the first part of the formula will
only assert that the number of Bs generated is equal to the number consumed.
That is, yp = yp .
In order to prevent such situations, Verma et al. show that it is enough tobe able to define a kind of spanning tree, rooted at the initial non-terminal withan edge between two nodes α and β if a rule p has been used that has α on
the right-hand size and β on the left. Thus, all terminals and non-terminals
appearing in the derivation tree must be rooted to the initial non-terminal inthis spanning tree.
To this end, the formula introduces variables zA and zB for each terminal
and non-terminal, representing the distance in the spanning tree from the root(and take the value 0 if the (non-)terminal does not appear). We conjunct– xA = 0 ∨ zA > 0 for each terminal A, and– For each terminal or non-terminal A where p1 , . . . , pl are the productions
with A on the right-hand side and B1W, . . . , Bl are their corresponding leftl
hand sides, then we have (zA = 0) ∨ i=1 (zA = zBi + 1 ∧ ypi > 0 ∧ zBi >0), unless Bi is the initial non-terminal, then the corresponding disjunct iszA = 1 ∧ ypi > 0.
However,W this formula is under-constrained: in the final conjunct we may havezA = 0 or li=1 (. . .). The first disjunct catches the case where a non-terminal A
17

is not generated, but does not enforce that it is in fact the case that A is not
generated.
Consider, for example, the CFG defined by p1 = S → A and p2 = B → AB,
for initial non-terminal S, non-terminal B and terminal A. The only derivation
is S → A. However, by assigning zS = 1, zA = 2, and zB = 0 we are able tosatisfy the formula with any assignment to xA and yp2 such that xA + 1 = yp2 .
We correct the second part of the formula by replacing (zA = 0) with (zA =Vl
0 ∧ i=1 ypi = 0), which enforces that, when zA = 0, the non-terminal A is norule generating A has been used. The full, corrected, second part of the formula
is given below.
– xA = 0 ∨ zA > 0 for each terminal A, and– For each terminal or non-terminal A where p1 , . . . , pl are the productions
with A on the right-hand side andVB1 , . . . , Bl areWtheir corresponding leftllhand sides, then we have (zA = 0 ∧ i=1 ypi = 0) ∨ i=1 (zA = zBi + 1 ∧ ypi >0 ∧ zBi > 0), unless Bi is the initial non-terminal, then the corresponding
disjunct is zA = 1 ∧ ypi > 0.

B

Correctness of the Reachability Reduction

We prove the following lemmas for the reduction presented in Section 3, which
implies Theorem 1. We begin by recalling the definitions missing from HasRun,
since these are required for the proofs.
nFirst, since a mode vector is amember of REGn × [0, r]n × {↑, ↓} × [0, k], weeee
set me to be a tuple of variables regj , revj , arrj | j ∈ [1, n] , where:– regje is a variable that will range over [1, 2h] denoting which region the jthcounter is in (a number of the form 2i + 1 refers to ϕi , while 2i refers to ψi ).
– revje is a variable that will range over [0, r] denoting the number of reversals
that have been used thus far by the jth counter.
– arrje is a variable that will range over {0, 1} denoting the current arrow
direction, e.g., 0/1 for ↑/↓ (non-decrementing/non-incrementing mode).

We begin with Init(m1 ), which asserts that the initial mode vector respects
the initial configuration (q, u, v), where v = (c1 , . . . , cn ). Recalling that REG ={ϕ1 , . . . , ϕh , ψ1 , . . . , ψh }, we set
!
h 
n
^
^
regj1 = 2i − 1 ⇐⇒ ϕi (cj ) ∧1.
revj = 0 ∧Init(m1 ) ≡regj1 = 2i ⇐⇒ ψi (cj )
i=1

j=1

Recall that the target configuration is (q ′ , u′ , v ′ ), where v ′ = (c′1 , . . . , c′n ). We
assert that the end counter values match v ′ . This definition is given as follows.


n
X
^

u × zf (ctrj ,u,e,l)  = c′j .
EndVal(z) ≡j=1(ctrj ,u,e,l)18

Next, GoodSeq ensures that the sequence of mode vectors m1 , . . . , mNmax is
valid. For example, if the direction of a counter changes, then an extra reversal
is incurred. The formula is a conjunction of smaller formulas defined below.
One conjunct says that each revje must be a number in [0, r]. Likewise, we add
conjuncts expressing that each regje (resp. arrje ) ranges over [1, 2h] (resp. {0, 1}).
We also need to state that changes in the direction arrows incur an extra reversal(otherwise, no reversal is incurred). Hence, we add
k N^
max
^

0 ≤ revje ≤ r ∧j=1 e=1

k Nmax^−1  arre 6= arre+1 ⇒ rev e+1 = rev e + 1∧ 
^
j

j=1

e=1

j

j

j

arrje = arrje+1 ⇒ revje+1 = revje.

 e Nmaxmax
Next, the sequence {regje }N
e=1 must obey the changes in arrj e=1 . Hence, wehavek Nmax
^−1
^

j=1

e=1


regje < regje+1 ⇒ arrje+1 = 0 ∧ regje > regje+1 ⇒ arrje+1 = 1 .

I.e., since regions denote increasing intervals, going to higher (resp. lower) regions
mean the counter mode must be non-decrementing (resp. non-incrementing).
This completes the definition of GoodSeq.
Lastly, we give the formula Respect which requires that the counter tests
and actions fired within a mode are allowed. For example, a subtraction may notoccur on a counter in a non-decreasing phase, and counter tests may only occurin sympathetic regions. Again, this is a conjunction. First, when the jth counteris non-incrementing (resp. non-decrementing), we allow only non-negative (resp.
non-positive) counter increments:Vzf (ctrj ,u,e,l) = 0 ∧arrje = 0 ⇒(ctrj , u, e, l)


n N^
max
^


u<0
 .

V
 arrje = 1 ⇒zf (ctrj ,u,e,l) = 0 
j=1 e=1 (ctrj , u, e, l)u>0Secondly, the value of the jth counter at the beginning and end of each modemust respect the guessed mode vector. Let us first introduce some notation.
Observe that the value
jth counter at the end of ethmode vector can beP of theP
e−1 P
expressed by cj +(ctrj ,u,e,0) u ×
e′ =1(ctrj ,u,e′ ,l)∈Γ ′ u × zf (ctrj ,u,e′ ,l) +ezf (ctrj ,u,e,0) . Let us denote this term by EndCounterj . Similarly, the value at
Pe−1 P
the beginning of the eth mode is cj + e′ =1 (ctrj ,u,e′ ,l)∈Γ ′ u × zf (ctrj ,u,e′ ,l) . We
denote this term by StartCounterej . Hence, this second conjunct is
 
h 
k N^
max ^
^
regje = 2l − 1 ⇒ ϕl (EndCounterej ) ∧ ϕl (StartCounterej ) ∧.
regje = 2l ⇒ ψl (EndCounterej ) ∧ ψl (StartCounterej )j=1 e=1 l=1

19

Finally, we need to express that no invalid counter tests are executed in a given
mode. To test whether a constraint θ is satisfied by the values v = (c1 , . . . , cn ) of
the counters, it is necessary and sufficient to test whether θ is satisfied by some
vector v ′ = (c′1 , . . . , c′n ), where each ci lies in the same region as c′i . Therefore,
the desired property can be expressed as:
N^
max
e=1

^

zf (θ,e) > 0 ⇒ θ (StartCountere1 , . . . , StartCounteren ) .

(θ,e)∈Γ ′We are now ready to prove the correctness of our reduction.
Lemma 1. If there is an r-reversal and k-synchronisation-bounded run from cto c′ , then HasRun is satisfiable.
Proof. Assume there is an r-reversal and k-synchronisation-bounded run of C.
γ2γ1γh
We show that HasRun is satisfiable. Let π = c0 =⇒ c1 =⇒ · · · =⇒ ch be the runof C, where c = c0 and c′ = ch .
First, we assign to m1 , . . . , mNmax the values corresponding to the evolutionof the modes in π.
Next, we assign z 1 , . . . , z m . We can divide c0 c1 . . . ch into k + 1 phases
C1 , . . . , Ck+1 such that there exist −1 = j0 ≤ · · · ≤ jk+1 = h and C1 = c0 . . . cj1 ,. . . , Ck = cj(k−1) +1 . . . cjk+1 . In addition, for all i ∈ [1, k + 1] and all j(i−1) < j <γ ji+1γ j+1ji , we have cj ===⇒ cj+1 is an internal transition, and, when i ≤ k, cji ===⇒ cji+1
is a synchronising transition. Note, that we allow the phases to be empty (whenthe start index is greater than the end index).
We will construct accepting runs of each Pi′ . We may split each phase further
by considering the evolution of the modes.
For each i ∈ [1, m], and each j ∈ [1, k + 1] extract from Cj all transitions
that are due to transitions of Pi . Furthermore, augment all control states withthe mode and the phase the transition took place in. This almost results in arun of Pi′ , except when an external process changes the mode. In this case weuse the rules
ε((q, e, g), a) ֒−→ ((q, e + 1, g), a)
to bridge the gap. Finally, we construct an accepting run of Pi′ by concatenating
the runs for each phase as follows.
For i > 1, we use the rules(δ,q,q′ ,e,g,l)((q, e, g), a) ֒−−−−−−−→ ((q ′ , e + l, g + 1), a)
to form the connections, where (δ, θ, u) is the synchronising transition used tobridge the phases, and l ∈ {0, 1} is 1 only if the counter updates caused a modechange. For i = 1, we use(δ,q,q′ ,e,g,l)(θ,e)(ctr1 ,u1 ,e,l)...(ctrn ,un ,e,l)((q, e, g), a) ֒−−−−−−−−−−−−−−−−−−−−−−−−−−−−→ ((q ′ , e, g + 1), a) .
20

We assign to z i the Parikh image of the run defined above. Because weassigned a valid sequence of modes to the mode vectors, and valid Parikh imagesof Pi′ to z i that respect the modes, we have that Init, GoodSeq, and Imagei aresatisfied. To see that Respect and EndVal are satisfied, observe that the counter
actions come from a valid accepting run. Finally, OneChange is true since only
one thread changed the mode, and Syncs is satisfied since we assigned valid
synchronising transitions to the output tuples (δ, q, q ′ , e, g, l).
Lemma 2. If the formula HasRun is satisfiable, then there is an r-reversal andk-synchronisation-bounded run from c to c′ .
Proof. Take an accepting assignment to m1 , . . . , mNmax and z 1 , . . . , z m . Because
Init, GoodSeq, Imagei , Respect and EndVal are satisfied, we obtain the following. First, since Init (m1 ) is satisfied, we know that the assignment to the firstmode vector is the initial vector. From GoodSeq (m1 , . . . , mNmax ), we know thatthe assignments to the sequenceof mode vectors represents
a valid progression ofP′
modes. Then, Respect1≤i≤m z i , m1 , . . . , mNmax ensures that each Pi onlyuses counter tests that are congruent with the mode e that Pi′ is operating in,that the counter updates (ctre , u, j, l) performed by the threads Pi′ are also congruent with the current mode e, and finally that the sum of all counter actions
performed by all threads results in counter values that respect their modes (since
all threads output the same characters for their counter actions Respect remains
correct whether one thread is performing counter actions, or several). Similarly,P
ensures that the total of the counter actions performed
EndVal1≤i≤m z i

throughout the collected runs of the Pi′ result in counter values matching thefinal configuration.
Given this, We will construct a valid r-reversal and k-synchronisation-bounded
run of C.
γi

γi

γ ih

i
2
1
· · · −−→
cihi be the accepting runs of the Pi′ . Since
ci1 −→Let πi = ci0 −→Syncs is satisfied, we know that each πi uses the same number of guessed synchronising transitions, and each phase change happens in the same mode of eachPi′ . For convenience, assume all k phases are used. For each g ∈ [1, k + 1], let
jg be the mode the gth phase starts in (this is the same for all i) and jg′ be theiiimode the gth phase ends in. Thus we can build Cgi = C(jC(j· · · C(j
′ ,g)
g ,g)
g +1,g)gifor all g ∈ [1, k + 1] where each C(j,g)
is the sub-run of Pi′ in mode j and phaseg.
For each phase g ∈ [1, k + 1] and mode j ∈ [1, Nmax] we build the following
run πjg of C. These will be used to build π g for each phase. Observe that, since
OneChange is true, only one mode change rule can be fired amongst all threads.
Hence, all but one Pi′ must change modes using the rules
ε((q, e, g), a) ֒−→ ((q, e + 1, g), a)in the case when it is not a synchronising transition that causes the mode change,and′(δ,q,q ,e,g,1)((q, e, g), a) ֒−−−−−−−−→ ((q ′ , e + 1, g + 1), a)21

iin the other case (note that this rule will not be used in a particular C(j,g), butrather as the synchronising transition discussed below).
i
In the first — non-synchronising — case, these rules bridge each C(j,g)
and
g
g
i
g
C(j+1,g) and are not included in πj or π . Let rj be the only mode changing
transition amongst all is connecting mode j in phase g and mode j + 1 (whenj + 1 ≤ Nmax ). Note that this transition does not appear in any sub-run spannediby a C(j,g)(since it connects two). If a synchronising transition causes the modechange, let rjg be some no-op rule assumed for convenience. Note, if a synchronising transition causes the mode change, j is the last mode in the phase.
i
The run πjg then is the concatenation of the runs of each C(j,g)
for each i inggany order. Then π is the concatenation of each πj in order of the js, using thetransition rjg to connect each mode together.
Finally, we append each π g in order of the gs to form the required run of
C. To glue each π g together, we use a synchronising transition that changes themode if required. We know that this is possible since Syncs is satisfied. That thecounters tests and actions are valid follows from Respect and EndVal. Note that
Syncs also ensures that all processes agree on whether a synchronising transition
also caused a mode change.

C

Alternative Synchronisation-Bounded Reachability
Construction

We present an alternative encoding of the synchronisation-bounded reachability
problem that results in smaller formulas than the encoding presented in the main
body. However, the reduced size, experimentally, comes at the cost of slower solve
times.
In the main text, we kept a component g in each P ′ that we constructed,
which stored the number of synchronisation-switches that had taken place. Conceptually, however, this number can be kept in a simple counter, and hence canbe stored in the mode vectors. Doing this naively, however, would result in many
more transitions of the pushdown systems as it would have to perform counterchecks to determine what synchronisation actions to perform. However, if wemake the encoding aware of the special nature of this extra counter, we do not
require any additional rules. However, this means that we require a more detailed
explanation of the reduction.
The final formula will take the shape
Init(m1 ) ∧ GoodSeq(m1 , . . . , mNmax )VImagei (z i )
∧


1≤i≤m




P



∧ Respect
z
,
m
,
.
.
.
,
m
i
1
N
∃m1 , . . . , mNmax ∃z 1 . . . z m 
max
1≤i≤m



P




∧ OneChangez1≤i≤m i



P
P
∧ EndVal1≤i≤m z i1≤i≤m z i ∧ Syncs
22


P
and Syncs (z 1 , . . . , z m ) are thewhere the formulas OneChange
1≤i≤m z imain differences compared to the single thread case. In addition, further adaptations need to be made within other aspects of the formula.
C.1

The Mode Vectors

We begin with the vectors m1 , . . . , mNmax . This part remains largely unchanged
from the first reduction, except for the addition of a mode component corresponding to the number of synchronisations performed so far.
n
A vector in REGn × [0, r]n × {↑, ↓} × [0, k] is said to be a mode vector.
Given a path π from configurations c to c′ , we may associate a mode vector toeach configuration in π that records for each counter: which region its value isin, how many reversals its used, whether its phase is non-decrementing (↑) or
non-incrementing (↓) and, in the final component, how many synchronisations
have taken place. There are at most Nmax := |REG| × (r + 1) × n + (k + 1) =2hn(r + 1) + (k + 1) distinct mode vectors in any valid sequence of mode vectors.
C.2

Constructing Pi′

We define the pushdown automataPi′ = Q′i , Σi , Γ ′ , ∆′i , qi0 , 1, 1 , {fi } × [1, Nmax ]for each Pi in C and assume that all Qi are pairwise disjoint.
As before Pi′ will make “visible” the counter tests, counter updates andsynchronisations performed. Additional constraints introduced later ensure thatthese operations are valid.
More formally, let Q′i = Qi × [1, Nmax ]. We define Γ ′ implicitly from thetransition relation. In fact, Γ ′ is a (finite) subset of{ (ctre , u, j, l) | e ∈ [1, n], u ∈ Z, j ∈ [1, Nmax ], l ∈ {0, 1} }S ∪ (ConstX × [1, Nmax ])(StateCons× Qi × Qi × [1, Nmax ]) .
∪1≤i≤mHere, elements in {0, 1} signify whether the mode vector should change. Weγ→ (q ′ , w, u) ∈ ∆i wheredefine ∆′i to be the smallest set such that, if (q, a, θ) ֒−u = (u1 , . . . , un ) then for each e ∈ [1, Nmax], ∆′i contains(θ,e)(ctr1 ,u1 ,e,0)...(ctrn ,un ,e,0)((q, e), a) ֒−−−−−−−−−−−−−−−−−−−−→ ((q ′ , e), w)
and, if e ∈ [1, Nmax ), ∆′i also has(θ,e)(ctr1 ,u1 ,e,1)...(ctrn ,un ,e,1)((q, e), a) ֒−−−−−−−−−−−−−−−−−−−−→ ((q ′ , e + 1), w) .
These rules are the rules required in the single thread case. We need additionalrules to reflect the multi-threaded environment. In particular, an external thread23

may change the mode, or a synchronising transition may occur. To account forthis ∆′i also has for each q ∈ Qi a ∈ Σi , e ∈ [1, Nmax ),ε((q, e), a) ֒−→ ((q, e + 1), a)
and, for each q, q ′ ∈ Qi , e ∈ [1, Nmax ) and (δ, θ, u) ∈ ∆g where u = (u1 , . . . , un ),when i > 1,
(δ,q,q′ ,e)((q, e), a) ֒−−−−−−→ ((q ′ , e + 1), a) .
and when i = 1,
(δ,q,q′ ,e)(θ,e)(ctr1 ,u1 ,e,0)...(ctrn ,un ,e,0)((q, e), a) ֒−−−−−−−−−−−−−−−−−−−−−−−−−−→ ((q ′ , e + 1), a) .
Additionally, we have when i = 1,
(δ,q,q′ ,e)(θ,e)(ctr1 ,u1 ,e,1)...(ctrn ,un ,e,1)((q, e), a) ֒−−−−−−−−−−−−−−−−−−−−−−−−−−→ ((q ′ , e + 1), a) .
That is, Pi′ non-deterministically guesses the effect of non-internal transitions
and P1′ is responsible for performing the required counter updates. Note thatthe information contained in the output character (δ, q, q ′ , e) allows us to checkthat synchronising transitions take place in the same order and in the samemodes across all threads.
C.3

Constructing The Formula

Fix an ordering γ1 < . . . < γl on Γ ′ . By f we denote a function mapping γi to ifor each i ∈ [1, l]. The formula we require is of the form given above. The formulas
Init, GoodSeq, Respect, and EndVal are defined as in the single thread case withadjustments to incorporate the number of synchronisations into the mode vector;
the reader may refer to [20] for the original definitions and description. For the
Imagei we apply the linear-time algorithm of [40] on each Pi′ to obtain Imagei
such that for each n ∈ Nl we have n ∈ P(L(Pi′ )) iff Imagei (n) holds.
nSince a mode vector is a memberof REGn × [0, r]n × {↑, ↓} × [0, k], we set
eeeme to be a tuple of variables regj , revj , arrj | j ∈ [1, n] , where:– regje is a variable that will range over [1, 2h] denoting which region the jthcounter is in (a number of the form 2i + 1 refers to ϕi , while 2i refers to ψi ).
– revje is a variable that will range over [0, r] denoting the number of reversals
that have been used thus far by the jth counter.
– arrje is a variable that will range over {0, 1} denoting the current arrow
direction, e.g., 0/1 for ↑/↓ (non-decrementing/non-incrementing mode).
– syne is a variable that ranges over [0, k] and denotes the number of synchronisations performed thus far.
24

We begin with Init(m1 ), which asserts that the initial mode vector respects
the initial configuration (q, u, v), where v = (c1 , . . . , cn ). More precisely,
!
h 
n
^
^
regj1 = 2i − 1 ⇐⇒ ϕi (cj ) ∧1∧ syn1 = 0 .
revj = 0 ∧Init(m1 ) ≡regj1 = 2i ⇐⇒ ψi (cj )
i=1

j=1

Next, GoodSeq ensures that the sequence of mode vectors m1 , . . . , mNmax is
valid. For example, if the direction of a counter changes, then an extra reversal isincurred on that counter, or, if a synchronisation occurs, then the synchronisation component is updated accordingly. The formula is a conjunction of smaller
formulas defined below. One conjunct says that each revje must be a number in[0, r]. Likewise, we add conjuncts expressing that each regje (resp. arrje , syne )ranges over [1, 2h] (resp. {0, 1}, [0, k]). We also need to state that changes inthe direction arrows incur an extra reversal (otherwise, no reversal is incurred).
Hence, we add
k N^
max
^

0 ≤ revje ≤ r ∧j=1 e=1

k Nmax^−1  arre 6= arre+1 ⇒ rev e+1 = rev e + 1∧ 
^
j

j=1

e=1

j

j

j

arrje = arrje+1 ⇒ revje+1 = revje.

 e Nmaxmax
The sequence {regje }N
e=1 must obey the changes in arrj e=1 . Hence, we havek Nmax
^−1
^

j=1

e=1


regje < regje+1 ⇒ arrje+1 = 0 ∧ regje > regje+1 ⇒ arrje+1 = 1 .

I.e., since regions denote increasing intervals, going to higher (resp. lower) regions
mean the counter mode must be non-decrementing (resp. non-incrementing).
Finally, we need to assert that the number of synchronisations only increases,
using
Nmax
^−1

syne = syne+1 ∨ syne = syne+1 + 1 .
e=1This completes the definition of GoodSeq.
The formula Respect requires that the counter tests and actions fired withina mode are allowed. For example, a subtraction may not occur on a counter in a
non-decreasing phase, and counter tests may only occur in sympathetic regions.
It remains unchanged from the sequential case, and is reproduced below. Again,
this is a conjunction. First, when the jth counter is non-incrementing (resp.
non-decrementing), we allow only non-negative (resp. non-positive) counter increments:Vzf (ctrj ,u,e,l) = 0 ∧arrje = 0 ⇒(ctrj , u, e, l)


n N^
max
^


u
<
0
 .

V

 arrje = 1 ⇒z=
0f (ctrj ,u,e,l)
j=1 e=1(ctrj , u, e, l)u>025

Secondly, the value of the jth counter at the beginning and end of each modemust respect the guessed mode vector. Let us first introduce some notation.
Observe that the value
jth counter at the end of ethmode vector can beP of theP
e−1 P
expressed by cj +(ctrj ,u,e,0) u ×
e′ =1(ctrj ,u,e′ ,l)∈Γ ′ u × zf (ctrj ,u,e′ ,l) +zf (ctrj ,u,e,0) . Let us denote this term by EndCounterej . Similarly, the value at
Pe−1 P
the beginning of the eth mode is cj + e′ =1 (ctrj ,u,e′ ,l)∈Γ ′ u × zf (ctrj ,u,e′ ,l) . We
denote this term by StartCounterej . Hence, this second conjunct is
 
k N^
h 
max ^
^
regje = 2l − 1 ⇒ ϕl (EndCounterej ) ∧ ϕl (StartCounterej ) ∧.
regje = 2l ⇒ ψl (EndCounterej ) ∧ ψl (StartCounterej )j=1 e=1 l=1

Finally, we need to express that no invalid counter tests are executed in a given
mode. To test whether a constraint θ is satisfied by the values v = (c1 , . . . , cn ) of
the counters, it is necessary and sufficient to test whether θ is satisfied by some
vector v ′ = (c′1 , . . . , c′n ), where each ci lies in the same region as c′i . Therefore,
the desired property can be expressed as:
N^
max

^

zf (θ,e) > 0 ⇒ θ (StartCountere1 , . . . , StartCounteren ) .

e=1 (θ,e)∈Γ ′The final formula we take from the sequential case is EndVal, which checks
that the counter operations applied during the run leave each counter in thecorrect value, as given in the final configuration. Recall that the target configuration is (q ′ , u′ , v ′ ), where v ′ = (c′1 , . . . , c′n ). We assert that the end countervalues match v ′ . This definition is given as follows.

EndVal(z) ≡

n
^

j=1




X

(ctrj ,u,e,l)u × zf (ctrj ,u,e,l)  = c′j .

It remains for us to define OneChange and Syncs. We use OneChange to assertthat only one thread may be responsible for firing the transition that changes agiven mode of the counters to the next. That is,
OneChange (z) ≡^zf (ctrj ,u,e,1) > 0 ⇒(ctrj , u, e, 1)(ctrj , u′ , e, 1)u′ 6= uzf (ctrj ,u,e,1) = 1∧ zf (ctrj ,u′ ,e,1) = 0

.

The role of Syncs is to ensure that the synchronising transitions taken by′
P1′ , . . . , Pm
are valid. Note that, by design, each Pi′ will only output at most one
26

character of the form (δ, q, q ′ , e) for each e ∈ [1, Nmax ). We define


e
e+1
syn
<
syn
⇒


V
W
 ∧

Sync(δ,e) (z) ∧ AllFired(δ,e)
1≤e<Nmax(δ,θ,u)∈∆g
Syncs (z) ≡!
VVsyne = syne+1 ⇒zf (δ,q,q′ ,e) = 0
1≤e<Nmax

δ,q,q′

where Sync(δ,e) is δ with each atomic state constraint yi = q replaced by theformula_zf (δ,q,q′ ,e) > 0(δ,q,q′ ,e)and each atomic state constraint yi′ = q ′ replaced by the formula_
zf (δ,q,q′ ,e) > 0 .
(δ,q,q′ ,e)Finally,
AllFired(δ,e) ≡^_zf (δ,q,q′ ,e) > 0 .

1≤i≤m q,q′ ∈Qi

C.4

Correctness

We prove the following lemmas, which give the correctness of our encoding.
Lemma 3. If there is an r-reversal and k-synchronisation-bounded run from cto c′ , then HasRun is satisfiable.
Proof. Assume there is an r-reversal and k-synchronisation-bounded run of C.
γ2γ1γh
We show that HasRun is satisfiable. Let π = c0 =⇒ c1 =⇒ · · · =⇒ ch be the runof C, where c = c0 and c′ = ch .
First, we assign to m1 , . . . , mNmax the values corresponding to the evolutionof the modes in π.
Next, we assign z 1 , . . . , z m . We can divide c0 c1 . . . ch into Nmax phases —according to the changes in mode vectors — such that there exist −1 = j0 ≤· · · ≤ jNmax = h and C1 = c0 . . . cj1 , . . . , CNmax = cj(Nmax −1) +1 . . . cjNmax . Inγ j+1

addition, for all e ∈ [1, Nmax ] and all j(e−1) < j < je , we have cj ===⇒ cj+1 is atransition that is not synchronising and does not change a counter mode, and,γ ji+1

when i < Nmax , cji ===⇒ cji+1 is a synchronising transition or a transition thatchanges a counter mode. Note, that we allow the phases to be empty (when thestart index is greater than the end index).
We will construct accepting runs of each Pi′ . For each j ∈ [1, Nmax ] extractfrom Cj all transitions that are due to transitions of Pi . Furthermore, augment
all control states with the mode the transition took place in. This results in arun of Pi′ .
27

Finally, we construct an accepting run of Pi′ by concatenating the runs foreach phase as follows.
For i > 1, we use the rules(δ,q,q′ ,e)((q, e), a) ֒−−−−−−→ ((q ′ , e + 1), a)
to form the connections when (δ, θ, u) is a synchronising transition used to bridge
the phases. For i = 1, we use(δ,q,q′ ,e)(θ,e)(ctr1 ,u1 ,e,l)...(ctrn ,un ,e,l)((q, e), a) ֒−−−−−−−−−−−−−−−−−−−−−−−−−−→ ((q ′ , e), a)
where l = 1 iff a counter mode is changed by the transition.
When the phases are bridged by a counter update by process j 6= i, we use
the rulesε((q, e), a) ֒−→ ((q, e + 1), a)
to bridge the gap. If the phases are bridged by a counter update by process i,
we use the corresponding transition(θ,e)(ctr1 ,u1 ,e,1)...(ctrn ,un ,e,1)((q, e), a) ֒−−−−−−−−−−−−−−−−−−−−→ ((q ′ , e + 1), w)
of Pi′ .
We assign to z i the Parikh image of the run defined above. Because weassigned a valid sequence of modes to the mode vectors, and valid Parikh imagesof Pi′ to z i that respect the modes, we have that Init, GoodSeq, and Imagei aresatisfied. To see that Respect and EndVal are satisfied, observe that the counter
actions come from a valid accepting run. Finally, OneChange is true since only
one thread changed the mode, and Syncs is satisfied since we assigned valid
synchronising transitions to the output tuples (δ, q, q ′ , e).
Lemma 4. If the formula HasRun is satisfiable, then there is an r-reversal andk-synchronisation-bounded run from c to c′ .
Proof. Take an accepting assignment to m1 , . . . , mNmax and z 1 , . . . , z m . Because
Init, GoodSeq, Imagei , Respect and EndVal are satisfied we know that there
are runs of Pi′ such that the counter operations in each mode respect the mode
vectors (which represent a valid mode sequence) and the initial and target values.
We will construct a valid k-synchronisation-bounded run of C.
γi

γi

γ ih

1
2
i
Let πi = ci0 −→ci1 −→· · · −−→
cihi be the accepting runs of the Pi′ . Since
Syncs is satisfied, we know that each πi uses the same number of guessed synchronising transitions, and each phase change happens in the same mode of eachPi′ . For convenience, assume all k phases are used. For each g ∈ [1, k + 1], let
jg be the mode the gth phase starts in (this is the same for all i) and jg′ be theiiimode the gth phase ends in. Thus we can build Cgi = C(jC(j· · · C(j
′ ,g)
g ,g)
g +1,g)gifor all g ∈ [0, k] where each C(j,g)
is the sub-run of Pi′ in mode j and phase g.

28

Observe that the mode changes during a phase can only be caused by counter
updates (since a synchronising transition will end the phase).
For each phase g ∈ [0, k] and mode j ∈ [1, Nmax] we build the following
run πjg of C. These will be used to build π g for each phase. Observe that, since
OneChange is true, only one mode change rule can be fired amongst all threads.
Hence, all but one Pi′ must change modes using the rules
ε((q, e), a) ֒−→ ((q, e + 1), a)in the case when it is not a synchronising transition that causes the mode change,and(δ,q,q′ ,e)((q, e), a) ֒−−−−−−→ ((q ′ , e + 1), a)iin the other case (note that this rule will not be used in a particular C(j,g), butrather as the synchronising transition discussed below).
i
In the first — non-synchronising — case, these rules bridge each C(j,g)
and
g
g
i
g
C(j+1,g) and are not included in πj or π . Let rj be the only mode changing
transition amongst all is connecting mode j in phase g and mode j + 1 (whenj + 1 ≤ Nmax ). Note that this transition does not appear in any sub-run spannediby a C(j,g)(since it connects two). If a synchronising transition causes the modechange, let rjg be some no-op rule assumed for convenience. Note, if a synchronising transition causes the mode change, j is the last mode in the phase.
ifor each i in
The run πjg then is the concatenation of the runs of each C(j,g)
ggany order. Then π is the concatenation of each πj in order of the js, using thetransition rjg to connect each mode together.
Finally, we append each π g in order of the gs to form the required run of
C. To glue each π g together, we use a synchronising transition that changes thecounters component of mode if required. We know that this is possible sinceSyncs is satisfied. That the counters tests and actions are valid follows from
Respect and EndVal.

D

Optimisation Proofs and Definitions

In this section we present proofs and definitions omitted from Section 5.
D.1

Context-Bounded Model Checking

We refine the encoding of context-bounded model checking given in Section 4 byminimising the number of positions where synchronisations may occur, leading
to performance gains in our experiments. To do this, we add a boolean flag tothe control state that indicates whether a synchronisation is permitted.
Definition 9. Given a n-ClPDS C = (P1 , . . . , Pm , G, X). Let # be a symbol not
in G. We define from each Pi = (Qi , Σi , {ε} , ∆i , X) with Qi = G × Q′i the pushdown system PiS = QSi ∪ {fi } , Σi , {ε} , ∆Si , X where QSi = Qi × (G ∪ {#}) ×{0, 1} and ∆Si is the smallest set containing
29

γ

γ

1. ((g1 , q1 , 0), a, θ1 ) ֒−→ ((g1 , q2 , 0), w, u1 ) when we have the rule ((g1 , q1 ), a, θ1 ) ֒−→((g2 , q2 ), w, u1 ) ∈ ∆i , andε2. ((g, q, 0), a, tt) ֒−→ (fi , w, 0) for all q, a appearing as a head in the final configuration and g = # or g appears in the final configuration, andγγ
3. ((g1 , q1 , 0), a, tt) ֒−→ ((g1 , q1 , 1), a, 0) whenever we have a rule ((g1 , q1 ), a, θ) ֒−→((g2 , q2 ), w, u) ∈ ∆i such that(a) an update to g occurs, i.e. g 6= g ′ , or(b) an update to the counters occurs, i.e. u contains a non-zero update, or(c) the counter values need to be up-to-date, i.e. θ is not independent of thecounter values, orγ
4. ((g, q1 , 0), a, tt) ֒−→ ((g, q1 , 1), a, 0) for all g ∈ G whenever the G componentγ
needs to be up-to-date, i.e. there exists some g ′ ∈ G such that ((g ′ , q1 ), a, θ) ֒−→((g ′ , q2 ), w, u) ∈ ∆i but we don’t have the rule for all g ′ ∈ G.
γ
5. ((g, q1 , 0), a, tt) ֒−→ ((g, q1 , 1), a, 0) for all g ∈ G whenever q1 appears in the
final configuration.
S
Finally, let CS = P1S , . . . , Pm
, ∆g , X, r , where ∆g = {(δ, tt, 0)} such thatthe formula δ(q11 , . . . , qn1 , q12 , . . . , qn2 ) holds only when there is some g ∈ G and
1 ≤ i 6= j ≤ n such that
1. qi1 = (g, q, 1) and qi2 = (#, q, 0) for some q, and2. qj1 = (#, q, 0) and qj2 = (g, q, 0) for some q, and3. for all i′ 6= i and i′ 6= j, qi1′ = (#, q, 0) and qi2′ = (#, q, 0) for some q.
We show that this simulation is correct.
Theorem 2. Given a n-ClPDSr C, there is an r-reversal and k-context-bounded
run from the initial configuration (g, q1 , w1 , . . . , qm , wm , v) to the given final con′′figuration (g ′ , q1′ , w1′ , . . . , qm
, wm
, v ′ ) iff there is an r-reversal and k-synchronisationS
bounded run of C from ((g, q1 , 0) , w1 , (#, q2 , 0) , . . . , (#, qm , 0) , wm , v) to the′configuration (f1 , w1′ , . . . , fm , wm
, v ′ ).
Proof. We prove the only if direction first. Take a run of C. From this we construct a run of CS . Let T1 , . . . , Tk be the k phases, which are sequences ti1 , . . . , tihiof the transitions fired during the ith phase. We can manipulate these phasessuch that the last configuration in each phase is of the form (g1 , . . . , qj , wj , . . .),where j is the active pushdown system and either qj is in the final configuration,or the next transition applied to Pj matches one of the cases 3-5 of Definition 9.
We do this as follows. First, suppose there are no more counter tests, updates
to the counters or g, or transitions depending on g occurring on Pj . The we canmove all subsequent transitions of Pj into the current phase since they neither
depend on nor update any globally accessible information. Otherwise, we takeall transitions occurring before the next such transition, and move them into thecurrent phase. There are then two cases: either the last configuration has a final
state of Pj or the next transition of Pj (in a later phase) leading from the lastconfiguration matches a case 3-5 of Definition 9.
30


1
1
Let g 1 , q11 , w11 , . . . , qm
, wm
, v 1 be the initial configuration of phase i and11
g 2 , q11 , w11 , . . . , qj2 , wj , . . . qm
, wm
, v 2 be the last. Using rules from case 1 of Definition 9 we obtain a run from
 1 1
1#, q11 , 0 , w11 , . . . , g 1 , qj1 , 0 , wj , . . . , #, qm, 0 , wm,v
to
 1 2
1#, q11 , 0 , w11 , . . . , g 2 , qj2 , 0 , wj , . . . , #, qm, 0 , wm,v .

Then, both of the above cases for the last configuration imply a transition to
the configuration
 1 2
1#, q11 , 0 , w11 , . . . , g 2 , qj2 , 1 , wj , . . . , #, qm, 0 , wm,v

from which we can apply a global synchronisation to the first configuration of thenext phase. We can then use rules from case 2 at the end of the last phase to reachthe final configuration. Hence, since there are k phases, only k synchronisations
are required, and we have a k-synchronisation-bounded run of CS .
In the if direction, we take an r-reversal and k-synchronisation-bounded runof CS . We separate this into phases T1 , . . . , Tk such that each Ti is connected to
the next by a global synchronisation. By construction, during each Ti only one
Pj may move, since all but one have # in their global component, from which
no transitions are possible.
Next, we remove the last transition of each phase which made a change ofthe final component of some control state from 0 to 1. Note that now each phase
only contains 0 in the last component of the control states. Finally, the lasttransition of each PiS replaces some g i , qi′ , 0 with fi where g i is either # or g ′ .
Note that by construction, all but one g i will be #, and the other will be g ′ .
We remove these final transitions. It is now straightforward to project the runin each phase to a run of C. These runs compose to form a k-context-bounded
run of C satisfying the properties required.
D.2

Minimising Communicating Pushdown Systems with Counters

We show that the minimisation by elimination of removable heads — given in
Definition 8 — preserves reachability properties.
Theorem 3. For any r-reversal and k-synchronisation-bounded run from theinitial to final configuration of a given n-SyncPDSr with a pushdown system
P with n counters and a removable head q, a, there exists an r-reversal andk-synchronisation-bounded accepting run of the n-SyncPDS with P replaced by
Pq,a with the same Parikh image, and vice versa.
Proof. We can divide the run of the n-SyncPDS in to a number h of phases
which we will represent as T0 , t1 , T1 . . . , Th−1 , th , Th where each Ti is a sequenceof rules (transitions) of a pushdown system in the n-SyncPDS. The phases are
such that between each ti is either a global synchronisation or non-zero countermodification, and there are no such transitions within an Ri .
31

Now, take any two transitions t and t′ in the run belonging to P that crossa configuration of P with the head q, a. Note that this cannot include any rules
ti since these are global synchronisations or counter updates, and no counter
update rule can contain a removable head. Let c1 , c2 and c3 be the configurations of P these rules connect. Observe that since c2 has a removable head, andremovable heads cannot loop, neither c1 nor c3 have the head q, a.
If t and t′ occur within the same Ti then we can safely replace them withthe rule formed by their concatenation as in ∆1 of the definition of Pq,a . Thisis because the counters are not changed and no global synchronisation used theconfiguration c2 .
If t appears in Ti and t′ in Tj such that i < j, then we can perform the same
replacement. This remains safe for two reasons. First, we know q, a is removableand hence t′ did not contain a counter test, so any counter updates between
Ti and Tj will not affect the applicability of t′ (hence it can be merged into t).
Secondly, if any of the transitions between Ti and Tj are global synchronisations,
we can use the fact that for q, a to remain removable, it must be the case that q
is a sink state. Hence, the control state after t′ remains q, and hence the global
synchronisations can still be applied.
Note that when combining rules, in order to remain within the definition of∆1 , we need that t is not a pop transition. This is implicit in c2 having the headq, a: if t were a pop transition, then q, a would be a return location, and hence
not removable.
Finally, we need to check that no removed transitions are used in the modified run. This follows since all instances of that are not in the initial or final
configuration q, a have been removed. Furthermore, since q, a is removable, itcannot occur in the initial configuration.
After these modifications, we have a run of Pq,a with the same Parikh image.
The proof in the opposite direction is straightforward: take any run of Pq,a .
For each transition t in ∆1 there exist two rules in ∆ with which t may bereplaced. The only subtlety in this replacement is that the counter test θ2 may
be invalidated by the update u1 . However, a condition on q, a being a removable
head is that θ2 does not depend on the counter values, hence the two transitions
may safely replace t.
D.3

Minimising CFG size via pushdown reachability table

We describe an algorithm for computing the reachability lookup table specialisedfor PDA from section 3. It is an adaptation of the pre∗ algorithm from [16].

E

Pushdown Translator Input Language

We present the syntax of the pushdown translator tool. A simple example program is as follows:32

Algorithm 1 Compute reachability lookup table for PDA output from ourtranslation

Input: P = Q, Σ, Γ, ∆, q 0 , 1, 1 , {f } × [1, Nmax ] × [1, k + 1]
Output: table rel with entries of form (p, a, q, d, d′ )rel := ∅; ∆′ := ∅; ∆1 := ∅;γ
for all t ∈ ∆ such that t = ((p, e, g), a) ֒−→ ((p′ , e′ , g ′ ), ǫ) do
d1 := e′ − e; d2 := g ′ − g;add (p, a, q, d1 , d2 ) to trans;
end forfor all t ∈ ∆ doγ
t = ((p, e, q), a) ֒−→ ((p′ , e′ , g ′ ), w);′
d1 := e − e; d2 := g ′ − g;add (p, a, q, w, d1 , d2 ) to ∆1 ;end for
while trans 6= ∅ do
pop t = (q, b, q ′ , d1 , d2 ) from trans;
if (q, b, q ′ , d′1 , d2 ) ∈/ rel for each d′1 ≤ d1 then
add t to rel;
for all (p, a, q, b, d′1 , d′2 ) ∈ ∆1 ∪ ∆′ do
if (p, a, q ′ , d, d2 + d′2 ) ∈/ trans for each d ≤ d1 + d′1 then′′add (p, a, q , d1 + d1 , d2 + d′2 ) to trans;
end ifend forfor all (p, a, q, bc, d′1 , d′2 ) ∈ ∆1 do
if (p, a, q ′ , c, d, d2 + d′2 ) ∈/ ∆′ for each d ≤ d1 + d′1 then′′add (p, a, q , c, d1 + d1 , d2 + d′2 ) to ∆′ ;end iffor all (q ′ , c, q ′′ , d′′1 , d′′2 ) ∈ rel doif (p, a, q ′′ , d, d2 + d′2 + d′′2 ) ∈/ trans for each d ≤ d1 + d′1 + d′′1 then′′′′′add (p, a, q , d1 + d1 + d1 , d2 + d′2 , d′′2 ) to trans;
end ifend forend forend ifend while
return rel

33

counter c reversals 0
start main1
start main2
constraint (once == 1) && (twice == 2) && (c == 1)
switches 1
procedure main1()
begin
c++;
echo once;
end;
procedure main2()
begin
echo twice;echo twice;
end;
E.1

Program Header

These statements appear before the program procedure declarations and specify
the shape of the program.
shared bool ident
Global boolean variable shared between all threads.
bool ident
Global boolean variable each thread has a copy of.
counter ident reversals nGlobal shared counter variable with n reversals.
start ident
A thread starting with method ident (first thread is first run).
constraint cc
A counter constraint cc that should hold at the end of a run for an error tohave occurred.
switches n
The number of context-switches.
34

E.2

Program Body

Procedures are defined with the following syntax.
procedure ident (bool ident , . . . , bool ident )bool ident...
bool ident
statement
A method declaration taking several parameters and having several local
variables. Note that return values should be passed through a global variable.
Statements then have the following form.
ident : statement
A statement labelled ident .
beginstatement...
statementend;
A sequence of statements.
ident = vc, . . . , ident = vc;
Assignment of boolean variables with boolean constraint evaluations. The
value of the right hand sides is determined by the variable values preceding
the statement.
lock ident ;Locks a shared boolean variable. This assigns 1 to the variable if it is 0, andblocks otherwise.
unlock ident ;Unlocks a shared boolean variable. This assigns 0 to the variable if it is 1,
and blocks otherwise.
ident ++;
Increment by one the counter ident .
ident −−;
Decrement by one the counter ident .
ident += n;Increment the counter ident by n.
35

ident -= n;Decrement the counter ident by n.
if {vc} [cc] thenstatement
elsestatement
A conditional branch. Note that either the boolean variable condition {vc}or the counter condition [cc] may be omitted. If both are present, both must
hold. Both may be replaced by ?? for a non-deterministic branch. The elsebranch may also be omitted.
while {vc} [cc] dostatement
While loop. The conditions are as in the if statement above.
switchcase: statement...
case: statement
end;
A non-deterministic branch: executes one of the case statements.
goto ident ;Jump to a given statement label.
ident (vc, . . . , vc);
Call procedure ident with parameter values given by the vc.
return;Return from a procedure. Note, return values should be passed using global
variables.
assert {vc} [cc];Assert a condition. Note that either the boolean variable condition {vc} or
the counter condition [cc] may be omitted. If both are present, both must
hold. An error is found if an assertion evaluations to false.
skip;
A no-op statement.
echo ident ;Output a ident action. The counts of these actions can be used in the constraint specified using constraint.

36