DFA-Foundation

Iterative Algorithm

Here is a classic iterative algorithm template for May & Forward analysis

Let’s view it in another way

Given a CFG with k nodes, the iterative algorithm updates OUT[n] for every node n in each iteration.
Assume the domain of the values in data flow analysis is V, let’s define a k-tuple: (OUT[n1], OUT[n2], …, OUT[nk]) as an element of set (V1 × V2 … × Vk) denoted as Vk, to hold the values of the analysis after each iteration.
Each iteration can be considered as taking an action to map an element of Vk to a new element of Vk, through applying the transfer functions and control-flow handing, abstracted as a function F: Vk → Vk
Then the algorithm outputs a series of k-tuples iteratively until a k-tuple is the same as the last one in two consecutive iterations.

X is a fixed point of function F if X = F(X)

We say the iterative algorithm reaches a fixed point.

Partial Order

poset

Some examples of poset:

(S, ≤) , S is a set of integers
(S, substring) , S is a set of English words
(S, subset) , S is the power set of set {a,b,c}

upper & lower bounds

Lattice

Some examples of lattice:

(S, ≤) , S is a set of integers
- ⊔ means “max”
- ⊓ means “min”
(S, subset) , S is the power set of set {a,b,c}
- ⊔ means ∪
- ⊓ means ∩

Semilattice

Complete Lattice

Some examples of complete lattice:

(S, ≤) , S is a set of integers
- × not a complete lattice
- it has no ⊔S（+∞）
(S, subset) , S is the power set of set {a,b,c}
- √

Note: the definition of bounds implies that the bounds are not necessarily in the subsets (but they must be in the lattice)

A complete lattice is not necessarily a finite lattice!

Product Lattice

DFA Framework via Lattice

Data flow analysis can be seen as iteratively applying transfer functions and meet/join operations on the values of a lattice

Monotonicity

Fixed Point Theorem

Proof：

Relate to Iterative Algorithm

two conditions of fixed point theorem:

L is finite
f is monotonic

If a product lattice Lk is a product of complete(and finite) lattices, i.e., (L, L, …, L), then Lk is also complete (and finite) =》 L is a finite and complete lattice

In each iteration, it is equivalent to think that we apply function F which consists of

transfer function fi: L → L for every node
join/meet function ⊔/⊓: L×L×L... → L

for control-flow confluence

How to prove function F is monotonic?

first, transfer function is obviously monotonic(Gen/Kill function is monotonic, IN/OUT never shrinks)

next, prove that ⊔/⊓ is monotonic

When will the algorithm reach the fixed point?

To sum up, we can draw these conclusions:

the iterative algorithm is guaranteed to terminate（reach the fixed point）
There may be more than one solution, but our solution is the best one（least/greatest fixed point）
Worst case of iterations: lattice height × nodes num in CFG