LARA

This is an old revision of the document!

Chaotic Iteration in Abstract Interpretation

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{array}{l} 

  g_1 = H_1(g_1,\ldots,g_n) \\
  \ldots \\
  g_i = H_i(g_1,\ldots,g_n) \\
  \ldots \\
  g_n = H_n(g_1,\ldots,g_n) \\

\end{array} \] where \[ 

 H_i = g_i \sqcup \bigsqcup_{(p_j,p_i) \in E} sp^{\#}(g_j,r(p_j,p_i))

\] 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{array}{ll} 

  g^{k+1}_1 = H_1(g^k_1,\ldots,g^k_n) \\
  \ldots \\
  g^{k+1}_i = H_i(g^k_1,\ldots,g^k_n) & \mbox{\bf parallel iteration} \\
  \ldots \\
  g^{k+1}_n = H_n(g^k_1,\ldots,g^k_n) \\

\end{array} \]

What happens if we update values one-by-one? Say in one iteration we update $i$-th value, keeping the rest same: \[ \begin{array}{ll} 

  g^{k+1}_i = H_i(g^k_1,\ldots,g^k_n)  \\
  g^{k+1}_j = g^k_j, \mbox{ for } j \neq i  & \mbox{\bf chaotic iteration}

\end{array} \] here we require that the new value $H_i(g^k_1,\ldots,g^k_n)$ differs from the old one $g^k_i$, otherwise we select a different one. Then we pick a different $i$, as long as the result changes. This is chaotic iteration.

Questions:

  • What is the cost of doing one chaotic versus one parallel iteration?
  • Does chaotic iteration converge if parallel converges?
  • If it converges, will it converge to same value?
  • If it converges, how many steps will convergence take?
  • What is a good way of choosing index $i$?

Let $\vec I,L_1,L_2,\ldots$ be vector of values $(g_1,\ldots,g_n)$ in parallel iteration and $I,C_1,C_2,\ldots$ be vector of values in chaotic iteration, starting from the same initial lattice value $I$.

Compare values $I$, $L_1$, $C_1$, $I_n$, $C_n$ in the lattice.

References

  • Principles of Program Analysis, Chapter 6