1: \documentclass{tlp}
2: \usepackage{graphicx}
3: \usepackage{proof}
4: \usepackage{latexsym}
5: \usepackage{amssymb}
6: \usepackage{amsfonts}
7: \usepackage{epic,eepic}
8: \usepackage{mysym}
9:
10:
11: \newcommand{\Exp}{\calE}
12: \newcommand{\CExp}{{\cal E}_{\mathrm{ch}}}
13:
14: \newcommand{\entailC}{ \sqsubseteq^c }
15: \newcommand{\entailM}{ \sqsubseteq^m }
16: \newcommand{\entailS}{ \sqsubseteq^p }
17: \newcommand{\entailString}{ \preccurlyeq^s }
18: \newcommand {\NC} {NC}
19: \newcommand {\MSR} {MSR}
20: \newcommand {\MSRC} {MSR(${\cal C}$)}
21: \newcommand{\scrA}{\calA}
22: \newcommand{\entailP}{\sqsubseteq^P}
23: \newcommand{\entailStr}{\sqsubseteq^s}
24: \newcommand{\Sol}{Sol}
25:
26: \newcommand{\arrowup}[3]{\setbox0=\hbox{$\ {}^{#2}\ $}
27: \setbox1=\hbox{$\longrightarrow$}
28: \ifdim\wd0<\wd1\setbox0=\box1\else\relax\fi
29: {#1}\,\mathop{\hbox to \wd0{\rightarrowfill}}\limits^{#2}\,{#3}
30: }
31:
32: \newcommand{\calA}{ {\cal A} }
33: \newcommand{\calB}{ {\cal B} }
34: \newcommand{\calC}{ {\cal C} }
35: \newcommand{\calE}{ {\cal E} }
36: \newcommand{\calI}{ {\cal I} }
37: \newcommand{\calH}{ {\cal H} }
38: \newcommand{\calO}{ {\cal O} }
39: \newcommand{\calP}{ {\cal P} }
40: \newcommand{\calQ}{ {\cal Q} }
41: \newcommand{\calR}{ {\cal R} }
42: \newcommand{\calS}{ {\cal S} }
43: \newcommand{\calT}{ {\cal T} }
44: \newcommand{\calL}{ {\cal L} }
45: \newcommand{\calM}{ {\cal M} }
46: \newcommand{\calN}{ {\cal N} }
47: \newcommand{\calV}{ {\cal V} }
48: \newcommand{\calD}{ {\cal D} }
49: \newcommand{\Int}{ \mathbb{Z} }
50: \newcommand{\Rat}{ \mathbb{Q} }
51:
52: \newcommand{\bfI} { {I} }
53: \newcommand{\bfU} { {U} }
54: \newcommand{\bfR} { {\bf R} }
55: \newcommand{\bfB} { {\bf B} }
56: \newcommand{\bfM} { {\bf M} }
57: \newcommand{\bfP} { {\bf P} }
58: \newcommand{\bfS} { {S} }
59: \newcommand{\bfPre} { {SPre} }
60: \newcommand{\barPre} { {\overline{Pre}} }
61: \newcommand{\den}[1] { [\![{#1}]\!]}
62: \newcommand{\comment}[1]{}
63: %\newcommand{\tuple}[1]{ \lguard #1 \rguard}
64: \newcommand{\tuple}[1]{ \langle {#1} \rangle}
65: \newcommand{\lguard}{[}
66: \newcommand{\rguard}{]}
67: %\newcommand{\TDLtoMSR}[1]{\ulcorner{#1}\urcorner}
68: \newcommand{\TDLtoMSR}[1]{#1^\bullet}
69: \newtheorem {definition}{Definition}
70: \newtheorem {proposition}{Proposition}
71: \newtheorem {lemma}{Lemma}
72: \newtheorem {theorem}{Theorem}
73: \newtheorem {corollary}{Corollary}
74: \newtheorem {es}{Example}
75: \newenvironment{example}{\begin{es}\rm}{\hspace*{\fill}$\Box$\end{es}}
76:
77: \title[Constraint-based Verification of Abstract Multithreaded Programs]
78: {Constraint-based Automatic Verification of Abstract Models of Multithreaded Programs}
79: \author[Giorgio Delzanno]
80: {GIORGIO DELZANNO\\
81: \begin{tabular}{c}
82: Dipartimento di Informatica e Scienze dell'Informazione,
83: Universit\`a di Genova\\
84: via Dodecaneso 35, 16146 Genova - Italy\\
85: \email{giorgio@disi.unige.it}
86: \end{tabular}
87: }
88:
89: \pagerange{\pageref{firstpage}--\pageref{lastpage}}
90:
91: \volume{}
92: \jdate{}
93: \setcounter{page}{1}
94: \pubyear{}
95:
96: \submitted{17 December 2003}
97: \revised{13 April 2005}
98: \accepted{15 January 2006}
99:
100: \begin{document}
101:
102: \label{firstpage}
103:
104: \maketitle
105:
106: \begin{abstract}
107: We present a technique for the automated verification of
108: {abstract models of multithreaded programs} providing {fresh name generation},
109: {name mobility}, and {unbounded control}.
110:
111: As high level specification language we adopt here an extension of
112: communication finite-state machines with local variables ranging over
113: an infinite name domain, called TDL programs.
114: Communication machines have been proved very effective for representing
115: communication protocols as well as for representing abstractions of
116: multithreaded software.
117:
118: The verification method that we propose is based on the encoding of TDL programs
119: into a low level language based on {multiset rewriting} and
120: {constraints} that can be viewed as an extension of Petri Nets.
121: By means of this encoding, the symbolic verification procedure developed for the
122: low level language in our previous work can now be applied to TDL programs.
123: Furthermore, the encoding allows us to isolate a decidable class of
124: verification problems for TDL programs that still provide
125: {fresh name generation}, {name mobility}, and {unbounded control}.
126: Our syntactic restrictions are in fact defined on the internal structure of
127: threads: In order to obtain a complete and terminating method,
128: threads are only allowed to have at most one local variable (ranging over an
129: infinite domain of names).
130: \end{abstract}
131: \begin{keywords}
132: Constraints, Multithreaded Programs, Verification.
133: \end{keywords}
134: \section{Introduction}
135: \label{sec:introduction}
136: Andrew Gordon \cite{Gor00} defines a {\em nominal calculus} to be a computational
137: formalism that includes a set of {\em pure names} and allows the
138: dynamic generation of {\em fresh}, {\em unguessable} names.
139: A name is {\em pure} whenever it is only useful for comparing for
140: identity with other names.
141: The use of pure names is ubiquitous in programming
142: languages. Some important examples are memory pointers in
143: imperative languages, identifiers in concurrent programming
144: languages, and nonces in security protocols.
145: %
146: In addition to pure names, a {\em nominal process calculus} should
147: provide mechanisms for {\em concurrency} and {\em inter-process
148: communication}. A computational model that provides all these features
149: is an adequate abstract formalism for the analysis of
150: {\em multithreaded} and {\em distributed} software.
151: %
152: \paragraph{The Problem}
153: %
154: Automated verification of specifications in a
155: nominal process calculus becomes particularly challenging in presence of
156: the following three features:
157: the possibility of generating fresh names ({\em name generation});
158: the possibility of transmitting names ({\em name mobility});
159: the possibility of dynamically adding new threads of control
160: ({\em unbounded control}).
161: In fact, a calculus that provides all the previous features can be used
162: to specify systems with a state-space infinite in {\em several dimensions}.
163: This feature makes difficult (if not impossible) the application of
164: finite-state verification techniques or techniques based on abstractions
165: of process specifications into Petri Nets or CCS-like models.
166: In recent years there have been several attempts of extending automated verification
167: methods from finite-state to infinite-state systems \cite{AN00,Pnueli}.
168: In this paper we are interested in investigating the possible application
169: of the methods we proposed in \cite{Del01} to verification problems of interest for
170: nominal process calculi.
171: %
172: \paragraph{Constraint-based Symbolic Model Checking}
173: In \cite{Del01} we introduced a specification language,
174: called MSR($\calC$), for the analysis of communication protocols whose
175: specifications are parametric in several dimensions (e.g. number of servers, clients,
176: and tickets as in the model of the ticket mutual exclusion algorithm shown in \cite{BD02}).
177: MSR($\calC$) combines multiset rewriting over first order atomic formulas
178: \cite{CDLMS99} with constraints programming. More specifically,
179: multiset rewriting is used to specify the {control part} of a concurrent
180: system, whereas {constraints} are used to symbolically specify the relations
181: over local data.
182: The verification method proposed in \cite{Del02} allows
183: us to symbolically reason on the behavior of MSR($\calC$) specifications.
184: To this aim, following \cite{ACJT96,AN00} we introduced a symbolic representation
185: of infinite collections of {global configurations} based on the combination
186: of multisets of atomic formulas and constraints, called constrained
187: configurations.\footnote{Notice that in \cite{ACJT96,AN00} a {\em constraint}
188: denotes a symbolic state whereas we use the word {\em constraint} to denote a symbolic
189: representation of the relation of data variables (e.g. a linear arithmetic formula)
190: used as part of the symbolic representation of sets of states (a constrained
191: configuration).}
192: The verification procedure performs a symbolic backward reachability analysis
193: by means of a symbolic {\em pre-image} operator that works over constrained
194: configurations \cite{Del02}.
195: The main feature of this method is the possibility of automatically
196: handling systems with an arbitrary number of components.
197: Furthermore, since we use a symbolic and finite representation of possibly
198: infinite sets of configurations, the analysis is carried out without loss
199: of precision.
200: \smallskip\\
201: A natural question for our research is whether and how these techniques
202: can be used for verification of abstract models of multithreaded programs.
203: \paragraph{Our Contribution}
204: In this paper we propose a sound, and fully automatic verification method
205: for abstract models of multithreaded programs that provide {\em name generation},
206: {\em name mobility}, and {\em unbounded control}.
207: As a high level specification language we adopt here an extension with value-passing
208: of the formalism of \cite{BCR01} based on families of state machines used to specify
209: abstractions of multithreaded software libraries.
210: The resulting language is called Thread Definition Language (TDL).
211: This formalism allows us to keep separate the {finite control component} of a
212: {thread definition} from the management of {local variables} (that in our
213: setting range over a infinite set of names), and to treat in isolation
214: the operations to generate fresh names, to transmit names, and
215: to create new threads.
216: In the present paper we will show that the extension of the model of
217: \cite{BCR01} with value-passing makes the model Turing equivalent.
218:
219: The verification methodology is based on the encoding of TDL programs
220: into a specification in the instance MSR$_{NC}$ of the language scheme
221: \MSRC~of\cite{Del01}.
222: MSR$_{NC}$ is obtained by taking as constraint system a subclass of linear
223: arithmetics with only $=$ and $>$ relations between variables, called name
224: constraints ($NC$).
225: The low level specification language MSR$_{NC}$ is not just instrumental for
226: the encoding of TDL programs. Indeed, it has
227: been applied to model consistency and mutual exclusion protocols
228: in \cite{BD02,Del02}.
229: Via this encoding, the verification method based on
230: symbolic backward reachability obtained by instantiating the general method
231: for \MSRC~to NC-constraints can now be applied to abstract models of multithreaded
232: programs.
233: Although termination is not guaranteed in general, the resulting verification method
234: can succeed on practical examples as the Challenge-Response TDL program
235: defined over binary predicates we will illustrated in the present paper.
236: Furthermore, by propagating the sufficient conditions for
237: termination defined in \cite{BD02,Del02} back to TDL programs,
238: we obtain an interesting class of decidable problems for
239: abstract models of multithreaded programs still providing name generation,
240: name mobility, and unbounded control.
241: \paragraph{Plan of the Paper}%
242: In Section \ref{NominalCalculus} we present the Thread Definition Language (TDL)
243: with examples of multithreaded programs. Furthermore, we discuss the expressiveness
244: of TDL programs showing that they can simulate Two Counter Machines.
245: In Section \ref{MSRTranslation}, after introducing the MSR$_{NC}$ formalism,
246: we show that TDL programs can be simulated by MSR$_{NC}$ specifications.
247: In Section \ref{Verification} we show how to transfer the verification methods
248: developed for \MSRC~to TDL programs. Furthermore, we show that safety properties
249: can be decided for the special class of monadic TDL programs.
250: In Section \ref{conclusions} we address some conclusions and discuss related work.
251: %
252: \section{Thread Definition Language (TDL)}
253: \label{NominalCalculus}
254: %
255: In this section we will define TDL programs.
256: This formalism is a natural extension with value-passing
257: of the communicating machines used by \cite{BCR01} to specify
258: abstractions of multithreaded software libraries.
259: \paragraph{Terminology}
260: Let $\calN$ be a denumerable set of {\em names} equipped with
261: the relations $=$ and $\neq$ and a special element $\bot$
262: such that $n\neq \bot$ for any $n\in\calN$.
263: Furthermore, let $\calV$ be a denumerable set of variables,
264: $\calC=\{c_1,\ldots,c_m\}$ a finite set of
265: constants, and $\calL$ a finite set of {\em internal action} labels.
266: For a fixed $V\subseteq\calV$, the set of {\em expressions} is defined as
267: $\Exp=V\cup\calC\cup\{\bot\}$ (when necessary we will use $\Exp(V)$ to explicit the set
268: of variables $V$ upon which expressions are defined).
269: The set of {\em channel expressions} is defined as $\CExp=V\cup \calC$.
270: Channel expressions will be used as synchronization labels so as to establish
271: communication links only at execution time.
272: \smallskip\\
273: A {\em guard over $V$} is a conjunction $\gamma_1,\ldots,\gamma_s$,
274: where $\gamma_i$ is either $true$, $x=e$ or $x\neq e$ with $x\in V$ and $e\in\Exp$
275: for $i:1,\ldots,s$.
276: An {\em assignment} $\alpha$ from $V$ to $W$ is a conjunction
277: like $x_i:=e_i$ where $x_i\in W$,
278: $e_i\in\Exp(V)$ for $i:1,\ldots k$ and $x_r\neq x_s$ for $r\neq s$.
279: A {\em message template $m$ over $V$} is a tuple $m=\tuple{x_1,\ldots,x_u}$
280: of variables in $V$.
281: %
282: \begin{definition}\rm
283: A {\em TDL program} is a set $\calT=\{P_1,\ldots,P_t\}$ of {\em thread definitions}
284: (with distinct names for local variables control locations).
285: A {\em thread definition} $P$ is a tuple $\tuple{Q,s_0,V,R}$,
286: where $Q$ is a finite set of {\em control locations}, $s_0\in Q$ is the initial location,
287: $V\subseteq\calV$ is a finite set of {\em local variables}, and
288: $R$ is a set of rules. Given $s,s'\in Q$, and $a\in\calL$,
289: a {\em rule} has one of the following forms\footnote{In this paper we keep assignments, name
290: generation, and thread creation separate in order to simplify the
291: presentation of the encoding into MSR.}:
292: \begin{itemize}
293: \item[$\bullet$] {\em Internal move}: $\arrowup{s}{a}{s'}\lguard\gamma,\alpha\rguard$,
294: where $\gamma$ is a {\em guard over $V$}, and $\alpha$ is an
295: {\em assignment} from $V$ to $V$;
296: %
297: \item[$\bullet$] {\em Name generation}: $\arrowup{s}{a}{s'}\lguard{x:=new}\rguard$, where
298: $x\in V$, and the expression $new$ denotes a {\em fresh name};
299: %
300: \item[$\bullet$] {\em Thread creation:} $\arrowup{s}{a}{s'}\lguard{run~P'~with~\alpha}\rguard$,
301: where $P'=\tuple{Q',t,W,R'}\in\calT$, and $\alpha$ is an {\em
302: assignment from $V$ to $W$} that specifies the initialization of
303: the local variables of the new thread;
304: %
305: \item[$\bullet$] {\em Message sending:} $\arrowup{s}{e!m}{s'}\lguard \gamma,\alpha\rguard$,
306: where $e$ is a {\em channel expression}, $m$ is a {\em message
307: template over $V$} that specify which names to pass,
308: $\gamma$ is a {\em guard over $V$}, and $\alpha$ is an {\em assignment} from $V$ to $V$.
309: %
310: \item[$\bullet$] {\em Message reception:} $\arrowup{s}{e?m}{s'}\lguard \gamma,\alpha\rguard$,
311: where $e$ is a channel expression, $m$ is a
312: message template over a {\em new} set of variables $V'$ ($V'\cap V=\emptyset$)
313: that specifies the names to receive,
314: $\gamma$ is a {\em guard over $V\cup V'$} and $\alpha$ is an {\em assignment}
315: from $V\cup V'$ to $V$.
316: \end{itemize}
317: \end{definition}
318: %
319: Before giving an example, we will formally introduce the operational
320: semantics of TDL programs.
321: \subsection{Operational Semantics}
322: In the following we will use $N$ to indicate the subset of {\em used names} of $\calN$.
323: Every constant $c\in\calC$ is mapped to a distinct name $n_c\neq\bot\in N$, and $\bot$
324: is mapped to $\bot$.
325: \\
326: Let $P=\tuple{Q,s,V,R}$ and $V=\{x_1,\ldots,x_k\}$.
327: A {\em local configuration} is a tuple $p=\tuple{s',n_1,\ldots,n_k}$ where $s'\in Q$ and $n_i\in N$ is the
328: current value of the variable $x_i\in V$ for $i:1,\ldots,k$.
329: \\
330: A {\em global configuration} $G=\tuple{N,p_{1},\ldots,p_{m}}$ is
331: such that $N\subseteq\calN$ and $p_{1},\ldots,p_{m}$ are local
332: configurations defined over $N$ and over the thread definitions in
333: $\calT$. Note that there is no relation between indexes in a
334: global configuration in $G$ and in $\calT$; $G$ is a {\em pool} of
335: active threads, and {\em several active threads} can be instances
336: of the same {\em thread definition}.
337: \\
338: Given a local configuration $p=\tuple{s',n_1,\ldots,n_k}$,
339: we define the {\em valuation} $\rho_p$ as
340: $\rho_p(x_i)=n_i$ if $x_i\in V$,
341: $\rho_p(c)=n_{c}$ if $c\in\calC$, and
342: $\rho_p(\bot)=\bot$.
343: Furthermore, we say that $\rho_p$ satisfies the guard $\gamma$ if $\rho_p(\gamma)\equiv true$,
344: where $\rho_p$ is extended to constraints in the natural way
345: ($\rho_p(\varphi_1\wedge \varphi_2)=\rho_p(\varphi_1)\wedge\rho_p(\varphi_2)$, etc.).
346: \smallskip\\
347: The execution of $x:=e$ has the effect of updating the local
348: variable $x$ of a thread with the current value of $e$ (a name
349: taken from the set of used values $N$). On the contrary, the
350: execution of $x:=new$ associates a {\em fresh unused name} to $x$.
351: The formula $run~P~with~\alpha$ has the effect of adding a new
352: thread (in its initial control location) to the current global
353: configuration. The initial values of the local variables of the
354: generated thread are determined by the execution of $\alpha$ whose
355: source variables are the local variables of the parent thread. The
356: channel names used in a rendez-vous are determined by evaluating
357: the channel expressions tagging sender and receiver rules. Value
358: passing is achieved by extending the evaluation associated to the
359: current configuration of the receiver so as to associate the
360: output message of the sender to the variables in the input
361: message template. The operational semantics is given via a binary
362: relation $\Rightarrow$ defined as follows.
363: \begin{definition}\rm
364: \label{sos}
365: Let $G=\tuple{N,\ldots,\mathbf{p},\ldots}$, and
366: $\mathbf{p}=\tuple{s,n_1,\ldots,n_k}$ be a local configuration for
367: $P=\tuple{Q,s,V,R}$, $V=\{x_1,\ldots,x_k\}$, then:
368: \begin{itemize}
369: \item[$\bullet$] If there exists a rule $\arrowup{s}{a}{s'}\lguard\gamma,\alpha\rguard$ in $R$
370: such that $\rho_{\mathbf{p}}$ satisfies $\gamma$, then
371: $G\Rightarrow\tuple{N,\ldots,\mathbf{p'},\ldots}$ (meaning that only $\mathbf{p}$ changes)
372: where $\mathbf{p'}=\tuple{s',n_1',\ldots,n_k'}$,
373: $n_i'=\rho_{\mathbf{p}}(e_i)$ if $x_i:=e_i$ is in $\alpha$,
374: $n_i'=n_i$ otherwise, for $i:1,\ldots,k$.
375: %
376: \item[$\bullet$]
377: If there exists a rule $\arrowup{s}{a}{s'}\lguard x_i:=new\rguard$ in $R$,
378: then
379: $G\Rightarrow\tuple{N',\ldots,\mathbf{p'},\ldots}$
380: where
381: $\mathbf{p'}=\tuple{s',n_1',\ldots,n_k'}$,
382: $n_i$ is an unused name, i.e., $n_i'\in \calN\setminus N$,
383: $n_j'=n_j$ for every $j\neq i$, and $N'=N\cup\{n_i'\}$;
384: %
385: \item[$\bullet$]
386: If there exists a rule
387: $\arrowup{s}{a}{s'}\lguard run~P'~with~\alpha\rguard$ in $R$ with
388: $P'=\tuple{Q',t_0,W,R'}$, $W=\{y_{1},\ldots,y_{u}\}$, and
389: $\alpha$ is defined as $y_{1}:=e_{1},\ldots,y_{u}:=e_{u}$
390: then
391: $G\Rightarrow\tuple{N,\ldots,\mathbf{p'},\ldots,\mathbf{q}}$
392: (we add a new thread whose initial local configuration is $\mathbf{q}$)
393: where
394: $\mathbf{p'}=\tuple{s',n_1,\ldots,n_k}$, and
395: $\mathbf{q}=\tuple{t_0,\rho_{\mathbf{p}}(e_{1}),\ldots,\rho_{\mathbf{p}}(e_{u})}$.
396: %
397: \item[$\bullet$]
398: Let $\mathbf{q}=\tuple{t,m_1,\ldots,m_r}$ (distinct from $\mathbf{p}$)
399: be a local configuration in $G$ associated with
400: $P'=\tuple{Q',t_0,W,R'}$.\\
401: Let $\arrowup{s}{e!m}{s'}\lguard\gamma,\alpha\rguard$ in $R$ and
402: $\arrowup{t}{e'?m'}{t'}\lguard\gamma',\alpha'\rguard$ in $R'$ be
403: two rules such that $m=\tuple{x_1,\ldots,x_u}$,
404: $m'=\tuple{y_1,\ldots,y_v}$ and $u=v$ (message templates match).
405: We define $\sigma$ as the {\em value passing} evaluation
406: $\sigma(y_i)=\rho_{\mathbf{p}}(x_{i})$ for $i:1,\ldots,u$, and
407: $\sigma(z)=\rho_{\mathbf{q}}(z)$ for $z\in W'$.
408: \\
409: Now if $\rho_{\mathbf{p}}(e)=\rho_{\mathbf{p}}(e')$ (channel names
410: match), $\rho_{\mathbf{p}}$ satisfies $\gamma$, and that $\sigma$
411: satisfies $\gamma'$, then
412: $
413: \tuple{N,\ldots,\mathbf{p},\ldots,\mathbf{q},\ldots}\Rightarrow
414: \tuple{N,\ldots,\mathbf{p'},\ldots,\mathbf{q'},\ldots}$ where
415: $\mathbf{p'}=\tuple{s',n_1',\ldots,n_k'}$,
416: $n_i'=\rho_{\mathbf{p}}(v)$ if $x_i:=v$ is in $\alpha$, $n_i'=n_i$
417: otherwise for $i:1,\ldots,k$;
418: $\mathbf{q'}=\tuple{t',m_1',\ldots,m_r'}$, $m_i'=\sigma(v)$ if
419: $u_i:=v$ is in $\alpha'$,
420: $m_i'=m_i$ otherwise for $i:1,\ldots,r$.
421: \end{itemize}
422: \end{definition}
423: %
424: \begin{definition}\rm
425: An {\em initial global configuration} $G_0$ has an {\em arbitrary
426: (but finite) number} of threads with local variables all set to
427: $\bot$. A {\em run} is a sequence $G_0G_1\ldots$ such that
428: $G_{i}\Rightarrow G_{i+1}$ for $i\geq 0$. A global configuration
429: $G$ is {\em reachable} from $G_0$ if there exists a run from $G_0$
430: to $G$.
431: \end{definition}
432: %
433:
434: \begin{example}
435: \label{AliceBob} Let us consider a {\em challenge and
436: response} protocol in which the goal of two agents Alice and Bob
437: is to exchange a pair of new names $\tuple{n_A,n_B}$,
438: the first one created by Alice and the second one created by Bob,
439: so as to build a composed secret key.
440: We can specify the protocol by using new names
441: to dynamically establish {\em private channel names} between
442: instances of the initiator and of the responder.
443: The TDL program in Figure \ref{model} follows this idea.
444: The thread $Init$ specifies the behavior of the initiator.
445: He first creates a new name using the internal action $fresh$, and stores it
446: in the local variable $n_A$.
447: Then, he sends $n_A$ on channel $c$ (a constant), waits for a name $y$ on a channel with the same
448: name as the value of the local variable $n_A$ (the channel is specified by variable $n_A$)
449: and then stores $y$ in the local variable $m_A$.
450: The thread $Resp$ specifies the behavior of the responder.
451: Upon reception of a name $x$ on channel $c$, he stores it in the local variable
452: $n_B$, then creates a new name stored in local variable $m_B$ and finally
453: sends the value in $m_B$ on channel with the same name as the value of $n_B$.
454: The thread $Main$ non-deterministically creates new thread instances of type $Init$ and $Resp$.
455: The local variable $x$ is used to store new names to be used for the creation of a new
456: thread instance.
457: Initially, all local variables of threads $Init/Resp$ are set to $\bot$.
458: In order to allow process instances to participate to several sessions
459: (potentially with different principals), we could also add the following rule
460: $$
461: \arrowup{stop_A}{restart}{init_{A}}\lguard n_A:=\bot,m_A:=\bot\rguard
462: $$
463: In this rule we require that {\em roles} and {\em identities} do not change from
464: session to session.\footnote{By means of thread and fresh name creation it is also possible
465: to specify a restart rule in which a given process takes a potential different
466: role or identity.}
467: %
468: \begin{figure*}[t]
469: $$
470: \begin{array}{l}
471: \begin{array}{l}
472: Thread~Init(local~id_A,n_A,m_A);
473: \smallskip\\
474: \begin{array}{ll}
475: ~~~\arrowup{init_A}{fresh}{gen_A} & \lguard n_A:=new\rguard
476: \\
477: ~~~\arrowup{gen_A}{c!\tuple{n_A}}{wait_A}&\lguard true\rguard
478: \\
479: ~~~\arrowup{wait_A}{n_A?\tuple{y}}{stop_A}&\lguard m_A:=y\rguard
480: \end{array}\end{array}
481: \\
482: \\
483: \begin{array}{l}
484: Thread~Resp(local~id,n_B,m_B);\smallskip\\
485: \begin{array}{ll}
486: ~~~\arrowup{init_B}{c?\tuple{x}}{gen_B}&\lguard n_B:=x\rguard
487: \\
488: ~~~\arrowup{gen_B}{fresh}{ready_B}&\lguard m_B:={new}\rguard
489: \\
490: ~~~\arrowup{ready_B}{n_B!\tuple{m_B}}{stop_B}&\lguard true\rguard
491: \end{array}\end{array}
492: \\
493: \\
494: \begin{array}{l}
495: Thread~Main(local~x);\smallskip\\
496: \begin{array}{ll}
497:
498: ~~~\arrowup{init_M}{id}{create}&\lguard x:=new\rguard
499: \\
500: ~~~\arrowup{create}{new_A}{init_M}&\lguard run~Init~with~id_A:=x,n_A:=\bot,m_A:=\bot,x:=\bot\rguard
501: \\
502: ~~~\arrowup{create}{new_B}{init_M}&\lguard run~Resp~with~id_B:=x,n_B:=\bot,m_B:=\bot,x:=\bot_B\rguard
503: \end{array}\end{array}
504: \end{array}
505: $$
506: \caption{Example of thread definitions.}
507: \label{model}
508: \end{figure*}
509: Starting from $G_0=\tuple{N_0,\tuple{init,\bot}}$, and running the {\em Main}
510: thread we can generate any number of copies of the threads $Init$
511: and $Resp$ each one with a unique identifier. Thus, we obtain
512: global configurations like
513: $$
514: \begin{array}{ll}
515: \langle N,&\tuple{init_M,\bot},\\
516: &\tuple{init_A,i_1,\bot,\bot},\ldots,\tuple{init_A,i_K,\bot,\bot},\\
517: & \tuple{init_B,i_{K+1},\bot,\bot},\ldots,\tuple{init_B,i_{K+L},\bot,\bot}~\rangle
518: \end{array}
519: $$
520: where $N=\{\bot,i_1,\ldots,i_K,i_{K+1},\ldots,i_{K+L}\}$ for $K,L\geq 0$. The
521: threads of type $Init$ and $Resp$ can start parallel sessions whenever
522: created. For $K=1$ and $L=1$ one possible session is as follows.
523: \\
524: Starting from
525: $$
526: \tuple{\{\bot,i_1,i_2\},\tuple{init_M,\bot},\tuple{init_A,i_1,\bot,\bot},\tuple{init_B,i_2,\bot,\bot}}\\
527: $$
528: if we apply the first rule of thread $Init$ to $\tuple{init_A,i_1,\bot,\bot}$ we obtain
529: $$
530: \tuple{\{\bot,i_1,i_2,a^1\},\tuple{init_M,\bot},\tuple{gen_A,i_1,a^1,\bot},\tuple{init_B,i_2,\bot,\bot}}
531: $$
532: where $a^1$ is the generated name ($a^1$ is distinct from $\bot$, $i_1$, and $i_2$).
533: Now if we apply the second rule of thread $Init$ and the first rule of thread $Resp$
534: (synchronization on channel $c$)
535: we obtain
536: $$
537: \tuple{\{\bot,i_1,i_2,a^1\},\tuple{init_M,\bot},\tuple{wait_A,i_1,a^1,\bot},\tuple{gen_B,i_2,a^1,\bot}}
538: $$
539: If we apply the second rule of thread $Resp$ we obtain
540: $$
541: \tuple{\{\bot,i_1,i_2,a^1,a^2\},\tuple{init_M,\bot},\tuple{wait_A,i_1,a^1,\bot},\tuple{ready_B,i_2,a^1,a^2}}
542: $$
543: Finally, if we apply the last rule of thread $Init$ and $Resp$
544: (synchronization on channel $a^1$) we obtain
545: $$
546: \tuple{\{\bot,i_1,i_2,a^1,a^2\},\tuple{init_M,\bot},\tuple{stop_A,i_1,a^1,a^2},\tuple{stop_B,i_2,a^1,a^2}}
547: $$
548: Thus, at the end of the session the thread instances $i_1$ and $i_2$ have
549: both a local copy of the fresh names $a^1$ and $a^2$.
550: Note that a copy of the main thread $\tuple{init_M,\bot}$ is
551: always active in any reachable configuration, and, at any time, it
552: may introduce new threads (either of type $Init$ or $Resp$) with
553: fresh identifiers. Generation of fresh names is also used by the
554: threads of type $Init$ and $Resp$ to create nonces. Furthermore,
555: threads can restart their life cycle (without changing
556: identifiers). Thus, in this example the set of possible reachable
557: configurations is infinite and contains configurations with {
558: arbitrarily many threads} and {fresh names}.
559: Since names are stored in the local variables of active threads,
560: the local data also range over an infinite domain.
561: \end{example}
562: %
563: \subsection{Expressive Power of TDL}
564: To study the expressive power of the TDL language, we will compare it
565: with the Turing equivalent formalism called {Two Counter Machines}.
566: %
567: A { Two Counters Machine} configurations is a tuple
568: $\tuple{\ell,c_1=n_1,c_2=n_2}$ where $\ell$ is control location taken from a
569: finite set $Q$,
570: and $n_1$ and $n_2$ are natural numbers that
571: represent the values of the counters $c_1$ and $c_2$.
572: Each counter can be incremented or decremented (if greater than zero)
573: by one.
574: Transitions combine operations on individual counters with changes
575: of control locations.
576: Specifically, the instructions for counter $c_i$ are as follows
577: $$
578: \begin{tabular}{l}
579: Inc: $\ell_1$: $c_i:=c_i+1$; goto $\ell_2$;\\
580: Dec: $\ell_1$: if $c_i>0$ then $c_i:=c_i-1$; goto $\ell_2$; else goto $\ell_3$;
581: \end{tabular}
582: $$
583: A { Two Counter Machine} consists then of a list of instructions and of
584: the initial state $\tuple{\ell_0,c_1=0,c_2=0}$.
585: The operational semantics is defined according to the intuitive semantics
586: of the instructions.
587: Problems like control state reachability are undecidable
588: for this computational model.
589: \\
590: The following property then holds.
591: \begin{theorem}
592: \label{twocounters}\rm
593: TDL programs can simulate { Two Counter Machines}.
594: \end{theorem}
595: \begin{proof}
596: In order to define a TDL program that simulates a
597: { Two Counter Machine} we proceed as follows.
598: \begin{figure}[t]
599: $$
600: \begin{array}{l}
601: \mathrm{Thread}~Last(local~id,last,aux);\\
602: \begin{array}{l}
603: \begin{array}{l}
604: \smallskip\\
605: \mathbf{(Zero~test)}
606: \smallskip\\
607: \begin{array}{ll}
608: ~~\arrowup{Idle}{Zero?\tuple{x}}{Busy} & \lguard id=x\rguard
609: \medskip\\
610: ~~\arrowup{Busy}{tstC!\tuple{id,last}}{Wait}
611: \medskip\\
612: ~~\arrowup{Wait}{nz?\tuple{x}}{AckNZ}& \lguard id=x\rguard
613: \medskip\\
614: ~~\arrowup{Wait}{z?\tuple{x}}{AckZ}& \lguard id=x\rguard
615: \medskip\\
616: ~~\arrowup{AckZ}{Yes!\tuple{id}}{Idle}
617: \medskip\\
618: ~~\arrowup{AckNZ}{No!\tuple{id}}{idle}
619: \end{array}\end{array}
620: \\
621: \\
622: \begin{array}{l}
623: \mathbf{(Decrement)}
624: \\
625: \\
626: \begin{array}{ll}
627: ~~\arrowup{Idle}{Dec?\tuple{x}}{Dbusy} & \lguard id=x\rguard
628: \\
629: \\
630: ~~\arrowup{DBusy}{decC!\tuple{id,last}}{DWait}
631: \\
632: \\
633: ~~\arrowup{DWait}{dack?\tuple{x,u}}{DAck} & \lguard id=x,last:=u\rguard
634: \\
635: \\
636: ~~\arrowup{DAck}{DAck!\tuple{id}}{Idle}
637: \end{array}\end{array}
638: \\
639: \\
640: \begin{array}{l}
641: \mathbf{(Increment)}
642: \\
643: \\\begin{array}{ll}
644: ~~\arrowup{Idle}{Inc?\tuple{x}}{INew}& \lguard id=x\rguard
645: \\
646: \\
647: ~~\arrowup{INew}{new}{IRun}&\lguard aux:=new\rguard
648: \\
649: \\
650: ~~\arrowup{IRun}{run}{IAck}&\lguard run~Cell~with~ idc:=id; prev:=last;next:=aux\rguard
651: \\
652: \\
653: ~~\arrowup{IAck}{IAck!\tuple{id}}{Idle}&\lguard last:=aux\rguard
654: \end{array}\end{array}
655: \end{array}
656: \end{array}
657: $$
658: \caption{The process defining the last cell of the linked list
659: associated to a counter} \label{lastcell}
660: \end{figure}
661: Every counter is represented via a {\em doubly linked list} implemented via a
662: collection of threads of type $Cell$ and with a unique thread of type
663: $Last$ pointing to the head of the list.
664: \begin{figure}[t]
665: $$
666: \begin{array}{l}
667: \mathrm{Thread}~Cell(local~idc,prev,next);
668: \medskip\\
669: \begin{array}{l}
670: \mathbf{(Zero~test)}
671: \smallskip\\
672: ~~\arrowup{idle}{tstC?\tuple{x,u}}{ackZ}~~\lguard x= idc,u=next,prev=next\rguard
673: \medskip\\
674: ~~\arrowup{idle}{tstC?\tuple{x,u}}{ackNZ}~~\lguard x=idc,u=next,prev\neq next \rguard
675: \medskip\\
676: ~~\arrowup{ackZ}{z!\tuple{idc}}{idle}
677: \medskip\\
678: ~~\arrowup{ackNZ}{nz!\tuple{idc}}{idle}
679: \end{array}
680: \\
681: \\
682: \begin{array}{l}
683: \mathbf{(Decrement)}
684: \\
685: \\
686: ~~\arrowup{idle}{dec?\tuple{x,u}}{dec}~~\lguard x=idc,u=next,prev\neq next\rguard
687: \medskip\\
688: ~~\arrowup{dec}{dack!\tuple{idc,prev}}{idle}
689: \end{array}
690: \end{array}
691: $$
692: \caption{The process defining a cell of the linked list associated
693: to a counter}
694: \label{thecell}
695: \end{figure}
696: The $i$-th counter having value zero is represented as the {\em empty
697: list} $Cell(i,v,v),Last(i,v,w)$ for some name $v$ and $w$ (we will explain later the use of
698: $w$).
699: The $i$-th counter having value $k$ is represented as
700: $$Cell(i,v_0,v_0),Cell(i,v_0,v_1),\ldots,C(i,v_{k-1},v_k),Last(i,v_k,w)$$
701: for distinct names $v_0,v_1,\ldots,v_k$.
702: The instructions on a counter are simulated by sending messages to the corresponding
703: $Last$ thread.
704: The messages are sent on channel $Zero$ (zero test), $Dec$ (decrement),
705: and $Inc$ (increment).
706: In reply to each of these messages, the thread $Last$ sends an acknowledgment, namely
707: $Yes/No$ for the zero test, $DAck$ for the decrement, $IAck$ for the increment operation.
708: $Last$ interacts with the $Cell$ threads via the messages $tstC$, $decC$, $incC$
709: acknowledged by messages $z/nz$, $dack$. $iack$.
710: The interactions between a $Last$ thread and the $Cell$ threads is as follows.
711: %
712: \paragraph{Zero Test}
713: %
714: Upon reception of a message $\tuple{x}$ on channel $Zero$, the
715: $Last$ thread with local variables $id,last,aux$ checks that its identifier $id$
716: matches $x$ - see transition from $Idle$ to $Busy$ -
717: sends a message $\tuple{id,last}$ on channel $tstC$
718: directed to the cell pointed to by $last$ (transition from $Busy$ to $Wait$),
719: and then waits for an answer.
720: If the answer is sent on channel $nz$, standing for non-zero, (resp. $z$ standing for
721: zero) - see transition from $Wait$ to $AckNZ$ (resp. $AckZ$) -
722: then it sends its identifier on channel $No$ (resp. $Yes$) as
723: an acknowledgment to the first message -
724: see transition from $AckNZ$ (resp. $Z$) to $Idle$.
725: As shown in Fig. \ref{thecell}, the thread $Cell$ with local variables
726: $idc$, $prev$, and $next$ that receives the message $tstC$, i.e.,
727: pointed to by a thread $Last$ with the same identifier as $idc$,
728: sends an acknowledgment on channel $z$ (zero) if $prev=next$, and on channel
729: $nz$ (non-zero) if $prev\neq next$.
730: %
731: \paragraph{Decrement}
732: %
733: Upon reception of a message $\tuple{x}$ on channel $Dec$, the
734: $Last$ thread with local variables $id,last,aux$ checks
735: that its identifier $id$ matches $x$ (transition from $Idle$ to $Dbusy$),
736: sends a message $\tuple{id,last}$ on channel $decC$
737: directed to the cell pointed to by $last$ (transition from $Busy$ to $Wait$),
738: and then waits for an answer.
739: If the answer is sent on channel $dack$ (transition from $DWait$ to $DAck$)
740: then it updates the local variable $last$ with the pointer $u$ sent by the thread
741: $Cell$,
742: namely the $prev$ pointer of the cell pointed to by the current value of
743: $last$, and then sends its identifier on channel $DAck$
744: to acknowledge the first message (transition from $DAck$ to $Idle$).
745:
746: As shown in Fig. \ref{thecell}, a thread $Cell$ with local variables $idc$,
747: $prev$, and $next$ that receives the message $decC$ and
748: such that $next=last$ sends as an acknowledgment on channel $dack$ the value $prev$.
749: \paragraph{Increment}
750: To simulate the increment operation, {\em Last} does not have to interact
751: with existing $Cell$ threads. Indeed, it only has to link a
752: new {\em Cell} thread to the head of the list (this is way the $Cell$ thread
753: has no operations to handle the increment operation).
754: As shown in Fig. \ref{lastcell} this can be done by creating a
755: new name stored in the local variable $aux$ (transition from $INew$ to $IRun$) and
756: spawning a new {\em Cell} thread (transition from $IRun$ to $IAck$)
757: with $prev$ pointer equal to $last$, and $next$ pointer equal to $aux$.
758: Finally, it acknowledges the increment request by sending its identifier
759: on channel $IAck$ and updates variable $last$ with the current value of $aux$.
760: %
761: \begin{figure}[t]
762: $$
763: \begin{array}{l}
764: \mathrm{Thread}~CM(local~id_1,id_2);
765: \medskip\\
766: ~~~~~~~~~~\vdots
767: \medskip\\
768: \begin{array}{l}
769: \mathbf{(Instruction: \ell_1:~c_{i}:=c_{i}+1;~goto ~\ell_2;)}
770: \smallskip\\
771: ~~\arrowup{\ell_1}{Inc!\tuple{id_i}}{wait_{\ell_1}}
772: \medskip\\
773: ~~\arrowup{wait_{\ell_1}}{IAck!\tuple{x}}{\ell_2}~~\lguard x=id_i\rguard
774: \end{array}
775: \\
776: ~~~~~~~~~~\vdots
777: \\
778: \begin{array}{l}
779: \mathbf{(Instruction: \ell_1:~c_{i}>0~then~c_{i}:=c_{i}-1;~goto ~\ell_2; else~goto~\ell_3;)}
780: \smallskip\\
781: ~~\arrowup{\ell_1}{Zero!\tuple{id_i}}{wait_{\ell_1}}
782: \medskip\\
783: ~~\arrowup{wait_{\ell_1}}{NZAck?\tuple{x}}{dec_{\ell_1}}~~\lguard x=id_i\rguard
784: \medskip\\
785: ~~\arrowup{dec_{\ell_1}}{Dec!\tuple{id_i}}{wdec_{\ell_1}}
786: \medskip\\
787: ~~\arrowup{wdec_{\ell_1}}{DAck?\tuple{y}}{\ell_2}~~\lguard y=id_i\rguard
788: \medskip\\
789: ~~\arrowup{wait_{\ell_1}}{ZAck?\tuple{x}}{\ell_3}~~\lguard x=id_i\rguard
790: \end{array}
791: \\
792: ~~~~~~~~~~\vdots
793: \end{array}
794: $$
795: \caption{The thread associated to a 2CM.}
796: \label{twocm}
797: \end{figure}
798:
799: %
800: \begin{figure}[t]
801: $$
802: \begin{array}{l}
803: \mathrm{Thread}~Init(local~nid_1,p_1,nid_2,p_2);
804: \medskip\\
805: \begin{array}{c}
806: \begin{array}{l}
807: ~~\arrowup{init}{freshId}{init_1}~~\lguard nid_1:=new\rguard
808: \medskip\\
809: ~~\arrowup{init_1}{freshP}{init_2}~~\lguard p_1:=new\rguard
810: \medskip\\
811: ~~\arrowup{init_2}{runC}{init_3}~~\lguard run~Cell~with~ idc:=nid_1; prev:=p_1;next:=p_1 \rguard
812: \medskip\\
813: ~~\arrowup{init_3}{runL}{init_4}~~\lguard run~Last~with~ idc:=nid_1; last:=p_1;aux:=\bot \rguard
814: \medskip\\
815: ~~\arrowup{init_4}{freshId}{init_5}~~\lguard nid_2:=new\rguard
816: \medskip\\
817: ~~\arrowup{init_5}{freshP}{init_6}~~\lguard p_2:=new\rguard
818: \medskip\\
819: ~~\arrowup{init_6}{runC}{init_7}~~\lguard run~Cell~with~ idc:=nid_2; prev:=p_2;next:=p_2\rguard
820: \medskip\\
821: ~~\arrowup{init_7}{runL}{init_8}~~\lguard run~Last~with~ idc:=nid_2; last:=p_2;aux:=\bot \rguard
822: \medskip\\
823: ~~\arrowup{init_8}{runCM}{init_9}~~\lguard run~2CM~with~ id_1:=nid_1; id_2:=nid_2\rguard
824: \end{array}
825: \end{array}
826: \end{array}
827: $$
828: \caption{The initialization thread.}
829: \label{init}
830: \end{figure}
831: \paragraph{Two Counter Machine Instructions}
832: %
833: We are now ready to use the operations provided by the thread $Last$
834: to simulate the instructions of a Two Counter Machine.
835: As shown in Fig. \ref{twocm}, we use a thread $CM$ with two local variables
836: $id_1,id_2$ to represent the list of instructions of a 2CM with counters $c_1,c_2$.
837: Control locations of the Two Counter Machines are used as local states of the thread
838: $CM$. The initial local state of the $CM$ thread is the initial control location.
839: The increment instruction on counter $c_i$ at control location $\ell_1$ is simulated by an
840: handshaking with the $Last$ thread with identifier $id_i$: we first send the message
841: $Inc!\tuple{id_i}$, wait for the acknowledgment on channel $IAck$ and then move to state $\ell_2$.
842: Similarly, for the decrement instruction on counter $c_i$ at
843: control location $\ell_1$
844: we first send the message $Zero!\tuple{id_i}$. If we receive an acknowledgment
845: on channel $NZAck$ we send a $Dec$ request, wait for completion
846: and then move to $\ell_2$.
847: If we receive an acknowledgment on channel $ZAck$ we directly move to $\ell_3$.
848: %
849: \paragraph{Initialization}
850: %
851: The last step of the encoding is the definition of the initial state of the system.
852: For this purpose, we use the thread $Init$ of Fig. \ref{init}.
853: The first four rules of $Init$ initialize the first counter:
854: they create two new names $nid_1$ (an identifier for counter $c_1$)
855: and $p_1$, and then spawn the new threads $Cell(nid_1,p_1,p_1),Last(nid_1,p_1,\bot)$.
856: The following four rules spawns the new threads
857: $Cell(nid_2,p_2,p_2),Last(nid_2,p_2,\bot)$.
858: After this stage, we create a thread of type $2CM$ to start the simulation of the
859: instructions of the Two Counter Machines.
860: The initial configuration of the whole system is $G_0=\tuple{init,\bot,\bot}$.
861: %
862: By construction we have that an execution step from
863: $\tuple{\ell_1,c_1=n_1,c_2=n_2}$ to $\tuple{\ell_2,c_1=m_1,c_2=m_2}$
864: is simulated by an execution run going from a global configuration in which
865: the local state of thread $CM$ is $\tuple{\ell_1,id_1,id_2}$ and in which
866: we have $n_i$ occurrences of thread $Cell$ with the same identifier $id_i$ for $i:1,2$,
867: to a global configuration in which
868: the local state of thread $CM$ is $\tuple{\ell_2,id_1,id_2}$ and in which
869: we have $m_i$ occurrences of thread $Cell$ with the same identifier $id_i$ for $i:1,2$.
870: Thus, every executions of a 2CM $M$ corresponds to an execution
871: of the corresponding TDL program that starts from the initial configuration
872: $G_0=\tuple{init,\bot,\bot}$.
873: \end{proof}
874: As a consequence of the previous
875: theorem, we have the following corollary.
876: \begin{corollary}\rm
877: \label{reachability} Given a TDL program, a global configurations
878: $G$, and a control location $\ell$, deciding if there exists a run
879: going from $G_0$ to a global configuration that contains $\ell$
880: (control state reachability) is an undecidable problem.
881: \end{corollary}
882: %
883: \section{From TDL to MSR$_{NC}$}
884: \label{MSRTranslation}
885: As mentioned in the introduction, our
886: verification methodology is based on a translation of TDL programs
887: into low level specifications given in MSR$_{NC}$. Our goal is to
888: extend the connection between CCS and Petri Nets \cite{GS92} to
889: TDL and MSR so as to be able to apply the verification methods
890: defined in \cite{Del02} to multithreaded programs. In
891: the next section we will summarize the main features of the
892: language MSR$_{NC}$ introduced in \cite{Del01}.
893: %
894: \subsection{Preliminaries on MSR$_{NC}$}
895: \label{MSRlanguage}
896: %
897: $NC$-constraints are { linear arithmetic constraints} in
898: which conjuncts have one of the following form: $true$, $x=y$,
899: $x>y$, $x=c$, or $x>c$, $x$ and $y$ being two variables from a
900: denumerable set $\calV$ that range over the rationals, and $c$
901: being an integer. The {\em solutions} $Sol$ of a constraint
902: $\varphi$ are defined as all evaluations (from $\calV$ to $\Rat$)
903: that satisfy $\varphi$. A {\em constraint} $\varphi$ is {\em
904: satisfiable} whenever $Sol(\varphi)\neq\emptyset$. Furthermore,
905: $\psi$ {\em entails} $\varphi$ whenever $Sol(\psi)\subseteq
906: Sol(\varphi)$. $NC$-constraints are closed under elimination of
907: existentially quantified variables.
908: \smallskip\\
909: Let $\calP$ be a set of predicate symbols. An {\em atomic formula}
910: $p(x_1,\ldots,x_n)$ is such that $p\in\calP$, and $x_1,\ldots,x_n$
911: are {\em distinct} variables in $\calV$. A {\em multiset} of
912: atomic formulas is indicated as $A_1~|~\ldots~|~A_k$, where $A_i$
913: and $A_j$ have distinct variables (we use variable renaming if necessary),
914: and $|$ is the multiset constructor.
915: \smallskip\\
916: In the rest of the paper we will use $\calM$, $\calN$,
917: $\ldots$ to denote {\em multisets} of atomic formulas,
918: $\epsilon$ to denote the {\em empty multiset},
919: $\oplus$ to denote {\em multiset union}
920: and $\ominus$ to denote {\em multiset difference}.
921: An MSR$_{NC}$ {\em configuration}
922: is a multiset of {\em ground atomic formulas}, i.e., atomic
923: formulas like $p(d_1,\ldots,d_n)$ where $d_i$ is a rational for
924: $i:1,\ldots,n$.
925: \smallskip\\
926: An MSR$_{NC}$ {\em rule} has the form
927: $\calM~\longrightarrow\calM'~{:}~\varphi$, where $\calM$ and
928: $\calM'$ are two (possibly empty) multisets of atomic formulas
929: with {\em distinct} variables built on predicates in $\calP$, and
930: $\varphi$ is an $NC$-constraint. The ground instances of an
931: MSR$_{NC}$ rule are defined as
932: $$
933: Inst(\calM\longrightarrow\calM':\varphi)=\{
934: \sigma(\calM)\longrightarrow\sigma(\calM')~|~\sigma~\in~Sol(\varphi)\}
935: $$
936: where $\sigma$ is extended in the natural way to multisets,
937: i.e., $\sigma(\calM)$ and $\sigma(\calM')$ are MSR$_{NC}$ configurations.
938: \smallskip\\
939: An MSR$_{NC}$ {\em specification} $\calS$ is a tuple
940: $\tuple{\calP,\calI,\calR}$, where $\calP$ is a finite set of predicate
941: symbols, $\calI$ is finite a set of ({\em initial}) MSR$_{NC}$
942: configurations, and $\calR$ is a finite set of MSR$_{NC}$ rules over
943: $\calP$.
944: \smallskip\\
945: The operational semantics describes the update from
946: a configuration $\calM$ to one of its possible successor configurations $\calM'$.
947: $\calM'$ is obtained from $\calM$ by rewriting (modulo associativity and commutativity)
948: the left-hand side
949: of an instance of a rule into the corresponding right-hand side.
950: In order to be fireable, the left-hand side must be included in $\calM$.
951: Since instances and rules are selected in a non deterministic way, in general a configuration
952: can have a (possibly infinite) set of (one-step) successors.\\
953: \smallskip\\
954: Formally, a rule $\calH~{\longrightarrow}~\calB~:~\varphi$ from $\calR$
955: is enabled at $\calM$ {\em via } the ground substitution $\sigma\in Sol(\varphi)$
956: if and only if $\sigma(\calH)\preccurlyeq \calM$.
957: Firing rule $R$ enabled at $\calM$ via $\sigma$ yields the new configuration
958: $$
959: \calM'~=~\sigma(\calB) \oplus (\calM\ominus \sigma(\calH))
960: $$
961: We use $\calM\Rightarrow_{MSR} \calM'$ to denote the firing of a rule at $\calM$
962: yielding $\calM'$.
963: \smallskip\\
964: A run is a sequence of configurations
965: $\calM_0\calM_1\ldots\calM_k$ with $\calM_0\in\calI$ such that
966: $\calM_{i}\Rightarrow_{MSR}\calM_{i+1}$ for $i\geq 0$.
967: A configuration $\calM$ is reachable if there exists $\calM_0\in\calI$ such that
968: $\calM_0\stackrel{*}{\Rightarrow}_{MSR}\calM$, where
969: $\stackrel{*}{\Rightarrow_{MSR}}$ is the transitive closure of $\Rightarrow_{MSR}$.
970: Finally, the successor and predecessor operators $Post$ and $Pre$ are defined
971: on a set of configurations $S$ as
972: $Post(S)=\{\calM'|\calM\Rightarrow_{MSR}\calM',\calM\in S\}
973: $ and $Pre(S)=\{\calM|\calM\Rightarrow_{MSR}\calM',\calM'\in S\}$, respectively.
974: $Pre^*$ and $Post^*$ denote their transitive closure.
975: \comment{
976: \begin{example}
977: The MSR$_{NC}$ rule $p(x)~|~q(y)\rightarrow
978: s(x')~|~p(y'):x=y,y'>x',x'>y$ symbolically represents a family of
979: rewriting rules on ground atomic formulas obtained instantiating
980: the variables with solution of the constraint. The ground multiset
981: rewriting rule $p(1)~|~q(1)\rightarrow s(3)~|~p(5)$ is one of its
982: instances. Given the instance $p(1)~|~q(1)\rightarrow s(3)~|~p(5)$
983: of the rule $p(x)~|~q(y)\rightarrow_{MSR}
984: s(x')~|~p(y'):x=y,y'>x',x'>y$, a possible rewriting step is
985: $p(3)~|~p(1)~|~q(1)~|~r(4)\Rightarrow p(3)~|~s(3)~|~p(5)~|~r(4)$.
986: \end{example}}
987: \smallskip\\
988: As shown in \cite{Del01,BD02}, Petri Nets represent a natural
989: abstractions of MSR$_{NC}$ (and more in general of MSR rule with constraints) specifications.
990: They can be encoded, in fact, in {\em propositional} MSR specifications
991: (e.g. abstracting away arguments from atomic formulas).
992: %
993: \subsection{Translation from TDL to MSR$_{NC}$}
994: %
995: The first thing to do is to find an adequate representation of names.
996: Since all we need is a way to distinguish old and new names,
997: we just need an infinite domain in which the $=$ and $\neq$ relation
998: are supported. Thus, we can interpret names in $\calN$ either as
999: integer of as rational numbers.
1000: Since operations like variable elimination are computationally less expensive
1001: than over integers, we choose to view names as non-negative rationals.
1002: Thus, a local (TDL) configuration $p=\tuple{s,n_1,\ldots,n_k}$ is
1003: encoded as the atomic formula $\TDLtoMSR{p}=s(n_1,\ldots,n_k)$,
1004: where $n_i$ is a non-negative rational.
1005: Furthermore, a global (TDL) configuration
1006: $G=\tuple{N,p_1,\ldots,p_m}$ is encoded as an MSR$_{NC}$
1007: configuration $\TDLtoMSR{G}$
1008: $$
1009: \TDLtoMSR{p_1}~|~\ldots~|~\TDLtoMSR{p_m}~|~fresh(n)
1010: $$
1011: where the value $n$ in the auxiliary atomic formula $fresh(n)$ is
1012: an rational number strictly greater than all values occurring in
1013: $\TDLtoMSR{p_1},\ldots,\TDLtoMSR{p_m}$.
1014: The predicate $fresh$ will allow us to generate unused names every time needed.
1015: \smallskip\\
1016: The translation of constants $\calC=\{c_1,\ldots,c_m\}$,
1017: and variables is defined as follows:
1018: $\TDLtoMSR{x}=x$ for $x\in\calV$, $\TDLtoMSR{\bot}=0$,
1019: $\TDLtoMSR{c_i}=i$ for $i:1,\ldots,m$.
1020: We extend ~$\TDLtoMSR{\cdot}$~ in the natural way on a guard $\gamma$, by
1021: decomposing every formula $x\neq e$ into $x<\TDLtoMSR{e}$ and
1022: $x>\TDLtoMSR{e}$. We will call $\TDLtoMSR{\gamma}$ the resulting
1023: {\em set} of $NC$-constraints.\footnote{As an example, if $\gamma$
1024: is the constraint $x=1,x\neq z$ then $\TDLtoMSR{\gamma}$ consists
1025: of the two constraints $x=1,x>z$ and $x=1,z>x$.}
1026: \smallskip\\
1027: Given $V=\{x_1,\ldots,x_k\}$, we define $V'$ as the set of new
1028: variables $\{x_1',\ldots,x_k'\}$. Now, let us consider the
1029: assignment $\alpha$ defined as $x_1:=e_1,\ldots,x_k:=e_k$ (we add
1030: assignments like $x_i:=x_i$ if some variable does not occur as
1031: target of $\alpha$). Then, $\TDLtoMSR{\alpha}$ is the
1032: $NC$-constraint $x_1'=\TDLtoMSR{e_1},\ldots,x_k'=\TDLtoMSR{e_k}$.
1033: \smallskip\\
1034: The translation of thread definitions is defined below (where we
1035: will often refer to Example \ref{AliceBob}).
1036: %
1037: \paragraph{Initial Global Configuration}
1038: %
1039: Given an initial global configuration consisting of the local configurations
1040: $\tuple{s_i,n_{i1},\ldots,n_{ik_i}}$ with $n_{ij}=\bot$ for $i:1,\ldots,u$,
1041: we define the following MSR$_{NC}$ rule
1042: $$
1043: \begin{array}{l}
1044: init\rightarrow s_1(x_{11},\ldots,x_{1k1})~|~\ldots~|~
1045: s_u(x_{u1},\ldots,x_{uk_u})~|~fresh(x)~:~\\
1046: ~~~~~~~~~~~~~~~~~~~~x>C,x_{11}=0,\ldots,x_{uk_u}=0
1047: \end{array}
1048: $$
1049: here $C$ is the largest rational used to interpret the constants in
1050: $\calC$.
1051: \smallskip\\
1052: For each thread definition $P=\tuple{Q,s_0,V,R}$ in $\calT$ with
1053: $V=\{x_1,\ldots,x_k\}$ we translate the rules in $R$ as described
1054: below.
1055: \paragraph{Internal Moves}
1056: For every {\em internal move} $\arrowup{s}{a}{s'}\lguard \gamma,\alpha\rguard$, and
1057: every $\nu\in\TDLtoMSR{\gamma}$ we define
1058: $$
1059: s(x_1,\ldots,x_k)\rightarrow s'(x_1',\ldots,x_k'):\nu,\TDLtoMSR{\alpha}
1060: $$
1061: \paragraph{Name Generation}
1062: For every {\em name generation} $\arrowup{s}{a}{s'}\lguard x_i:=new\rguard$,
1063: we define
1064: $$
1065: s(x_1,\ldots,x_k)~|~fresh(x)\rightarrow
1066: s'(x_1',\ldots,x_k')~|~fresh(y): y>x'_i,x_i'>x,\bigwedge_{j\neq i} x_j'=x_j
1067: $$
1068: For instance, the name generation
1069: $\arrowup{init_A}{fresh}{gen_A}\lguard n:=new\rguard$ is mapped into the
1070: MSR$_{NC}$ rule
1071: $\arrowup{init_A(id,x,y)|~fresh(u)}{}{gen_A(id',x',y')~|~fresh(u')}:\varphi$
1072: where $\varphi$ is the constraint $u'>x',x'>u,y'=y,id'=id$. The
1073: constraint $x'>u$ represents the fact that the new name associated
1074: to the local variable $n$ (the second argument of the atoms
1075: representing the thread) is fresh, whereas $u'>x'$ updates the
1076: current value of $fresh$ to ensure that the next generated names
1077: will be picked up from unused values.
1078: %
1079: \paragraph{Thread Creation}
1080: Let $P=\tuple{Q',t_0,V',R'}$ and $V'=\{y_{1},\ldots,y_{u}\}$.
1081: Then, for every {\em thread creation} $\arrowup{s}{a}{s'}\lguard
1082: run~P~with~\alpha\rguard$,
1083: we define
1084: $$
1085: \begin{array}{l}
1086: s(x_1,\ldots,x_k)\rightarrow
1087: s'(x_1',\ldots,x_k')~|~t(y_{1}',\ldots,y_{u}')~:~
1088: x_1'=x_1,\ldots,x_k'=x_k,\TDLtoMSR{\alpha}.
1089: \end{array}
1090: $$
1091: E.g., consider the rule
1092: $\arrowup{create}{new_A}{init_M}\lguard run~Init~with~id:=x,\ldots\rguard$ of Example
1093: \ref{AliceBob}. Its encoding yields the MSR$_{NC}$ rule
1094: $\arrowup{create(x)}{}{init_M(x')~|~init_{A}(id',n',m')}:\psi$, where
1095: $\psi$ represents the initialization of the local variables of the new thread
1096: $x'=x,id'=x,n'=0,m'=0$.
1097: %
1098: \paragraph{Rendez-vous}
1099: The encoding of rendez-vous communication is based on the use of
1100: constraint operations like variable elimination.
1101: Let $P$ and $P'$ be a pair of thread definitions, with
1102: local variables $V=\{x_1,\ldots,x_k\}$ and
1103: $V'=\{y_1,\ldots,y_l\}$ with $V\cap V'=\emptyset$. We first select
1104: all rules $\arrowup{s}{e!m}{s'}\lguard \gamma,\alpha\rguard$ in $R$ and
1105: $\arrowup{t}{e'?m'}{t'}\lguard \gamma',\alpha'\rguard$ in $R'$, such that
1106: $m=\tuple{w_1,\ldots,w_u}$, $m'=\tuple{w_1',\ldots,w_v'}$ and
1107: $u=v$.
1108: Then, we define the new MSR$_{NC}$ rule
1109: $$
1110: s(x_1,\ldots,x_k)~|~t(y_1,\ldots,y_l) \rightarrow
1111: s'(x_1',\ldots,x_k')~|~t'(y_1',\ldots,y_l') :\varphi
1112: $$
1113: for every $\nu\in\TDLtoMSR{\gamma}$ and
1114: $\nu'\in\TDLtoMSR{\gamma'}$ such that the NC-constraint $\varphi$
1115: obtained by eliminating
1116: $w_1',\ldots,w_v'$ from the constraint
1117: $\nu\wedge\nu'\wedge\TDLtoMSR{\alpha}\wedge\TDLtoMSR{\alpha'}\wedge
1118: w_1=w_1'\wedge\ldots\wedge w_v=w_v'$ is {\em satisfiable}.
1119: For instance, consider the rules
1120: $\arrowup{wait_A}{n_A?\tuple{y}}{stop_A}\lguard m_A:=y\rguard$ and
1121: $\arrowup{ready_B}{n_B!\tuple{m_B}}{stop_B}\lguard true\rguard$.
1122: We first build up a new constraint by conjoining the NC-constraints $y=m_B$
1123: (matching of message templates), and
1124: $n_A=n_B,m_A'=y,n_A'=n_A,m_B'=m_B,n_B'=n_B,id_1'=id_1,id_2'=id_2$
1125: (guards and actions of sender and receiver).
1126: After eliminating $y$ we obtain the constraint $\varphi$ defined as
1127: $n_B=n_A,m_A'=m_B,n_A'=n_A,m_B'=m_B,n_B'=n_B,id_1'=id_1,id_2'=id_2$
1128: defined over the variables of the two considered threads. This
1129: step allows us to {\em symbolically} represent the passing of
1130: names. After this step, we can represent the synchronization of
1131: the two threads by using a rule that simultaneously rewrite all
1132: instances that satisfy the constraints on the local data expressed
1133: by $\varphi$, i.e., we obtain the rule
1134: $$
1135: \begin{array}{l}
1136: wait_A(id_1,n_A,m_A)|~ready_B(id_2,n_B,m_B)\longrightarrow\\
1137: ~~~~~~~~~~~~~~stop_A(id_1',n_A',m_A')~|~stop_B(id_2',n_B',m_B'):\varphi
1138: \end{array}
1139: $$
1140: %
1141: \begin{figure*}[t]
1142: {
1143: $
1144: \begin{array}{l}
1145: \arrowup{init}{}{fresh(x)~|~init_M(y)}~:~x>0,y=0.
1146: \smallskip\\
1147: \arrowup{fresh(x)~|~init_{M}(y)}{}{fresh(x')~|~create(y')}~:~x'>y',y'>x.
1148: \smallskip\\
1149: \arrowup{create(x)}{}{init_M(x')~|~init_{A}(id',n',m')}~:~x'=x,id'=x,n'=0,m'=0.
1150: \smallskip\\
1151: \arrowup{create(x)}{}{init_M(x')~|~init_{B}(id',n',m')}~:~x'=x,id'=x,n'=0,m'=0.
1152: \smallskip\\
1153: \arrowup{init_A(id,n,m)|~fresh(u)}{}
1154: {gen_A(id,n',m)~|~fresh(u')}~:~u'>n',n'>u.
1155: \smallskip\\
1156: \arrowup{gen_A(id_1,n,m)|~init_B(id_2,u,v)}{}
1157: {wait_A(id_1,n,m)~|~gen_B(id_2',u',v')}~:~u'=n,v'=v
1158: \smallskip\\
1159: \arrowup{gen_B(id,n,m)|~fresh(u)}{}
1160: {ready_B(id,n,m')~|~fresh(u')}~:~u'>m',m'>u.
1161: \smallskip\\
1162: \arrowup{wait_A(id_1,n,m)|~ready_B(id_2,u,v)}{}
1163: {stop_A(id_1,n,m')~|~stop_B(id_2,u,v)}~:~
1164: n=u,m'=v.
1165: \smallskip\\
1166: \arrowup{stop_A(id,n,m)}{}
1167: {init_A(id',n',m')}~:~n'=0,m'=0,id'=id.
1168: \smallskip\\
1169: \arrowup{stop_B(id,n,m)}{}
1170: {init_B(id',n',m')}~:~n'=0,m'=0,id'=id.
1171: \end{array}
1172: $
1173: } \caption{Encoding of Example \ref{AliceBob}: for simplicity we embed constraints like $x=x'$
1174: into the MSR formulas.} \label{ABMSR}
1175: \end{figure*}
1176: %
1177: The complete translation of Example \ref{AliceBob} is shown in
1178: Fig. \ref{ABMSR} (for simplicity we have applied a renaming of
1179: variables in the resulting rules). An example of run in the
1180: resulting MSR$_{NC}$ specification is shown in Figure \ref{runABMSR}.
1181: %
1182: \begin{figure*}[t]
1183: {
1184: $
1185: \begin{array}{l}
1186: init\Rightarrow\ldots\Rightarrow
1187: fresh(4)~|~init_M(0)~|~init_A(2,0,0)~|~init_B(3,0,0)\\
1188: \Rightarrow
1189: fresh(8)~|~init_M(0)~|~gen_A(2,6,0)~|~init_B(3,0,0)\\
1190: \Rightarrow
1191: fresh(8)~|~init_M(0)~|~wait_A(2,6,0)~|~gen_B(3,6,0)\\
1192: \Rightarrow\ldots\Rightarrow
1193: fresh(16)~|~init_M(0)~|~wait_A(2,6,0)~|~gen_B(3,6,0)~|~init_A(11,0,0)
1194: \end{array}
1195: $}
1196: \caption{A run in the encoded program.} \label{runABMSR}
1197: \end{figure*}
1198: %
1199: Note that, a fresh name is selected between all values strictly
1200: greater than the current value of $fresh$ (e.g. in the second step
1201: $6>4$), and then $fresh$ is updated to a value strictly greater
1202: than all newly generated names (e.g. $8>6>4$).
1203:
1204: Let $\calT=\tuple{P_1,\ldots,P_t}$ be a collection of thread
1205: definitions and $G_0$ be an initial global state. Let
1206: $\calS$ be the MSR$_{NC}$ specification that results from the
1207: translation described in the previous section.
1208: \smallskip\\
1209: Let $G=\tuple{N,p_1,\ldots,p_n}$ be a global configuration with
1210: $p_i=\tuple{s_i,v_{i1},\ldots,v_{ik_i}}$, and let $h:N\leadsto \Rat_+$
1211: be an injective mapping. Then, we define $\TDLtoMSR{G}(h)$ as the
1212: MSR$_{NC}$ configuration
1213: $$
1214: s_1(h(v_{11}),\ldots,h(v_{1k_1}))~|~\ldots~|~s_n(h(v_{n1}),\ldots,h(v_{nk_n}))~|~fresh(v)
1215: $$
1216: where $v$ is a the first value strictly greater than all values in the range of $h$.
1217: Given an MSR$_{NC}$ configuration $\calM$ defined as
1218: $s_1(v_{11},\ldots,v_{1k_1})~|~\ldots~|~s_n(v_{n1},\ldots,v_{nk_n})$
1219: with $s_{ij}\in \Rat_+$, let $V(\calM)\subseteq\Rat_+$ be the set
1220: of values occurring in $\calM$. Then, given a bijective
1221: mapping $f:V(\calM)\leadsto N\subseteq \calN$, we
1222: define $\TDLtoMSR{\calM}(f)$ as the global configuration
1223: $\tuple{N,p_1,\ldots,p_n}$ where
1224: $p_i=\tuple{s_i,f(v_{i1}),\ldots,f(v_{ik_i})}$.
1225: \smallskip\\
1226: Based on the previous definitions, the following property then holds.
1227: \begin{theorem}\rm
1228: \label{soundcomp}
1229: For every run $G_0 G_1 \ldots$ in $\calT$ with corresponding set
1230: of names $N_0 N_1\ldots$, there exist sets $D_0 D_1 \ldots$ and
1231: bijective mappings $h_0 h_1 \ldots$ with
1232: $h_i:N_i\leadsto D_i\subseteq\Rat_+$ for $i\geq 0$, such that
1233: $init~\TDLtoMSR{G_0}({h_0})\TDLtoMSR{G_1}({h_1})\ldots$ is a run of
1234: $\calS$. Vice versa, if $init~\calM_0\calM_1\ldots$ is a run of
1235: $\calS$, then there exist sets $N_0 N_1 \ldots$ in $\calN$ and
1236: bijective mappings $f_0 f_1 \ldots$ with
1237: $f_i:V(\calM_i)\leadsto N_i$ for $i\geq 0$, such that
1238: $\TDLtoMSR{\calM_0}({f_0})\TDLtoMSR{\calM_1}({f_1})\ldots$ is a run in
1239: $\calT$.
1240: \end{theorem}
1241:
1242: \begin{proof}
1243: We first prove that every run in $\calT$ is simulated by a run in $\calS$.
1244:
1245: Let $G_0\ldots G_l$ be a run in $\calT$, i.e., a sequence
1246: of global states (with associated set of names $N_0\ldots N_l$)
1247: such that $G_i\Rightarrow G_{i+1}$ and $N_i\subseteq N_{i+1}$ for $i\geq 0$.
1248: \\
1249: We prove that it can be simulated in $\calS$ by induction on its length $l$.
1250: \\
1251: Specifically, suppose that there exist
1252: sets of non negative rationals $D_0 \ldots D_{l}$ and bijective mappings $h_0 \ldots h_{l}$ with
1253: $h_i:N_i\leadsto D_i$ for $0\leq i \leq {l}$, such that
1254:
1255: $$init~\widehat{G_0}({h_0})\ldots\widehat{G_l}({h_l})$$
1256: is a run of $\calS$.
1257: Furthermore, suppose $G_{l}\Rightarrow G_{l+1}$.
1258: \\
1259: We prove the thesis by a case-analysis on the type
1260: of rule applied in the last step of the run.
1261: \\
1262: Let $G_l=\tuple{N_l,p_1,\ldots,p_r}$ and
1263: $p_j=\tuple{s,n_1,\ldots,n_k}$ be a local configuration for the
1264: thread definition
1265: $P=\tuple{Q,s,V,R}$ with $V=\{x_1,\ldots,x_k\}$
1266: and $n_i\in N_l$ for $i:1,\ldots,k$.
1267: \\
1268: {\em Assignment} Suppose there exists a rule $\arrowup{s}{a}{s'}[\gamma,\alpha]$ in $R$
1269: such that $\rho_{p_j}$ satisfies $\gamma$,
1270: $G_l=\tuple{N_l,\ldots,p_j,\ldots}\Rightarrow\tuple{N_{l+1},\ldots,p_j',\ldots}=G_{l+1}$
1271: $N_l=N_{l+1}$,
1272: $p_j'=\tuple{s',n_1',\ldots,n_k'}$,
1273: and if $x_i:=y_i$ occurs in $\alpha$, then $n_i'=\rho_{p_j}(y_i)$,
1274: otherwise $n_i'=n_i$ for $i:1,\ldots,k$.
1275: \\
1276: The encoding of the rule returns one $MSR_{NC}$ rule having the form
1277: $$
1278: s(x_1,\ldots,x_k)\rightarrow s'(x_1',\ldots,x_k'):\gamma',\widehat{\alpha}
1279: $$
1280: for every $\gamma'\in\widehat{\gamma}$.
1281: \\
1282: By inductive hypothesis,
1283: $\widehat{G_l}({h_l})$ is a multiset of atomic formulas that contains the
1284: formula $s(h_l(n_1),\ldots,h_l(n_k))$.
1285: \\
1286: Now let us define $h_{l+1}$ as the mapping from $N_l$ to $D_l$ such that
1287: $h_{l+1}(n_i')=h_l(n_j)$ if $x_i:=x_j$ is in $\alpha$ and
1288: $h_{l+1}(n_i')=0$ if $x_i:=\bot$ is in $\alpha$.
1289: Furthermore, let us the define the evaluation
1290: $$
1291: \sigma=\tuple{x_1\mapsto h_l(n_1),\ldots,x_k\mapsto h_l(n_k),
1292: x_1'\mapsto h_{l+1}(n_1'),\ldots,x_k'\mapsto h_{l+1}(n_k')}
1293: $$
1294: \\
1295: Then, by construction of the set of constraints $\widehat{\gamma}$ and of
1296: the constraint $\widehat{\alpha}$,
1297: it follows that $\sigma$ is a solution for $\gamma',\widehat{\alpha}$ for some
1298: $\gamma'\in\widehat{\gamma}$.
1299: As a consequence, we have that
1300: $$
1301: s(n_1,\ldots,n_k)\rightarrow s'(n_1',\ldots,n_k')
1302: $$
1303: is a ground instance of one of the considered $MSR_{NC}$ rules.
1304: \\
1305: Thus, starting from the $MSR_{NC}$ configuration
1306: $\widehat{G_l}({h_l})$, if we apply a rewriting step we obtain a
1307: new configuration in which $s(n_1,\ldots,n_k)$ is replaced by $s'(n_1',\ldots,n_k')$,
1308: and all the other atomic formulas in $\widehat{G_{l+1}}({h_{l+1}})$ are the same as
1309: in $\widehat{G_l}({h_l})$.
1310: The resulting $MSR_{NC}$ configuration coincides then with the definition of
1311: $\widehat{G_{l+1}}({h_{l+1}})$.
1312: \\
1313: {\em Creation of new names}
1314: Let us now consider the case of fresh name generation.
1315: Suppose there exists a rule $\arrowup{s}{a}{s'}[x_i:=new]$ in $R$,
1316: and let $n\not\in N_l$,
1317: and suppose
1318: $
1319: \tuple{N_l,\ldots,p_j,\ldots}\Rightarrow\tuple{N_{l+1},\ldots,p_j',\ldots}
1320: $
1321: where $N_{l+1}=N_l\cup\{v\}$,
1322: $p_j'=\tuple{s',n_1',\ldots,n_k'}$ where $n_i'=n$, and $n_j'=n_j$ for $j\neq i$.
1323: \\
1324: We note than that the encoding of the previous rule returns the $MSR_{NC}$ rule
1325: $$
1326: s(x_1,\ldots,x_k)~|~fresh(x)\rightarrow s'(x_1',\ldots,x_k')~|~fresh(x'):\varphi
1327: $$
1328: where $\varphi$ consists of the constraints $y>x'_i,x_i'>x$ and $x_j'=x_j$ for $j\neq i$.
1329: By inductive hypothesis,
1330: $\widehat{G_l}({h_l})$ is a multiset of atomic formulas that contains the
1331: formulas $s(h_l(n_1),\ldots,h_l(n_k))$ and $fresh(v)$ where $h_l$ is a mapping into $D_l$,
1332: and $v$ is the first non-negative rational strictly greater than all
1333: values occurring in the formulas denoting processes.
1334: \\
1335: Let $v$ be a non negative rational strictly greater than all values in $D_l$.
1336: Furthermore, let us define $v'=v+1$ and
1337: $D_{l+1}=D_l\cup\{v,v'\}$.
1338: \\
1339: Furthermore, we define $h_{l+1}$ as follows
1340: $h_{l+1}(n)=h_{l}(n)$ for $n\in N_l$, and $h_{l+1}(n_i')=h_{l+1}(n)=v'$.
1341: Furthermore, we define the following evaluation
1342: $$
1343: \begin{array}{lcl}
1344: \sigma & = \langle &
1345: x\mapsto v,x_1\mapsto h_l(n_1),\ldots,x_k\mapsto h_l(n_k),\\
1346: & & x'\mapsto v',x_1'\mapsto h_{l+1}(n_1'),\ldots,x_k'\mapsto h_{l+1}(n_k')
1347: ~~~\rangle
1348: \end{array}
1349: $$
1350: Then, by construction of $\sigma$ and $\widehat{\alpha}$,
1351: it follows that $\sigma$ is a solution for $\widehat{\alpha}$.
1352: Thus,
1353: $$
1354: s(n_1,\ldots,n_k)~|~fresh(v)\rightarrow s'(n_1',\ldots,n_k')~|~fresh(v')
1355: $$
1356: is a ground instance of the considered $MSR_{NC}$ rule.
1357: \\
1358: Starting from the $MSR_{NC}$ configuration
1359: $\widehat{G_l}({h_l})$, if we apply a rewriting step we obtain a
1360: new configuration in which $s(n_1,\ldots,n_k)$ and $fresh(v)$ are
1361: substituted by $s'(n_1',\ldots,n_k')$ and $fresh(v')$,
1362: and all the other atomic formulas in $\widehat{G_{l+1}}({h_{l+1}})$ are the same
1363: as in $\widehat{G_l}({h_l})$.
1364: We conclude by noting that this formula coincides with the definition
1365: of $\widehat{G_{l+1}}({h_{l+1}})$.
1366: \\
1367: For sake of brevity we omit the case of {\em thread creation}
1368: whose only difference from the previous cases is the creation of
1369: several new atoms instead (with values obtained by evaluating the action)
1370: of only one.
1371: \\
1372: {\em Rendez-vous}
1373: Let
1374: $p_i=\tuple{s,n_1,\ldots,n_k}$ and $p_j=\tuple{t,m_1,\ldots,m_u}$
1375: two local configurations for threads $P\neq P'$,
1376: $n_i\in N_l$ for $i:1,\ldots,k$ and $m_i\in N_l$ for
1377: $i:1,\ldots,u$.
1378: \\
1379: Suppose
1380: $\arrowup{s}{c!m}{s'}[\gamma,\alpha]$ and
1381: $\arrowup{t}{c?m'}{t'}[\gamma',\alpha']$,
1382: where $m=\tuple{x_{i_1},\ldots,x_{i_v}}$, and
1383: $m'=\tuple{y_1,\ldots,y_v}$ (
1384: all defined over distinct variables)
1385: are rules in $R$.
1386: \\
1387: Furthermore, suppose that $\rho_{p_i}$ satisfies $\gamma$, and that $\rho'$
1388: (see definition of the operational semantics)
1389: satisfies $\gamma'$, and suppose that
1390: $G_l=\tuple{N_l,\ldots,p_i,\ldots,p_j,\ldots}\Rightarrow
1391: \tuple{N_{l+1},\ldots,p_i',\ldots,p_j',\ldots}=G_{l+1},
1392: $
1393: where $N_{l+1}=N_l$, $p_i'=\tuple{s',n_1',\ldots,n_k'}$,
1394: $p_j'=\tuple{t',m_1',\ldots,m_u'}$,
1395: and if $x_i:=e$ occurs in $\alpha$, then $n_i'=\rho_{p_i}(e)$,
1396: otherwise $n_i'=n_i$ for $i:1,\ldots,k$;
1397: if $u_i:=e$ occurs in $\alpha'$, then $m_i'=\rho'(e)$,
1398: otherwise $m_i'=m_i$ for $i:1,\ldots,u$.
1399: \\
1400: By inductive hypothesis,
1401: $\widehat{G_l}({h_l})$ is a multiset of atomic formulas that contains the
1402: formulas $s(h_l(n_1),\ldots,h_l(n_k))$ and $t(h_l(m_1),\ldots,h_l(m_u))$.
1403: \\
1404: Now, let us define $h_{l+1}$ as the mapping from $N_l$ to $D_l$ such that
1405: $h_{l+1}(n_i')=h_l(n_j)$ if $x_i:=x_j$ is in $\alpha$,
1406: $h_{l+1}(m_i')=h_l(m_j)$ if $u_i:=u_j$ is in $\alpha'$,
1407: $h_{l+1}(n_i')=0$ if $x_i:=\bot$ is in $\alpha$,
1408: $h_{l+1}(m_i')=0$ if $u_i:=\bot$ is in $\alpha'$.
1409: \\
1410: Now, let us define $\sigma$ as the evaluation from $N_l$ to $D_l$ such that
1411: $$
1412: \begin{array}{l}
1413: \sigma=\sigma_1\cup\sigma_2\\
1414: \sigma_1=\tuple{x_1\mapsto h_l(n_1),\ldots,x_k\mapsto h_l(n_k),
1415: u_1\mapsto h_l(m_1),\ldots,u_u\mapsto h_l(m_u)}
1416: \\
1417: \sigma_2=\tuple{x_1'\mapsto h_{l+1}(n_1'),\ldots,x_k'\mapsto h_{l+1}(n_k'),
1418: u_1'\mapsto h_{l+1}(m_1'),\ldots,u_u'\mapsto h_{l+1}(m_u')}.
1419: \end{array}
1420: $$
1421: Then, by construction of
1422: the sets of constraints $\widehat{\gamma},\widehat{\gamma'},\widehat{\alpha}$ and
1423: $\widehat{\alpha'}$ it follows that $\sigma$ is a solution for the constraint
1424: $\exists w_1'.\ldots\exists w_p'.
1425: \theta\wedge\theta'\wedge\widehat{\alpha}\wedge\widehat{\alpha'}\wedge
1426: w_1=w_1'\wedge\ldots\wedge w_p=w_p'$
1427: for some $\theta\in \widehat{\gamma}$ and $\theta'\in \widehat{\gamma'}$.
1428: Note in fact that the equalities $w_i=w_i'$ express the passing of values defined
1429: via the evaluation $\rho'$ in the operational semantics.
1430: \\
1431: As a consequence,
1432: $$
1433: s(n_1,\ldots,n_k)~|~t(m_1,\ldots,m_u)
1434: \rightarrow
1435: s'(n_1',\ldots,n_k')~|~t'(m_1',\ldots,m_u')
1436: $$
1437: is a ground instance of one of the considered $MSR_{NC}$ rules.
1438: \\
1439: Thus, starting from the $MSR_{NC}$ configuration
1440: $\widehat{G_l}({h_l})$, if we apply a rewriting step we obtain a
1441: new configuration in which $s(n_1,\ldots,n_k)$ has been replaced by $s'(n_1',\ldots,n_k')$,
1442: and $t'(m_1',\ldots,m_k')$ has been replaced by $t(m_1',\ldots,m_u')$,
1443: and all the other atomic formulas are as in $\widehat{G_l}({h_l})$.
1444: This formula coincides with the definition of $\widehat{G_{l+1}}({h_{l+1}})$.
1445:
1446: The proof of completeness is by induction on the length of an MSR run,
1447: and by case-analysis on the application of the rules.
1448: The structure of the case analysis is similar to the previous one
1449: and it is omitted for brevity.
1450: \end{proof}
1451:
1452: %
1453: \section{Verification of TDL Programs}
1454: \label{Verification}\label{Safety}
1455: %The connection between TDL and MSR$_{NC}$ allows us to explo a verification
1456: %method for {\em safety properties} of abstract models of multithreaded programs.
1457: Safety and invariant properties are probably the most important class of correctness
1458: specifications for the validation of a concurrent system.
1459: For instance, in Example \ref{AliceBob} we could be interested in proving
1460: that every time a session terminates, two instances of thread $Init$ and $Resp$
1461: have exchanged the two names generated during the session.
1462: To prove the protocol correct independently from the number of names and threads
1463: generated during an execution, we have to show that from the initial configuration
1464: $G_0$ it is not possible to reach a configuration that violates the aforementioned
1465: property.
1466: The configurations that violate the property are those in which two
1467: instances of $Init$ and $Resp$ conclude the execution of the protocol exchanging
1468: only the first nonce. These configurations can be represented by looking at only two
1469: threads and at the relationship among their local data. Thus, we
1470: can reduce the verification problem of this safety property to
1471: the following problem:
1472: Given an initial configuration $G_0$ we would like to decide
1473: if a global
1474: configuration that {\em contains} {\em at least} two local
1475: configurations having the form $\tuple{stop_A,i,n,m}$ and
1476: $\tuple{stop_B,i',n',m'}$ with $n'=n$ and $m\neq m'$ for some
1477: $i,i',n,n',m,m'$ is reachable.
1478: This problem can be viewed as an extension of the {\em control
1479: state reachability problem} defined in \cite{AN00} in which we consider
1480: both {control locations} and {local variables}.
1481: Although control state reachability is undecidable
1482: (see Corollary \ref{reachability}),
1483: the encoding of TDL into MSR$_{NC}$ can be used to define a {sound} and {automatic}
1484: verification methods for TDL programs.
1485: For this purpose, we will exploit a verification method introduced for
1486: \MSRC~in \cite{Del01,Del02}. In the rest of this section we will briefly
1487: summarize how to adapt the main results in \cite{Del01,Del02} to the specific
1488: case of MSR$_{NC}$.
1489:
1490: Let us first reformulate the control state reachability problem
1491: of Example \ref{AliceBob} for the aforementioned safety property
1492: on the low level encoding into MSR$_{NC}$.
1493: Given the MSR$_{NC}$ initial configuration $init$ we would like to
1494: check that no configuration in $Post^*(\{init\})$ has the following
1495: form
1496: $$
1497: \{stop_A(a_1,v_1,w_1),stop_B(a_2,v_2,w_2)\}\oplus \calM
1498: $$
1499: for $a_i,v_i,w_i\in \Rat~i:1,2$ and an arbitrary multiset of ground atoms $\calM$.
1500: Let us call $U$ the set of {\em bad MSR$_{NC}$ configurations} having the
1501: aforementioned shape.
1502: Notice that $U$ is upward closed with respect to multiset inclusion, i.e.,
1503: if $\calM\in U$ and $\calM\preccurlyeq\calM'$, then $\calM'\in U$.
1504: Furthermore, for if $U$ is upward closed, so is $Pre(U)$.
1505: On the basis of this property, we can try to apply the methodology proposed
1506: in \cite{AN00} to develop a procedure to compute a finite representation $R$
1507: of $Pre^*U)$.
1508: For this purpose, we need the following ingredients:
1509: \begin{enumerate}
1510: \item a symbolic representation of upward closed sets of configurations
1511: (e.g. a set of assertions $S$ whose denotation $\den{S}$ is $U$);
1512: \item a computable symbolic predecessor operator $\bfPre$ working on sets of formulas
1513: such that $\den{\bfPre(S)}=Pre(\den{S})$;
1514: \item a (decidable) entailment relation $Ent$ to compare
1515: the denotations of symbolic representations, i.e., such that
1516: $Ent(N,M)$ implies $\den{N}\subseteq \den{M}$.
1517: If such a relation $Ent$ exists, then it can be naturally extended to sets
1518: of formulas as follows: $Ent^S(S,S')$ if and only if for all $N\in S$ there exists $M\in S'$
1519: such that $Ent(N,M)$ holds (clearly, if $Ent$ is an entailment, then
1520: $Ent^S(S,S')$ implies $\den{S}\subseteq \den{S'}$).
1521: \end{enumerate}
1522: The combination of these three ingredients can be used to define
1523: a verification methods based on backward reasoning as explained next.
1524: \paragraph{Symbolic Backward Reachability}
1525: Suppose that $M_1,\ldots,M_n$ are the formulas of our assertional language
1526: representing the infinite set $U$ consisting of all bad configurations.
1527: The {symbolic backward reachability procedure} (SBR) procedure
1528: computes a chain $\{I_i\}_{i\geq 0}$ of sets of assertions such that
1529: $$
1530: \begin{array}{l}
1531: I_0=\{M_1,\ldots,M_n\}\\
1532: I_{i+1}=I_i~\cup~\bfPre(I_i)~~\hbox{for}~i\geq 0
1533: \end{array}
1534: $$
1535: The procedure SBR stops when $\bfPre$ produces only redundant information, i.e.,
1536: $Ent^S(I_{i+1},I_i)$.
1537: Notice that $Ent^S(I_i,I_{i+1})$ always holds since $I_i\subseteq I_{i+1}$.
1538: %
1539: \paragraph{Symbolic Representation}
1540: In order to find an adequate represention of infinite sets of MSR$_{NC}$
1541: configurations we can resort to the notion of {\em constrained configuration}
1542: introduced in \cite{Del01} for the language scheme MSR($\calC$) defined
1543: for a generic constraint system $\calC$.
1544: We can instantiate this notion with $NC$ constraints as follows.
1545: A {constrained configuration} over $\calP$ is a formula
1546: $$
1547: p_1(x_{11},\ldots,x_{1k_1})~|~\ldots~|~p_n(x_{n1},\ldots,x_{nk_n}):\varphi
1548: $$
1549: where $p_1,\ldots,p_n\in\calP$, $x_{i1},\ldots,x_{ik_i}\in\calV$
1550: for any $i:1,\ldots n$ and $\varphi$ is an $NC$-constraint.
1551: The denotation a constrained configuration
1552: $M\doteq (\calM:\varphi)$ is defined by taking the upward closure
1553: with respect to multiset inclusion of the set of ground instances, namely
1554: $$
1555: \den{M}=\{ \calM'~|~\sigma(\calM)\preccurlyeq \calM',~\sigma\in\Sol(\varphi)\}
1556: $$
1557: This definition can be extended to sets of MSR$_{NC}$ constrained
1558: configurations with {\em disjoint variables} (we use variable renaming to avoid
1559: variable name clashing) in the natural way.
1560:
1561: In our example the following set $S_U$ of MSR$_{NC}$ constrained
1562: configurations (with distinct variables) can be used to finitely
1563: represent all possible violations $U$ to the considered safety property
1564: $$
1565: \begin{array}{ll}
1566: S_U=\{ & stop_A(i_1,n_1,m_1)~|~stop_B(i_2,n_2,m_2)~:~n_1=n_2,m_1>m_2\\
1567: & stop_A(i_1,n_1,m_1)~|~stop_B(i_2,n_2,m_2)~:~n_1=n_2,m_2>m_1\}
1568: \end{array}
1569: $$
1570: Notice that we need two formulas to represent $m_1\neq m_2$
1571: using a disjunction of $>$ constraints.
1572: The MSR$_{NC}$ configurations $stop_B(1,2,6)~|~stop_A(4,2,5)$, and
1573: $stop_B(1,2,6)~|~stop_A(4,2,5)~|~wait_A(2,7,3)$ are both
1574: contained in the denotation of $S_U$.
1575: Actually, we have that $\den{S_U}=U$.
1576: This symbolic representation allows us to reason on infinite sets
1577: of MSR$_{NC}$ configurations, and thus on global configurations of
1578: a TDL program, forgetting the actual number or threads of a given run.
1579:
1580: To manipulate constrained configurations, we can instantiate
1581: to $NC$-constraints the {symbolic predecessor
1582: operator} $\bfPre$ defined for a generic constraint system in \cite{Del02}.
1583: Its definition is also given in Section \ref{PreOp} in Appendix.
1584: From the general properties proved in \cite{Del02},
1585: we have that when applied to a finite set of
1586: MSR$_{NC}$ constrained configurations $S$, $\bfPre_{NC}$ returns a finite set
1587: of constrained configuration such that
1588: $\den{\bfPre_{NC}(S)}=Pre(\den{S})$, i.e., $\bfPre_{NC}(S)$ is
1589: a symbolic representation of the immediate predecessors of
1590: the configurations in the denotation (an upward closed set) of $S$.
1591: Similarly we can instantiate the generic entailment operator defined
1592: in \cite{Del02} to MSR$_{NC}$ constrained configurations so as to obtain
1593: an a relation $Ent$ such that $Ent_{NC}(N,M)$ implies $\den{N}\subseteq \den{M}$.
1594: Based on these properties, we have the following result.
1595: \begin{proposition}
1596: Let $\calT$ be a TDL program with initial global configuration $G_0$,
1597: Furthermore, let $\calS$ be the corresponding MSR$_{NC}$ encoding.
1598: and $S_U$ be the set of MSR$_{NC}$ constrained configurations denoting a given
1599: set of bad TDL configurations.
1600: Then, $init\not\in\bfPre_{NC}^*(S_U)$ if and only if
1601: there is no finite run $G_0\ldots G_n$ and mappings $h_0,\ldots,h_n$ from the
1602: names occurring in $G$ to non-negative rationals such that
1603: $\TDLtoMSR{init}~\TDLtoMSR{G_0}({h_0})\ldots\TDLtoMSR{G_n}({h_n})$
1604: is a run in $\calS$ and $\TDLtoMSR{G_n}({h_n})\in\den{U}.$
1605: \end{proposition}
1606: \begin{proof}
1607: Suppose $init\not\in\bfPre_{NC}^*(U)$.
1608: Since $\den{\bfPre_{NC}(S)}=pre(\den{S})$ for any $S$,
1609: it follows that there cannot exist runs
1610: $init \calM_0 \ldots \calM_n$ in $\calS$
1611: such that $\calM_n\in \den{U}$.
1612: The thesis then follows from the Theorem \ref{soundcomp}.
1613: \end{proof}
1614: %
1615: As discussed in \cite{BD02}, we have implemented our verification
1616: procedure based on $MSR$ and {\em linear constraints} using a
1617: CLP system with linear arithmetics.
1618: By the translation presented in this paper, we can now reduce the
1619: verification of safety properties of multithreaded programs
1620: to a fixpoint computation built on {\em constraint operations}.
1621: As example, we have applied our CLP-prototype to automatically verify
1622: the specification of Fig. \ref{ABMSR}.
1623: The unsafe states are those described in Section \ref{Verification}.
1624: Symbolic backward reachability terminates after 18 iterations
1625: and returns a symbolic representation of the fixpoint with 2590 constrained
1626: configurations.
1627: The initial state $init$ is not part of the resulting set.
1628: This proves our original thread definitions correct with respect to
1629: the considered safety property.
1630: %
1631: \subsection{An Interesting Class of TDL Programs}
1632: \label{Decidable}
1633: The proof of Theorem \ref{twocounters} shows
1634: that verification of safety properties is undecidable for TDL
1635: specifications in which threads have several local variables (they
1636: are used to create linked lists). As mentioned in the introduction,
1637: we can apply the sufficient conditions for the termination of the procedure SBR
1638: given in \cite{BD02,Del02} to identify the following interesting subclass
1639: of TDL programs.
1640: %
1641: \begin{definition}\rm
1642: A monadic TDL thread definition $P=\tuple{Q,s,V,R}$ is such that $V$
1643: is at most a singleton, and every message template in $R$ has at most one variable.
1644: \end{definition}
1645: %
1646: A monadic thread definition can be encoded into the monadic fragment
1647: of MSR$_{NC}$ studied in \cite{Del02}. Monadic MSR$_{NC}$ specifications are
1648: defined over atomic formulas of the form $p$ or $p(x)$ with $p$ is a predicate symbol
1649: and $x$ is a variable, and on atomic constraints of the form $x=y$, and $x>y$.
1650: To encode a monadic TDL thread definitions into a Monadic MSR$_{NC}$ specification,
1651: we first need the following observation.
1652: Since in our encoding we only use the constant $0$, we
1653: first notice that we can restrict our attention to MSR$_{NC}$ specifications in which
1654: constraints have no constants at all.
1655: Specifically, to encode the generation of fresh names we only have to add an
1656: auxiliary atomic formula $zero(z)$, and refer to it every time we need to express the
1657: constant $0$. As an example, we could write rules like
1658: $$
1659: \arrowup{init}{}{fresh(x)~|~init_M(y)~|~zero(z)}~:~x>z,y=z
1660: $$
1661: for
1662: initialization, and
1663: $$
1664: \begin{array}{l}
1665: \arrowup{create(x)~|~zero(z)}{}
1666: {init_M(x')~|~init_{A}(id',n',m')~|~zero(z)}~:~\\
1667: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~x'=x,id'=x,n'=z,m'=z,z'=z
1668: \end{array}
1669: $$
1670: for all assignments involving the constant $0$.
1671: By using this trick an by following the encoding of Section \ref{MSRTranslation},
1672: the translation of a collection of monadic thread definitions directly returns
1673: a {\em monadic} MSR$_{NC}$ specification.
1674: By exploiting this property, we obtain the following result.
1675: \begin{theorem}\label{termination1}
1676: The verification of safety properties whose violations can be
1677: represented via an upward closed set $U$ of global configurations is
1678: decidable for a collection $\calT$ of monadic TDL definitions.
1679: \end{theorem}
1680: \begin{proof}
1681: Let $\calS$ be the MSR$_{NC}$ encoding of $\calT$
1682: and $S_U$ be the set of constrained configuration such that $S_U=U$.
1683: The proof is based on the following properties.
1684: First of all, the MSR$_{NC}$ specification $\calS$ is monadic.
1685: Furthermore, as shown in \cite{Del02}, the class of monadic MSR$_{NC}$ constrained
1686: configurations is closed under application of the operator $\bfPre_{NC}$.
1687: Finally, as shown in \cite{Del02}, there exists an entailment relation $CEnt$
1688: for monadic constrained configurations that ensures the
1689: termination of the SBR procedure applied to a monadic MSR$_{NC}$ specification.
1690: Thus, for the monadic MSR$_{NC}$ specification $\calS$,
1691: the chain defined as $I_0=S_U$, $I_{i+1}=I_i\cup \bfPre(I_i)$
1692: always reaches a point $k\geq 1$ in which $CEnt^S(I_{k+1},I_k)$,
1693: i.e. $\den{I_k}$ is a fixpoint for $Pre$.
1694: Finally, we note that we can always check for membership of
1695: $init$ in the resulting set $I_k$.
1696: \end{proof}
1697: As shown in \cite{Sch02}, the complexity of verification methods based on
1698: symbolic backward reachability relying on the general results in \cite{AN00,FS01}
1699: is non primitive recursive.
1700: %
1701: %
1702: %Monadic TDL programs are more expressive than Petri Nets.
1703: %In this setting we can define in fact models with an
1704: %unbounded number of threads (tokens), and constraints over
1705: %value stored in their (one-place) memory.
1706: %Time dependent models (e.g. time-stamps), relations over process identifiers
1707: %or channel names are all examples of systems that can be modeled in this setting.
1708: %
1709: \section{Conclusions and Related Work}
1710: \label{conclusions}
1711: %
1712: In this paper we have defined the theoretical grounds for the possible application of
1713: constraint-based symbolic model checking for the automated analysis of abstract models
1714: of multithreaded concurrent systems providing name generation, name mobility, and unbounded control.
1715: %
1716: Our verification approach is based on an encoding into a low level
1717: formalism based on the combination of multiset rewriting and constraints that allows
1718: us to naturally implement name generation, value passing, and
1719: dynamic creation of threads.
1720: %
1721: Our verification method makes use of symbolic
1722: representations of infinite set of system states and of symbolic
1723: backward reachability. For this reason, it can be viewed as a conservative
1724: extension of traditional finite-state model checking methods.
1725: The use of symbolic state analysis is strictly related to the analysis methods based on
1726: abstract interpretation. A deeper study of the connections with abstract interpretation
1727: is an interesting direction for future research.
1728:
1729: \paragraph{Related Work}
1730: The high level syntax we used to present the abstract models of
1731: multithreaded programs is an extension of the communicating finite state
1732: machines used in protocol verification \cite{Boc78},
1733: and used for representing abstraction of multithreaded software
1734: programs \cite{BCR01}. In our setting we enrich the formalism
1735: with local variables, name generation and mobility, and unbounded control.
1736: Our verification approach is inspired by the recent work of Abdulla and Jonsson.
1737: In \cite{AJ03}, Abdulla and Jonsson proposed an assertional
1738: language for Timed Networks in which they use dedicated data
1739: structures to symbolically represent configurations parametric in the
1740: number of tokens and in the {\em age} (a real number) associated
1741: to tokens. In \cite{AN00}, Abdulla and Nyl\'{e}n formulate a
1742: symbolic algorithm using {\em existential zones} to represent
1743: the state-space of Timed Petri Nets. Our approach generalizes the
1744: ideas of \cite{AJ03,AN00} to systems specified via multiset
1745: rewriting and with more general classes of constraints.
1746: In \cite{AJ01}, the authors apply
1747: similar ideas to (unbounded) channel systems in which messages can
1748: vary over an infinite {\em name} domain and can be stored in a
1749: finite (and fixed a priori) number of data variables.
1750: However, they do not relate these results to multithreaded programs.
1751: Multiset rewriting over first order atomic formulas has been proposed
1752: for specifying security protocols by Cervesato et al. in \cite{CDLMS99}.
1753: The relationships between this framework and concurrent languages based on
1754: process algebra have been recently studied in \cite{BCLM03}.
1755: Apart from approaches based on Petri Net-like models (as in \cite{GS92,BCR01}),
1756: networks of {\em finite-state} processes can also be verified by means of
1757: automata theoretic techniques as in \cite{BJNT00}.
1758: In this setting the set of possible {\em local states} of individual
1759: processes are abstracted into a {\em finite alphabet}. Sets of
1760: global states are represented then as {\em regular languages}, and
1761: transitions as relations on languages. Differently from the
1762: automata theoretic approach, in our setting we handle
1763: parameterized systems in which individual components have local
1764: variables that range over {\em unbounded} values.
1765: The use of constraints for the verification of concurrent systems is
1766: related to previous works connecting Constraint
1767: Logic Programming and verification, see e.g. \cite{DP99}. In this
1768: setting transition systems are encoded via CLP programs used to
1769: encode the {\em global} state of a system and its updates. In the approach
1770: proposed in \cite{Del01,BD02}, we refine this idea by using multiset rewriting
1771: and constraints to {\em locally} specify updates to the {\em global} state.
1772: In \cite{Del01}, we defined the general framework of multiset rewriting with
1773: constraints and the corresponding symbolic analysis technique.
1774: The language proposed in \cite{Del01} is given for a generic constraint system
1775: $\calC$ (taking inspiration from $CLP$ the language is called
1776: $MSR(\calC)$). In \cite{BD02}, we applied this formalism to verify properties
1777: of mutual exclusion protocols (variations of the {\em ticket algorithm})
1778: for systems with an arbitrary number of processes.
1779: In the same paper we also formulated sufficient conditions for the termination
1780: of the backward analysis.
1781: The present paper is the first attempt of relating the low level language proposed
1782: in \cite{Del01} to a high level language with explicit management of names and
1783: threads.
1784: %
1785: \paragraph{Acknowledgments}
1786: The author would like to thank Ahmed Bouajjani, Andrew Gordon, Fabio Martinelli,
1787: Catuscia Palamidessi, Luca Paolini, and Sriram Rajamani and the anonymous reviewers
1788: for several fruitful comments and suggestions.
1789: %
1790: \bibliographystyle{acmtrans}
1791: \begin{thebibliography}{}
1792:
1793: \bibitem[\protect\citeauthoryear{Abdulla, {C}er{\=a}ns, Jonsson, and
1794: Tsay}{Abdulla et~al\mbox{.}}{1996}]{ACJT96}
1795: {\sc Abdulla, P.~A.}, {\sc {C}er{\=a}ns, K.}, {\sc Jonsson, B.}, {\sc and} {\sc
1796: Tsay, Y.-K.} 1996.
1797: \newblock {General Decidability Theorems for Infinite-State Systems}.
1798: \newblock In {\em {Proceedings 11th Annual International Symposium on Logic in
1799: Computer Science (LICS'96)}}. {IEEE Computer Society Press}, New Brunswick,
1800: New Jersey, 313--321.
1801:
1802: \bibitem[\protect\citeauthoryear{Abdulla and Jonsson}{Abdulla and
1803: Jonsson}{2001}]{AJ01}
1804: {\sc Abdulla, P.~A.} {\sc and} {\sc Jonsson, B.} 2001.
1805: \newblock {Ensuring Completeness of Symbolic Verification Methods for
1806: Infinite-State Systems}.
1807: \newblock {\em {Theoretical Computer Science}\/}~{\em 256,\/}~1-2, 145--167.
1808:
1809: \bibitem[\protect\citeauthoryear{Abdulla and Jonsson}{Abdulla and
1810: Jonsson}{2003}]{AJ03}
1811: {\sc Abdulla, P.~A.} {\sc and} {\sc Jonsson, B.} 2003.
1812: \newblock {Model checking of systems with many identical timed processes}.
1813: \newblock {\em {Theoretical Computer Science}\/}~{\em 290,\/}~1, 241--264.
1814:
1815: \bibitem[\protect\citeauthoryear{Abdulla and Nyl{\'{e}}n}{Abdulla and
1816: Nyl{\'{e}}n}{2000}]{AN00}
1817: {\sc Abdulla, P.~A.} {\sc and} {\sc Nyl{\'{e}}n, A.} 2000.
1818: \newblock {Better is Better than Well: On Efficient Verification of
1819: Infinite-State Systems}.
1820: \newblock In {\em {Proceedings 15th Annual International Symposium on Logic in
1821: Computer Science (LICS'00)}}. {IEEE Computer Society Press}, {Santa Barbara,
1822: California}, 132--140.
1823:
1824: \bibitem[\protect\citeauthoryear{Ball, Chaki, and Rajamani}{Ball
1825: et~al\mbox{.}}{2001}]{BCR01}
1826: {\sc Ball, T.}, {\sc Chaki, S.}, {\sc and} {\sc Rajamani, S.~K.} 2001.
1827: \newblock {Parameterized Verification of Multithreaded Software Libraries}.
1828: \newblock In {\em {7th International Conference on Tools and Algorithms for
1829: Construction and Analysis of Systems (TACAS 2001), Genova, Italy, April
1830: 2-6,}}. {LNCS}, vol. 2031. {Springer-Verlag}, 158--173.
1831:
1832: \bibitem[\protect\citeauthoryear{Bistarelli, Cervesato, Lenzini, and
1833: Martinelli}{Bistarelli et~al\mbox{.}}{2005}]{BCLM03}
1834: {\sc Bistarelli, S.}, {\sc Cervesato, I.}, {\sc Lenzini, G.}, {\sc and} {\sc
1835: Martinelli, F.} 2005.
1836: \newblock Relating multiset rewriting and process algebras for security
1837: protocol analysis.
1838: \newblock {\em Journal of Computer Security\/}~{\em 13,\/}~1, 3--47.
1839:
1840: \bibitem[\protect\citeauthoryear{Bochmann}{Bochmann}{1978}]{Boc78}
1841: {\sc Bochmann, G.~V.} 1978.
1842: \newblock Finite state descriptions of communicating protocols.
1843: \newblock {\em Computer Networks\/}~{\em 2}, 46--57.
1844:
1845: \bibitem[\protect\citeauthoryear{Bouajjani, Jonsson, Nilsson, and
1846: Touili}{Bouajjani et~al\mbox{.}}{2000}]{BJNT00}
1847: {\sc Bouajjani, A.}, {\sc Jonsson, B.}, {\sc Nilsson, M.}, {\sc and} {\sc
1848: Touili, T.} 2000.
1849: \newblock {Regular Model Checking}.
1850: \newblock In {\em {Proceedings 12th International Conference on Computer Aided
1851: Verification (CAV'00)}}, {E.~A. Emerson} {and} {A.~P. Sistla}, Eds. {LNCS},
1852: vol. 1855. {Springer-Verlag}, {Chicago, Illinois}, 403--418.
1853:
1854: \bibitem[\protect\citeauthoryear{Bozzano and Delzanno}{Bozzano and
1855: Delzanno}{2002}]{BD02}
1856: {\sc Bozzano, M.} {\sc and} {\sc Delzanno, G.} 2002.
1857: \newblock Algorithmic verification of invalidation-based protocols.
1858: \newblock In {\em 14th International Conference on Computer Aided Verification,
1859: CAV '02}. Lecture Notes in Computer Science, vol. 2404. Springer.
1860:
1861: \bibitem[\protect\citeauthoryear{Cervesato, Durgin, Lincoln, Mitchell, and
1862: Scedrov}{Cervesato et~al\mbox{.}}{1999}]{CDLMS99}
1863: {\sc Cervesato, I.}, {\sc Durgin, N.}, {\sc Lincoln, P.}, {\sc Mitchell, J.},
1864: {\sc and} {\sc Scedrov, A.} 1999.
1865: \newblock {A Meta-notation for Protocol Analysis}.
1866: \newblock In {\em {12th Computer Security Foundations Workshop (CSFW'99)}}.
1867: {IEEE Computer Society Press}, {Mordano, Italy}, 55--69.
1868:
1869: \bibitem[\protect\citeauthoryear{Delzanno}{Delzanno}{2001}]{Del01}
1870: {\sc Delzanno, G.} 2001.
1871: \newblock {An Assertional Language for Systems Parametric in Several
1872: Dimensions}.
1873: \newblock In {\em {Verification of Parameterized Systems - VEPAS 2001}}.
1874: {ENTCS}, vol.~50.
1875:
1876: \bibitem[\protect\citeauthoryear{Delzanno}{Delzanno}{2005}]{Del02}
1877: {\sc Delzanno, G.} 2005.
1878: \newblock {Constraint Multiset Rewriting}.
1879: \newblock Tech. Rep. TR-05-08, Dipartimento Informatica e Scienze
1880: dell'Informazione, Universit\`a di Genova, Italia.
1881:
1882: \bibitem[\protect\citeauthoryear{Delzanno and Podelski}{Delzanno and
1883: Podelski}{1999}]{DP99}
1884: {\sc Delzanno, G.} {\sc and} {\sc Podelski, A.} 1999.
1885: \newblock {Model checking in CLP}.
1886: \newblock In {\em {Proceedings 5th International Conference on Tools and
1887: Algorithms for Construction and Analysis of Systems (TACAS'99)}}. Lecture
1888: Notes in Computer Science, vol. 1579. {Springer-Verlag}, Amsterdam, The
1889: Netherlands, 223--239.
1890:
1891: \bibitem[\protect\citeauthoryear{Finkel and Schnoebelen}{Finkel and
1892: Schnoebelen}{2001}]{FS01}
1893: {\sc Finkel, A.} {\sc and} {\sc Schnoebelen, P.} 2001.
1894: \newblock {Well-Structured Transition Systems Everywhere!}
1895: \newblock {\em {Theoretical Computer Science}\/}~{\em 256,\/}~1-2, 63--92.
1896:
1897: \bibitem[\protect\citeauthoryear{German and Sistla}{German and
1898: Sistla}{1992}]{GS92}
1899: {\sc German, S.~M.} {\sc and} {\sc Sistla, A.~P.} 1992.
1900: \newblock {Reasoning about Systems with Many Processes}.
1901: \newblock {\em {Journal of the ACM}\/}~{\em 39,\/}~3, 675--735.
1902:
1903: \bibitem[\protect\citeauthoryear{Gordon}{Gordon}{2001}]{Gor00}
1904: {\sc Gordon, A.~D.} 2001.
1905: \newblock Notes on nominal calculi for security and mobility.
1906: \newblock In {\em Foundations of Security Analysis and Design, Tutorial
1907: Lectures}. Lecture Notes in Computer Science, vol. 2171. Springer, 262--330.
1908:
1909: \bibitem[\protect\citeauthoryear{Kesten, Maler, Marcus, Pnueli, and
1910: Shahar}{Kesten et~al\mbox{.}}{2001}]{Pnueli}
1911: {\sc Kesten, Y.}, {\sc Maler, O.}, {\sc Marcus, M.}, {\sc Pnueli, A.}, {\sc
1912: and} {\sc Shahar, E.} 2001.
1913: \newblock Symbolic model checking with rich assertional languages.
1914: \newblock {\em Theoretical Computer Science\/}~{\em 256,\/}~1, 93--112.
1915:
1916: \bibitem[\protect\citeauthoryear{Schnoebelen}{Schnoebelen}{2002}]{Sch02}
1917: {\sc Schnoebelen, P.} 2002.
1918: \newblock {Verifying Lossy Channel Systems has Nonprimitive Recursive
1919: Complexity}.
1920: \newblock {\em {Information Processing Letters}\/}~{\em 83,\/}~5, 251--261.
1921:
1922: \end{thebibliography}
1923:
1924: \appendix
1925: \section{Symbolic Predecessor Operator}
1926: \label{PreOp}
1927: Given a set of MSR$_{NC}$ configurations $S$, consider the
1928: MSR$_{NC}$ {\em predecessor} operator
1929: $Pre(S)=\{\calM|\calM\Rightarrow_{MSR}\calM',\calM'\in S\}$.
1930: In our assertional language, we can define a symbolic version
1931: $\bfPre_{NC}$ of $Pre$ defined on a set $\bfS$ containing
1932: MSR$_{NC}$ constrained multisets (with {\em disjoint} variables)
1933: as follows:
1934: $$
1935: \begin{array}{ll}
1936: \bfPre_{NC}(\bfS)=\{~(\calA\oplus\calN~:~\xi)~~|~~
1937: & (\calA\longrightarrow\calB : \psi)\in\calR,~~(\calM:\varphi)\in\bfS,\\
1938: & \calM'\preccurlyeq\calM,~~\calB'\preccurlyeq\calB,\\
1939: & (\calM':\varphi)~=_{\theta}~(\calB':\psi),~~\calN=\calM\ominus\calM',\\
1940: & \xi\equiv (\exists x_1.\ldots x_k.\theta)\\
1941: & \hbox{and}~x_1,\ldots, x_k~\hbox{are all variables not in}~\calA\oplus\calN\}.
1942: \end{array}
1943: $$
1944: where $=_{\theta}$ is a matching relation between constrained configurations
1945: that also takes in consideration the constraint satisfaction, namely
1946: $$
1947: (A_1~|~\ldots~|~A_n:\varphi)~=_{\theta}~(B_1~|~\ldots~|~B_m:\psi)
1948: $$
1949: provided $m=n$ and there exists a permutation
1950: $j_1,\ldots,j_n$ of $1,\ldots,n$ such that
1951: the constraint
1952: $\theta~=~\varphi\wedge\psi\wedge\bigwedge_{i=1}^n~A_i=B_{j_i}$
1953: is {\em satisfiable}; here $p(x_1,\ldots,x_r)=q(y_1,\ldots,y_s)$
1954: is an abbreviation for the constraints $x_1=y_1\wedge \ldots\wedge
1955: x_r=y_s$ if $p=q$ and $s=r$, $false$ otherwise.
1956:
1957: As proved in \cite{Del02},
1958: the symbolic operator $\bfPre_{NC}$ returns a set of MSR$_{NC}$
1959: constrained configurations and it is correct and complete with
1960: respect to $Pre$, i.e., $\den{\bfPre_{NC}(\bfS)}=Pre(\den{\bfS})$ for
1961: any $\bfS$.
1962: It is important to note the difference between $\bfPre_{NC}$ and a
1963: simple backward rewriting step.
1964:
1965: For instance, given the
1966: constrained configurations $M$ defined as $p(x,z)~|~f(y):~z>y$ and the rule
1967: $s(u,m)~|~r(t,v)\rightarrow p(u',m')~|~r(t',v')~:~u=t,m'=v,v'=v,u'=u,t'=t$
1968: (that simulates a rendez-vous ($u,t$ are channels) and value passing ($m'=v$)),
1969: the application of $\bfPre$ returns
1970: $s(u,m)~|~r(t,v)~|~f(y):~u=t,v>y$
1971: as well as $s(u,m)~|~r(t,v)~|~p(x,z)~|~f(y):~u=t,x>y$
1972: (the common multiset here is $\epsilon$).
1973: \end{document}
1974: