Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:chaotic_iteration_in_abstract_interpretation [2008/05/20 18:50] vkuncak |
sav08:chaotic_iteration_in_abstract_interpretation [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Chaotic Iteration in Abstract Interpretation ====== | + | ====== Chaotic Iteration in Abstract Interpretation: How to compute the fixpoint? ====== |
In [[Abstract Interpretation Recipe]], note that if the set of program points is $p'_1,\ldots,p'_n$, then we are solving the system of eqautions in $n$ variables $g_1,\ldots,g_n$ | In [[Abstract Interpretation Recipe]], note that if the set of program points is $p'_1,\ldots,p'_n$, then we are solving the system of eqautions in $n$ variables $g_1,\ldots,g_n$ | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
g_1 = H_1(g_1,\ldots,g_n) \\ | g_1 = H_1(g_1,\ldots,g_n) \\ | ||
Line 10: | Line 10: | ||
g_n = H_n(g_1,\ldots,g_n) \\ | g_n = H_n(g_1,\ldots,g_n) \\ | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
where | where | ||
- | \[ | + | \begin{equation*} |
H_i = g_i \sqcup \bigsqcup_{(p_j,p_i) \in E} sp^{\#}(g_j,r(p_j,p_i)) | H_i = g_i \sqcup \bigsqcup_{(p_j,p_i) \in E} sp^{\#}(g_j,r(p_j,p_i)) | ||
- | \] | + | \end{equation*} |
The approach given in [[Abstract Interpretation Recipe]] computes in iteration $k$ values $g^k_i$ by applying all equations in parallel to previous values: | The approach given in [[Abstract Interpretation Recipe]] computes in iteration $k$ values $g^k_i$ by applying all equations in parallel to previous values: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{ll} | \begin{array}{ll} | ||
g^{k+1}_1 = H_1(g^k_1,\ldots,g^k_n) \\ | g^{k+1}_1 = H_1(g^k_1,\ldots,g^k_n) \\ | ||
Line 24: | Line 24: | ||
g^{k+1}_n = H_n(g^k_1,\ldots,g^k_n) \\ | g^{k+1}_n = H_n(g^k_1,\ldots,g^k_n) \\ | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
What happens if we update values one-by-one? Say in one iteration we update $i$-th value, keeping the rest same: | What happens if we update values one-by-one? Say in one iteration we update $i$-th value, keeping the rest same: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{ll} | \begin{array}{ll} | ||
g^{k+1}_i = H_i(g^k_1,\ldots,g^k_n) \\ | g^{k+1}_i = H_i(g^k_1,\ldots,g^k_n) \\ | ||
Line 33: | Line 33: | ||
g^{k+1}_j = g^k_j, \mbox{ for } j \neq i | g^{k+1}_j = g^k_j, \mbox{ for } j \neq i | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
here we require that the new value $H_i(g^k_1,\ldots,g^k_n)$ differs from the old one $g^k_i$. An iteration where at each step we select some equation $i$ (arbitrarily) is called //chaotic iteration//. It is abstract representation of different iteration strategies. | here we require that the new value $H_i(g^k_1,\ldots,g^k_n)$ differs from the old one $g^k_i$. An iteration where at each step we select some equation $i$ (arbitrarily) is called //chaotic iteration//. It is abstract representation of different iteration strategies. | ||