Chaotic Iteration in Abstract Interpretation: How to compute the fixpoint?
In Abstract Interpretation Recipe, note that if the set of program points is , then we are solving the system of eqautions in variables
The approach given in Abstract Interpretation Recipe computes in iteration values by applying all equations in parallel to previous values:
What happens if we update values one-by-one? Say in one iteration we update -th value, keeping the rest same:
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.
- What is the cost of doing one chaotic versus one parallel iteration? (chaotic is 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 (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.
be vectors of values in parallel iteration and
be vectors of values in chaotic iteration
These two sequences are given by monotonic functions and and the second one is clearly smaller i.e.
Compare values , , …, , in the lattice:
- , generally (proof by induction)
- when selecting equations by fixed permutation , generally
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 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 CFG node indices into worklist
- choose , compute new , remove from worklist
- if has changed, update it and add to worklist all where is a 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
If we generate control-flow graph from our simple language, what do strongly connected components correspond to?
- Principles of Program Analysis Book, Chapter 6