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  where 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.

Questions:

1. What is the cost of doing one chaotic versus one parallel iteration?
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 (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

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

• Principles of Program Analysis, Chapter 6