1: %
2: % TODO : Verifier et CORRIGER si besoin la proposition sur les equivalences de notions d'acceleration
3: %
4: %
5: % A VOIR : definir les notations de lub et glb indicées par le treillis L = (A, \leq), puis dire qu'on drop les indices lorsque pas d'ambiguité ?
6: %
7:
8:
9: \section{Acceleration in Data Flow Analysis}
10: \label{sec:dataflowanalysis}
11:
12: This section is devoted to the notion of acceleration in the context of data-flow analysis. Acceleration techniques for (concrete) reachability set computations~\cite{Boigelot:1994:CAV, Boigelot:1997:SAS, Comon:1998:CAV, Finkel:2003:IC, Finkel:2002:FSTTCS, Leroux:2005:ATVA, Bardin:2005:ATVA} may be equivalently formulated in terms of control-flow path languages or control-flow graph unfoldings. We shall observe that this equivalence does not hold anymore when these notions are lifted to data-flow analysis. All results in this section can easily be derived from the definitions, and they are thus presented without proofs.
13:
14: \subsection{Lattices, words and graphs} %-------------------------------------------------------------------------------
15:
16: We respectively denote by $\Nat$ and $\Z$ the usual sets of nonnegative integers and integers. For any set $S$, we write $\pow{S}$ for the set of subsets of $S$. The \emph{identity} function over $S$ is written $\Id_{S}$, and shortly $\Id$ when the set $S$ is clear from the context.
17:
18: \medskip
19:
20: Recall that a \emph{complete lattice} is any partially ordered set $(A, \sqsubseteq)$ such that every subset $X \subseteq A$ has a \emph{least upper bound} $\bigsqcup X$ and a \emph{greatest lower bound} $\bigsqcap X$. The \emph{supremum} $\bigsqcup A$ and the \emph{infimum} $\bigsqcap A$ are respectively denoted by $\top$ and $\bot$. A function $f \in A \rightarrow A$ is \emph{monotonic}
21: %(resp. \emph{continuous})
22: if $f(x) \sqsubseteq f(y)$ for all $x \sqsubseteq y$ in $A$.
23: %(resp. if $f(\bigsqcup X) = \bigsqcup \, \{f(x) \st x \in X\}$ for every subset $X \subseteq A$).
24: Recall that from Knaster-Tarski's Fix-point Theorem, any monotonic function $f \in A \rightarrow A$ has a \emph{least fix-point} given by $\bigsqcap \, \{a \in A \st f(a) \sqsubseteq a\}$. For any monotonic function $f \in A \rightarrow A$, we denote by $f^*$ the monotonic function in $A \rightarrow A$ defined by $f^*(x) = \bigsqcap \, \{a \in A \st (x \sqcup f(a)) \sqsubseteq a\}$, in other words $f^*(x)$ is the least post-fix-point of $f$ greater than $x$.
25:
26: \smallskip
27:
28: For any complete lattice $(A, \sqsubseteq)$ and any set $S$, we also denote by $\sqsubseteq$ the partial order on $S \rightarrow A$ defined as the point-wise extension of $\sqsubseteq$, i.e. $f \sqsubseteq g$ iff $f(x) \sqsubseteq g(x)$ for all $x \in S$. The partially ordered set $(S \rightarrow A, \sqsubseteq)$ is also a complete lattice, with lub $\bigsqcup$ and glb $\bigsqcap$ satisfying $(\bigsqcup F)(s) = \bigsqcup \, \{f(s) \st f \in F\}$ and $(\bigsqcap F)(s) = \bigsqcap \, \{f(s) \st f \in F\}$ for any subset $F \subseteq S \rightarrow A$.
29: %
30: Given any integer $n \geq 0$, we denote by $A^n$ the set of $n$-tuples over $A$. We identify $A^n$ with the set $\{1, \ldots, n\} \rightarrow A$, and therefore $A^n$ equipped with the point-wise extension of $\sqsubseteq$ also forms a complete lattice.
31:
32: \medskip
33:
34: Let $\Sigma$ be an \emph{alphabet} (a finite set of \emph{letters}). We write $\Sigma^*$ for the set of all (finite) \emph{words} $l_0 \cdots l_n$ over $\Sigma$, and $\varepsilon$ denotes the empty word. Given any two words $x$ and $y$, we denote by $x \cdot y$ (shortly written $x y$) their \emph{concatenation}. A subset of $\Sigma^*$ is called a \emph{language}.
35:
36: \medskip
37:
38: A (directed) \emph{graph} is any pair $G = (V, \rightarrow)$ where $V$ is a set of \emph{vertices} and $\rightarrow$ is a binary relation over $V$. A pair $(v, v')$ in $\rightarrow$ is called an \emph{edge}. A (finite) \emph{path} in $G$ is any (non-empty) sequence $v_0, \ldots, v_k$ of vertices, also written $v_0 \rightarrow v_1 \cdots v_{k-1} \rightarrow v_k$, such that $v_{i-1} \rightarrow v_i$ for all $1 \leq i \leq k$. The nonnegative integer $k$ is called the \emph{length} of the path, and the vertices $v_0$ and $v_k$ are respectively called the \emph{source} and \emph{target} of the path. A \emph{cycle} on a vertex $v$ is any path of non-zero length with source and target equal to $v$. A cycle with no repeated vertices other than the source and the target is called \emph{elementary}. We write $\stackrel{*}{\rightarrow}$ for the reflexive-transitive closure of $\rightarrow$. A \emph{strongly connected component} (shortly \emph{SCC}) in $G$ is any equivalence class for the equivalence relation $\stackrel{*}{\leftrightarrow}$ on $V$ defined by: $v \stackrel{*}{\leftrightarrow} v'$ if $v \stackrel{*}{\rightarrow} v'$ and $v' \stackrel{*}{\rightarrow} v$. We say that an SCC is \emph{cyclic} when it contains a unique elementary cycle up to cyclic permutation.
39:
40:
41: \subsection{Programs and data-flow solutions} %-------------------------------------------------------------------------
42:
43: For the rest of this section, we consider a complete lattice $(A, \sqsubseteq)$. In our setting, a program will represent an instance (for some concrete program) of a data-flow analysis framework over $(A, \sqsubseteq)$. To simplify the presentation, we will consider programs given as unstructured collections of commands (this is not restrictive as control-flow may be expressed through variables).
44:
45: \medskip
46:
47: Formally, assume a finite set $\Var$ of \emph{variables}. A \emph{command} on $\Var$ is any tuple $\langle X_1, \ldots, X_n ; f ; X \rangle$, also written $X := f(X_1, \ldots, X_n)$, where $n \in \Nat$ is an \emph{arity}, $X_1, \ldots, X_n \in \Var$ are pairwise disjoint \emph{input variables}, $f \in A^n \rightarrow A$ is a monotonic \emph{transfer function}, and $X \in \Var$ is an \emph{output variable}. Intuitively, a command $X := f(X_1, \ldots, X_n)$ assigns variable $X$ to $f(X_1, \ldots, X_n)$ and lets all other variables untouched.
48: %
49: A \emph{valuation} on $\Var$ is any function $\rho$ in $\Var \rightarrow A$. The \emph{data-flow semantics} $\dbrkts{c}$ of any command $c = \langle X_1, \ldots, X_n ; f ; X \rangle$ on $\Var$ is the monotonic function in $(\Var \rightarrow A) \rightarrow (\Var \rightarrow A)$ defined by $\dbrkts{c}\!(\rho)(X) = f(\rho(X_1), \ldots, \rho(X_n))$ and $\dbrkts{c}\!(\rho)(Y) = \rho(Y)$ for all $Y \neq X$.
50:
51: \medskip
52:
53: A \emph{program} over $(A, \sqsubseteq)$ is any pair $\Prog = (\Var, C)$ where $\Var$ is a finite set of \emph{variables} and $C$ is a finite set of commands on $\Var$.
54:
55: \begin{example} \label{ex:program}
56: Consider the C-style source code given on the left-hand side below, that we want to analyse with the complete lattice $(\Int, \sqsubseteq)$ of intervals of $\Z$. The corresponding program $\ExaProg$ is depicted graphically on the right-hand side below.
57: \begin{center}
58: \begin{minipage}{4.75cm}
59: \begin{lstlisting}[language=C,frame=none]
60: x = 1;
61: while (x $\leq$ 100) {
62: if (x $\geq$ 50) x = x-3;
63: else x = x+2;
64: }
65: \end{lstlisting}
66: \end{minipage}%
67: \begin{minipage}{6.5cm}
68: \begin{picture}(70,40)(-35,-20)
69: %\put(-35,-20){\framebox(70,40){}}
70: \gasset{Nw=7,Nh=7}
71: \node(X1)(-30,15){$X_1$}
72: \node(X2)(0,15){$X_2$}
73: \node(X3)(0,-15){$X_3$}
74: \node(X4)(30,15){$X_5$}
75:
76: \node[Nmr=0.0](c0)(-30,0){$c_0$}
77: \node[Nmr=0.0](c1)(-15,15){$c_1$}
78: \node[Nmr=0.0](c2)(-15,0){$c_2$}
79: \node[Nmr=0.0](c3)(5,0){$c_3$}
80: \node[Nmr=0.0](c4)(20,0){$c_4$}
81: \node[Nmr=0.0](c5)(15,15){$c_5$}
82:
83: \drawedge(c0,X1){}
84: \drawedge(X1,c1){}
85: \drawedge(c1,X2){}
86: \drawedge[curvedepth=-2.0](X2,c2){}
87: \drawedge[curvedepth=-2.0](c2,X3){}
88: \drawedge[curvedepth=-2.0](X3,c3){}
89: \drawedge[curvedepth=-2.0](X3,c4){}
90: \drawedge[curvedepth=-2.0](c3,X2){}
91: \drawedge[curvedepth=-2.0](c4,X2){}
92: \drawedge(X2,c5){}
93: \drawedge(c5,X4){}
94: \end{picture}
95: \end{minipage}%
96: \end{center}
97: Formally, the set of variables of $\ExaProg$ is $\{X_1, X_2, X_3, X_5\}$, representing the value of the variable $x$ at program points 1, 2, 3 and 5. The set of commands of $\ExaProg$ is $\{c_0, c_1, c_2, c_3, c_4, c_5\}$, with:
98: $$
99: \begin{array}{rcl@{\qquad\quad}rcl}
100: c_0 & : \ & X_1 := \top & c_3 & : \ & X_2 := (X_3 \,\sqcap\, [50, +\infty]) - \{3\} \\
101: c_1 & : \ & X_2 := (\{0\} \,.\, X_1) + \{1\} & c_4 & : \ & X_2 := (X_3 \,\sqcap\, ]-\infty, 49]) + \{2\} \\
102: c_2 & : \ & X_3 := X_2 \,\sqcap\, ]-\infty, 100] & c_5 & : \ & X_5 := X_2 \,\sqcap\, [101, +\infty[
103: \end{array}
104: $$
105: \end{example}
106:
107: We will use language-theoretic terminology and notations for traces in a program. A \emph{trace} in $\Prog$ is any word $c_1 \cdots c_k$ over $C$. The empty word $\varepsilon$ denotes the empty trace and $C^*$ denotes the set of all traces in $\Prog$. The data-flow semantics is extended to traces in the obvious way: $\dbrkts{\varepsilon} = \Id$ and $\dbrkts{c \cdot \sigma} = \dbrkts{\sigma} \circ \dbrkts{c}$. Observe that $\dbrkts{\sigma \cdot \sigma'} = \dbrkts{\sigma'} \circ \dbrkts{\sigma}$ for every $\sigma, \sigma' \in C^*$. We also extend the data-flow semantics to sets of traces by $\dbrkts{L} = \bigsqcup_{\sigma \in L} \dbrkts{\sigma}$ for every $L \subseteq C^*$. Observe that $\dbrkts{L}$ is a monotonic function in $(\Var \rightarrow A) \rightarrow (\Var \rightarrow A)$, and moreover $\dbrkts{L_1 \cup L_2} = \dbrkts{L_1} \sqcup \dbrkts{L_2}$ for every $L_1, L_2 \subseteq C^*$.
108:
109: \medskip
110:
111: Given a program $\Prog = (\Var, C)$ over $(A, \sqsubseteq)$,
112: %the \emph{merge over all paths solution} (\emph{MOP-solution)} of $\Prog$, written $\mop{\Prog}$, and
113: the \emph{minimum fix-point solution} (\emph{MFP-solution)} of $\Prog$, written $\lst{\Prog}$, is the valuation defined as follows:
114: \begin{eqnarray*}
115: % \mop{\Prog} & \ = \ & \bigsqcup \ \left\{ \dbrkts{\sigma}\!(\bot) \st \sigma \in C^* \right\}\\
116: \lst{\Prog} & \ = \ & \bigsqcap \ \left\{ \rho \in \Var \rightarrow A \st \dbrkts{c}\!(\rho) \sqsubseteq \rho \mbox{ for all } c \in C \right\}
117: \end{eqnarray*}
118:
119: \begin{example} \label{ex:program-solutions}
120: % For this program, the MOP-solution and the MFP-solution are equal and given by the following valuation:
121: The MFP-solution of the program $\ExaProg$ from Example~\ref{ex:program} is the valuation:
122: $$
123: % \mop{\ExaProg} \ = \
124: \lst{\ExaProg} \ = \ \{X_1 \mapsto \top, \ X_2 \mapsto [1, 51], \ X_3 \mapsto [1, 51], \ X_5 \mapsto \bot\}
125: $$
126: \end{example}
127:
128: %A program $\Prog = (\Var, C)$ over $(A, \sqsubseteq)$ is called \emph{continuous} if the transfer function of every command $c \in C$ is continuous. If $\Prog$ is continuous then $\dbrkts{L}$ is continuous for every $L \subseteq C^*$ and therefore $\dbrkts{L_1 \cdot L_2} = \dbrkts{L_2} \circ \dbrkts{L_1}$ for every $L_1, L_2 \subseteq C^*$ (we only have $\dbrkts{L_1 \cdot L_2} \sqsubseteq \dbrkts{L_2} \circ \dbrkts{L_1}$ in general).
129: %
130: %The following proposition recalls well-known links between the MOP-solution, the MFP-solution and the ascending Kleene chain.
131: Recall that we denote by $\dbrkts{C}^*\!(\rho)$ the least post-fix-point of $\dbrkts{C}$ greater than $\rho$. Therefore it follows from the definitions that $\lst{\Prog} = \dbrkts{C}^*\!(\bot)$. In our framework, the \emph{merge over all paths solution} (\emph{MOP-solution)} may be defined as the valuation $\dbrkts{C^*}\!(\bot)$, and the following proposition recalls well-known links between the MOP-solution, the MFP-solution and the ascending Kleene chain.
132:
133: \begin{proposition} \label{prop:mop-mfp-and-kleene}
134: For any program $\Prog = (\Var, C)$ over a complete lattice $(A, \sqsubseteq)$, we have:
135: $$
136: % \mop{\Prog} \quad = \quad
137: \dbrkts{C^*}\!(\bot) \quad \sqsubseteq \quad \bigsqcup_{k \in \Nat} \ \dbrkts{C}^k\!(\bot) \quad \sqsubseteq \quad \dbrkts{C}^*\!(\bot) \quad = \quad \lst{\Prog}
138: $$
139: % and all these valuations are equal when $\Prog$ is continuous.
140: \end{proposition}
141:
142: \subsection{Accelerability and flattening} %----------------------------------------------------------------------------
143:
144: We now extend notions from accelerated symbolic verification to this data-flow analysis framework. Acceleration in symbolic verification was first introduced semantically, in the form of \emph{meta-transitions}~\cite{Boigelot:1994:CAV, Boigelot:1997:SAS}, which basically simulate the effect of taking a given control-flow loop arbitrarily many times. This leads us to the following proposition and definition.
145:
146: %\begin{lemma} \label{lemma:dbrkts-languages}
147: % Let $(\Var, C)$ denote a program over $(A, \sqsubseteq)$. For any language $L \subseteq C^*$, we have $\dbrkts{L^*} \sqsubseteq \dbrkts{L}^*$, and moreover $\dbrkts{L^*} = \dbrkts{L}^*$ if $\Prog$ is continuous.
148: %\end{lemma}
149:
150: \begin{proposition}
151: Let $\Prog = (\Var, C)$ denote a program over $(A, \sqsubseteq)$. For any languages $L_1, \ldots, L_k \subseteq C^*$, we have $(\dbrkts{L_k}^* \circ \cdots \circ \dbrkts{L_1}^*)(\bot) \ \sqsubseteq \ \lst{\Prog}$.
152: % \vspace{-5pt}
153: % $$
154: % \begin{array}[c]{ccccc}
155: % & & \mop{\Prog} & & \\
156: % \dbrkts{L_1^* \cdots L_k^*}\!(\bot) & \quad \sqsubseteq \quad & & \quad \sqsubseteq \quad & \lst{\Prog} \\
157: % & & (\dbrkts{L_k}^* \circ \cdots \circ \dbrkts{L_1}^*)(\bot) & & \\
158: % \end{array}
159: % $$
160: \end{proposition}
161:
162: \begin{definition}
163: A program $\Prog = (\Var, C)$ over a complete lattice $(A, \sqsubseteq)$ is called
164: % \begin{center}
165: % \begin{tabular}[c]{l}
166: % \emph{MOP-accelerable}\\
167: \emph{MFP-accelerable}
168: % \end{tabular}
169: % \qquad if \qquad
170: if
171: % $\begin{array}[c]{rcl}
172: % \mop{\Prog} & = & \dbrkts{\sigma_1^* \cdots \sigma_k^*}\!(\bot)\\
173: $\lst{\Prog} = (\dbrkts{\sigma_k}^* \circ \cdots \circ \dbrkts{\sigma_1}^*)(\bot)$
174: % \end{array}$
175: % \end{center}
176: for some words $\sigma_1, \ldots, \sigma_k \in C^*$.
177: \end{definition}
178: %\begin{remark}
179: % It follows from Lemma~\ref{lemma:dbrkts-languages} that MOP-accelerability and MFP-accelerability are equivalent notions for continuous programs.
180: %\end{remark}
181:
182: The following proposition shows that any program $\Prog$ for which the ascending Kleene chain stabilizes after finitely many steps is MFP-accelerable.
183: \begin{proposition}
184: Let $\Prog = (\Var, C)$ denote a program over $(A, \sqsubseteq)$. If we have $\dbrkts{C}^k\!(\bot) = \lst{\Prog}$ for some $k \in \Nat$, then $\Prog$ is MFP-accelerable.
185: \end{proposition}
186:
187: Acceleration in symbolic verification was later expressed syntactically, in terms of flat graph unfoldings. When lifted to data-flow analysis, this leads to a more general concept than accelerability,
188: %for continuous programs,
189: and we will show that these two notions coincide for ``concrete'' programs (as in symbolic verification). We say that a program $\Prog$ is \emph{single-input} if the arity of every command in $\Prog$ is at most $1$.
190:
191: \medskip
192:
193: Given a program $\Prog = (\Var, C)$ over $(A, \sqsubseteq)$, an \emph{unfolding} of $\Prog$ is any pair $(\Prog', \varren)$ where $\Prog' = (\Var', C')$ is a program and $\varren \in \Var' \rightarrow \Var$ is a variable \emph{renaming}, and such that $\langle \varren(X'_1), \ldots, \varren(X'_n) ; f ; \varren(X') \rangle$ is a command in $C$ for every command $\langle X'_1, \ldots, X'_n ; f ; X' \rangle$ in $C'$. The renaming $\varren$ induces a Galois surjection $(\Var' \rightarrow A, \sqsubseteq) \galois{\valren}{\backvalren} (\Var \rightarrow A, \sqsubseteq)$ where $\backvalren$ and $\valren$ are defined as expected by $\displaystyle \backvalren(\rho) = \rho \circ \kappa$ and $\displaystyle \valren(\rho')(X) = \bigsqcup_{\varren(X') = X} \rho'(X')$.
194:
195: \medskip
196:
197: We associate a bipartite graph to any program in a natural way: vertices are either variables or commands, and edges denote input and output variables of commands. Formally, given a program $\Prog = (\Var, C)$, the \emph{program graph} of $\Prog$ is the labeled graph $G_{\Prog}$ where $\Var \cup C$ is the set of vertices and with edges $(c, X)$ and $(X_i, c)$ for every command $c = \langle X_1, \ldots, X_n ; f ; X \rangle$ in $C$ and $1 \leq i \leq n$. We say that $\Prog$ is \emph{flat} if there is no SCC in $G_{\Prog}$ containing two distinct commands with the same output variable. A \emph{flattening} of $\Prog$ is any unfolding $(\Prog', \varren)$ of $\Prog$ such that $\Prog'$ is flat.
198:
199: \begin{example}
200: A flattening of the program $\ExaProg$ from Example~\ref{ex:program} is given below. Intuitively, this flattening represents a possible unrolling of the while-loop where the two branches of the inner conditional alternate.
201: \begin{center}
202: \begin{picture}(110,40)(-55,-20)
203: %\put(-55,-20){\framebox(110,40){}}
204: \gasset{Nw=7,Nh=7}
205: \node(X1)(-50,15){$X_1$}
206: \node(X2)(0,15){$X_2$}
207: \node(X'2)(0,-15){$X'_2$}
208: \node(X3)(-30,-15){$X_3$}
209: \node(X'3)(30,-15){$X'_3$}
210: \node(X2)(0,15){$X_2$}
211: \node(X4)(50,15){$X_5$}
212:
213: \node[Nmr=0.0](c0)(-50,0){$c_0$}
214: \node[Nmr=0.0](c1)(-25,15){$c_1$}
215: \node[Nmr=0.0](c2)(-20,0){$c_2$}
216: \node[Nmr=0.0](c4)(20,0){$c_4$}
217: \node[Nmr=0.0](c5)(25,15){$c_5$}
218: \node[Nmr=0.0](c'2)(15,-15){$c'_2$}
219: \node[Nmr=0.0](c3)(-15,-15){$c_3$}
220:
221: \drawedge(c0,X1){}
222: \drawedge(X1,c1){}
223: \drawedge(c1,X2){}
224: \drawedge[curvedepth=-2.0](X2,c2){}
225: \drawedge(c2,X3){}
226: \drawedge(X3,c3){}
227: \drawedge(c3,X'2){}
228: \drawedge(X'2,c'2){}
229: \drawedge(c'2,X'3){}
230: \drawedge(X'3,c4){}
231: \drawedge[curvedepth=-2.0](c4,X2){}
232: \drawedge(X2,c5){}
233: \drawedge(c5,X4){}
234: \end{picture}
235: \end{center}
236: \end{example}
237:
238: \begin{lemma} \label{lemma:fix-point-under-approximation}
239: Let $\Prog = (\Var, C)$ denote a program over $(A, \sqsubseteq)$. For any unfolding $(\Prog', \varren)$ of $\Prog$, with $\Prog' = (\Var', C')$, we have $\valren \circ \dbrkts{C'}^* \circ \backvalren \ \sqsubseteq \ \dbrkts{C}^*$.
240: \end{lemma}
241:
242: \begin{proposition}
243: Let $\Prog = (\Var, C)$ denote a program over $(A, \sqsubseteq)$. For any unfolding $(\Prog', \varren)$ of $\Prog$, we have $\valren(\lst{\Prog'}) \ \sqsubseteq \ \lst{\Prog}$.
244: % $\valren(\mop{\Prog'}) \ \sqsubseteq \ \valren(\lst{\Prog'}) \ \sqsubseteq \ \lst{\Prog}$, and moreover $\valren(\mop{\Prog'}) \ \sqsubseteq \ \mop{\Prog}$ if $\Prog$ is continuous or single-input.
245: \end{proposition}
246:
247: %It turns out that $\valren(\mop{\Prog'}) \not \sqsubseteq \mop{\Prog}$ in general, since valuations corresponding to different traces in a program $\Prog$ may be ``merged'' on some command of the unfolding $(\Prog', \varren)$ of $\Prog$.
248: %
249: \begin{definition}
250: A program $\Prog = (\Var, C)$ over a complete lattice $(A, \sqsubseteq)$ is called
251: % \begin{center}
252: % \begin{tabular}[c]{l}
253: % \emph{MOP-flattable}\\
254: \emph{MFP-flattable}
255: % \end{tabular}
256: % \qquad if \qquad
257: if
258: % $\begin{array}[c]{rcl}
259: % \mop{\Prog} & = & \valren(\mop{\Prog'})\\
260: $\lst{\Prog} = \valren(\lst{\Prog'})$
261: % \end{array}$
262: % \end{center}
263: for some flattening $(\Prog', \varren)$ of $\Prog$.
264: \end{definition}
265: %\begin{remark}
266: % It follows from Proposition~\ref{prop:mop-mfp-and-kleene} that MOP-flattability and MFP-flattability are equivalent notions for continuous programs.
267: %\end{remark}
268:
269: Observe that any flat program is trivially MFP-flattable.
270: The following proposition establishes
271: %several
272: links between accelerability and flattability. As a corollary to the proposition, we obtain that
273: %\{MOP,MFP\}-\{accelerability,flattability\}
274: MFP-accelerability and MFP-flattability
275: are
276: %all
277: equivalent for single-input
278: %continuous
279: programs.
280:
281: \begin{proposition}
282: The following relationships hold for programs over $(A, \sqsubseteq)$:
283: \begin{enumerate}
284: \item[$i)$] MFP-accelerability implies MFP-flattability.
285: \item[$ii)$] MFP-flattability implies MFP-accelerability for single-input programs.
286: % \item[$iii)$] MOP-accelerability and MOP-flattability are equivalent for single-input programs.
287: \end{enumerate}
288: \end{proposition}
289: \begin{proof}[Sketch]
290: To prove $i)$,
291: %and direction $\Rightarrow$ of $iii)$,
292: we use the fact that for every words $\sigma_1, \ldots, \sigma_k \in C^*$, there exists a finite-state automaton $\Aut$ without nested cycles recognizing $\sigma_1^* \cdots \sigma_k^*$. The ``product'' of any program $\Prog$ with $\Aut$ yields a flattening that ``simulates'' the effect of $\sigma_1^* \cdots \sigma_k^*$ on $\Prog$. To prove $ii)$,
293: %and direction $\Leftarrow$ of $iii)$,
294: we observe that for any flat single-input program $\Prog$, each non-trivial SCC of $G_{\Prog}$ is cyclic. We pick a ``cyclic'' trace (which is unique up to circular permutation) for each SCC, and we arrange these traces to prove that $\Prog$ is accelerable. Backward preservation of accelerability under unfolding
295: %for single input programs
296: concludes the proof.
297: \qed
298: \end{proof}
299:
300: \begin{remark}
301: For any labeled transition system $\LTS$ with a set $S$ of states, the forward collecting semantics of $\LTS$ may naturally be given as a single-input
302: %continuous
303: program $\Prog_{\LTS}$ over $(\pow{S}, \subseteq)$. With respect to this translation (from $\LTS$ to $\Prog_{\LTS}$), the notion of flattability developped for accelerated symbolic verification of labeled transition systems coincide with the notions of MFP-accelerability and MFP-flattability defined above.
304: \end{remark}
305:
306: Recall that our main goal is to compute (exact)
307: MFP-solutions
308: %data-flow solutions (MOP or MFP)
309: using accele\-ration-based techniques. According to the previous propositions, flattening-based computation of the MFP-solution seems to be the most promising approach, and we will focus on this approach for the rest of the paper.
310: %, since (1) it is modular : we compute the MFP for each SCC and we can decide whether the fix-point is reached and we always stay below the target solution, and (2) the computation is guaranted to terminate for MFP-flattable programs.
311:
312: \subsection{Generic flattening-based constraint solving} %--------------------------------------------------------------
313:
314: It is well known that the MFP-solution of a program may also be expressed as the least solution of a constraint system, and we will use this formulation for the rest of the paper. We will use some new terminology to reflect this new formulation, however notations and definitions will remain the same. A command $\langle X_1, \ldots, X_n ; f ; X \rangle$ will now be called a \emph{constraint}, and will also be written $X \sqsupseteq f(X_1, \ldots, X_n)$. A program over $(A, \sqsubseteq)$ will now be called a \emph{constraint system} over $(A, \sqsubseteq)$, and the MFP-solution will be called the \emph{least solution}. Among all acceleration-based notions defined previously, we will only consider MFP-flattability for constraint systems, and hence we will shortly write \emph{flattable} instead of MFP-flattable.
315:
316: \medskip
317:
318: Given a constraint system $\CS = (\Var, C)$ over $(A, \sqsubseteq)$, any valuation $\rho \in \Var \rightarrow A$ such that $\rho \sqsubseteq \dbrkts{C}\!(\rho)$ (resp. $\rho \sqsupseteq \dbrkts{C}\!(\rho)$) is called a \emph{pre-solution} (resp. a \emph{post-solution}). A post-solution is also shortly called a \emph{solution}. Observe that the least solution $\lst{\CS}$ is the greatest lower bound of all solutions of $C$.
319:
320: \medskip
321:
322: We now present a generic flattening-based semi-algorithm for constraint solving. Intuitively, this semi-algorithm performs a propagation of constraints starting from the valuation $\bot$, but at each step we extract a flat ``subset'' of constraints (possibly by duplicating some variables) and we update the current valuation with the least solution of this flat ``subset'' of constraints.
323:
324: \medskip
325: \begin{lstlisting}[emph={Solve}]
326: Solve($\CS = (\Var, C)$ : a constraint system)
327: $\rho \leftarrow \bot$
328: while $\dbrkts{C}\!(\rho) \not\sqsubseteq \rho$
329: construct a flattening $(\Prog', \varren)$ of $\Prog$, where $\Prog' = (\Var', C')$
330: $\rho' \leftarrow \rho \circ \varren$
331: $\rho'' \leftarrow \dbrkts{C'}^*\!(\rho')$ $\hspace{27mm}$ { $\valren(\rho'') \sqsubseteq \dbrkts{C}^*\!(\rho)$ from Lemma $\mbox{\ref{lemma:fix-point-under-approximation}}$ }
332: $\rho \leftarrow \rho \sqcup \valren(\rho'')$
333: return $\rho$
334: \end{lstlisting}
335: \medskip
336:
337: The \textsf{Solve} semi-algorithm may be viewed as a generic template for applying acceleration-based techniques to constraint solving. The two main challenges are (1) the construction of a suitable flattening at line~4, and (2) the computation of the least solution for flat constraint systems (line~6). However, assuming that all involved operations are effective, this semi-algorithm is \emph{correct} (i.e. if it terminates then the returned valuation is the least solution of input constraint system), and it is \emph{complete} for flattable constraint systems (i.e. the input constraint system is flattable if and only if there exists choices of flattenings at line~4 such that the while-loop terminates).
338: %
339: We will show in the sequel how to instantiate the \textsf{Solve} semi-algorithm in order to obtain an efficient constraint solver for integers and intervals.
340:
341:
342:
343: %%%%% OLD TEXT THAT MIGHT STILL BE USEFUL %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
344:
345: %We denote by $S_1 \rightarrow S_2$ the set of functions from a set $S_1$ to a set $S_2$. If $f \in S_1 \rightarrow S_2$ and $g \in S_2 \rightarrow S_3$ are two functions, we respectively write $f ; g$ and $g \circ f$ for their forward and backward compositions ($(f ; g)(x) = (g \circ f)(x) = g(f(x))$.
346:
347: %Slightly abusing notations, we will sometimes simply write $\sigma$ instead of $\dbrkts{\sigma}$ when the meaning is clear from the context.
348:
349: %An \emph{initialized constraint system} is any pair $(C, \rho_0)$ where $C$ is a constraint system and $\rho_0$ is a valuation with finite support, i.e. such that $\rho_0(X) \neq \bot$ for at most finitely many $X$ in $\V$. To simplify the presentation, we will often identify an initialized constraint system $(C, \rho_0)$ with the constraint system $C' = C \cup \{X \sqsupseteq \rho_0(X) \st \rho_0(X) \neq \bot\}$. In particular, the least solution of $(C, \rho_0)$ is the least solution of $C$ greater than $\rho_0$.
350: