Foundations of Dataflow Analysis

Global constant propagation algorithm

Consider the following example:

d0: y = 3
d1: x = y + 4
d2: y = 11
d3: if e ...

Consider an alternate representation of constant information using sets where all variables are tracked simultaneously. This representation can provide both better precision and better efficiency, than running the single-variable implementation multiple times.

There are two options for the transfer function for d1: either use the in value to determine that x is a constant too, or simply represent the transfer function as a GEN/KILL set (as a function of the statement, but independent of the input value).

This representation allows transfer functions to be written using generate (Gen[s]) and propagate (in[s] - Kill[s]) definitions.

Can summarize a basic block through its own composite transfer function as follows:

• Gen[d0] = (y,3), Kill[d0] = (y,*), out[d0] = (in[d0] - Kill[d0]) U Gen[d0]
• Gen[d1] = empty, Kill[d1] = (x,*), out[d1] = (in[d1] - Kill[d1]) U Gen[d1]
• Gen[d2] = (y,11), Kill[d2] = (y,*), out[d2] = (in[d2] - Kill[d2]) U Gen[d2]
• ...

Gen[B]: locally exposed constant definitions, definitions available at the end of the basic block B

Kill[B]: the set of constant definitions killed by B

Effects of edges: nodes with multiple predecessor: meet operator is Intersection: in[b] = out[p1] n out[p2] ... n out[pn], for p1..pn predecessors of b

Cyclic graphs: equations still hold:

• out[b] = fb(in[b])
• in[b] = Intersection over out[pi] for preds pi of b

input: control flow graph CFG = (N, E, Entry, Exit)

//Boundary condition
OUT[Entry] = empty set

//Initialization for iterative algorithm
For each basic block B other than Entry
  OUT[B] = {(x,\Top) for all x}

//Iterate
While (changes to any OUT occur) {
    For each basic block B other than Entry {
      in[B] = intersection over (out[p]), for all preds p of B
      out[B] = fB(in[B]) //out[B] = gen[B] u (in[B] - kill[B])
    }
}

Summary of reaching definitions

	Reaching Definitions
Domain	Sets of constant definitions
Transfer function fb(x)	forward: out[b] = fb(in[b]) out[b] = Gen[b] U (x - Kill[b])
Meet operation	in[b] = n out[predecessors] intersection
Boundary condition	out[entry] = empty
Initial interior points	out[b] = {(x,\top): for all variables x}

Live Variable analysis

• Direction: backward: in[b] = fb(out[b])
• Transfer function for statement s: x = y + z
  • generate live variables: Use[s] = {y, z}
  • propagate live variables: out[s] - Def[s], Def[s] = x
  • in[s] = Use[s] U (out[s] - Def[s])
• Transfer function for basic block B:
  • in[b] = Use[b] U (out[b] - Def[B])
  • Use[b] : set of locally exposed uses in B, i.e., uses not covered by definitions in B
  • Def[b] = set of variables defined in B.
• Meet operator: intersection: out[B] = in[s1] U in[s2] ... U in[sn], for successors s1, .., sn of B
• Boundary condition: in[exit] = empty (or return value as the case might be)

Liveness : Iterative algorithm

input: control flow graph CFG = (N, E, Entry, Exit)

//Boundary condition
In[Exit] = empty

//Initialization for iterative algorithm
For each basic block B other than Exit
    In[B] = empty

//Iterate
While (changes to any IN occur) {
  For each basic block B other than Exit {
    out[B] = U (in[s]) for all successors s of B
    in[B] = fB(out[B]) //in[B]=Use[B] U (out[B] - Def[B])
  }
}

Framework

	Reaching Definitions	Live variables
Domain	Sets of constant definitions	Sets of variables
Direction and Transfer function fb(x)	forward: out[b] = fb(in[b]) out[b] = Gen[b] U (x - Kill[b]) in[b] = n out[predecessors]	backward: in[B] = fb(out[B]) in[b] = Use[b] U (x - Def[b]) out[B] = U in[succ[B]]
Meet operation	intersection	union
Boundary condition	out[entry] = empty	in[exit] = empty
Initial interior points	out[b] = {(x,\top): for all variables x}	in[b] = empty

Exercise: must-reach definitions

• A definition D(a = b+c) must reach point P iff
  • D appears at least once along all paths leading to P
  • a is not redefined along any path after last appearance of D and before P

Exercise: reaching definitions

• A definition D(a = b+c) reaches point P if there exists a path from the point immediately following D to P, such that D is not killed (overwritten) along that path.

