Every dataflow analysis you meet — reaching definitions, available expressions, live variables, constant propagation — looks like a different puzzle with its own gen/kill sets and its own initial values. But they are all secretly the same algorithm, and that algorithm rests on one piece of order theory: the lattice. Casting an analysis as "iterate a monotone function over a lattice until it stops changing" is what lets us answer, once and for all and for every analysis at once, three questions a working compiler writer cannot dodge: Does the iteration terminate? Is the answer it lands on the right one? And how precise is it compared to the truth?

This is the theory Gary Kildall laid down in 1973 and Kam & Ullman sharpened. It sits directly beneath the dataflow framework: the framework tells you how to set up gen/kill and meet; this page tells you why the setup is guaranteed to work.

Partial orders and meet-semilattices

The dataflow "facts" at a program point form a set L with an ordering \sqsubseteq that reads as "is at least as conservative as" (or "carries no more information than"). It is a partial order — reflexive, antisymmetric, transitive — partial because some facts are simply incomparable (neither x \sqsubseteq y nor y \sqsubseteq x). What makes it a meet-semilattice is that any two elements have a greatest lower bound, their meet x \wedge y — the operation that combines the facts arriving on different control-flow edges.

The workhorse example is the powerset lattice above: all subsets of a universe (here \{a,b,c\}), ordered by \subseteq (or its reverse), drawn as a Hasse diagram — an edge upward means "immediately above in the order". Two special elements anchor it:

Meet is idempotent, commutative and associative, and it induces the order: x \sqsubseteq y \iff x \wedge y = x. That single algebraic fact is the hinge the whole termination argument will swing on.

Transfer functions: monotone, and sometimes distributive

Each basic block acts on facts through a transfer function f_B : L \to L. Two properties of these functions decide everything:

Monotonicity says the function never inverts the order: feed it more information and you never get out less. It is a mild, almost always satisfiable condition — every gen/kill function f(x) = \mathit{gen} \cup (x \setminus \mathit{kill}) is monotone — and it is exactly what we need for the iteration to converge sensibly. Distributivity is strictly stronger: it says the function commutes with meet, so that merging paths and then transforming gives the same answer as transforming and then merging. Every bit-vector analysis (reaching defs, available expressions, liveness) is distributive; constant propagation is the famous analysis that is monotone but not distributive — and, as we will see, it pays a precision price for that.

Why the iteration terminates

The iterative solver starts every point at \top and repeatedly applies transfer functions and meets until nothing changes. Each such step can only move a value down the lattice (or leave it), producing a descending chain x_0 \sqsupseteq x_1 \sqsupseteq x_2 \sqsupseteq \cdots. If that chain can only descend finitely far, the process must stop. Two equivalent guarantees ensure it:

The height even bounds the cost: a value at any single point can change at most h times, so a round-robin solver over n points converges in O(n \cdot h) value-updates. For a powerset lattice over a universe of size k, h = k; for constant propagation, h = 3 per variable. Finite height is not a technicality — it is the entire reason a compiler can promise the optimiser will actually finish.

That the fixed point exists at all is Knaster–Tarski: a monotone function on a complete lattice has a complete lattice of fixed points, with a greatest and a least one. Iterating from \top converges to the greatest fixed point below your start — the MFP.

Iterating to a fixed point, in code

Concretely, "solve the analysis" means "find x with x = f(x) by iterating from \top". Below, a tiny powerset lattice over \{0,1,2,3\} (as a 4-bit set) and a monotone function that removes bit 3, keeps bit 0, and adds bit 1. We iterate from \top (all bits) and count the rounds until the value stops changing.

The value only ever loses or holds bits — a descending chain — so with a lattice of height 4 it must settle fast, and it does: after the first application it is already at the fixed point {0,1}, confirmed by a second round that changes nothing. Swap in any other monotone f and the same guarantee holds; write a non-monotone one (say, toggle a bit) and you can make it oscillate forever — which is precisely why monotonicity is not optional.

MFP versus MOP — how good is the answer?

There is an "ideal" solution against which to judge the iterative one. The Meet-Over-all-Paths (MOP) solution at a point p runs each path to p separately, composing that path's transfer functions, and then meets the results over all paths:

MOP is what you would ideally want — but it is generally uncomputable, because a loop creates infinitely many paths. The iterative MFP solution is the computable stand-in, and the relationship between them is the central theorem of dataflow analysis (Kam & Ullman, 1977):

In words: the iterative solution is always a safe approximation — at or below MOP in the lattice, i.e. never more optimistic than the truth — and it is exactly MOP when the framework is distributive. Because the MFP meets values early (at each merge, before applying the next transfer), while MOP meets late (only at the very end), a non-distributive f can lose precision: constant propagation's a{+}b-after-a-merge example is the canonical gap, where MFP reports NAC and MOP would have found a constant. The bit-vector analyses close the gap entirely, which is why they are so beloved: for them, the cheap computable answer is the ideal one.