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$

$\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 = 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:

$\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:

What is the cost of doing one chaotic versus one parallel iteration? chaotic is $n$ times cheaper
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$ (iteration strategy), example: take some permutation of equations

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

$I,C_1,C_2,\ldots,C_n,\ldots,$ be vectors of values $(g^k_1,\ldots,g^k_n)$ 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

in general $C_1 \sqsubseteq L_1$ , generally $C_i \sqsubseteq L_i$
when selecting equations by fixed permutation $L_1 \sqsubseteq C_n$ , generally $L_i \sqsubseteq C_{ni}$

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 $p_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 equations in worklist
choose $i$ , find new $g_i$ , remove $i$ from worklist
if $g_i$ has changed, update it and add to worklist $j$ for $p_j$ successor of $p_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

Principles of Program Analysis, Chapter 6