arXiv:cs/0601038v1 [cs.LO] 10 Jan 2006

Under consideration for publication in Theory and Practice of Logic Programming

1

Constraint-based Automatic Verification of
Abstract Models of Multithreaded Programs
GIORGIO DELZANNO
Dipartimento di Informatica e Scienze dell’Informazione, Università di Genova
via Dodecaneso 35, 16146 Genova - Italy
(e-mail: giorgio@disi.unige.it)
submitted 17 December 2003; revised 13 April 2005; accepted 15 January 2006

Abstract
We present a technique for the automated verification of abstract models of multithreaded
programs providing fresh name generation, name mobility, and unbounded control.
As high level specification language we adopt here an extension of communication finitestate machines with local variables ranging over an infinite name domain, called TDL
programs. Communication machines have been proved very effective for representing communication protocols as well as for representing abstractions of multithreaded software.
The verification method that we propose is based on the encoding of TDL programs
into a low level language based on multiset rewriting and constraints that can be viewed as
an extension of Petri Nets. By means of this encoding, the symbolic verification procedure
developed for the low level language in our previous work can now be applied to TDL
programs. Furthermore, the encoding allows us to isolate a decidable class of verification
problems for TDL programs that still provide fresh name generation, name mobility, and
unbounded control. Our syntactic restrictions are in fact defined on the internal structure
of threads: In order to obtain a complete and terminating method, threads are only allowed
to have at most one local variable (ranging over an infinite domain of names).
KEYWORDS: Constraints, Multithreaded Programs, Verification.

1 Introduction
Andrew Gordon (Gordon 2001) defines a nominal calculus to be a computational
formalism that includes a set of pure names and allows the dynamic generation of
fresh, unguessable names. A name is pure whenever it is only useful for comparing
for identity with other names. The use of pure names is ubiquitous in programming
languages. Some important examples are memory pointers in imperative languages,
identifiers in concurrent programming languages, and nonces in security protocols.
In addition to pure names, a nominal process calculus should provide mechanisms
for concurrency and inter-process communication. A computational model that provides all these features is an adequate abstract formalism for the analysis of multithreaded and distributed software.

2

Giorgio Delzanno

The Problem Automated verification of specifications in a nominal process calculus
becomes particularly challenging in presence of the following three features: the possibility of generating fresh names (name generation); the possibility of transmitting
names (name mobility); the possibility of dynamically adding new threads of control
(unbounded control). In fact, a calculus that provides all the previous features can
be used to specify systems with a state-space infinite in several dimensions. This
feature makes difficult (if not impossible) the application of finite-state verification
techniques or techniques based on abstractions of process specifications into Petri
Nets or CCS-like models. In recent years there have been several attempts of extending automated verification methods from finite-state to infinite-state systems
(Abdulla and Nylén 2000; Kesten et al. 2001). In this paper we are interested in investigating the possible application of the methods we proposed in (Delzanno 2001)
to verification problems of interest for nominal process calculi.
Constraint-based Symbolic Model Checking In (Delzanno 2001) we introduced a
specification language, called MSR(C), for the analysis of communication protocols
whose specifications are parametric in several dimensions (e.g. number of servers,
clients, and tickets as in the model of the ticket mutual exclusion algorithm shown
in (Bozzano and Delzanno 2002)). MSR(C) combines multiset rewriting over first
order atomic formulas (Cervesato et al. 1999) with constraints programming. More
specifically, multiset rewriting is used to specify the control part of a concurrent
system, whereas constraints are used to symbolically specify the relations over local data. The verification method proposed in (Delzanno 2005) allows us to symbolically reason on the behavior of MSR(C) specifications. To this aim, following
(Abdulla et al. 1996; Abdulla and Nylén 2000) we introduced a symbolic representation of infinite collections of global configurations based on the combination of
multisets of atomic formulas and constraints, called constrained configurations.1
The verification procedure performs a symbolic backward reachability analysis by
means of a symbolic pre-image operator that works over constrained configurations
(Delzanno 2005). The main feature of this method is the possibility of automatically
handling systems with an arbitrary number of components. Furthermore, since we
use a symbolic and finite representation of possibly infinite sets of configurations,
the analysis is carried out without loss of precision.
A natural question for our research is whether and how these techniques can be
used for verification of abstract models of multithreaded programs.
Our Contribution In this paper we propose a sound, and fully automatic verification
method for abstract models of multithreaded programs that provide name generation, name mobility, and unbounded control. As a high level specification language
we adopt here an extension with value-passing of the formalism of (Ball et al. 2001)
1

Notice that in (Abdulla et al. 1996; Abdulla and Nylén 2000) a constraint denotes a symbolic
state whereas we use the word constraint to denote a symbolic representation of the relation of
data variables (e.g. a linear arithmetic formula) used as part of the symbolic representation of
sets of states (a constrained configuration).

Constraint-based Verification of Abstract Multithreaded Programs

3

based on families of state machines used to specify abstractions of multithreaded
software libraries. The resulting language is called Thread Definition Language
(TDL). This formalism allows us to keep separate the finite control component of a
thread definition from the management of local variables (that in our setting range
over a infinite set of names), and to treat in isolation the operations to generate
fresh names, to transmit names, and to create new threads. In the present paper we
will show that the extension of the model of (Ball et al. 2001) with value-passing
makes the model Turing equivalent.
The verification methodology is based on the encoding of TDL programs into a
specification in the instance MSRN C of the language scheme MSR(C) of(Delzanno 2001).
MSRN C is obtained by taking as constraint system a subclass of linear arithmetics
with only = and > relations between variables, called name constraints (N C). The
low level specification language MSRN C is not just instrumental for the encoding
of TDL programs. Indeed, it has been applied to model consistency and mutual
exclusion protocols in (Bozzano and Delzanno 2002; Delzanno 2005). Via this encoding, the verification method based on symbolic backward reachability obtained
by instantiating the general method for MSR(C) to NC-constraints can now be applied to abstract models of multithreaded programs. Although termination is not
guaranteed in general, the resulting verification method can succeed on practical
examples as the Challenge-Response TDL program defined over binary predicates
we will illustrated in the present paper. Furthermore, by propagating the sufficient
conditions for termination defined in (Bozzano and Delzanno 2002; Delzanno 2005)
back to TDL programs, we obtain an interesting class of decidable problems for abstract models of multithreaded programs still providing name generation, name
mobility, and unbounded control.
Plan of the Paper In Section 2 we present the Thread Definition Language (TDL)
with examples of multithreaded programs. Furthermore, we discuss the expressiveness of TDL programs showing that they can simulate Two Counter Machines. In
Section 3, after introducing the MSRN C formalism, we show that TDL programs
can be simulated by MSRN C specifications. In Section 4 we show how to transfer
the verification methods developed for MSR(C) to TDL programs. Furthermore, we
show that safety properties can be decided for the special class of monadic TDL
programs. In Section 5 we address some conclusions and discuss related work.
2 Thread Definition Language (TDL)
In this section we will define TDL programs. This formalism is a natural extension
with value-passing of the communicating machines used by (Ball et al. 2001) to
specify abstractions of multithreaded software libraries.
Terminology Let N be a denumerable set of names equipped with the relations =
and 6= and a special element ⊥ such that n 6= ⊥ for any n ∈ N . Furthermore, let
V be a denumerable set of variables, C = {c1 , . . . , cm } a finite set of constants, and
L a finite set of internal action labels. For a fixed V ⊆ V, the set of expressions is

4

Giorgio Delzanno

defined as E = V ∪ C ∪ {⊥} (when necessary we will use E(V ) to explicit the set of
variables V upon which expressions are defined). The set of channel expressions is
defined as Ech = V ∪ C. Channel expressions will be used as synchronization labels
so as to establish communication links only at execution time.
A guard over V is a conjunction γ1 , . . . , γs , where γi is either true, x = e or x 6= e
with x ∈ V and e ∈ E for i : 1, . . . , s. An assignment α from V to W is a conjunction
like xi := ei where xi ∈ W , ei ∈ E(V ) for i : 1, . . . k and xr 6= xs for r 6= s. A
message template m over V is a tuple m = hx1 , . . . , xu i of variables in V .
Definition 1
A TDL program is a set T = {P1 , . . . , Pt } of thread definitions (with distinct names
for local variables control locations). A thread definition P is a tuple hQ, s0 , V, Ri,
where Q is a finite set of control locations, s0 ∈ Q is the initial location, V ⊆ V is
a finite set of local variables, and R is a set of rules. Given s, s′ ∈ Q, and a ∈ L, a
rule has one of the following forms2 :
a

