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 , then we are solving the system of eqautions in variables \[ \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 values 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 -th value, keeping the rest same: \[ \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} \] here we require that the new value differs from the old one . An iteration where at each step we select some equation (arbitrarily) is called chaotic iteration. It is abstract representation of different iteration strategies.
Questions:
- 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 (iteration strategy), example: take some permutation of equations
be vectors of values in parallel iteration and
be vectors of values in chaotic iteration
(starting from the same initial lattice value )
Compare values , , , , in the lattice
- in general
- when selecting equations by fixed permutation
Worklist Algorithm and Iteration Strategies
Observation: in practice depends only on small number of , namely predecessors of node
Consequence: if we chose , next time it suffices to look at successors of (saves traversing CFG)
This leads to a worklist algorithm:
- initialize lattice, put all equations in worklist
- choose , find new , remove from worklist
- if has changed, update it and add to worklist for successor of
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
References
- Principles of Program Analysis, Chapter 6