Programming Languages: Lecture #5 Page 12 of 12
Programming Languages Semantics /Noam Rinetzky Mooly Sagiv
Lecture #5, 22 April 2004: Chaotic iterations for constant propagation
Notes by: Dotan Patrich
Introduction
In this lecture, we will go over the process of chaotic iteration as an algorithm for constant propagation and generalize it to a broader class of problems. Continuing from last lesson, we will go into details about the algorithm's mathematical properties and its behavior.
In the second half of the lecture we, define the Galois connection between the abstract semantics as it is defined in the algorithm's domain and a concrete semantics, in our case a collecting variation of structural operation semantics. In the last part we will build ground for proving the soundness of the algorithm.
Chaotic Iterations Algorithm
In the last lecture, we saw a general chaotic iteration algorithm over a control flow graph (CFG) for a given program, this lesson we will go over a specialized version of the algorithm for the problem of constant propagation. We will go over the details of the algorithm in this section in several steps:
· Show examples of the algorithm's behavior on sample programs
· Formulate it's behavior using a system of equations and see it’s solutions properties
· Prove the algorithm correctness in finding a least fixed point
· Analyze the complexity of the algorithm.
For the moment, we assume that our programming language does not include procedures and that the control flow of the program is given.
For simplicity, we initially ignore exceptions and other constructs which complicates the task of defining control flow graph. Under these restrictions, it is easier to construct the CFG for the algorithm statically.
We also assume, without loss of generality, that there is a designated control flow node s which is the start node and that this node has no incoming edges.
The algorithm
Chaotic(G(V, E): Graph, s: Node, τ: L, f: E ®(L ®L) ) {
for each v in V do dfentry[v] :=
dfentry[s] = τ
WL = {s}
while (WL ¹ ) do
select and remove an element u WL
for each v, such that e=(u, v) ÎE do
temp = f(e)(dfentry[u])
new := temp dfentry[v]
if (new ¹ dfentry[v]) then
dfentry[v] := new;
WL := WL È{v}
It is an iterative algorithm that given - a monotonic transfer function in each edge of the control flow graph - f, initial values for the variables at the start of the program – τ and a starting node in the CFG – s, computes the least fixed point of a system of equations defined by the CFG of the program.
The iterative algorithm goes over each node v in the worklist, and computes the changes in the states of nodes that are the successors of v in the CFG, by applying function f on the state of v and performing meet operation with the state in v ‘s successors. When a change is detected in an abstract state of a node we add it to the worklist. This way the change of a state is propagating to its descendent nodes. The order of going through the nodes in the worklist is not defined and we will see that it only affects the number of iterations.
At node v in the control flow graph the program state is represented by the (algoritm) variable dfentry[v]. The value of these variables are taken from some lattice. In the constant propagation, the lattice is a finite map from the program variable names to another complete lattice L'. Where the lattice L` represents the possible values of a single variable and it is Z{,}. An example of an element in the lattice L which can occur at a CFG node is [x1, y, z0], where 1, and 0 in this example are the values from L` and the state of all variables is a value in L.
We compute the lattice element at each node by computing dfentry. dfentry[v] holds the possible state of the program variables at a node's statement. .
As we have seen last lesson, the transfer function in each edge of the control flow graph is monotonic. The algorithm works in a complete lattice given (L,,,,,) and in each iteration a larger value is generated for some CFG nodes, or the worklist shrinks.
Also, we will see in this section that the algorithm computes the least fixed point (lfp) of a monotone function, which is the minimal solution for each node's state in the control flow graph.
Examples of the algorithm run
We begin with a simple example than was shown last lesson on how to create the control flow graph and transfer function of it:
/ WL / dfentry[v]{1}
{2} / df[2]:=[x0, y0,z3]
{3} / df[3]:=[x1, y0,z3]
{4} / df[4]:=[x1, y0,z3]
{5} / df[5]:=[x1, y0,z3]
{7} / df[7]:=[x1, y7,z3]
{8} / df[8]:=[x3, y7,z3]
{3} / df[3]:=[x, y,z3]
{4} / df[4]:=[x, y,z3]
{5,6} / df[5]:=[x1, y,z3]
{6,7} / df[6]:=[x, y,z3]
{7} / df[7]:=[x, y7,z3]
In the example above, the left shows the control flow graph of a given program with the transfer function f on each edge of the control graph. On the right, there is a table that details the changes in the work-list and the node's states after each iteration of the algorithm.
Order of traversal example
The order of traversing the nodes of the control flow graph is not defined in the algorithm, and it affects the number of iterations of the algorithm. Next, is an example of in which the in which the algorithm was applied to the same program above, but the nodes were traversed in a different order. We can see how the different order affect the number of iterations. It is important to note that regardless of the traversal order the algorithm is guaranteed to produce the least fix point.
/ WL / dfentry[v]{1}
{2} / df[2]:=[x0, y0,z3]
{3} / df[3]:=[x1, y0,z3]
{4} / df[4]:=[x1, y0,z3]
{5} / df[5]:=[x1, y0,z3]
{7} / df[7]:=[x1, y7,z3]
{8} / df[8]:=[x3, y7,z3]
{3} / df[3]:=[x, y,z3]
{4} / df[4]:=[x, y,z3]
{5,6} / df[6]:=[x, y,z3]
{5,7} / df[7]:=[x, y7,z3]
{5,8} / df[8]:=[x3, y7,z3]
{5} / df[5]:=[x1, y,z3]
{7} / df[7]:=[x, y7,z3]
As we can see in this example we need 13 iterations of the algorithm before we reach a fix-point, compared to 11 iterations in the previous example. While it does not seem such a big difference, remember that this depends on the number of variables and the length of the program.
One heuristic of traversing the nodes is a DFS walk on the graph or post-order on the work-list. However, we are guarantied to end the execution of the algorithm in a limited number of iterations in the worst case, whatever traversal method we choose, as we will prove in the section about the complexity of the algorithm.
Yet another example
Here is another example that should give you a better understanding of the role of the variable value lattice and how the chaotic iteration differ from the actual run of the program.
The program we will use is:
y:=x
z:=1
while (y>1)
z:=z*y
y:=y-1
y:=0
Again for this program we will build a control flow graph and transition function on the edges. In the table bellow on the left is the CFG and on the right are the changes in states and the worklist:
/ WL / dfentry[v]{1}
{2} / df[2]:=[x3, y3,z5]
{3} / df[3]:=[x3, y3,z1]
{4,6} / df[4]:=[x3, y3,z1]
{5,6} / df[5]:=[x3, y3,z3]
{3,6} / df[3]:=[x3, y,z]
{4,6} / df[4]:=[x3, y,z]
{5,6} / df[5]:=[x3, y,z]
{3,6} / df[3]:=[x3, y,z]
{6} / df[6]:=[x3, y,z]
The interesting thing about this algorithm is that the number of iterations over the while loop is not related to the number of iterations in the actual runtime, but to the lattice changes. This example shows clearly the difference of this static analysis algorithm to the actual execution of the program.
Another thing to notice in this example is the change in the lattice value for the y and z variables. Although, the variables change their value during run time many times they will change their value in the static analysis only twice, as this is the height of the lattice L` used.
Mathematical behavior of the algorithm
We will write a system of equation that describes the algorithm behavior and deduce by its properties that the chaotic iterations algorithm computes the least fixed point of the lattice. For every node v in the control flow graph an equation will be generated that take into account all the predecessor nodes of v and define the requirements on that node's state accordingly.
S={ / dfentry[s]=τ / }dfentry[v]= {f(u,v) (dfentry[u]) | (u,v)E}
The chaotic iterations algorithm applies this system of equations and by starting with value at each node (except for the starting node s which gets some initial value τ) it iteratively computes a minimal solution for this system of equations.
A solution for the system of equation is also referred to as a fixed point, as after applying the functions of the algorithm on the states in the solution, they will not change. There may be more than one fixed point to this system of equation, but first let us show that at least one exists.
We will show that a fixed point for the system of equations exists and the lfp (least fixed point) of it is well-defined by using Tarski's theorem. To do so, we need to convert the system of equations above to an equivalent monotone function FS:LnLn:
FS (X)[s] = τ
FS (X)[v] ={f(u,v) (X[u]) | (u,v)E}
The function FS "looks" at all the nodes in the CFG at once (FS operates on a vector of variables) and computes their new values according to the function at each edge of the CFG simultaneously. The functions at each edge of the CFG are monotone and by the definition of FS we get the FS is monotone as well, as it is composed of monotone functions at each component of the vector.
By Tarski's theorem on FS we conclude that the least fixed point is well-defined. Also, by the equality between the system of equations and FS we get that lfp(S)=lfp(FS).
To show the properties of such a fixed point, and what ``solution’’ is not a fixed point for the system of equations above, we show the examples bellow.
/ Node # / Non-Solution 11 / df[1]:=[x0,y0,z0]
2 / df[2]:=[x0,y0,z3]
3 / df[3]:=[x, y7,z3]
4 / df[4]:=[x, y7,z3]
5 / df[5]:=[x1, y7,z3]
6 / df[6]:=[x, y7,z3]
7 / df[7]:=[x, y7,z3]
8 / df[8]:=[x3, y7,z3]
Node # / Solution 2
1 / df[1]:=[x0,y0,z0]
2 / df[2]:=[x0,y0,z3]
3 / df[3]:=[x, y,z3]
4 / df[4]:=[x, y,z3]
5 / df[5]:=[x1, y,z3]
6 / df[6]:=[x, y,z3]
7 / df[7]:=[x, y7,z3]
8 / df[8]:=[x3, y7,z3]
The first example is not a solution to the system of equations as in node 3 the value of y should be . Note that when the program runs, the first time we reach this node the value of y is 0, afterwards the value of of y is always 7. Thus, the value of y is not a constant in this point. In the static analysis, we merge the abstract state of the after the assignment in node 2 (in which y is found to be always 0) and print statement in node 8 (in which y is found to have the constant value 7) and we get that the (abstract) value of y is in node 3. Any more iterations over the loop do not change this value as it is the maximal in the lattice. Also note that this solution is not sound as it report y to be constant in node 3, whereas it is not. We return to the issue of soundness in the second part of the lecture.
The second example is a solution to the system of equations. We can see that applying any of the monotone transfer functions from the CFG on a value at any node, does not change the states of its successor. In this sense, the solution is a fixed point.
As we start with a value in each node and each step apply a monotone function on the states, the state of each node must not "decrease" at each iteration, thus the solution we get must be the least fixed point of the equations. In the next section, we will prove that the algorithm stops.
Complexity of the algorithm
The algorithm is based on the complete lattice (L, ,,,,) given and at each step apply a monotone function f, taken from an edge of the control flow graph, on a node state from this lattice. In the case of constant propagation, the lattice is actually a finite map of variables name to variable values represented by lattice L`. Where lattice L` is composed of 3 states: ; a constant number state; and . The height of the lattice L` is 2, so after applying a monotone function on L` twice at most we will reach the maximum value in L`. From this, the height of the lattice L is 2|V|, since the abstract value of any variable can change at most 2 time. In particular, the abstract value of a node in L, cannot after applying a monotone function on L at most 2|V| times at most on a node we will reach the maximum value - in L.
At each of the algorithm iterations, we remove one node from the worklist. We place other nodes in the worklist, only if the value of their abstract state. Each time the abstract state changes, it increases in the lattice (note, that in the computation of new, that the old value is merged with the propagated information). Since the lattice has a bounded size, as we have just seen, the value of the abstract state at a node can be changed at most 2|V| times. Thus, we get that each node can appear in the worklist at most 2|V| times. We conclude, that after a limited number of iterations the worklist will be empty and the algorithm will stop.