Download Presentation
## Termination

- - - - - - - - - - - - - - - - - - - - - - - - - - - E N D - - - - - - - - - - - - - - - - - - - - - - - - - - -

**Termination**• Still, it’s annoying to have to perform a join in the worklist algorithm • It would be nice to get rid of it, if there is a property of the flow functions that would allow us to do so while (worklist.empty.not) do let n := worklist.remove_any; let info_in := m(n.incoming_edges); let info_out := F(n, info_in); for i := 0 .. info_out.length do let new_info := m(n.outgoing_edges[i]) t info_out[i]; if (m(n.outgoing_edges[i]) new_info]) m(n.outgoing_edges[i]) := new_info; worklist.add(n.outgoing_edges[i].dst);**Even more formal**• To reason more formally about termination and precision, we re-express our worklist algorithm mathematically • We will use fixed points to formalize our algorithm**Fixed points**• Recall, we are computing m, a map from edges to dataflow information • Define a global flow function F as follows: F takes a map m as a parameter and returns a new map m’, in which individual local flow functions have been applied**Fixed points**• We want to find a fixed point of F, that is to say a map m such that m = F(m) • Approach to doing this? • Define ?, which is ? lifted to be a map: ? = e. ? • Compute F(?), then F(F(?)), then F(F(F(?))), ... until the result doesn’t change anymore**Fixed points**• Formally: • We would like the sequence Fi(?) for i = 0, 1, 2 ... to be increasing, so we can get rid of the outer join • Require that F be monotonic: • 8 a, b . a v b ) F(a) v F(b)**Back to termination**• So if F is monotonic, we have what we want: finite height ) termination, without the outer join • Also, if the local flow functions are monotonic, then global flow function F is monotonic**Another benefit of monotonicity**• Suppose Marsians came to earth, and miraculously give you a fixed point of F, call it fp. • Then:**Another benefit of monotonicity**• Suppose Marsians came to earth, and miraculously give you a fixed point of F, call it fp. • Then:**Another benefit of monotonicity**• We are computing the least fixed point...**Recap**• Let’s do a recap of what we’ve seen so far • Started with worklist algorithm for reaching definitions**Worklist algorithm for reaching defns**let m: map from edge to computed value at edge let worklist: work list of nodes for each edge e in CFG do m(e) := ; for each node n do worklist.add(n) while (worklist.empty.not) do let n := worklist.remove_any; let info_in := m(n.incoming_edges); let info_out := F(n, info_in); for i := 0 .. info_out.length do let new_info := m(n.outgoing_edges[i]) [ info_out[i]; if (m(n.outgoing_edges[i]) new_info]) m(n.outgoing_edges[i]) := new_info; worklist.add(n.outgoing_edges[i].dst);**Generalized algorithm using lattices**let m: map from edge to computed value at edge let worklist: work list of nodes for each edge e in CFG do m(e) := ? for each node n do worklist.add(n) while (worklist.empty.not) do let n := worklist.remove_any; let info_in := m(n.incoming_edges); let info_out := F(n, info_in); for i := 0 .. info_out.length do let new_info := m(n.outgoing_edges[i]) t info_out[i]; if (m(n.outgoing_edges[i]) new_info]) m(n.outgoing_edges[i]) := new_info; worklist.add(n.outgoing_edges[i].dst);**Next step: removed outer join**• Wanted to remove the outer join, while still providing termination guarantee • To do this, we re-expressed our algorithm more formally • We first defined a “global” flow function F, and then expressed our algorithm as a fixed point computation**Guarantees**• If F is monotonic, don’t need outer join • If F is monotonic and height of lattice is finite: iterative algorithm terminates • If F is monotonic, the fixed point we find is the least fixed point. • Any questions so far?**What about if we start at top?**• What if we start with >: F(>), F(F(>)), F(F(F(>)))**What about if we start at top?**• What if we start with >: F(>), F(F(>)), F(F(F(>))) • We get the greatest fixed point • Why do we prefer the least fixed point? • More precise**Graphically**y 10 10 x**Graphically**y 10 10 x**Graphically**y 10 10 x**Another example: constant prop**• Set D = in x := N Fx := N(in) = out in x := y op z Fx := y op z(in) = out**Another example: constant prop**• Set D = 2 { x ! N | x 2 Vars Æ N 2 Z } in x := N Fx := N(in) = in – { x ! * } [ { x ! N } out in x := y op z Fx := y op z(in) = in – { x ! * } [ { x ! N | ( y ! N1 ) 2 in Æ ( z ! N2 ) 2 in Æ N = N1 op N2 } out**Another example: constant prop**in Fx := *y(in) = x := *y out in F*x := y(in) = *x := y out**Another example: constant prop**in Fx := *y(in) = in – { x ! * } [ { x ! N | 8 z 2 may-point-to(x) . (z ! N) 2 in } x := *y out in F*x := y(in) = in – { z ! * | z 2 may-point(x) } [ { z ! N | z 2 must-point-to(x) Æ y ! N 2 in } [ { z ! N | (y ! N) 2 in Æ (z ! N) 2 in } *x := y out**Another example: constant prop**in *x := *y + *z F*x := *y + *z(in) = out in x := f(...) Fx := f(...)(in) = out**Another example: constant prop**in *x := *y + *z F*x := *y + *z(in) = Fa := *y;b := *z;c := a + b; *x := c(in) out in x := f(...) Fx := f(...)(in) = ; out**Another example: constant prop**in s: if (...) out[0] out[1] in[0] in[1] merge out