question/help with dominance frontiers

OK, all you SSA/Sparse evaluation graph fans, can you help me out here?


I'm trying to prove a conjecture. The enclosed message is somewhat
lengthy. The goal is to replace the 'dominance frontier' with another
concept, the 'ancestor frontier'.


Given a CFG with distinguished Entry node, and a DFST. Let the ANC
relation be the ancestor relation on the given DFST: X ANC Y means X
is an ancestor of Y in the DFST; X !ANC Y means X is not an ancestor,
and X sANC Y means X is a strict or proper ancestor of Y (X ANC Y and
X != Y).


PRED(X), SUCC(X) are immediate predecessor/successor relations in CFG.
PARENT(X), CHILD(X) are parent/child relations in DFST.
ancestor and descendant relations are relative to the DFST.


Define the ancestor frontier AF(X) as the set of nodes Z
AF(X) = { Z | exists Y1,Y2 in PRED(Z), X ANC Y1 and X !ANC Y2 }


in other words, AF(X) is the set of nodes Z where X is an ancestor of
a predecessor of Z but not of all predecessors of Z.
[note correspondence and differences to definition of DF(X); DF(X)
can be defined as set of nodes Z where X dominates some predecessor of Z
but not all predecessors of Z, or, by most literature, where X dominates
some predecessor of Z but does not strictly dominate Z itself.
The definition of AF as above is needed for the proofs.]


If S is a set of nodes, let AF(S) = the union AF(X), for all X in S.
Let the iterated AF be defined as usual
AF^1(S) = AF(S)
AF^2(S) = AF(S U AF^1(S))
AF^i(S) = AF(S U AF^{i-1}(S))
AF^+(S) = limit_{i -> infty} AF^i(S)


I want to prove the equivalence of J^+(S) and AF^+(S), where J(S) is the
join set, defined as usual for the SSA/SEG work.


In the following, --> means an edge, -*-> means a potentially trivial path,
and -+-> means a nontrivial path.




Step 1: prove J^+(S) subseteq AF^+(S).


Lemma 1: Given a path p:X-*->Y and edge Y-->Z, either Z in AF^+(X) or
there is a W in {X} U AF^+(X) such that W ANC Z.


Let W be the last node on the path p that is a member of {X} U AF^+(X).
Claim: W ANC Y. If not, there is an edge U-->V on the subpath W-+->Y such that
W ANC U and W !ANC V (this just means there is an edge that leave the subtree
rooted at W to get to Y). By definition, V in AF(W), and therefore,
V in AF^+(X), contradicting the choice of W. Therefore, W ANC Y.


If W ANC Z, we are done; otherwise, W ANC Y and Y in PRED(Z), so
Z in AF(W), and again, Z in AF^+(X). This proves Lemma 1.




Lemma 2. Given X1 != X2, Z in J(X1,X2), show Z in AF^+(X1) U AF^+(X2).


Since Z in J(X1,X2), there are paths p1:X1-*->Y1 and p2:X2-*->Y2,
where Y1 and Y2 are predecessors of Z, and where the nodes on the paths
are disjoint (from definition of join).


Let W1 be the last node on the path p1 that appears in {X1,X2} U AF^+({X1,X2});
let W2 the the last node on path p2 that appears in {X1,X2} U AF^+({X1,X2}).
Since p1 and p2 are node-disjoint, W1 != W2.


>From Lemma 1, either W1 ANC Z or Z in AF^+(X1).
also, either W2 ANC Z or Z in AF^+(X2).


If W1 !ANC Z or W2 !ANC Z, Z in AF^+(X1) U AF^+(X2).


If W1 ANC Z and W2 ANC Z, then either W1 sANC W2 or W2 sANC W1.
Without loss of generality, say W2 sANC W1.
Now we have the situation where W2 is a proper ancestor of W1, and W1 is
an ancestor of Z, in the DFST.
There is some edge U-->V on path p2 after W2 that 'enters' the
subtree of the DFST rooted at W1, that is, where W1 !ANC U and W1 ANC V.
Note that V cannot be W1, since paths p1 and p2 are disjoint.
If this edge is U-->Z, then W1 is an ancestor of some
predecessor of Z, its tree parent, but not of all predecessors (not of U),
so Z in AF(W1), and therefore Z in AF^+(X1), and we are done.


If V is not Z, then V is in AF(W1), by the same argument; this contradicts
W2 as the last node on path P2 in {X1,X2} U AF^+({X1,X2}).


Therefore, Z must be in AF^+(X1) U AF^+(X2); this complete the proof of Lemma 2.




Simple extension of Lemma 2 shows that J(S) is a subset of AF^+(S) for any
nonempty set S. Induction on 'i' in iterated join gives us:


        J^{i+1)(S) = J(S U J^i(S))
subseteq J(S U AF^+(S))
subseteq AF^+(S U AF^+(S)) = AF^+(S);
thus J^+(S) subseteq AF^+(S)




Containment in the other direction is even simpler.
Let Entry be a member of S.


Show that AF(S) is a subset of J(S).
Given X in S and Z in AF(X), there must be a path from X to some predecessor
Y of Z where all the nodes on the path are descendants of X;
there is some other predecessor V of Z where X !ANC V. Taking the tree
path from X to Y, and edge Y-->Z, then taking the tree path from Entry to V
and the edge V-->Z, gives two paths proving Z in J(Entry,X).




Question: Has this been shown before? If not, it is a relatively
straightforward modification to the dominance frontier proofs.


Question 2: The SSA/SEG stuff really needs the iterated dominance frontier,
or I believe, iterated ancestor frontier. The quadratic term dealing with
iterated dominance frontiers arises because each DF may be as big as O(N),
number of nodes. However, if we consider DF to be a relation, and find RDF,
the transitive reduction of DF, we can see that RDF^+ = DF^+, and RDF
is smaller. Has anyone explored this?


thanks - Michael Wolfe, mwolfe@cse.ogi.edu, soon to be mwolfe@pgroup.com
--

Return to the comp.compilers page.
Search the comp.compilers archives again.