• Internal move: s −−→ s′ [γ, α], where γ is a guard over V , and α is an assignment from V to V ;
a
• Name generation: s −−→ s′ [x := new], where x ∈ V , and the expression new
denotes a fresh name;
a
• Thread creation: s −−→ s′ [run P ′ with α], where P ′ = hQ′ , t, W, R′ i ∈ T , and
α is an assignment from V to W that specifies the initialization of the local
variables of the new thread;
e!m
• Message sending: s −−→ s′ [γ, α], where e is a channel expression, m is a message template over V that specify which names to pass, γ is a guard over V ,
and α is an assignment from V to V .
e?m
• Message reception: s −−−→ s′ [γ, α], where e is a channel expression, m is a
message template over a new set of variables V ′ (V ′ ∩ V = ∅) that specifies
the names to receive, γ is a guard over V ∪ V ′ and α is an assignment from
V ∪ V ′ to V .
Before giving an example, we will formally introduce the operational semantics of
TDL programs.
2.1 Operational Semantics
In the following we will use N to indicate the subset of used names of N . Every
constant c ∈ C is mapped to a distinct name nc 6= ⊥ ∈ N , and ⊥ is mapped to ⊥.
Let P = hQ, s, V, Ri and V = {x1 , . . . , xk }. A local configuration is a tuple p =
hs′ , n1 , . . . , nk i where s′ ∈ Q and ni ∈ N is the current value of the variable xi ∈ V
for i : 1, . . . , k.
A global configuration G = hN, p1 , . . . , pm i is such that N ⊆ N and p1 , . . . , pm are
local configurations defined over N and over the thread definitions in T . Note that
2

In this paper we keep assignments, name generation, and thread creation separate in order to
simplify the presentation of the encoding into MSR.

Constraint-based Verification of Abstract Multithreaded Programs

5

there is no relation between indexes in a global configuration in G and in T ; G is
a pool of active threads, and several active threads can be instances of the same
thread definition.
Given a local configuration p = hs′ , n1 , . . . , nk i, we define the valuation ρp as
ρp (xi ) = ni if xi ∈ V , ρp (c) = nc if c ∈ C, and ρp (⊥) = ⊥. Furthermore, we
say that ρp satisfies the guard γ if ρp (γ) ≡ true, where ρp is extended to constraints in the natural way (ρp (ϕ1 ∧ ϕ2 ) = ρp (ϕ1 ) ∧ ρp (ϕ2 ), etc.).
The execution of x := e has the effect of updating the local variable x of a thread
with the current value of e (a name taken from the set of used values N ). On the contrary, the execution of x := new associates a fresh unused name to x. The formula
run P with α has the effect of adding a new thread (in its initial control location)
to the current global configuration. The initial values of the local variables of the
generated thread are determined by the execution of α whose source variables are
the local variables of the parent thread. The channel names used in a rendez-vous
are determined by evaluating the channel expressions tagging sender and receiver
rules. Value passing is achieved by extending the evaluation associated to the current configuration of the receiver so as to associate the output message of the sender
to the variables in the input message template. The operational semantics is given
via a binary relation ⇒ defined as follows.
Definition 2
Let G = hN, . . . , p, . . .i, and p = hs, n1 , . . . , nk i be a local configuration for P =
hQ, s, V, Ri, V = {x1 , . . . , xk }, then:
a

• If there exists a rule s −−→ s′ [γ, α] in R such that ρp satisfies γ, then G ⇒
hN, . . . , p′ , . . .i (meaning that only p changes) where p′ = hs′ , n′1 , . . . , n′k i,
n′i = ρp (ei ) if xi := ei is in α, n′i = ni otherwise, for i : 1, . . . , k.
a
• If there exists a rule s −−→ s′ [xi := new] in R, then G ⇒ hN ′ , . . . , p′ , . . .i
′
′
′
′
where p = hs , n1 , . . . , nk i, ni is an unused name, i.e., n′i ∈ N \ N , n′j = nj
for every j 6= i, and N ′ = N ∪ {n′i };
a
• If there exists a rule s −−→ s′ [run P ′ with α] in R with P ′ = hQ′ , t0 , W, R′ i,
W = {y1 , . . . , yu }, and α is defined as y1 := e1 , . . . , yu := eu then G ⇒
hN, . . . , p′ , . . . , qi (we add a new thread whose initial local configuration is q)
where p′ = hs′ , n1 , . . . , nk i, and q = ht0 , ρp (e1 ), . . . , ρp (eu )i.
• Let q = ht, m1 , . . . , mr i (distinct from p) be a local configuration in G associated with P ′ = hQ′ , t0 , W, R′ i.
e!m

e′ ?m′

Let s −−→ s′ [γ, α] in R and t −−−−→ t′ [γ ′ , α′ ] in R′ be two rules such that
m = hx1 , . . . , xu i, m′ = hy1 , . . . , yv i and u = v (message templates match).
We define σ as the value passing evaluation σ(yi ) = ρp (xi ) for i : 1, . . . , u,
and σ(z) = ρq (z) for z ∈ W ′ .
Now if ρp (e) = ρp (e′ ) (channel names match), ρp satisfies γ, and that σ
satisfies γ ′ , then hN, . . . , p, . . . , q, . . .i ⇒ hN, . . . , p′ , . . . , q′ , . . .i where p′ =
hs′ , n′1 , . . . , n′k i, n′i = ρp (v) if xi := v is in α, n′i = ni otherwise for i : 1, . . . , k;
q′ = ht′ , m′1 , . . . , m′r i, m′i = σ(v) if ui := v is in α′ , m′i = mi otherwise for
i : 1, . . . , r.

6

Giorgio Delzanno

Definition 3
An initial global configuration G0 has an arbitrary (but finite) number of threads
with local variables all set to ⊥. A run is a sequence G0 G1 . . . such that Gi ⇒ Gi+1
for i ≥ 0. A global configuration G is reachable from G0 if there exists a run from
G0 to G.
Example 1
Let us consider a challenge and response protocol in which the goal of two agents
Alice and Bob is to exchange a pair of new names hnA , nB i, the first one created
by Alice and the second one created by Bob, so as to build a composed secret key.
We can specify the protocol by using new names to dynamically establish private
channel names between instances of the initiator and of the responder. The TDL
program in Figure 1 follows this idea. The thread Init specifies the behavior of the
initiator. He first creates a new name using the internal action f resh, and stores
it in the local variable nA . Then, he sends nA on channel c (a constant), waits for
a name y on a channel with the same name as the value of the local variable nA
(the channel is specified by variable nA ) and then stores y in the local variable
mA . The thread Resp specifies the behavior of the responder. Upon reception of
a name x on channel c, he stores it in the local variable nB , then creates a new
name stored in local variable mB and finally sends the value in mB on channel with
the same name as the value of nB . The thread M ain non-deterministically creates
new thread instances of type Init and Resp. The local variable x is used to store
new names to be used for the creation of a new thread instance. Initially, all local
variables of threads Init/Resp are set to ⊥. In order to allow process instances to
participate to several sessions (potentially with different principals), we could also
add the following rule
restart

stopA −−−−−→ initA [nA := ⊥, mA := ⊥]
In this rule we require that roles and identities do not change from session to
session.3 Starting from G0 = hN0 , hinit, ⊥ii, and running the Main thread we can
generate any number of copies of the threads Init and Resp each one with a unique
identifier. Thus, we obtain global configurations like
hN, hinitM , ⊥i,
hinitA , i1 , ⊥, ⊥i, . . . , hinitA , iK , ⊥, ⊥i,
hinitB , iK+1 , ⊥, ⊥i, . . . , hinitB , iK+L , ⊥, ⊥i i
where N = {⊥, i1, . . . , iK , iK+1 , . . . , iK+L } for K, L ≥ 0. The threads of type Init
and Resp can start parallel sessions whenever created. For K = 1 and L = 1 one
possible session is as follows.
Starting from
h{⊥, i1 , i2 }, hinitM , ⊥i, hinitA , i1 , ⊥, ⊥i, hinitB , i2 , ⊥, ⊥ii
3

By means of thread and fresh name creation it is also possible to specify a restart rule in which
a given process takes a potential different role or identity.

Constraint-based Verification of Abstract Multithreaded Programs

7

T hread Init(local idA , nA , mA );
f resh

initA −−−−→ genA
c!hnA i

genA −−−−→ waitA
n ?hyi

waitA −−A
−−−→ stopA

[nA := new]
[true]
[mA := y]

T hread Resp(local id, nB , mB );
c?hxi

initB −−−→ genB

[nB := x]

f resh

genB −−−−→ readyB
n !hm i

[mB := new]

B
readyB −−B−−−−
→ stopB

[true]

T hread M ain(local x);
id

initM −−→ create
newA
create −−−−→
initM
new
→ initM
create −−−−B

[x := new]
[run Init with idA := x, nA := ⊥, mA := ⊥, x := ⊥]
[run Resp with idB := x, nB := ⊥, mB := ⊥, x := ⊥B ]

Fig. 1. Example of thread definitions.

if we apply the first rule of thread Init to hinitA , i1 , ⊥, ⊥i we obtain
h{⊥, i1 , i2 , a1 }, hinitM , ⊥i, hgenA , i1 , a1 , ⊥i, hinitB , i2 , ⊥, ⊥ii
where a1 is the generated name (a1 is distinct from ⊥, i1 , and i2 ). Now if we apply
the second rule of thread Init and the first rule of thread Resp (synchronization
on channel c) we obtain
h{⊥, i1 , i2 , a1 }, hinitM , ⊥i, hwaitA , i1 , a1 , ⊥i, hgenB , i2 , a1 , ⊥ii
If we apply the second rule of thread Resp we obtain
h{⊥, i1 , i2 , a1 , a2 }, hinitM , ⊥i, hwaitA , i1 , a1 , ⊥i, hreadyB , i2 , a1 , a2 ii
Finally, if we apply the last rule of thread Init and Resp (synchronization on
channel a1 ) we obtain
h{⊥, i1 , i2 , a1 , a2 }, hinitM , ⊥i, hstopA , i1 , a1 , a2 i, hstopB , i2 , a1 , a2 ii
Thus, at the end of the session the thread instances i1 and i2 have both a local
copy of the fresh names a1 and a2 . Note that a copy of the main thread hinitM , ⊥i
is always active in any reachable configuration, and, at any time, it may introduce
new threads (either of type Init or Resp) with fresh identifiers. Generation of fresh
names is also used by the threads of type Init and Resp to create nonces. Furthermore, threads can restart their life cycle (without changing identifiers). Thus,
in this example the set of possible reachable configurations is infinite and contains
configurations with arbitrarily many threads and fresh names. Since names are
stored in the local variables of active threads, the local data also range over an
infinite domain.
✷

