MIT 23 Dataflow analysis frameworks (798429), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

The result, which we called X1 , must beordered with respect to X0 ; that is, X1 v X0 . Because F is monotonic, F(X1 ) v F(X0 ); that is, X2 v X1 . Thispattern must continue: for all n, Xn+1 v Xn , which we can see by induction. If we assume that Xn v Xn−1 ,then by monotonicity of F, Xn+1 v Xn . Therefore the successive dataflow values produced by the algorithmform a chain of distinct elements:Xk v Xk−1 v . . .

v X2 v X1 v X0NIf the lattice L has infinite height, there is no guarantee that this chain won’t continue indefinitely. Butfor most of the problems we care about, the lattice L has some finite height (call it h). Therefore, the latticeof tuples LN has height at most Nh. Once the iterative analysis algorithm has run Nh iterations, it must havearrived at the bottom of the chain: convergence is achieved in k iterations where k ≤ Nh.5Example: live variable analysisIn live variable analysis, the dataflow values are sets of live variables.

We want to find as few variables liveas possible to enable the most optimization, so the ordering v is ⊇, the top element > is ∅, and the meetoperator u is ∪.Are the transfer functions monotonic? Recall that:Fn (l) = use(n) ∪ (l − def (n))So if l v l , then l ⊇ l . Suppose we have an element x ∈ Fn (l0 ) = use(n) ∪ (l0 − def (n)).

Then either x ∈ use(n),or else x ∈ l0 − def (n), in which case x ∈ l − def (n). In either case x ∈ Fn (l). Since this is true for arbitrary x,Fn (l) ⊇ Fn (l0 ), as required.060The meet-over-all-paths solution and distributivityWe know that we get a solution to the dataflow equations if we run iterative analysis. But is it the bestpossible solution? For example, in live variable analysis, we defined a variable as live if there is any pathleading from the current program point where that variable will be used. The set of live variables is thereforethe union (i.e., the meet) over all possible paths of the variables that are live along any of the paths. In mostdataflow analyses, like this one, we are trying to arrive at the meet-over-all-paths (MOP) solution:out(n) =Fn (Fpk (Fpk−1 (.

. . (Fp1 (. . . (Fp0 (>)))))))all paths p0 p1 ...pk nThe reason we might not get the MOP solution is that even if that our transfer functions capture perfectreasoning, there is still the possibility of losing information whenever we take a meet. If meet doesn’t loseinformation, then we should get the same answer to the dataflow analysis when we duplicate the subsequentnode, perform the analysis on the replicas, and then recombine the results using meet (see Figure 4).If this is true, we say that the transfer functions are distributive, and we can pull a meet operation outfrom the argument to Fn and take it after applying Fn :Fn (l1 u l2 ) = Fn (l1 ) u Fn (l2 )What the iterative analysis computes is an alternating application of meet and transfer functions (theupdates to in(n) and out(n), respectively), so the result is something like this:   out(n) = Fn Fn0 Fn00 . .

.n0 ≺nn00 ≺n0n000 ≺n00But if the Fn ’s are all distributive, that means we can pull out all the meets, giving us exactly the MOPsolution.5l1l2l1l2nnl1 ⊓ l2nFn(l2)Fn(l1)Fn(l1 ⊓ l2)Fn(l1) ⊓ Fn(l2)Figure 4: Analyses that are equivalent if meet loses no information7Example: live variable analysisDoes live variable analysis give us the MOP solution? Yes, which we can see by showing that Fn isdistributive:Fn (x u y) = use(n) ∪ ((x ∪ y) − def (n))= use(n) ∪ ((x − def (n)) ∪ (y − def (n)))= (use(n) ∪ (x − def (n))) ∪ (use(n) ∪ (y − def (n)))= Fn (x) u Fn (y)8Example: constant propagationIn “classic” constant propagation, the dataflow value is a mapping from variables to either a constant valuec, the “don’t know” value ⊥, or the “no assignment yet” value >, with ⊥ v c v > for all c.

For a nodez = x OP y, then, we compute the outgoing value of x as follows (? represents any value):xc1⊥?>?yc2?⊥?>zc1 OP c2⊥⊥>>The transfer function is not distributive. Consider a node that computes z = x + y and has twopredecessor nodes with output values {x 7→ 2, y 7→ 3} and {x 7→ 3, y 7→ 2}. The meet of these values is{x 7→ ⊥, y 7→ ⊥}, so the node will compute {x 7→ ⊥, y 7→ k, z 7→ ⊥}.

However, applying the transfer functionto the individual values yields {x 7→ 2, y 7→ 3, z 7→ 5} and {x 7→ 3, y 7→ 2, z 7→ 5}, and the resulting meet is{x 7→ ⊥, y 7→ ⊥, z 7→ 5}. Thus, information is lost by taking the meet before applying the transfer function.6.

Характеристики

Список файлов статьи