The Iterative Algorithm for General Frameworks
Introduction: We can generalize Algorithm 9.11 to make it work for a large variety of data-flow problems.
Algorithm: Iterative solution to general data-flow frameworks.
INPUT: A data-flow framework with the following components:
1. A data-flow graph, with specially labeled ENTRY and EXIT nodes,
2. A direction of the data-flow D,
3. A set of values V,
4. A meet operator A,
5. A set of functions F, where fs in F is the transfer function for block B, and
6. A constant value GENTRY or f EXIT in V, representing the boundary condition for forward and backward frameworks, respectively.
OUTPUT: Values in V for IN[B] and OUT[B] for each block B in the data-flow graph.
METHOD: The algorithms for solving forward and backward data-flow problems are shown in Fig. 9.23(a) and 9.23(b), respectively. As with the familiar iterative data-flow algorithms from Section 9.2, we compute IN and O U T for each block by successive approximation.
It is possible to write the forward and backward versions of Algorithm 9.25 so that a function implementing the meet operation is a parameter, as is a function that implements the transfer function for each block. The flow graph itself and the boundary value are also parameters. In this way, the compiler implementor can avoid recoding the basic iterative algorithm for each data-flow framework used by the optimization phase of the compiler.
We can use the abstract framework discussed so far to prove a number of useful properties of the iterative algorithm:
1. If Algorithm 9.25 converges, the result is a solution to the data-flow equations.
2. If the framework is monotone, then the solution found is the maximum fixedpoint (MFP) of the data-flow equations. A maximum fixedpoint is a solution with the property that in any other solution, the values of IN[B] and O U T [B] are < the corresponding values of the MFP.
3. If the semilattice of the framework is monotone and of finite height, then the algorithm is guaranteed to converge.
We shall argue these points assuming that the framework is forward. The case of backwards frameworks is essentially the same. The first property is easy to show. If the equations are not satisfied by the time the while-loop ends, then there will be at least one change to an OUT (in the forward case) or IN (in the backward case), and we must go around the loop again.
To prove the second property, we first show that the values taken on by IN[5] and OUT[P] for any B can only decrease (in the sense of the < relationship for lattices) as the algorithm iterates. This claim can be proven by induction.
BASIS: The base case is to show that the value of IN[B] and OUT[B] after the first iteration is not greater than the initialized value. This statement is trivial because m[B] and OUT[P] for all blocks B ^ ENTRY are initialized with T.
INDUCTION: Assume that after the fcth iteration, the values are all no greater than those after the (k — l)st iteration, and show the same for iteration k 1 compared with iteration k. Line (5) of Fig. 9.23(a) has
Let us use the notation IN[S] * and OUT[P]* to denote the values of m[B] and OUT[P] after iteration i. Assuming OVT[P]k < O U T f P ] * - 1 , we know that w[B]k 1 < w[B]k because of the properties of the meet operator. Next, line (6)
OUT[£] = / B ( l N [ £ ] ) .
Since m[B]k 1 < m[B]k, we have OUT[B]k 1 < OVT[B]k by monotonicity. Note that every change observed for values of IN[J3] and OUTpS] is necessary to satisfy the equation. The meet operators return the greatest lower bound of their inputs, and the transfer functions return the only solution that is consistent with the block itself and its given input. Thus, if the iterative algorithm terminates, the result must have values that are at least as great as the corresponding values in any other solution; that is, the result of Algorithm 9.25 is the MFP of the equations.
Finally, consider the third point, where the data-flow framework has finite height. Since the values of every IN[B] and OUT[£] decrease with each change, and the algorithm stops if at some round nothing changes, the algorithm is guaranteed to converge after a number of rounds no greater than the product of the height of the framework and the number of nodes of the flow graph.