Would the following be a legal solution to reaching definitions?

Entry --> BB1

BB1 --> BB2

BB2 --> BB2

BB2 --> BB3

BB3 contains (d1: b = 1) definition

BB3 --> exit

in[BB1] = empty
out[BB1] = empty
in[BB2] = {d1}
out[BB2] = {d1}
in[BB3] = {d1}
out[BB3] = {d1}
in[exit] = {d1}

Answer: this is a legal fixed-point solution to the system of equations. However this is not a maximum fixed-point (later).

Framework

1. Prove properties of entire family of problems once and for all, e.g., will the program converge? what do the solution to the set of equations mean? how do we ensure the best solution?
2. Aid in software engineering: re-use code

Data-flow problems (F, V, ^) are defined by

• A semilattice
  • domain of values (V)
  • meet operator (^)
• A family of transfer functions (F: V --> F)

• A semi-lattice S = < a set of values V, a meet operator ^ >
• Properties of the meet operator
  • idempotent: x ^ x = x
  • commutative: x ^ y = y ^ x
  • associative: x ^ (y ^ z) = (x ^ y) ^ z
• Examples of meet operators: set-union, set-intersection, and, or, max, min
• Non-examples: add, subtract, multiply, ...

Example of a semi-lattice diagram: V = { x | x is a subset of {d1,d2,d3}}, ^ = set-union

Draw the semi-lattice with arrows pointing downwards (>= relation)

Some interesting properties

• x^y is the first common descendant of x and y
• Define top element \Top such that x ^ \Top = x
• Define bottom element \Bottom such that x ^ \Bottom = \Bottom
• Semi-lattice diagram: picture of a partial order

A meet-operator defines a partial-order and vice-versa

• Definition of partial order ≤: x ≤ y if and only if x^y = x
• In the diagram, x ≤ y indicates that there is path from y to x, and vice versa
• Properties of meet operator guarantee that ≤ is a partial order
  • Reflexive: x ≤ x
  • Antisymmetric: if x≤y and y≤x then x=y
  • Transitive: if x ≤ y and y ≤ z then x ≤ z
• x < y is equivalent to ((x ≤ y) and !(x == y))
• A semi-lattice diagram:
  • Set of nodes: set of values
  • Set of edges: {(y,x): x<y and \not\existsz s.t. (x<z)^(z<y)}
• Example: meet operator = \union, partial order ≤ is ?
• Another example: meet operator = \intersection, partial order ≤ is ? Draw semilattice diagram for this

Summary:

• Three ways to define a semi-lattice:
  • Set of values + meet operator
    • idempotent: x ^ x = x
    • commutative: x ^ y = y ^ x
    • associative: x ^ (y ^ z) = (x ^ y) ^ z
  • Set of values + partial order
    • Reflexive: x ≤ x
    • Antisymmetric: if x ≤ y and y ≤ x then x = y
    • Transitive: if x ≤ y and y ≤ z then x ≤ z
  • A semi-lattice diagram
    • No cycles
    • \Top is on top of everything
    • \Bottom is at the bottom of everything.
    • \Top or \Bottom may not necessarily exist; e.g., if domain is integers, and meet operator is Max, then bottom is \infinity.

Another example: semi-lattice with V = {x | such that x is a subset of {d1, d2, d3}}, ^ = \intersection

One element at a time

• A semi-lattice for data flow problems can get quite large; 2^n elements for n var/definitions, for example
• A useful technique
  • define semi-lattice for 1 element
  • product of semi-lattices for all elements
• Example: union of definitions
  • For each element d1, lattice is : {} --> {d1}
  • Similarly, for d2, lattice is : {} --> {d2}
  • Product lattice is: {} --> {d1}, {} --> {d2}, {d1} --> {d1, d2}, {d2} --> {d1, d2}.
• Defining product of lattices: <x1,x2> ≤ <y1,y2> iff x1≤y1 and x2≤y2

Descending chain

• Definition: The height of a lattice is the largest number of > relations that will fit in a descending chain:

  x0 > x1 > x2 > ... > ...
  

• Height of lattice in reaching definitions? Number of definitions
• Height of lattice in live variables? Number of variables
• Important property for the algorithm to work: finite descending chains
  • if V=integers, and ^=min, then height = \infinity
  • Note that it is not necessary for an infinite semi-lattice to have infinite height. example? constant propagation over integers

Transfer functions