8

Giorgio Delzanno
2.2 Expressive Power of TDL

To study the expressive power of the TDL language, we will compare it with the
Turing equivalent formalism called Two Counter Machines. A Two Counters Machine configurations is a tuple hℓ, c1 = n1 , c2 = n2 i where ℓ is control location taken
from a finite set Q, and n1 and n2 are natural numbers that represent the values
of the counters c1 and c2 . Each counter can be incremented or decremented (if
greater than zero) by one. Transitions combine operations on individual counters
with changes of control locations. Specifically, the instructions for counter ci are as
follows
Inc: ℓ1 : ci := ci + 1; goto ℓ2 ;
Dec: ℓ1 : if ci > 0 then ci := ci − 1; goto ℓ2 ; else goto ℓ3 ;
A Two Counter Machine consists then of a list of instructions and of the initial
state hℓ0 , c1 = 0, c2 = 0i. The operational semantics is defined according to the intuitive semantics of the instructions. Problems like control state reachability are
undecidable for this computational model.
The following property then holds.
Theorem 1
TDL programs can simulate Two Counter Machines.
Proof
In order to define a TDL program that simulates a Two Counter Machine we
proceed as follows. Every counter is represented via a doubly linked list implemented
via a collection of threads of type Cell and with a unique thread of type Last
pointing to the head of the list. The i-th counter having value zero is represented
as the empty list Cell(i, v, v), Last(i, v, w) for some name v and w (we will explain
later the use of w). The i-th counter having value k is represented as
Cell(i, v0 , v0 ), Cell(i, v0 , v1 ), . . . , C(i, vk−1 , vk ), Last(i, vk , w)
for distinct names v0 , v1 , . . . , vk . The instructions on a counter are simulated by
sending messages to the corresponding Last thread. The messages are sent on
channel Zero (zero test), Dec (decrement), and Inc (increment). In reply to each
of these messages, the thread Last sends an acknowledgment, namely Y es/N o for
the zero test, DAck for the decrement, IAck for the increment operation. Last
interacts with the Cell threads via the messages tstC, decC, incC acknowledged
by messages z/nz, dack. iack. The interactions between a Last thread and the Cell
threads is as follows.
Zero Test Upon reception of a message hxi on channel Zero, the Last thread with
local variables id, last, aux checks that its identifier id matches x - see transition
from Idle to Busy - sends a message hid, lasti on channel tstC directed to the cell
pointed to by last (transition from Busy to W ait), and then waits for an answer. If
the answer is sent on channel nz, standing for non-zero, (resp. z standing for zero)
- see transition from W ait to AckN Z (resp. AckZ) - then it sends its identifier on

Constraint-based Verification of Abstract Multithreaded Programs

9

Thread Last(local id, last, aux);
(Zero test)
Zero?hxi

Idle −−−−−−→ Busy

[id = x]

tstC!hid,lasti

Busy −−−−−−−−−→ W ait
nz?hxi

W ait −−−−→ AckN Z

[id = x]

z?hxi

W ait −−−→ AckZ

[id = x]

Y es!hidi

AckZ −−−−−→ Idle
No!hidi

AckN Z −−−−−→ idle
(Decrement)
Dec?hxi

Idle −−−−−→ Dbusy

[id = x]

decC!hid,lasti

DBusy −−−−−−−−−→ DW ait
dack?hx,ui

DW ait −−−−−−−→ DAck

[id = x, last := u]

DAck!hidi

DAck −−−−−−−→ Idle
(Increment)
Inc?hxi

Idle −−−−−→ IN ew

[id = x]

new

[aux := new]

run

[run Cell with idc := id; prev := last; next := aux]

IN ew −−−→ IRun
IRun −−→ IAck
IAck!hidi

IAck −−−−−−→ Idle

[last := aux]

Fig. 2. The process defining the last cell of the linked list associated to a counter

channel N o (resp. Y es) as an acknowledgment to the first message - see transition
from AckN Z (resp. Z) to Idle. As shown in Fig. 3, the thread Cell with local
variables idc, prev, and next that receives the message tstC, i.e., pointed to by a
thread Last with the same identifier as idc, sends an acknowledgment on channel
z (zero) if prev = next, and on channel nz (non-zero) if prev 6= next.
Decrement Upon reception of a message hxi on channel Dec, the Last thread with
local variables id, last, aux checks that its identifier id matches x (transition from
Idle to Dbusy), sends a message hid, lasti on channel decC directed to the cell
pointed to by last (transition from Busy to W ait), and then waits for an answer.

10

Giorgio Delzanno
Thread Cell(local idc, prev, next);
(Zero test)
tstC?hx,ui

idle −−−−−−−→ ackZ [x = idc, u = next, prev = next]
tstC?hx,ui

idle −−−−−−−→ ackN Z [x = idc, u = next, prev 6= next]
z!hidci

ackZ −−−−→ idle
nz!hidci

ackN Z −−−−−→ idle
(Decrement)
dec?hx,ui

idle −−−−−−→ dec [x = idc, u = next, prev 6= next]
dack!hidc,previ

dec −−−−−−−−−−→ idle

Fig. 3. The process defining a cell of the linked list associated to a counter
If the answer is sent on channel dack (transition from DW ait to DAck) then it
updates the local variable last with the pointer u sent by the thread Cell, namely
the prev pointer of the cell pointed to by the current value of last, and then sends
its identifier on channel DAck to acknowledge the first message (transition from
DAck to Idle).
As shown in Fig. 3, a thread Cell with local variables idc, prev, and next that
receives the message decC and such that next = last sends as an acknowledgment
on channel dack the value prev.
Increment To simulate the increment operation, Last does not have to interact with
existing Cell threads. Indeed, it only has to link a new Cell thread to the head of
the list (this is way the Cell thread has no operations to handle the increment
operation). As shown in Fig. 2 this can be done by creating a new name stored in
the local variable aux (transition from IN ew to IRun) and spawning a new Cell
thread (transition from IRun to IAck) with prev pointer equal to last, and next
pointer equal to aux. Finally, it acknowledges the increment request by sending its
identifier on channel IAck and updates variable last with the current value of aux.

Two Counter Machine Instructions We are now ready to use the operations provided by the thread Last to simulate the instructions of a Two Counter Machine.
As shown in Fig. 4, we use a thread CM with two local variables id1 , id2 to represent the list of instructions of a 2CM with counters c1 , c2 . Control locations of the
Two Counter Machines are used as local states of the thread CM . The initial local
state of the CM thread is the initial control location. The increment instruction
on counter ci at control location ℓ1 is simulated by an handshaking with the Last
thread with identifier idi : we first send the message Inc!hidi i, wait for the acknowledgment on channel IAck and then move to state ℓ2 . Similarly, for the decrement

Constraint-based Verification of Abstract Multithreaded Programs

11

Thread CM (local id1 , id2 );
..
.
(Instruction : ℓ1 : ci := ci + 1; goto ℓ2 ; )
Inc!hid i

ℓ1 −−−−−−i→ waitℓ1
IAck!hxi

waitℓ1 −−−−−−→ ℓ2 [x = idi ]
..
.
(Instruction : ℓ1 : ci > 0 then ci := ci − 1; goto ℓ2 ; else goto ℓ3 ; )
Zero!hid i

ℓ1 −−−−−−−i→ waitℓ1
NZAck?hxi

waitℓ1 −
−−−−−−−
→ decℓ1 [x = idi ]
Dec!hid i

decℓ1 −−−−−−i→ wdecℓ1
DAck?hyi

wdecℓ1 −−−−−−→ ℓ2 [y = idi ]
ZAck?hxi

waitℓ1 −−−−−−→ ℓ3 [x = idi ]
..
.

Fig. 4. The thread associated to a 2CM.

Thread Init(local nid1 , p1 , nid2 , p2 );
f reshId

init −−−−−→ init1 [nid1 := new]
f reshP

init1 −−−−−→ init2 [p1 := new]
runC

init2 −
−−−→ init3 [run Cell with idc := nid1 ; prev := p1 ; next := p1 ]
runL

init3 −−−→ init4 [run Last with idc := nid1 ; last := p1 ; aux := ⊥]
f reshId

init4 −−−−−→ init5 [nid2 := new]
f reshP

init5 −−−−−→ init6 [p2 := new]
runC

init6 −
−−−→ init7 [run Cell with idc := nid2 ; prev := p2 ; next := p2 ]
runL

init7 −−−→ init8 [run Last with idc := nid2 ; last := p2 ; aux := ⊥]
runCM

init8 −−−−−→ init9 [run 2CM with id1 := nid1 ; id2 := nid2 ]

Fig. 5. The initialization thread.

