Foundations of Data-Flow Analysis
Introduction: Having shown several useful examples of the data-flow abstraction, we now study the family of data-flow schemas as a whole, abstractly. We shall answer several basic questions about data-flow algorithms formally:
1. Under what circumstances is the iterative algorithm used in data-flow analysis correct?
2. How precise is the solution obtained by the iterative algorithm?
3. Will the iterative algorithm converge?
4. What is the meaning of the solution to the equations?
In Section 9.2, we addressed each of the questions above informally when describing the reaching-definitions problem. Instead of answering the same questions for each subsequent problem from scratch, we relied on analogies with the problems we had already discussed to explain the new problems. Here we present a general approach that answers all these questions, once and for all, rigorously, and for a large family of data-flow problems. We first identify the properties desired of data-flow schemas and prove the implications of these properties on the correctness, precision, and convergence of the data-flow algorithm, as well as the meaning of the solution. Thus, to understand old algorithms or formulate new ones, we simply show that the proposed data-flow problem definitions have certain properties, and the answers to all the above difficult questions are available immediately.
The concept of having a common theoretical framework for a class of schemas also has practical implications. The framework helps us identify the reusable components of the algorithm in our software design. Not only is coding effort reduced, but programming errors are reduced by not having to recode similar details several times.
A data-flow analysis framework (D,V,A:F) consists of
1. A direction of the data flow D, which is either FORWARDS or BACKWARDS.
2. A semilattice (see Section 9.3.1 for the definition), which includes a domain of values V and a meet operator A.
3. A family F of transfer functions from V to V. This family must include functions suitable for the boundary conditions, which are constant transfer functions for the special nodes ENTRY and EXIT in any flow graph.
Semilattices: A semilattice is a set V and a binary meet operator A such that for all x, y,and z in V:
1. x A x — x (meet is idempotent).
2. x Ay = y A x (meet is commutative).
3. x A (y A z) = (x A y) A z (meet is associative).
A semilattice has a top element, denoted T, such that
for all x in V, T A x — x.
Optionally, a semilattice may have a bottom element, denoted ±, such that
for all x in V, _L A x = ±.
Partial Orders: As we shall see, the meet operator of a semilattice defines a partial order onthe values of the domain. A relation < is a partial order on a set V if for all x,y, and z in V:
1. x < x (the partial order is reflexive).
2. If x < y and y < x, then x = y (the partial order is antisymmetric).
3. If x < y and y < z, then x < z (the partial order is transitive).
The pair (V, <) is called a poset, or partially ordered set. It is also convenient to have a < relation for a poset, defined as
x < y if and only if (x < y) and (x / y).
The Partial Order for a Semilattice: It is useful to define a partial order < for a semilattice (V, A). For all x and y in V, we define
x < y if and only if x A y = x.
Because the meet operator A is idempotent, commutative, and associative, the < order as defined is reflexive, antisymmetric, and transitive. To see why, observe that:
- Reflexivity: for all x, x < x. The proof is that x A x = x since meet is idempotent.
- Antisymmetry: if x < y and y < x, then x — y. In proof, x < y means x Ay = x and y < x means y A x = y. By commutativity of A, x = (x Ay) = (y Ax) = y.
- Transitivity: if x < y and y < z, then x < z. In proof, x < y and y < z means that x A y = x and y A z - y. Then (x A z) = ((x A y) A z) = (x A (y A z)) = (x A y) = x, using associativity of meet. Since x A z = x has been shown, we have x < z, proving transitivity.