• A family of transfer functions F
• Basic properties f: V --> V
  • Has an identity function, i.e., \Exists f such that f(x) = x for all x.
  • Closed under composition, i.e., if f1,f2 \in F, then f1.f2 \in F.

Monotonicity

• A framework (F, V, ^) is monotone iff x ≤ y implies f(x) ≤ f(y)
• Equivalently, a framework (F, V, ^) is monotone iff
  • f(x^y) ≤ f(x)^f(y)
  • (meet inputs, then apply f) ≤ (apply f individually to inputs, then meet results)

Example: reaching definitions: f(x) = Gen \union (x - Kill), ^ = \union

• Definition 1: Let x1 ≤ x2 (x1 is a superset of x2); f(x1): Gen \Union (x1 - Kill); f(x2): Gen \Union (x2 - Kill)
• Clearly, f(x1) ≤ f(x2) (because f(x1) is a superset of f(x2))

• Definition 2:
  • f(x1^x2) = Gen \union ((x1 \union x2) - Kill)
  • f(x1)^f(x2) = (Gen \union (x1 - Kill)) \Union (Gen \Union (x2 - Kill))
  • (x1 \union x2) - Kill = (x1 - Kill) \union (x2 - Kill)
  • hence monotone; actually distributive, because f(x1^x2)=f(x1)^f(x2)

Important: monotone framework does not mean that f(x) ≤ x.

• e.g., reaching definition for two definitions in a program, d1 and d2. Suppose f: Gen = {d1}; Kill = {d2}; f({}) = {d1} which is not ≤ {}.
• x: {} ≥ {d1} ≥ {d1,d2}; f(x): {d1} ≥ {d1} ≥ {d1}.
• No relationship between f(x) and x!

Distributivity: A framework (F, V, ^) is distributive if and only if:

• f(x^y) = f(x)^f(y)

Distributivity implies monotonicity, but not vice-versa.

Example: the framework for constant propagation is not distributive: example: if (...) { x = 2; y = 3; } else { x = 3; y = 2; }; z = x + y; f(x)^f(y) = 5; f(x^y) = \Bottom.

Properties of Iterative Algorithm

• Given:
  • ^ and monotone data flow framework
  • finite descending chain
  • THEN converges!
• Initialization of interior points to \Top.
  • yields Maximum Fixed Point (MFP) solution of equations.

Behaviour of iterative algorithm (intuitively): For each IN/OUT of an interior program point:

• It's value cannot go up (new value < old value) during algorithm.
• Start with \Top (largest value)
• Proof by induction:
  • Apply first transfer function / meet operator ≤ old value (\Top)
  • Inputs to meet changes (get smaller), reapply
    • since input gets smaller, new output ≤ old output
  • Inputs to transfer function changes (get smaller), reapply
    • because of monotonicity of transfer function: since input gets smaller, new output ≤ old output
• Values do not come down unless some constraints drive them down (ensures "maximum")
• Algorithm iterates until equations are satisfied.
• Therefore, finds the largest solution that satisfies the equations.

What does the solution mean?

• Let f1, .., fm: \in F, fi is the transfer function for node i
• For a path p, fp = fn.f(n-1)...(f1), if p is a path through nodes n1,..,nk
• For an empty path p, fp = identity function
• For each node n: ^fp (boundary value) for all possibly executed paths p reaching n.
• example: if (sqr(y) ≥ 0) { x = 0; } else { x = 1; }. Here, the ideal solution is that x = 0 at the end of this program.
• However, determining all possibly executed paths is undecidable.

Meet over paths MOP solution:

• Err in the conservative direction
• Meet over paths MOP (over all paths, not just executed paths):
  • Assume every edge is traversed
  • For each node n: MOP(n) = ^ f(p) for all paths p reaching n
• Compare MOP with IDEAL
  • MOP includes more paths than IDEAL
  • MOP = IDEAL ^ Result(unexecuted paths)
  • MOP ≤ IDEAL
  • MOP is a "smaller" solution, more conservative, safe
• Data flow solution ≤ MOP ≤ IDEAL
  • because we don't just meet at the end, we meet all the time.
  • as close to MOP from below as possible.

What is the difference between MOP and MFP of data flow equations? Consider two paths F1.F3 and F2.F3. MOP = F3F1(x) ^ F3F2(x). MFP (through iterative algo) = F3(F1(x) ^ F2(x)). Therefore

• any FP ≤ MFP ≤ MOP ≤ IDEAL
• FP, MFP, MOP are safe
• If framework is distributive, FP ≤ MFP = MOP ≤ IDEAL