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. | ||