instruction on counter ci at control location ℓ1 we first send the message Zero!hidi i.
If we receive an acknowledgment on channel N ZAck we send a Dec request, wait
for completion and then move to ℓ2 . If we receive an acknowledgment on channel
ZAck we directly move to ℓ3 .

12

Giorgio Delzanno

Initialization The last step of the encoding is the definition of the initial state of the
system. For this purpose, we use the thread Init of Fig. 5. The first four rules of Init
initialize the first counter: they create two new names nid1 (an identifier for counter
c1 ) and p1 , and then spawn the new threads Cell(nid1 , p1 , p1 ), Last(nid1 , p1 , ⊥).
The following four rules spawns the new threads Cell(nid2 , p2 , p2 ), Last(nid2 , p2 , ⊥).
After this stage, we create a thread of type 2CM to start the simulation of the instructions of the Two Counter Machines. The initial configuration of the whole
system is G0 = hinit, ⊥, ⊥i. By construction we have that an execution step from
hℓ1 , c1 = n1 , c2 = n2 i to hℓ2 , c1 = m1 , c2 = m2 i is simulated by an execution run going from a global configuration in which the local state of thread CM is hℓ1 , id1 , id2 i
and in which we have ni occurrences of thread Cell with the same identifier idi
for i : 1, 2, to a global configuration in which the local state of thread CM is
hℓ2 , id1 , id2 i and in which we have mi occurrences of thread Cell with the same
identifier idi for i : 1, 2. Thus, every executions of a 2CM M corresponds to an execution of the corresponding TDL program that starts from the initial configuration
G0 = hinit, ⊥, ⊥i.
As a consequence of the previous theorem, we have the following corollary.
Corollary 1
Given a TDL program, a global configurations G, and a control location ℓ, deciding
if there exists a run going from G0 to a global configuration that contains ℓ (control
state reachability) is an undecidable problem.
3 From TDL to MSRN C
As mentioned in the introduction, our verification methodology is based on a translation of TDL programs into low level specifications given in MSRN C . Our goal is
to extend the connection between CCS and Petri Nets (German and Sistla 1992)
to TDL and MSR so as to be able to apply the verification methods defined in
(Delzanno 2005) to multithreaded programs. In the next section we will summarize
the main features of the language MSRN C introduced in (Delzanno 2001).
3.1 Preliminaries on MSRN C
N C-constraints are linear arithmetic constraints in which conjuncts have one of
the following form: true, x = y, x > y, x = c, or x > c, x and y being two variables
from a denumerable set V that range over the rationals, and c being an integer.
The solutions Sol of a constraint ϕ are defined as all evaluations (from V to Q)
that satisfy ϕ. A constraint ϕ is satisfiable whenever Sol(ϕ) 6= ∅. Furthermore, ψ
entails ϕ whenever Sol(ψ) ⊆ Sol(ϕ). N C-constraints are closed under elimination
of existentially quantified variables.
Let P be a set of predicate symbols. An atomic formula p(x1 , . . . , xn ) is such that
p ∈ P, and x1 , . . . , xn are distinct variables in V. A multiset of atomic formulas is
indicated as A1 | . . . | Ak , where Ai and Aj have distinct variables (we use variable
renaming if necessary), and | is the multiset constructor.

Constraint-based Verification of Abstract Multithreaded Programs

13

In the rest of the paper we will use M, N , . . . to denote multisets of atomic formulas,
ǫ to denote the empty multiset, ⊕ to denote multiset union and ⊖ to denote multiset
difference. An MSRN C configuration is a multiset of ground atomic formulas, i.e.,
atomic formulas like p(d1 , . . . , dn ) where di is a rational for i : 1, . . . , n.
An MSRN C rule has the form M −→ M′ : ϕ, where M and M′ are two (possibly
empty) multisets of atomic formulas with distinct variables built on predicates in
P, and ϕ is an N C-constraint. The ground instances of an MSRN C rule are defined
as
Inst(M −→ M′ : ϕ) = {σ(M) −→ σ(M′ ) | σ ∈ Sol(ϕ)}
where σ is extended in the natural way to multisets, i.e., σ(M) and σ(M′ ) are
MSRN C configurations.
An MSRN C specification S is a tuple hP, I, Ri, where P is a finite set of predicate
symbols, I is finite a set of (initial) MSRN C configurations, and R is a finite set of
MSRN C rules over P.
The operational semantics describes the update from a configuration M to one of its
possible successor configurations M′ . M′ is obtained from M by rewriting (modulo
associativity and commutativity) the left-hand side of an instance of a rule into the
corresponding right-hand side. In order to be fireable, the left-hand side must be
included in M. Since instances and rules are selected in a non deterministic way, in
general a configuration can have a (possibly infinite) set of (one-step) successors.
Formally, a rule H −→ B : ϕ from R is enabled at M via the ground substitution
σ ∈ Sol(ϕ) if and only if σ(H) 4 M. Firing rule R enabled at M via σ yields the
new configuration
M′ = σ(B) ⊕ (M ⊖ σ(H))
We use M ⇒MSR M′ to denote the firing of a rule at M yielding M′ .
A run is a sequence of configurations M0 M1 . . . Mk with M0 ∈ I such that
Mi ⇒MSR Mi+1 for i ≥ 0. A configuration M is reachable if there exists M0 ∈ I
∗
∗
such that M0 ⇒MSR M, where ⇒MSR is the transitive closure of ⇒MSR . Finally, the successor and predecessor operators P ost and P re are defined on a set
of configurations S as P ost(S) = {M′ |M ⇒MSR M′ , M ∈ S} and P re(S) =
{M|M ⇒MSR M′ , M′ ∈ S}, respectively. P re∗ and P ost∗ denote their transitive
closure.
As shown in (Delzanno 2001; Bozzano and Delzanno 2002), Petri Nets represent a
natural abstractions of MSRN C (and more in general of MSR rule with constraints)
specifications. They can be encoded, in fact, in propositional MSR specifications
(e.g. abstracting away arguments from atomic formulas).
3.2 Translation from TDL to MSRN C
The first thing to do is to find an adequate representation of names. Since all we
need is a way to distinguish old and new names, we just need an infinite domain
in which the = and 6= relation are supported. Thus, we can interpret names in N

14

Giorgio Delzanno

either as integer of as rational numbers. Since operations like variable elimination
are computationally less expensive than over integers, we choose to view names
as non-negative rationals. Thus, a local (TDL) configuration p = hs, n1 , . . . , nk i
is encoded as the atomic formula p• = s(n1 , . . . , nk ), where ni is a non-negative
rational. Furthermore, a global (TDL) configuration G = hN, p1 , . . . , pm i is encoded
as an MSRN C configuration G•
p•1 | . . . | p•m | f resh(n)
where the value n in the auxiliary atomic formula f resh(n) is an rational number
strictly greater than all values occurring in p•1 , . . . , p•m . The predicate f resh will
allow us to generate unused names every time needed.
The translation of constants C = {c1 , . . . , cm }, and variables is defined as follows:
x• = x for x ∈ V, ⊥• = 0, c•i = i for i : 1, . . . , m. We extend ·• in the natural way
on a guard γ, by decomposing every formula x 6= e into x < e• and x > e• . We will
call γ • the resulting set of N C-constraints.4
Given V = {x1 , . . . , xk }, we define V ′ as the set of new variables {x′1 , . . . , x′k }.
Now, let us consider the assignment α defined as x1 := e1 , . . . , xk := ek (we add
assignments like xi := xi if some variable does not occur as target of α). Then, α•
is the N C-constraint x′1 = e•1 , . . . , x′k = e•k .
The translation of thread definitions is defined below (where we will often refer to
Example 1).
Initial Global Configuration Given an initial global configuration consisting of the
local configurations hsi , ni1 , . . . , niki i with nij = ⊥ for i : 1, . . . , u, we define the
following MSRN C rule
init → s1 (x11 , . . . , x1k1 ) | . . . | su (xu1 , . . . , xuku ) | f resh(x) :
x > C, x11 = 0, . . . , xuku = 0
here C is the largest rational used to interpret the constants in C.
For each thread definition P = hQ, s0 , V, Ri in T with V = {x1 , . . . , xk } we translate
the rules in R as described below.
a

Internal Moves For every internal move s −−→ s′ [γ, α], and every ν ∈ γ • we define
s(x1 , . . . , xk ) → s′ (x′1 , . . . , x′k ) : ν, α•
a

Name Generation For every name generation s −−→ s′ [xi := new], we define
^
s(x1 , . . . , xk ) | f resh(x) → s′ (x′1 , . . . , x′k ) | f resh(y) : y > x′i , x′i > x,
x′j = xj
j6=i
f resh

For instance, the name generation initA −−−−→ genA [n := new] is mapped into the
MSRN C rule initA (id, x, y)| f resh(u) −−→ genA (id′ , x′ , y ′ ) | f resh(u′ ) : ϕ where ϕ
4

As an example, if γ is the constraint x = 1, x 6= z then γ • consists of the two constraints
x = 1, x > z and x = 1, z > x.

Constraint-based Verification of Abstract Multithreaded Programs

15

