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) \\ 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 differs from the old one
, otherwise we select a different one.
Then we pick a different
, as long as the result changes. This is chaotic iteration.
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