MIT 23 Dataflow analysis frameworks (798429)
Текст из файла
CS 4120 Lecture 23Dataflow analysis frameworks19 October 2011Lecturer: Andrew Myers1Iterative analysisA dataflow analysis can be characterized as a four-tuple (D, L, u, F): the direction of analysis D, the space ofvalues L, transfer functions Fn , and a meet operator u. We’re not yet guaranteed that iterative analysis suchas the worklist algorithm works, however.Let’s consider a simpler algorithm that computes the answer to a dataflow analysis.
If the dataflowanalysis framework satisfies certain properties to be identified, this algorithm will compute the same thingas the worklist algorithm, but less efficiently. We can think of the worklist algorithm as an optimized versionof this iterative analysis algorithm, which avoids recomputing out(n) for nodes n whose value couldn’t havechanged (because it hasn’t changed for any predecessors of n).Iterative analysis (forward):• for all n, out(n) := >• repeat until no change:– in(n) := n0 ≺n out(n0 )– out(n) := Fn (in(n))The algorithm updates out(n) for all n on each iteration.
If we imagine each of the nodes n as having one ofthe distinct indices 1, . . . , N, we can think of all the values out(n) as forming an N-tuple (out(n1 ), . . . , out(nN )),which is an element of the set LN .We can think of the action of each iteration of the loop as mapping an element of LN to a new elementof LN ; that is, it is a function F : LN → LN . The action of the algorithm produces a series of tuples until thesame tuple happens on two consecutive iterations:(>, >, . .
. , >)−→ (l11 , l12 , . . . , l1N )−→ (l21 , l22 , . . . , l2N )...−→ (lk1 , lk2 , . . . , lkN )−→ (lk1 , lk2 , . . . , lkN )• When is this algorithm guaranteed to terminate, i.e., converge on a tuple, and how big can the iterationcount k be?• When does it produce a solution to the dataflow equations?• When does it produce the best solution to the equations?To get answers to these questions, we need to understand the theory of partial orders, because we willwant the space of dataflow values L to be a partial order.1Hasse diagram: 2{a,b,c},• Given a subset B S, y is an uof B if x B .
x y• y is a least upper bound ( B)all upper bounds z• A chain is a sequence of elemx0, x1, x2, … such that x0 x1• For any finite chain x0,…,xn,• What about infinite chains?y{a,b,c}{b,c}LUBs and Chainx{a,c}yx{c}{a,b}{b}={a}{}CS 611 Fall '00 -- Andrew Myers, Cornell University9CS 611 Fall '00 -- Andrew Myers, Cornell UniversityFigure 1: Hasse diagram2Partial ordersA partial order (or partially ordered set, or poset) is a set of elements (called the carrier of the partial order) alongComplete partial ordersInformation contwith a relation v that is:• We consider one domain elem• A complete partial order (cpo) is a partial• reflexive: x v x for all x.less than another if it gives lesorder in which every chain has a leastinformationupper• transitive: if x v y and y v z, thenx boundv z.•Non-termination gives less in• Examples (S, )than any store (x)• antisymmetric: if x v y and y v Sx, then x and y are the same element.(2 , )• Stores are incomparable un{ },) is that it is possible for two elements to be incomparable;The key thing that makes this a (partialorder……they are not related in either direction.([0,1], ):For dataflow analysis, we interpretthe(S,orderingl1 v l2 to means that l2 is a better or more informative(S,=)?)?• Recall: trying to find least fixeresult.• cpo may have least element : pointed; how to order functionSome examples of partial orders are the integers ordered by ≤ (i.e., (Z, ≤), types ordered by the subtypingCS611Fall'00-AndrewMyers,CornellUniversity11CS611Fall'00 -- Andrew Myers, Cornell Universityrelation ≤ (in many languages), sets ordered by ⊆ (or ⊇), booleans ordered by ⇒.
If (L, v) is a partial order,the dual partial order (L, w) is too. Some examples of non-partial orders are the reals ordered by < and pairsof integers ordered by their sums.2.1Hasse diagramA useful way to visualize a partial order is through a Hasse diagram, as shown in Figure 1. This is adiagram for the subsets of {a, b, c} with the ordering relation ⊆. In the diagram, elements that are ordered areconnected by a line if there is no intermediate element that lies between them in the ordering.
And elementsconnected by a line are displaced vertically to show which is the greater in the relation. Therefore, any tworelated elements are connected by a path that goes consistently upward or downward in the diagram.The height of a partial order is the number of edges n on the longest chain of elements l0 v l1 v l2 v . . . ln .Therefore, the height of the example in Figure 1 is 3.2.2LatticesA lower bound of two elements x and y is an element that is less than both of them. Some partial orders havethe property that every two elements have a greatest lower bound, or GLB, or meet.
It is written x u y, andpronounced as “x meet y”.The meet of two elements is above all other lower bounds in the ordering: z v x ∧ z v y ⇒ z v x u y.Dually, for some partial orders, every two elements have a greatest upper bound (LUB), written x t yand pronounced “x join y”.If a partial order has both a meet and a join for every pair of elements, it is called a lattice. If it has a meetfor every pair of elements, it is a lower semilattice.
If it has a join for every pair of elements, it is an uppersemilattice. We will be interested only in meets, so we will be working with lower semilattices, which wemay simply abbreviate to “lattice” (and most of the partial orders we care about are, in fact, full lattices).22.3TuplesSuppose that L is a partial order. Then the set of tuples LN is also a partial order under the componentwiseordering:(l1 , l2 , .
. . , lN ) v (l01 , l02 , . . . , l0N ) ⇐⇒ ∀i∈1..N li v l0iYou can check for yourself that if L is a partial order, this ordering on LN is also reflexive, transitive, andantisymmetric.If L is a lattice, then LN is also a lattice, with the meet (or join) taken componentwise:(l1 , . . . , lN ) u (l01 , . . . , l0N ) = (l1 u l01 , . . . , lN u l0N )(l1 , . . . , lN ) t (l01 , . . . , l0N ) = (l1 t l01 , .
. . , lN t l0N )To see that this works for meets, we need to show that (l1 u l01 , . . . , lN u l0N ) is greater than any otherlower bound for (l1 , . . . , lN ) and (l01 , . . . , l0N ). Suppose we have such a lower bound (l00, . . . , l00). Since it is aN100000000lower bound, for all i, li v li and also li v li . But that implies that li v li u li . Therefore, according to the) v (l1 u l01 , . .
. , lN u l0N ).componentwise ordering on LN , (l00, . . . , l00N13MonotonicityThe iterative analysis algorithm starts from the top of the lattice LN , (>, >, . . . , >), and repeatedly applies afunction F : LN → LN to it, until a fixed point of the function is reached: a tuple X = (lk1 , . . .
, lkN ) such that F(X) =X. As the algorithm executes, a series of tuples X0 , X1 , X2 , . . . , Xk is produced, where X0 = (>, >, . . . , >) andXk is the fixed point of F.Given that a fixed point is reached, all the dataflow equations must be satisfied; otherwise, a differenttuple would have resulted from the last iteration of the loop.
So if the algorithm terminates, it does find asolution. How do we know that it finds a solution?The key is to observe that the transfer functions Fn are normally monotonic, and therefore the function Fis too. A function on a partial order is monotonic if it preserves ordering:Monotonicity: A function f : L → L is monotonic if x v y ⇒ f (x) v f (y).In the context of dataflow analysis, monotonicity makes sense. We can think about the transfer functionsFn as describing what we know after a node executes, given what we know beforehand. Having moreinformation before the node executes should not cause us to have less information afterward; it should onlyhelp or at worst have no benefit.The function F is constructed out of the transfer functions Fn and the meet operator.
If the transferfunctions are monotonic on L, the function F is monotonic on LN . To see why, let us first check that the meetoperator is monotonic.Theorem 1 (The meet operator is monotonic on its arguments)xv y⇒xuzv yuzThis proposition is depicted in Figure 2. Since the ordering v is transitive, we know that x u z v y. Thismeans x u z is a lower bound for both y and z, and therefore, it is bounded above by the greatest lowerbound for y and z, which is y u z.The function F is formed by the composition of monotonic transfer functions and the monotonic meetoperator, as depicted in Figure 3, so it is also monotonic.3yzy⊓z?xx⊓zFigure 2: Monotonicity of meetl1ll2l3l1l2l3⊓liF(l)⊓ liTransfer functionF(⊓li)Meet operatorA node in a CFGFigure 3: Dataflow analysis framework components44TerminationIterative analysis starts with top element X0 and applies F to it.
Характеристики
Тип файла PDF
PDF-формат наиболее широко используется для просмотра любого типа файлов на любом устройстве. В него можно сохранить документ, таблицы, презентацию, текст, чертежи, вычисления, графики и всё остальное, что можно показать на экране любого устройства. Именно его лучше всего использовать для печати.
Например, если Вам нужно распечатать чертёж из автокада, Вы сохраните чертёж на флешку, но будет ли автокад в пункте печати? А если будет, то нужная версия с нужными библиотеками? Именно для этого и нужен формат PDF - в нём точно будет показано верно вне зависимости от того, в какой программе создали PDF-файл и есть ли нужная программа для его просмотра.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