is the constraint u′ > x′ , x′ > u, y ′ = y, id′ = id. The constraint x′ > u represents
the fact that the new name associated to the local variable n (the second argument
of the atoms representing the thread) is fresh, whereas u′ > x′ updates the current
value of f resh to ensure that the next generated names will be picked up from
unused values.
Thread Creation Let P = hQ′ , t0 , V ′ , R′ i and V ′ = {y1 , . . . , yu }. Then, for every
a
thread creation s −−→ s′ [run P with α], we define
s(x1 , . . . , xk ) → s′ (x′1 , . . . , x′k ) | t(y1′ , . . . , yu′ ) : x′1 = x1 , . . . , x′k = xk , α• .
new

A
initM [run Init with id := x, . . .] of Example 1.
E.g., consider the rule create −−−−→
Its encoding yields the MSRN C rule create(x) −−→ initM (x′ ) | initA (id′ , n′ , m′ ) : ψ,
where ψ represents the initialization of the local variables of the new thread x′ =
x, id′ = x, n′ = 0, m′ = 0.

Rendez-vous The encoding of rendez-vous communication is based on the use of
constraint operations like variable elimination. Let P and P ′ be a pair of thread
definitions, with local variables V = {x1 , . . . , xk } and V ′ = {y1 , . . . , yl } with V ∩
e′ ?m′

e!m

V ′ = ∅. We first select all rules s −−→ s′ [γ, α] in R and t −−−−→ t′ [γ ′ , α′ ] in R′ ,
such that m = hw1 , . . . , wu i, m′ = hw1′ , . . . , wv′ i and u = v. Then, we define the new
MSRN C rule
s(x1 , . . . , xk ) | t(y1 , . . . , yl ) → s′ (x′1 , . . . , x′k ) | t′ (y1′ , . . . , yl′ ) : ϕ
for every ν ∈ γ • and ν ′ ∈ γ ′• such that the NC-constraint ϕ obtained by eliminating w1′ , . . . , wv′ from the constraint ν ∧ ν ′ ∧ α• ∧ α′• ∧ w1 = w1′ ∧ . . . ∧ wv = wv′
nA ?hyi

is satisfiable. For instance, consider the rules waitA −−−−−→ stopA [mA := y] and
nB !hmB i

readyB −−−−−−→ stopB [true]. We first build up a new constraint by conjoining the
NC-constraints y = mB (matching of message templates), and nA = nB , m′A =
y, n′A = nA , m′B = mB , n′B = nB , id′1 = id1 , id′2 = id2 (guards and actions of
sender and receiver). After eliminating y we obtain the constraint ϕ defined as
nB = nA , m′A = mB , n′A = nA , m′B = mB , n′B = nB , id′1 = id1 , id′2 = id2 defined
over the variables of the two considered threads. This step allows us to symbolically
represent the passing of names. After this step, we can represent the synchronization of the two threads by using a rule that simultaneously rewrite all instances
that satisfy the constraints on the local data expressed by ϕ, i.e., we obtain the
rule
waitA (id1 , nA , mA )| readyB (id2 , nB , mB ) −→
stopA (id′1 , n′A , m′A ) | stopB (id′2 , n′B , m′B ) : ϕ
The complete translation of Example 1 is shown in Fig. 6 (for simplicity we have
applied a renaming of variables in the resulting rules). An example of run in the
resulting MSRN C specification is shown in Figure 7. Note that, a fresh name is
selected between all values strictly greater than the current value of f resh (e.g. in
the second step 6 > 4), and then f resh is updated to a value strictly greater than
all newly generated names (e.g. 8 > 6 > 4).

16

Giorgio Delzanno

init −−→ f resh(x) | initM (y) : x > 0, y = 0.
f resh(x) | initM (y) −−→ f resh(x′ ) | create(y ′ ) : x′ > y ′ , y ′ > x.
create(x) −−→ initM (x′ ) | initA (id′ , n′ , m′ ) : x′ = x, id′ = x, n′ = 0, m′ = 0.
create(x) −−→ initM (x′ ) | initB (id′ , n′ , m′ ) : x′ = x, id′ = x, n′ = 0, m′ = 0.
initA (id, n, m)| f resh(u) −−→ genA (id, n′ , m) | f resh(u′ ) : u′ > n′ , n′ > u.
genA (id1 , n, m)| initB (id2 , u, v) −−→ waitA (id1 , n, m) | genB (id′2 , u′ , v ′ ) : u′ = n, v ′ = v
genB (id, n, m)| f resh(u) −−→ readyB (id, n, m′ ) | f resh(u′ ) : u′ > m′ , m′ > u.
waitA (id1 , n, m)| readyB (id2 , u, v) −−→ stopA (id1 , n, m′ ) | stopB (id2 , u, v) : n = u, m′ = v.
stopA (id, n, m) −−→ initA (id′ , n′ , m′ ) : n′ = 0, m′ = 0, id′ = id.
stopB (id, n, m) −−→ initB (id′ , n′ , m′ ) : n′ = 0, m′ = 0, id′ = id.

Fig. 6. Encoding of Example 1: for simplicity we embed constraints like x = x′ into
the MSR formulas.
init ⇒ . . . ⇒ f resh(4) | initM (0) | initA (2, 0, 0) | initB (3, 0, 0)
⇒ f resh(8) | initM (0) | genA (2, 6, 0) | initB (3, 0, 0)
⇒ f resh(8) | initM (0) | waitA (2, 6, 0) | genB (3, 6, 0)
⇒ . . . ⇒ f resh(16) | initM (0) | waitA (2, 6, 0) | genB (3, 6, 0) | initA (11, 0, 0)

Fig. 7. A run in the encoded program.
Let T = hP1 , . . . , Pt i be a collection of thread definitions and G0 be an initial
global state. Let S be the MSRN C specification that results from the translation
described in the previous section.
Let G = hN, p1 , . . . , pn i be a global configuration with pi = hsi , vi1 , . . . , viki i, and
let h : N ❀ Q+ be an injective mapping. Then, we define G• (h) as the MSRN C
configuration
s1 (h(v11 ), . . . , h(v1k1 )) | . . . | sn (h(vn1 ), . . . , h(vnkn )) | f resh(v)
where v is a the first value strictly greater than all values in the range of h. Given
an MSRN C configuration M defined as s1 (v11 , . . . , v1k1 ) | . . . | sn (vn1 , . . . , vnkn )
with sij ∈ Q+ , let V (M) ⊆ Q+ be the set of values occurring in M. Then, given a
bijective mapping f : V (M) ❀ N ⊆ N , we define M• (f ) as the global configuration hN, p1 , . . . , pn i where pi = hsi , f (vi1 ), . . . , f (viki )i.
Based on the previous definitions, the following property then holds.
Theorem 2
For every run G0 G1 . . . in T with corresponding set of names N0 N1 . . ., there exist
sets D0 D1 . . . and bijective mappings h0 h1 . . . with hi : Ni ❀ Di ⊆ Q+ for i ≥ 0,
such that init G•0 (h0 )G•1 (h1 ) . . . is a run of S. Vice versa, if init M0 M1 . . . is a
run of S, then there exist sets N0 N1 . . . in N and bijective mappings f0 f1 . . . with
fi : V (Mi ) ❀ Ni for i ≥ 0, such that M•0 (f0 )M•1 (f1 ) . . . is a run in T .
Proof
We first prove that every run in T is simulated by a run in S.
Let G0 . . . Gl be a run in T , i.e., a sequence of global states (with associated set

Constraint-based Verification of Abstract Multithreaded Programs

17

of names N0 . . . Nl ) such that Gi ⇒ Gi+1 and Ni ⊆ Ni+1 for i ≥ 0.
We prove that it can be simulated in S by induction on its length l.
Specifically, suppose that there exist sets of non negative rationals D0 . . . Dl and
bijective mappings h0 . . . hl with hi : Ni ❀ Di for 0 ≤ i ≤ l, such that
c0 (h0 ) . . . G
cl (hl )
init G

is a run of S. Furthermore, suppose Gl ⇒ Gl+1 .
We prove the thesis by a case-analysis on the type of rule applied in the last step
of the run.
Let Gl = hNl , p1 , . . . , pr i and pj = hs, n1 , . . . , nk i be a local configuration for the
thread definition P = hQ, s, V, Ri with V = {x1 , . . . , xk } and ni ∈ Nl for i : 1, . . . , k.
a
Assignment Suppose there exists a rule s −−→ s′ [γ, α] in R such that ρpj satisfies γ,
Gl = hNl , . . . , pj , . . .i ⇒ hNl+1 , . . . , p′j , . . .i = Gl+1 Nl = Nl+1 , p′j = hs′ , n′1 , . . . , n′k i,
and if xi := yi occurs in α, then n′i = ρpj (yi ), otherwise n′i = ni for i : 1, . . . , k.
The encoding of the rule returns one M SRN C rule having the form
s(x1 , . . . , xk ) → s′ (x′1 , . . . , x′k ) : γ ′ , α
b

for every γ ′ ∈ γ
b.
cl (hl ) is a multiset of atomic formulas that contains the
By inductive hypothesis, G
formula s(hl (n1 ), . . . , hl (nk )).
Now let us define hl+1 as the mapping from Nl to Dl such that hl+1 (n′i ) = hl (nj ) if
xi := xj is in α and hl+1 (n′i ) = 0 if xi := ⊥ is in α. Furthermore, let us the define
the evaluation
σ = hx1 7→ hl (n1 ), . . . , xk 7→ hl (nk ), x′1 7→ hl+1 (n′1 ), . . . , x′k 7→ hl+1 (n′k )i
Then, by construction of the set of constraints b
γ and of the constraint α
b, it follows
that σ is a solution for γ ′ , α
b for some γ ′ ∈ b
γ . As a consequence, we have that
s(n1 , . . . , nk ) → s′ (n′1 , . . . , n′k )

