LARA

Chaotic Iteration in Abstract Interpretation: How to compute the fixpoint?

In Abstract Interpretation Recipe, note that if the set of program points is $v_1,\ldots,v_n$, then we are solving the system of eqautions in $n$ variables $g_1,\ldots,g_n$

\begin{equation*} \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} \end{equation*}

where

\begin{equation*} H_i = Init_i \sqcup \bigsqcup_{(v_j,v_i) \in E} sp^{\#}(g_j,r(v_j,v_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:

\begin{equation*} \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} \end{equation*}

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} g^{k+1}_i = H_i(g^k_1,\ldots,g^k_n) \\ & \mbox{\bf chaotic iteration} \\ g^{k+1}_j = g^k_j, \mbox{ for } j \neq i \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.

Questions:

  1. What is the cost of doing one chaotic versus one parallel iteration? (chaotic is $n$ times cheaper)
  2. Does chaotic iteration converge if parallel converges?
  3. If it converges, will it converge to same value?
  4. If it converges, how many steps will convergence take?
  5. What is a good way of choosing index $i$ (iteration strategy), example: take some permutation of equations. More generally: fair strategy, for each vertex and each position in the sequence, there exists a position afterwards where this vertex is chosen.

$\bot,L_1,L_2,\ldots,L_n,\ldots,$ be vectors of values $(g^k_1,\ldots,g^k_n)$ in parallel iteration and

$\bot,C_1,C_2,\ldots,C_n,\ldots,$ be vectors of values $(g^k_1,\ldots,g^k_n)$ in chaotic iteration

These two sequences are given by monotonic functions $F^{\#}_C$ and $F^{\#}_L$ and the second one is clearly smaller i.e.

\begin{equation*} F^{\#}_C(g_1,\ldots,g_n) \sqsubseteq F^{\#}_L(g_1,\ldots,g_n) \end{equation*}

Compare values $L_1$, $C_1$, …, $I_n$, $C_n$ in the lattice:

  • $C_0 \sqsubseteq L_0$, generally $C_i \sqsubseteq L_i$ (proof by induction)
  • when selecting equations by fixed permutation $L_1 \sqsubseteq C_n$, generally $L_i \sqsubseteq C_{ni}$

Therefore, using the Lemma from Comparing Fixpoints of Sequences twice, we have that these two sequences converge to the same value.

Worklist Algorithm and Iteration Strategies

Observation: in practice $H_i(g_1,\ldots,g_n)$ depends only on small number of $g_j$, namely predecessors of node $v_i$.

Consequence: if we chose $i$, next time it suffices to look at successors of $i$ (saves traversing CFG).

This leads to a worklist algorithm:

  • initialize lattice, put all CFG node indices into worklist
  • choose $i$, compute new $g_i$, remove $i$ from worklist
  • if $g_i$ has changed, update it and add to worklist all $j$ where $v_j$ is a successor of $v_i$

Algorithm terminates when worklist is empty (no more changes).

Useful iteration strategy: reverse postorder and strongly connected components.

Reverse postorder: follow changes through successors in the graph.

Strongly connected component (SCC) of a directed graph: path between each two nodes of component.

  • compute until fixpoint within each SCC

If we generate control-flow graph from our simple language, what do strongly connected components correspond to?

References