• English only

# Differences

This shows you the differences between two versions of the page.

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.