is a ground instance of one of the considered M SRN C rules.
cl (hl ), if we apply a rewriting step
Thus, starting from the M SRN C configuration G
we obtain a new configuration in which s(n1 , . . . , nk ) is replaced by s′ (n′1 , . . . , n′k ),
c
[
and all the other atomic formulas in G
l+1 (hl+1 ) are the same as in Gl (hl ). The
[
resulting M SRN C configuration coincides then with the definition of G
l+1 (hl+1 ).
Creation of new names Let us now consider the case of fresh name generation.
a
Suppose there exists a rule s −−→ s′ [xi := new] in R, and let n 6∈ Nl , and suppose
hNl , . . . , pj , . . .i ⇒ hNl+1 , . . . , p′j , . . .i where Nl+1 = Nl ∪ {v}, p′j = hs′ , n′1 , . . . , n′k i
where n′i = n, and n′j = nj for j 6= i.
We note than that the encoding of the previous rule returns the M SRN C rule
s(x1 , . . . , xk ) | f resh(x) → s′ (x′1 , . . . , x′k ) | f resh(x′ ) : ϕ
where ϕ consists of the constraints y > x′i , x′i > x and x′j = xj for j 6= i. By
cl (hl ) is a multiset of atomic formulas that contains the
inductive hypothesis, G

18

Giorgio Delzanno

formulas s(hl (n1 ), . . . , hl (nk )) and f resh(v) where hl is a mapping into Dl , and v
is the first non-negative rational strictly greater than all values occurring in the
formulas denoting processes.
Let v be a non negative rational strictly greater than all values in Dl . Furthermore,
let us define v ′ = v + 1 and Dl+1 = Dl ∪ {v, v ′ }.
Furthermore, we define hl+1 as follows hl+1 (n) = hl (n) for n ∈ Nl , and hl+1 (n′i ) =
hl+1 (n) = v ′ . Furthermore, we define the following evaluation
σ

= h x 7→ v, x1 7→ hl (n1 ), . . . , xk 7→ hl (nk ),
x′ 7→ v ′ , x′1 7→ hl+1 (n′1 ), . . . , x′k 7→ hl+1 (n′k ) i

Then, by construction of σ and α
b, it follows that σ is a solution for α
b. Thus,
s(n1 , . . . , nk ) | f resh(v) → s′ (n′1 , . . . , n′k ) | f resh(v ′ )

is a ground instance of the considered M SRN C rule.
cl (hl ), if we apply a rewriting step we
Starting from the M SRN C configuration G
obtain a new configuration in which s(n1 , . . . , nk ) and f resh(v) are substituted by
[
s′ (n′1 , . . . , n′k ) and f resh(v ′ ), and all the other atomic formulas in G
l+1 (hl+1 ) are
c
the same as in Gl (hl ). We conclude by noting that this formula coincides with the
[
definition of G
l+1 (hl+1 ).
For sake of brevity we omit the case of thread creation whose only difference from
the previous cases is the creation of several new atoms instead (with values obtained
by evaluating the action) of only one.
Rendez-vous Let pi = hs, n1 , . . . , nk i and pj = ht, m1 , . . . , mu i two local configurations for threads P 6= P ′ , ni ∈ Nl for i : 1, . . . , k and mi ∈ Nl for i : 1, . . . , u.
c!m

c?m′

Suppose s −−→ s′ [γ, α] and t −−−→ t′ [γ ′ , α′ ], where m = hxi1 , . . . , xiv i, and m′ =
hy1 , . . . , yv i ( all defined over distinct variables) are rules in R.
Furthermore, suppose that ρpi satisfies γ, and that ρ′ (see definition of the operational semantics) satisfies γ ′ , and suppose that Gl = hNl , . . . , pi , . . . , pj , . . .i ⇒
hNl+1 , . . . , p′i , . . . , p′j , . . .i = Gl+1 , where Nl+1 = Nl , p′i = hs′ , n′1 , . . . , n′k i, p′j =
ht′ , m′1 , . . . , m′u i, and if xi := e occurs in α, then n′i = ρpi (e), otherwise n′i = ni
for i : 1, . . . , k; if ui := e occurs in α′ , then m′i = ρ′ (e), otherwise m′i = mi for
i : 1, . . . , u.
cl (hl ) is a multiset of atomic formulas that contains the
By inductive hypothesis, G
formulas s(hl (n1 ), . . . , hl (nk )) and t(hl (m1 ), . . . , hl (mu )).
Now, let us define hl+1 as the mapping from Nl to Dl such that hl+1 (n′i ) = hl (nj )
if xi := xj is in α, hl+1 (m′i ) = hl (mj ) if ui := uj is in α′ , hl+1 (n′i ) = 0 if xi := ⊥ is
in α, hl+1 (m′i ) = 0 if ui := ⊥ is in α′ .
Now, let us define σ as the evaluation from Nl to Dl such that
σ = σ1 ∪ σ2
σ1 = hx1 7→ hl (n1 ), . . . , xk 7→ hl (nk ), u1 7→ hl (m1 ), . . . , uu 7→ hl (mu )i
σ2 = hx′1 7→ hl+1 (n′1 ), . . . , x′k 7→ hl+1 (n′k ), u′1 7→ hl+1 (m′1 ), . . . , u′u 7→ hl+1 (m′u )i.
Then, by construction of the sets of constraints γ
b, γb′ , α
b and αb′ it follows that σ is
′
′
′
a solution for the constraint ∃w1 . . . . ∃wp .θ ∧ θ ∧ α
b ∧ αb′ ∧ w1 = w1′ ∧ . . . ∧ wp = wp′
for some θ ∈ γ
b and θ′ ∈ γb′ . Note in fact that the equalities wi = wi′ express the

Constraint-based Verification of Abstract Multithreaded Programs

19

passing of values defined via the evaluation ρ′ in the operational semantics.
As a consequence,
s(n1 , . . . , nk ) | t(m1 , . . . , mu ) → s′ (n′1 , . . . , n′k ) | t′ (m′1 , . . . , m′u )
is a ground instance of one of the considered M SRN C rules.
cl (hl ), if we apply a rewriting
Thus, starting from the M SRN C configuration G
step we obtain a new configuration in which s(n1 , . . . , nk ) has been replaced by
s′ (n′1 , . . . , n′k ), and t′ (m′1 , . . . , m′k ) has been replaced by t(m′1 , . . . , m′u ), and all the
cl (hl ). This formula coincides with the definition
other atomic formulas are as in G
[
of Gl+1 (hl+1 ).
The proof of completeness is by induction on the length of an MSR run, and by
case-analysis on the application of the rules. The structure of the case analysis is
similar to the previous one and it is omitted for brevity.

4 Verification of TDL Programs
Safety and invariant properties are probably the most important class of correctness
specifications for the validation of a concurrent system. For instance, in Example
1 we could be interested in proving that every time a session terminates, two instances of thread Init and Resp have exchanged the two names generated during
the session. To prove the protocol correct independently from the number of names
and threads generated during an execution, we have to show that from the initial configuration G0 it is not possible to reach a configuration that violates the
aforementioned property. The configurations that violate the property are those in
which two instances of Init and Resp conclude the execution of the protocol exchanging only the first nonce. These configurations can be represented by looking
at only two threads and at the relationship among their local data. Thus, we can
reduce the verification problem of this safety property to the following problem:
Given an initial configuration G0 we would like to decide if a global configuration that contains at least two local configurations having the form hstopA , i, n, mi
and hstopB , i′ , n′ , m′ i with n′ = n and m 6= m′ for some i, i′ , n, n′ , m, m′ is reachable. This problem can be viewed as an extension of the control state reachability
problem defined in (Abdulla and Nylén 2000) in which we consider both control locations and local variables. Although control state reachability is undecidable (see
Corollary 1), the encoding of TDL into MSRN C can be used to define a sound and
automatic verification methods for TDL programs. For this purpose, we will exploit
a verification method introduced for MSR(C) in (Delzanno 2001; Delzanno 2005).
In the rest of this section we will briefly summarize how to adapt the main results
in (Delzanno 2001; Delzanno 2005) to the specific case of MSRN C .
Let us first reformulate the control state reachability problem of Example 1 for
the aforementioned safety property on the low level encoding into MSRN C . Given
the MSRN C initial configuration init we would like to check that no configuration
in P ost∗ ({init}) has the following form
{stopA (a1 , v1 , w1 ), stopB (a2 , v2 , w2 )} ⊕ M

20

Giorgio Delzanno

for ai , vi , wi ∈ Q i : 1, 2 and an arbitrary multiset of ground atoms M. Let us call
U the set of bad MSRN C configurations having the aforementioned shape. Notice
that U is upward closed with respect to multiset inclusion, i.e., if M ∈ U and
M 4 M′ , then M′ ∈ U . Furthermore, for if U is upward closed, so is P re(U ).
On the basis of this property, we can try to apply the methodology proposed in
(Abdulla and Nylén 2000) to develop a procedure to compute a finite representation
R of P re∗ U ). For this purpose, we need the following ingredients:
1. a symbolic representation of upward closed sets of configurations (e.g. a set
of assertions S whose denotation [[S]] is U );
2. a computable symbolic predecessor operator SP re working on sets of formulas
such that [[SP re(S)]] = P re([[S]]);
3. a (decidable) entailment relation Ent to compare the denotations of symbolic
representations, i.e., such that Ent(N, M ) implies [[N ]] ⊆ [[M ]]. If such a relation Ent exists, then it can be naturally extended to sets of formulas as
follows: EntS (S, S ′ ) if and only if for all N ∈ S there exists M ∈ S ′ such that
Ent(N, M ) holds (clearly, if Ent is an entailment, then EntS (S, S ′ ) implies
[[S]] ⊆ [[S ′ ]]).
The combination of these three ingredients can be used to define a verification
methods based on backward reasoning as explained next.
Symbolic Backward Reachability Suppose that M1 , . . . , Mn are the formulas of our
assertional language representing the infinite set U consisting of all bad configurations. The symbolic backward reachability procedure (SBR) procedure computes a
chain {Ii }i≥0 of sets of assertions such that
I0 = {M1 , . . . , Mn }
Ii+1 = Ii ∪ SP re(Ii ) for i ≥ 0
The procedure SBR stops when SP re produces only redundant information, i.e.,
EntS (Ii+1 , Ii ). Notice that EntS (Ii , Ii+1 ) always holds since Ii ⊆ Ii+1 .
Symbolic Representation In order to find an adequate represention of infinite sets of
MSRN C configurations we can resort to the notion of constrained configuration introduced in (Delzanno 2001) for the language scheme MSR(C) defined for a generic
constraint system C. We can instantiate this notion with N C constraints as follows.
A constrained configuration over P is a formula
p1 (x11 , . . . , x1k1 ) | . . . | pn (xn1 , . . . , xnkn ) : ϕ
where p1 , . . . , pn ∈ P, xi1 , . . . , xiki ∈ V for any i : 1, . . . n and ϕ is an N C-constraint.
.
The denotation a constrained configuration M = (M : ϕ) is defined by taking the
upward closure with respect to multiset inclusion of the set of ground instances,
namely
[[M ]] = {M′ | σ(M) 4 M′ , σ ∈ Sol(ϕ)}

Constraint-based Verification of Abstract Multithreaded Programs

21

This definition can be extended to sets of MSRN C constrained configurations with
disjoint variables (we use variable renaming to avoid variable name clashing) in the
natural way.
In our example the following set SU of MSRN C constrained configurations (with
distinct variables) can be used to finitely represent all possible violations U to the
considered safety property
SU = { stopA (i1 , n1 , m1 ) | stopB (i2 , n2 , m2 ) : n1 = n2 , m1 > m2
stopA (i1 , n1 , m1 ) | stopB (i2 , n2 , m2 ) : n1 = n2 , m2 > m1 }
Notice that we need two formulas to represent m1 6= m2 using a disjunction
of > constraints. The MSRN C configurations stopB (1, 2, 6) | stopA (4, 2, 5), and
stopB (1, 2, 6) | stopA (4, 2, 5) | waitA (2, 7, 3) are both contained in the denotation
of SU . Actually, we have that [[SU ]] = U . This symbolic representation allows us to
reason on infinite sets of MSRN C configurations, and thus on global configurations
of a TDL program, forgetting the actual number or threads of a given run.
To manipulate constrained configurations, we can instantiate to N C-constraints
the symbolic predecessor operator SP re defined for a generic constraint system in
(Delzanno 2005). Its definition is also given in Section Appendix A in Appendix.
From the general properties proved in (Delzanno 2005), we have that when applied
to a finite set of MSRN C constrained configurations S, SP reN C returns a finite set
of constrained configuration such that [[SP reN C (S)]] = P re([[S]]), i.e., SP reN C (S)
is a symbolic representation of the immediate predecessors of the configurations in
the denotation (an upward closed set) of S. Similarly we can instantiate the generic
entailment operator defined in (Delzanno 2005) to MSRN C constrained configurations so as to obtain an a relation Ent such that EntN C (N, M ) implies [[N ]] ⊆ [[M ]].
Based on these properties, we have the following result.
Proposition 1
Let T be a TDL program with initial global configuration G0 , Furthermore, let
S be the corresponding MSRN C encoding. and SU be the set of MSRN C constrained configurations denoting a given set of bad TDL configurations. Then,
init 6∈ SP re∗N C (SU ) if and only if there is no finite run G0 . . . Gn and mappings h0 , . . . , hn from the names occurring in G to non-negative rationals such
that init• G•0 (h0 ) . . . G•n (hn ) is a run in S and G•n (hn ) ∈ [[U ]].
Proof
Suppose init 6∈ SP re∗N C (U ). Since [[SP reN C (S)]] = pre([[S]]) for any S, it follows
that there cannot exist runs initM0 . . . Mn in S such that Mn ∈ [[U ]]. The thesis
then follows from the Theorem 2.
As discussed in (Bozzano and Delzanno 2002), we have implemented our verification procedure based on M SR and linear constraints using a CLP system with linear
arithmetics. By the translation presented in this paper, we can now reduce the verification of safety properties of multithreaded programs to a fixpoint computation
built on constraint operations. As example, we have applied our CLP-prototype
to automatically verify the specification of Fig. 6. The unsafe states are those described in Section 4. Symbolic backward reachability terminates after 18 iterations

22

Giorgio Delzanno

and returns a symbolic representation of the fixpoint with 2590 constrained configurations. The initial state init is not part of the resulting set. This proves our
original thread definitions correct with respect to the considered safety property.
4.1 An Interesting Class of TDL Programs
The proof of Theorem 1 shows that verification of safety properties is undecidable for TDL specifications in which threads have several local variables (they
are used to create linked lists). As mentioned in the introduction, we can apply the sufficient conditions for the termination of the procedure SBR given in
(Bozzano and Delzanno 2002; Delzanno 2005) to identify the following interesting
subclass of TDL programs.
Definition 4
A monadic TDL thread definition P = hQ, s, V, Ri is such that V is at most a
singleton, and every message template in R has at most one variable.
A monadic thread definition can be encoded into the monadic fragment of MSRN C
studied in (Delzanno 2005). Monadic MSRN C specifications are defined over atomic
formulas of the form p or p(x) with p is a predicate symbol and x is a variable, and
on atomic constraints of the form x = y, and x > y. To encode a monadic TDL
thread definitions into a Monadic MSRN C specification, we first need the following
observation. Since in our encoding we only use the constant 0, we first notice that
we can restrict our attention to MSRN C specifications in which constraints have no
constants at all. Specifically, to encode the generation of fresh names we only have
to add an auxiliary atomic formula zero(z), and refer to it every time we need to
express the constant 0. As an example, we could write rules like
init −−→ f resh(x) | initM (y) | zero(z) : x > z, y = z
for initialization, and
create(x) | zero(z) −−→ initM (x′ ) | initA (id′ , n′ , m′ ) | zero(z) :
x′ = x, id′ = x, n′ = z, m′ = z, z ′ = z
for all assignments involving the constant 0. By using this trick an by following the
encoding of Section 3, the translation of a collection of monadic thread definitions
directly returns a monadic MSRN C specification. By exploiting this property, we
obtain the following result.
Theorem 3
The verification of safety properties whose violations can be represented via an
upward closed set U of global configurations is decidable for a collection T of
monadic TDL definitions.
Proof
Let S be the MSRN C encoding of T and SU be the set of constrained configuration
such that SU = U . The proof is based on the following properties. First of all, the
MSRN C specification S is monadic. Furthermore, as shown in (Delzanno 2005),

Constraint-based Verification of Abstract Multithreaded Programs

23

the class of monadic MSRN C constrained configurations is closed under application
of the operator SP reN C . Finally, as shown in (Delzanno 2005), there exists an
entailment relation CEnt for monadic constrained configurations that ensures the
termination of the SBR procedure applied to a monadic MSRN C specification.
Thus, for the monadic MSRN C specification S, the chain defined as I0 = SU ,
Ii+1 = Ii ∪ SP re(Ii ) always reaches a point k ≥ 1 in which CEntS (Ik+1 , Ik ), i.e.
[[Ik ]] is a fixpoint for P re. Finally, we note that we can always check for membership
of init in the resulting set Ik .
As shown in (Schnoebelen 2002), the complexity of verification methods based on
symbolic backward reachability relying on the general results in (Abdulla and Nylén 2000;
Finkel and Schnoebelen 2001) is non primitive recursive.

5 Conclusions and Related Work
In this paper we have defined the theoretical grounds for the possible application
of constraint-based symbolic model checking for the automated analysis of abstract
models of multithreaded concurrent systems providing name generation, name mobility, and unbounded control. Our verification approach is based on an encoding
into a low level formalism based on the combination of multiset rewriting and
constraints that allows us to naturally implement name generation, value passing,
and dynamic creation of threads. Our verification method makes use of symbolic
representations of infinite set of system states and of symbolic backward reachability. For this reason, it can be viewed as a conservative extension of traditional
finite-state model checking methods. The use of symbolic state analysis is strictly
related to the analysis methods based on abstract interpretation. A deeper study
of the connections with abstract interpretation is an interesting direction for future
research.
Related Work The high level syntax we used to present the abstract models of
multithreaded programs is an extension of the communicating finite state machines
used in protocol verification (Bochmann 1978), and used for representing abstraction of multithreaded software programs (Ball et al. 2001). In our setting we enrich
the formalism with local variables, name generation and mobility, and unbounded
control. Our verification approach is inspired by the recent work of Abdulla and
Jonsson. In (Abdulla and Jonsson 2003), Abdulla and Jonsson proposed an assertional language for Timed Networks in which they use dedicated data structures
to symbolically represent configurations parametric in the number of tokens and
in the age (a real number) associated to tokens. In (Abdulla and Nylén 2000), Abdulla and Nylén formulate a symbolic algorithm using existential zones to represent the state-space of Timed Petri Nets. Our approach generalizes the ideas of
(Abdulla and Jonsson 2003; Abdulla and Nylén 2000) to systems specified via multiset rewriting and with more general classes of constraints. In (Abdulla and Jonsson 2001),
the authors apply similar ideas to (unbounded) channel systems in which messages
can vary over an infinite name domain and can be stored in a finite (and fixed a

24

Giorgio Delzanno

priori) number of data variables. However, they do not relate these results to multithreaded programs. Multiset rewriting over first order atomic formulas has been proposed for specifying security protocols by Cervesato et al. in (Cervesato et al. 1999).
The relationships between this framework and concurrent languages based on process algebra have been recently studied in (Bistarelli et al. 2005). Apart from approaches based on Petri Net-like models (as in (German and Sistla 1992; Ball et al. 2001)),
networks of finite-state processes can also be verified by means of automata theoretic techniques as in (Bouajjani et al. 2000). In this setting the set of possible
local states of individual processes are abstracted into a finite alphabet. Sets of
global states are represented then as regular languages, and transitions as relations
on languages. Differently from the automata theoretic approach, in our setting
we handle parameterized systems in which individual components have local variables that range over unbounded values. The use of constraints for the verification
of concurrent systems is related to previous works connecting Constraint Logic
Programming and verification, see e.g. (Delzanno and Podelski 1999). In this setting transition systems are encoded via CLP programs used to encode the global
state of a system and its updates. In the approach proposed in (Delzanno 2001;
Bozzano and Delzanno 2002), we refine this idea by using multiset rewriting and
constraints to locally specify updates to the global state. In (Delzanno 2001), we
defined the general framework of multiset rewriting with constraints and the corresponding symbolic analysis technique. The language proposed in (Delzanno 2001) is
given for a generic constraint system C (taking inspiration from CLP the language
is called M SR(C)). In (Bozzano and Delzanno 2002), we applied this formalism to
verify properties of mutual exclusion protocols (variations of the ticket algorithm)
for systems with an arbitrary number of processes. In the same paper we also formulated sufficient conditions for the termination of the backward analysis. The
present paper is the first attempt of relating the low level language proposed in
(Delzanno 2001) to a high level language with explicit management of names and
threads.
Acknowledgments The author would like to thank Ahmed Bouajjani, Andrew Gordon, Fabio Martinelli, Catuscia Palamidessi, Luca Paolini, and Sriram Rajamani
and the anonymous reviewers for several fruitful comments and suggestions.
References
Abdulla, P. A., Cerāns, K., Jonsson, B., and Tsay, Y.-K. 1996. General Decidability Theorems for Infinite-State Systems. In Proceedings 11th Annual International
Symposium on Logic in Computer Science (LICS’96). IEEE Computer Society Press,
New Brunswick, New Jersey, 313–321.
Abdulla, P. A. and Jonsson, B. 2001. Ensuring Completeness of Symbolic Verification
Methods for Infinite-State Systems. Theoretical Computer Science 256, 1-2, 145–167.
Abdulla, P. A. and Jonsson, B. 2003. Model checking of systems with many identical
timed processes. Theoretical Computer Science 290, 1, 241–264.
Abdulla, P. A. and Nylén, A. 2000. Better is Better than Well: On Efficient Verification
of Infinite-State Systems. In Proceedings 15th Annual International Symposium on

Constraint-based Verification of Abstract Multithreaded Programs

25

Logic in Computer Science (LICS’00). IEEE Computer Society Press, Santa Barbara,
California, 132–140.
Ball, T., Chaki, S., and Rajamani, S. K. 2001. Parameterized Verification of Multithreaded Software Libraries. In 7th International Conference on Tools and Algorithms
for Construction and Analysis of Systems (TACAS 2001), Genova, Italy, April 2-6,.
LNCS, vol. 2031. Springer-Verlag, 158–173.
Bistarelli, S., Cervesato, I., Lenzini, G., and Martinelli, F. 2005. Relating multiset
rewriting and process algebras for security protocol analysis. Journal of Computer
Security 13, 1, 3–47.
Bochmann, G. V. 1978. Finite state descriptions of communicating protocols. Computer
Networks 2, 46–57.
Bouajjani, A., Jonsson, B., Nilsson, M., and Touili, T. 2000. Regular Model Checking. In Proceedings 12th International Conference on Computer Aided Verification
(CAV’00), E. A. Emerson and A. P. Sistla, Eds. LNCS, vol. 1855. Springer-Verlag,
Chicago, Illinois, 403–418.
Bozzano, M. and Delzanno, G. 2002. Algorithmic verification of invalidation-based
protocols. In 14th International Conference on Computer Aided Verification, CAV ’02.
Lecture Notes in Computer Science, vol. 2404. Springer.
Cervesato, I., Durgin, N., Lincoln, P., Mitchell, J., and Scedrov, A. 1999. A
Meta-notation for Protocol Analysis. In 12th Computer Security Foundations Workshop
(CSFW’99). IEEE Computer Society Press, Mordano, Italy, 55–69.
Delzanno, G. 2001. An Assertional Language for Systems Parametric in Several Dimensions. In Verification of Parameterized Systems - VEPAS 2001. ENTCS, vol. 50.
Delzanno, G. 2005. Constraint Multiset Rewriting. Tech. Rep. TR-05-08, Dipartimento
Informatica e Scienze dell’Informazione, Università di Genova, Italia.
Delzanno, G. and Podelski, A. 1999. Model checking in CLP. In Proceedings 5th
International Conference on Tools and Algorithms for Construction and Analysis of
Systems (TACAS’99). Lecture Notes in Computer Science, vol. 1579. Springer-Verlag,
Amsterdam, The Netherlands, 223–239.
Finkel, A. and Schnoebelen, P. 2001. Well-Structured Transition Systems Everywhere!
Theoretical Computer Science 256, 1-2, 63–92.
German, S. M. and Sistla, A. P. 1992. Reasoning about Systems with Many Processes.
Journal of the ACM 39, 3, 675–735.
Gordon, A. D. 2001. Notes on nominal calculi for security and mobility. In Foundations
of Security Analysis and Design, Tutorial Lectures. Lecture Notes in Computer Science,
vol. 2171. Springer, 262–330.
Kesten, Y., Maler, O., Marcus, M., Pnueli, A., and Shahar, E. 2001. Symbolic
model checking with rich assertional languages. Theoretical Computer Science 256, 1,
93–112.
Schnoebelen, P. 2002. Verifying Lossy Channel Systems has Nonprimitive Recursive
Complexity. Information Processing Letters 83, 5, 251–261.

Appendix A Symbolic Predecessor Operator
Given a set of MSRN C configurations S, consider the MSRN C predecessor operator
P re(S) = {M|M ⇒MSR M′ , M′ ∈ S}. In our assertional language, we can define a
symbolic version SP reN C of P re defined on a set S containing MSRN C constrained

26

Giorgio Delzanno

multisets (with disjoint variables) as follows:
SP reN C (S) = { (A ⊕ N : ξ) |

(A −→ B : ψ) ∈ R, (M : ϕ) ∈ S,
M′ 4 M, B ′ 4 B,
(M′ : ϕ) =θ (B ′ : ψ), N = M ⊖ M′ ,
ξ ≡ (∃x1 . . . . xk .θ)
and x1 , . . . , xk are all variables not in A ⊕ N }.

where =θ is a matching relation between constrained configurations that also takes
in consideration the constraint satisfaction, namely
(A1 | . . . | An : ϕ) =θ (B1 | . . . | Bm : ψ)
provided m = n and there exists a permutation j1 , . . . , jn of 1, . . . , n such that
Vn
the constraint θ = ϕ ∧ ψ ∧ i=1 Ai = Bji is satisfiable; here p(x1 , . . . , xr ) =
q(y1 , . . . , ys ) is an abbreviation for the constraints x1 = y1 ∧ . . . ∧ xr = ys if p = q
and s = r, f alse otherwise.
As proved in (Delzanno 2005), the symbolic operator SP reN C returns a set of
MSRN C constrained configurations and it is correct and complete with respect to
P re, i.e., [[SP reN C (S)]] = P re([[S]]) for any S. It is important to note the difference
between SP reN C and a simple backward rewriting step.
For instance, given the constrained configurations M defined as p(x, z) | f (y) : z >
y and the rule s(u, m) | r(t, v) → p(u′ , m′ ) | r(t′ , v ′ ) : u = t, m′ = v, v ′ =
v, u′ = u, t′ = t (that simulates a rendez-vous (u, t are channels) and value passing
(m′ = v)), the application of SP re returns s(u, m) | r(t, v) | f (y) : u = t, v > y as
well as s(u, m) | r(t, v) | p(x, z) | f (y) : u = t, x > y (the common multiset here is
ǫ).

