
%\documentstyle[psfig]{article}

\documentclass{article}

\usepackage{psfig}
\usepackage{latexsym}

%-------------------------------------------------------------------------
% take the % away on next line to produce the final camera-ready version
%\pagestyle{empty}

%-------------------------------------------------------------------------

\begin{document}

\def\DOM{\, \mbox{DOM} \,}
\def\NDOM{\, \overline{\mbox{DOM}} \,}
\def\SDOM{\, \mbox{SDOM} \,}
\def\NSDOM{\, \overline{\mbox{SDOM}} \,}
\def\IDOM{\, \mbox{IDOM} \,}
\def\NIDOM{\, \overline{\mbox{IDOM}} \,}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

\newenvironment{proof}{{\bf Proof}:}{$\Box$\newline}


\title{Notes on Dominators and Dominance Frontiers}

\author{Bryan Carpenter \\
NPAC at Syracuse University\\ Syracuse, NY 13244 \\
\{dbc\}@npac.syr.edu\\
}

\maketitle

\section{Dominators\label{sec:dominators}}

A {\em control flow graph} (CFG) is a directed graph with a unique source
node called {\em Entry}, and a path from {\em Entry} to every node in
the graph.  Node $X$ in a CFG is said to {\em dominate} node $Y$ if
every path from {\em Entry} to $Y$ passes through $X$.  This property
is written mathematically as a relation:
\begin{displaymath}
X \DOM Y
\end{displaymath}
The set of nodes dominated by $X$ is sometimes written as $\mbox{DOM}^{-1}(X)$.
Four important properties of the dominance relation follow from the definition.
\begin{enumerate}
\item
Every node dominates itself:
\begin{displaymath}
X \DOM X
\end{displaymath}
This property is called {\em reflexivity}.
\item
If a node $X$ dominates $Y$ and the node $Y$ dominates $Z$, then $X$
dominates $Z$:
\begin{displaymath}
X \DOM Y \wedge Y \DOM Z \Rightarrow X \DOM Z
\end{displaymath}
This property is called {\em transitivity}.
\item
If a node $X$ dominates $Y$, then $Y$ does not dominate $X$ unless $X$
and $Y$ are identical:
\begin{displaymath}
X \DOM Y \wedge Y \DOM X \Rightarrow X = Y
\end{displaymath}
This property is called {\em antisymmetry}.
\item
If two nodes $X$ and $Y$ both dominate $Z$, then either $X$ dominates $Y$ or
$Y$ dominates $X$:
\begin{displaymath}
X \DOM Z \wedge Y \DOM Z \Rightarrow X \DOM Y \vee Y \DOM X
\end{displaymath}
\end{enumerate}
Property 1 is obvious.  Property 2 follows because if every path from
{\em Entry} to $Z$ goes through $Y$ and every path from {\em Entry} to
$Y$ goes through $X$, clearly every path from {\em Entry} to $Z$ goes
through $X$.

To prove property 3, assume $X$ and $Y$ dominate one another and
are distinct.  Choose a path from {\em Entry} that passes through $X$.
Node $Y$ must appear on the path before the first occurrence of $X$, because
$Y$ dominates $X$.  But then $X$ must appear again before $Y$, because
$X$ dominates $Y$.  So $X$ appears on the path before its first
appearance, which is a contradiction.

To prove property 4, choose a cycle-free path, $p$, from {\em Entry}
to $Z$.  Since $X$ and $Y$ both dominate $Z$, they must both appear on
the path.  If $X$ and $Y$ are identical the property is trivial, so assume
they are distinct.  Suppose $X$ appears on $p$ before $Y$.  If $X$ does
not dominate $Y$ then there is another path, q, from {\em Entry} to $Y$
that does not pass through $X$.  But that means that by following
$q$ from {\em Entry} to $Y$ then following the remainder of the original
path to $Z$, we reach $Z$ without passing through $X$ (Figure
\ref{fig:strictness}).  This contradicts the premise the $X$ dominates
$Z$.  We conclude that $X$ {\em does} dominate $Y$.  Conversely if
$Y$ appears before $X$ on $p$, we conclude that $Y$ dominates $X$%
\footnote{This proof is taken from ``Principles of Compiler Design'' by
Aho and Ullman, Section 13.1, p443.}%
.

\begin{figure*}[p]
\centerline{\psfig{figure=strictness.eps,height=2in}}
\caption{Paths in proof of property 4\label{fig:strictness}}
\end{figure*}

\paragraph{DOM is a partial order.}  Properties 1 to 3 establish
that the dominance relation is a partial order on the nodes of the
control flow graph.

\paragraph{The dominators of any given node are totally ordered.}
Property 4 implies that furthermore the DOM relation is a
{\em total order} on the nodes that dominate $Z$---every dominator
of $Z$ is related to every other by the DOM relation.

\section{Strict and Immediate Dominators}

Node $X$ {\em strictly dominates} node $Y$ if $X$ dominates $Y$, and
$X$ and $Y$ are distinct.  This property is written mathematically as:
\begin{displaymath}
X \SDOM Y
\end{displaymath}
At the end of the last section we noted that the dominators of any
particular node form a set that is totally ordered by the dominance
relation.  Of course the strict dominators of a node $Y$ (being
a subset of the dominators)
are also totally ordered by DOM.  If $X$ is the {\em least} element of
the strict dominators of $Y$ (the one closest to $Y$), $X$ is called
the {\em immediate dominator} of $Y$.  This is written
\begin{displaymath}
X \IDOM Y
\end{displaymath}
As an alternative characterization of the immediate dominator, note that
if $p$ is {\em any} path from {\em Entry} to $Y$, the immediate dominator
of $Y$ is the last node on $p$ that strictly dominates $Y$.

Because all dominators of a particular node are totally ordered, they can
be arranged in a line with adjacent points related by IDOM.  This line
is the path reaching the given node through the {\em dominance tree}.
A dominance tree is uniquely associated with any CFG.  It is a graph
with the same nodes as the original CFG, but the significance of its
edges is completely different.  The root of the tree is {\em Entry} and
an edge represents an IDOM relationship.

A convenient recursive formula for the dominance relation is
\begin{equation}
X \DOM Y \Leftrightarrow (X = Y) \vee
\left(
\begin{array}{c} \forall \\ P \in \mbox{Pred}(Y) \end{array} X \DOM P
\right)
\label{eq:domdef}
\end{equation}
As a special case a node dominates itself.  If $X \ne Y$ and $X$ does
not dominate some predecessor of $Y$ then there is a path from
{\em Entry} through that predecessor to $Y$ that does not pass through
$X$, so $X$ does not dominate $Y$.  This establishes $\Rightarrow$.
To establish $\Leftarrow$ when $X \ne Y$ note that every path to $Y$
passes through some predecessor of $Y$.  So if all the predecessors
are dominated by $X$, every path from {\em Entry} to $Y$ passes through
$X$.

Note that although a node can dominate some of its own predecessors,
it cannot dominate all of them, otherwise every path from {\em Entry}
to $X$ would pass through $X$ before reaching $X$, which is impossible
(Figure \ref{fig:selfdom}).  So if $X = Y$ the second term on the
RHS of Equation \ref{eq:domdef} is false.  Conversely if the second
term is true $X \ne Y$.  This leads to a simple formula for strict
dominance:
\begin{equation}
X \SDOM Y \Leftrightarrow
\begin{array}{c} \forall \\ P \in \mbox{Pred}(Y) \end{array} X \DOM P
\label{eq:sdomdef}
\end{equation}
In words: $X$ strictly dominates $Y$ if and only if $X$ dominates all
predecessors of $Y$.  A useful corollary is
\begin{lemma}
\label{lem:sdomtail}
Suppose node $Z$ does {\em not} lie on a path
$p:X\stackrel{*}{\rightarrow}Y$, and $Z$ strictly dominates $Y$.
Then $Z$ strictly dominates {\em all} nodes on $p$.
\end{lemma}
\begin{proof}
Since $Z$ strictly dominates $Y$, it dominates
all predecessors of this node (by Equation \ref{eq:sdomdef}).
In particular it dominates the penultimate node of $p$.  Because
this node is distinct from $Z$ ($Z$ does not lie on $p$),
$Z$ also dominates it strictly.
Repeat this argument inductively to show that $Z$
strictly dominates {\em every} node in $p$.
\end{proof}

\begin{figure*}[p]
\centerline{\psfig{figure=selfdom.eps,height=1.3in}}
\caption{A node $X$ can dominate {\em some} of its own predecessors (eg
$X \DOM Y$), but it cannot dominate {\em all} of them (eg $X \NDOM U$),
because there must be a path from {\em Entry} to $X$.\label{fig:selfdom}}
\end{figure*}

\section{Dominance Frontiers\label{sec:df}}

The {\em dominance frontier} of a node $X$, denoted by $\mbox{DF}(X)$,
is the set of nodes, $Y$, such that $X$ dominates some predecessor of $Y$,
but $X$ doesn't strictly dominate $Y$:
\begin{equation}
\mbox{DF}(X) = \left\{ Y \left|
\left(
\begin{array}{c} \exists \\ P \in \mbox{Pred}(Y) \end{array} X \DOM P
\right)
\wedge X \NSDOM Y
\right. \right\}
\label{eq:dfdef}
\end{equation}
The situation is illustrated in Figure \ref{fig:df}.  Note that if we
follow any path from $X$, the first node after the startpoint that is
{\em not} strictly dominated by $X$ must belong to $\mbox{DF}(X)$.

% Prove that.  State it as a lemma?

\begin{figure*}[p]
\centerline{\psfig{figure=df.eps,height=2in}}
\caption{Node $Y$ is in $\mbox{DF}(X)$ because its predecessor
$U$ is dominated by $X$, but $Y$ is not strictly dominated by
$X$ (so, unless $X=Y$, there exists a path from {\em Entry} to $Y$ with no $X$
on it).\label{fig:df}}
\end{figure*}

The dominance frontier of a set, $S$, of nodes is defined as the union of the
dominance frontiers of the elements:
\begin{displaymath}
\mbox{DF}(S) = \bigcup_{X \in S} \mbox{DF}(X)
\end{displaymath}
The {\em iterated dominance fronter}, $\mbox{DF}^+(S)$, of the set of nodes is
defined as the limit of the sequence
\begin{eqnarray*}
  \mbox{DF}_1(S)     & = & \mbox{DF}(S) \\
  \mbox{DF}_{i+1}(S) & = & \mbox{DF}(S \cup \mbox{DF}_i(S))
\end{eqnarray*}
The following lemma about iterated dominance frontiers will be important:
\begin{lemma}
\label{lem:indfplus}
If a path $p:X \stackrel{+}{\rightarrow} Y$ has the property that no
node on $p$ strictly dominates its endpoint, $Y$,
then $Y \in \mbox{DF}^+(\{X\})$.
\end{lemma}
\begin{proof}
Suppose for a contradiction that $Y \notin \mbox{DF}^+(\{X\})$.  Let $X'$ be the
last node on the path that {\em is} in $\mbox{DF}^+(\{X\})$.  If no node on the
path is in $\mbox{DF}^+(\{X\})$, define $X'$ to be $X$.  Clearly no node following
$X'$ on $p$ is in $\mbox{DF}(X')$, otherwise that node would also be in $\mbox{DF}^+(\{X\})$.
So $X'$ strictly dominates the nodes following it, and in particular
it strictly dominates $Y$.  This contradicts the premise that no node
on $p$ strictly dominates $Y$, so we can infer $Y \in \mbox{DF}^+(\{X\})$.
\end{proof}

\begin{figure*}[p]
\centerline{\psfig{figure=itdf.eps,height=2.5in}}
\caption{A path to a node on the iterated dominance frontier.
Nodes $X_1$, $X_2$, $Y$ are in $\mbox{DF}^+(\{X\})$.  Intervening nodes
are strictly dominated by nodes on the preceding member of the
subsequence $(X, X_1, X_2)$.
\label{fig:itdf}}
\end{figure*}

(In fact this lemma can be strengthen with a reverse implication,
and we can characterize the iterated dominance frontier as follows:
\begin{theorem}
Node $Y$ is an element of $\mbox{DF}^+(\{X\})$ if and only if there
exists a path $p:X \stackrel{+}{\rightarrow} Y$ with the property that no
node on $p$ strictly dominates its endpoint, $Y$.
\end{theorem}
To prove ``only if'' assume $Y \in \mbox{DF}^+(\{X\})$ and consider Figure
\ref{fig:itdf}.  Such a path must exist if $Y$ is in $\mbox{DF}^+(\{X\})$.
Suppose there is a node, $X'$, on the path that strictly dominates
$Y$.  $X'$ will strictly dominate all nodes in the portion of the path
following the last occurrence of $X'$, by Lemma \ref{lem:sdomtail}.  Either this
occurrence of $X'$ is in the subsequence $(X, X_1, X_2, \ldots)$, or the
last member of the subsequence preceding the occurrence strictly
dominates $X'$.  In the latter case the transitivity properties of
strict dominance mean the preceding member of the sequence strictly
dominates all nodes that follow {\em it} on the path.  In either case
there is a member of $(X, X_1, X_2, \ldots)$ that strictly dominates all
its successors on the path, up to and including $Y$.  So $Y$ cannot be
in the dominance frontier of the last member of the subsequence, which
contradicts the choice of path.  We conclude $X'$ does not exist, so $p$
has the required property\footnote{Note that not {\em every} path from
$X$ to an element of $\mbox{DF}^+(\{X\})$ has the required property.
Figure \ref{fig:itdfpathdep} displays a counter-example.}.)

\begin{figure*}[p]
\centerline{\psfig{figure=itdfpathdep.eps,height=2.5in}}
\caption{$Y$ belongs to $\mbox{DF}(X) = \{Y, Z\}$, but there
is a path $q:X \rightarrow Z \rightarrow Y$ including a node,
$Z$, that strictly dominates $Y$.
\label{fig:itdfpathdep}}
\end{figure*}


% -------------------------------------------------------------------------
% Lemma:
%             +                                   +
%   If Y in DF ({X}), then there exists a path p:X->Y such that no node
%   on p strictly dominates Y.
% 
% Proof:
% 
%   The node Y is in DF+({X}) because there is a sequence of nodes
% 
%   X, X , ..., X   , Y
%       1        n-1
% 
% with the property
% 
%   X  in DF(X), X  in DF(X ), ..., Y in DF(X   )
%    1            2        1                 n-1
% 
% Hence there is a path p from X to Y passing through this sequence
% of nodes with the property that any nodes between X_{i-1} and X_i are
% strictly dominated by X_{i-1} (we understand X_0 = X and X_n = Y).
% (See Figure \ref{fig:itdf}.)
% 
% Now, suppose X' on p strictly dominates Y.  Let p':X->X' be the path
% p truncated at the *last* appearance of X' on p.  X' strictly dominates
% all nodes on the remainder of the path (p - p'), because X' strictly
% dominates the tail of this path and X' does not appear after its head.
% 
% Let X_r (r in 0 .. n-1) be the last member of the sequence (X_i)
% appearing on the subpath p'.  X_r dominates any nodes that follow it
% on p'.  These include X'.  By the transitivity properties of dominance
% and strict dominance, X_r then dominates all nodes that follow it on p,
% and in particular it strictly dominates Y.  This contradicts the assumptions
% about the sequence (X_i)---it means that no element on p following X_r
% is in DF(X_r).
% -------------------------------------------------------------------------
%
% Need to tidy that up.  Also give (and prove) an analogous characterization
% of the uniterated dominance fronter:
%                                         +
%   Y in DF(X) iff there exists a path p:X->Y such that X strictly dominates
%   every node between X and Y, but does not strictly dominate Y.

\section{Join sets\label{sec:join}}

The {\em join set}, $J(X, Y)$, of nodes $X$ and $Y$ is the set of nodes
$Z$ for which there exist two paths $p:X \stackrel{+}{\rightarrow} Z$ and
$q:Y \stackrel{+}{\rightarrow} Z$ that are disjoint except at node $Z$.

\begin{lemma}
\label{lem:atmostone}
At most one of the two paths $p$, $q$ includes a node that strictly
dominates $Z$.
\end{lemma}
\begin{proof}
Suppose a node $X'$ on $p$ strictly dominates $Z$.  Due to the
disjointness property, $X'$ does not appear anywhere on $q$.  
By Lemma \ref{lem:sdomtail}, $X'$
strictly dominates {\em every} node in $q$.

Similarly if a node $Y'$ on $q$ strictly dominates $Z$, then
$Y'$ strictly dominates {\em every} node in $p$.

But if both these conditions obtain, we have in particular that
$X' \SDOM Y'$ and $Y' \SDOM X'$.  This contradicts the asymmetry
property of dominance.
\end{proof}

\begin{corollary}
$Z \in \mbox{DF}^+(\{X, Y\})$.
\end{corollary}
\begin{proof}
By the preceding lemma, one of $p$, $q$ includes no node that strictly
dominates $Z$.  Hence, by Lemma \ref{lem:indfplus}, $Z$ is either an element
of $\mbox{DF}^+(\{X\})$ or of $\mbox{DF}^+(\{Y\})$.
\end{proof}

The join of a set, $S$, of nodes is defined as the union of the
join sets of pairs of elements:
\begin{displaymath}
\mbox{J}(S) = \bigcup_{X, Y \in S} J(X,Y)
\end{displaymath}
The preceding corollary establishes
\begin{lemma}
\label{lem:JinDFplus}
$J(S) \subset \mbox{DF}^+(S)$.
\end{lemma}
\begin{proof}
Because $J(X,Y) \subset \mbox{DF}^+(\{X, Y\})$.
\end{proof}

\begin{lemma}
\label{lem:DFinJ}
For any set, $S$, of nodes containing {\em Entry}, $\mbox{DF}(S) \subset J(S)$.
\end{lemma}
\begin{proof}
Consider a node $X \ne \mbox{\em Entry}$ in $S$, and any $Y \in \mbox{DF}(X)$.
There is a path from $X$ to $Y$ where all nodes before $Y$ are dominated
by $X$.  There is also a path from {\em Entry} to $Y$ where {\em none} of the
nodes are dominated by $X$ (because there is a path to $Y$ that does not
pass through $X$, so by definition no nodes on this path are dominated by $X$).
Hence the paths are disjoint except at $X$, and $Y \in J(X, \mbox{\em Entry})$.
\end{proof}

The {\em iterated join}, $J^+(S)$, of a set of nodes is
defined as the limit of the sequence
\begin{eqnarray*}
  J_1(S)     & = & J(S) \\
  J_{i+1}(S) & = & J(S \cup J_i)
\end{eqnarray*}
The importance of the iterated join set is that if $S$ is the set
of assignments to some variable, $J^+(S)$ defines the points in the CFG
where $\phi$ terms for that variable must be added in minimal Static
Single Assignment form or in Factored Use-Def Chains.  We want to prove an
equivalence between iterated join sets and iterated dominance frontiers%
\footnote{The remainder of this section is copied from
``Efficiently Computing Static Single Assignment Form and the Control
Dependence Graph'', by Cytron et al, section 4.3.}%
.
\begin{theorem}
\label{thm:DFisJ}
If $\mbox{\em Entry} \in S$, then
\begin{displaymath}
J^+(S) = \mbox{DF}^+(S).
\end{displaymath}
\end{theorem}
\begin{proof}
By Lemma \ref{lem:JinDFplus} and induction on $i$ we show
\begin{displaymath}
J^+(S) \subset \mbox{DF}^+(S).
\end{displaymath}
The induction step is
\begin{eqnarray*}
J_{i+1} & =       & J(S \cup J_i) \,\,\subset\,\, J(S \cup \mbox{DF}^+(S)) \\
        & \subset & \mbox{DF}^+(S \cup \mbox{DF}^+(S)) \,\,=\,\, \mbox{DF}^+(S)
\end{eqnarray*}
Lemma \ref{lem:DFinJ} and induction imply
\begin{displaymath}
\mbox{DF}^+(S) \subset J^+(S).
\end{displaymath}
The induction step is
\begin{eqnarray*}
\mbox{DF}_{i+1} & = & \mbox{DF}(S \cup \mbox{DF}_i)
                      \,\,\subset\,\, \mbox{DF}(S \cup J^+(S)) \\
        & \subset & J^+(S \cup J^+(S)) \,\,=\,\, J^+(S)
\end{eqnarray*}
\end{proof}

\section{Computation of Dominance Frontiers}

Section \ref{sec:df} introduced some basic definitions and lemmas about
dominance frontiers, and Section \ref{sec:join} suggested that they
may have important applications through their relation to join sets.
But to be truly useful, there must be an efficient way to compute them.

For the purposes of this section we assume that the {\em dominance tree}
(see Section \ref{sec:dominators}) has already been computed for the control
flow graph.  In fact efficient computation of the dominance tree is an
interesting and non-trivial problem in itself.  For now we just note that
a fast, practical algorithm exists\footnote{See ``A Fast Algorithm for
Finding Dominators in a Flowgraph'', T.\ Lengauer and R.\ E.\ Tarjan,
TOPLAS, Vol.\ 1, No.\ 1, 1979.}.

The set of children of node $X$ in the dominance tree is written
$\mbox{Children}(X)$.  By definition of the dominace tree, this
is the set of nodes that $X$ immediately dominates.  Do not confuse
$\mbox{Children}(X)$ with $\mbox{Succ}(X)$---the set of successors of
$X$ in the {\em control flow graph}.  The parent of $X$ in the dominance
tree is sometimes written $\mbox{idom}(X)$---the immediate dominator
of $X$.

The algorithm for computing dominance frontiers is based on the equation
\begin{equation}
\mbox{DF}(X) = \mbox{DF}_{\mbox{\scriptsize local}}(X) \cup
               \bigcup_{Z \in \mbox{\scriptsize Children}(X)}
               \mbox{DF}_{\mbox{\scriptsize up}}(Z)
\label{eqn:dfformula}
\end{equation}
where the sets $\mbox{DF}_{\mbox{\scriptsize local}}(X)$ and $\mbox{DF}_{\mbox{\scriptsize up}}(Z)$
are separate contributions to $\mbox{DF}(X)$ from the successors and the
children of $X$.  They are defined as follows
\begin{eqnarray}
\mbox{DF}_{\mbox{\scriptsize local}}(X) & \stackrel{\mbox{\scriptsize def}}{=} &
             \left\{ Y \in \mbox{Succ}(X) \left| X \NSDOM Y \right. \right\}
\label{eqn:dflocal} \\
\mbox{DF}_{\mbox{\scriptsize up}}(Z)    & \stackrel{\mbox{\scriptsize def}}{=} &
             \left\{ Y \in \mbox{DF}(Z) \left| X \NSDOM Y \right. \right\}
\label{eqn:dfup}
\end{eqnarray}
(to make the second formula self-contained, replace $X$ by $\mbox{idom}(Z)$).

\begin{proof}
Dominance is reflexive, so in equation \ref{eqn:dflocal}, $X$ dominates a
predecessor of $Y$.  So 
$\mbox{DF}_{\mbox{\scriptsize local}}(X) \subset \mbox{DF}(X)$.  
Dominance is transitive, so in the equation \ref{eqn:dfup}
$X$ dominates any predecessor of $Y$ that $Z$ does; there is
at least one such predecessor because $Y \in \mbox{DF}(Z)$.  So
$\mbox{DF}_{\mbox{\scriptsize up}}(Z) \subset \mbox{DF}(X)$.  Hence the
RHS of \ref{eqn:dfformula} is contained in $\mbox{DF}(X)$.

To establish containment of $\mbox{DF}(X)$ in the RHS,
suppose $Y \in \mbox{DF}(X)$ and $P$ is a predecessor of $Y$ that is
dominated by $X$.  We have that $X \NSDOM Y$.  By consideration of
the dominance tree, $P \DOM X$ implies 1) $P = X$ or 2) there exists
some $Z$ such that $X \IDOM Z$ and $Z \DOM P$.
If 1), then $Y \in \mbox{DF}_{\mbox{\scriptsize local}}(X)$.  If 2), $Z$
cannot strictly dominate $Y$, otherwise $X$ would, by the transitivity
properties of strict dominance.  So $Z$ dominates a predecessor of $Y$
but does not strictly dominate $Y$, ie $Y \in \mbox{DF}(Z)$.  Since $X
\NSDOM Y$, $Y$ is a member of $\mbox{DF}_{\mbox{\scriptsize up}}(Z)$.
\end{proof}

This establishes the validity of \ref{eqn:dfformula}.  The strict dominance
tests in \ref{eqn:dflocal} and \ref{eqn:dfup} can be strengthened to
immediate dominance tests as follows:
\begin{eqnarray}
\mbox{DF}_{\mbox{\scriptsize local}}(X) & = &
             \left\{ Y \in \mbox{Succ}(X) \left| X \NIDOM Y \right. \right\}
\label{eqn:dflocal2} \\
\mbox{DF}_{\mbox{\scriptsize up}}(Z)    & = &
             \left\{ Y \in \mbox{DF}(Z) \left| X \NIDOM Y \right. \right\}
\label{eqn:dfup2}
\end{eqnarray}
This simplifies computations, because immediate dominators will be encoded
directly in any sensible representation of the dominance tree.

\begin{proof}
To prove \ref{eqn:dflocal2} we show that if $Y \in \mbox{Succ}(X)$
\begin{equation}
X \SDOM Y \Leftrightarrow X \IDOM Y
\label{eqn:sdomisidom}
\end{equation}
The $\Leftarrow$ part follows trivially from the definition of $\IDOM$.
For the $\Rightarrow$ part suppose $X \SDOM Y$.  Then by consideration
of the dominance tree, either 1) $X \IDOM Y$ or 2) there exists some $V$
such that $X \IDOM V$ and $V \SDOM Y$ (ie, either $Y$ is an immediate
child of $X$, or there is some intervening node in the dominance tree).
But if $V$ strictly dominates $Y$ it dominates its predecessor $X$, and
and $V \DOM X$ contradicts $X \IDOM V$, due to the antisymmetry of
the dominance.  So 2) is impossible and we must have $X \IDOM V$.

To prove \ref{eqn:dfup2} we show that $Y \in \mbox{DF}(Z)$ also leads to
Equation \ref{eqn:sdomisidom}.  Again the $\Leftarrow$ part is trivial.
The proof that $X \SDOM Y \Rightarrow X \IDOM Y$ is sketched in Figure
\ref{fig:dfcons}.
\end{proof}

\begin{figure*}[p]
\centerline{\psfig{figure=dfcons.eps,height=5in}}
\caption{$Y \in \mbox{DF}(Z)$ and $X \SDOM Y$ implies $X \IDOM Y$.
\label{fig:dfcons}}
\end{figure*}

Equations \ref{eqn:dfformula}, \ref{eqn:dflocal2} and \ref{eqn:dfup2} 
immediately give an algorithm for computing the dominance frontiers
by post-order (bottom up) traversal of the dominance tree.

\section{Reduction to Minimal SSA form}

A program is in Static Single Assignment (SSA) form if the program
text contains only a single assignment to each variable appearing in
the program.  Converting a general program to SSA generally involves
adding assignments of {\em $\phi$-expressions} to some variables.
In a node $X$ that has $n$ CFG predecessors, any $\phi$-expression must
have $n$ arguments.  In a program execution where control enters a
node from predecessor $i$, the run-time value of a $\phi$-expression is
the value of its $i$-th argument.

To reach Minimal Static Single Assignment we place a trivial $\phi$-term
\begin{tabbing}
\verb$    V = $$\phi$\verb$(V, ..., V)$
\end{tabbing}
at the entry of any node of the control flow graph belonging to
$\mbox{J}^+(S)$, where $S$ is the set of nodes containing an assignment
to $V$---it includes {\em Entry} because we can assume each
variable gets a default, possibly undefined, value at the start of
the program.  According to Theorem \ref{thm:DFisJ} the set of nodes
requiring $\phi$-terms is identical to $\mbox{DF}^+(S)$.  After placing
$\phi$-terms, each occurrence of a variable $V$ anywhere in the program
is replaced by an occurrence of a new variable $V_i$, such that the
original semantics of the program is unchanged, but the new program text
only contains one assignment to $V_i$.
\begin{lemma}
Consider a path $p:\mbox{\em Entry} \stackrel{+}{\rightarrow} Y$
and assume $Y \notin \mbox{DF}^+(S)$ for some set of nodes, $S$, that
includes {\em Entry}.  Then the last node on $p$ before its endpoint
that belongs to $S \cup \mbox{DF}^+(S)$ strictly dominates $Y$.
\end{lemma}
\begin{proof}
Similar to proof of Lemma \ref{lem:indfplus}.
Let $X'$ be the last node on the path before the endpoint that
belongs to $S \cup \mbox{DF}^+(S)$.  $X'$ exists because {\em Entry} is in $S$.
No node following $X'$ on $p$ is in $\mbox{DF}(X')$ (or else it would
be in $\mbox{DF}^+(S)$).  The result follows.
\end{proof}
\begin{corollary}
If a program is in Minimal SSA form and a CFG node $Y$ does {\em not}
have a $\phi$-term for $V$, the last assignment to $V$ before entering
$Y$ by any path of program execution occurs in a CFG node that
strictly dominates $Y$.
\end{corollary}
\begin{proof}
Immediate from the preceding lemma.  Identify $S$ with the set of nodes
containing ordinary assignments to $V$ and $\mbox{DF}^+(S)$ with the
set of nodes containing  $\phi$-terms for $V$.  Since $Y$ does not have
a $\phi$-term for $V$ it is not in $\mbox{DF}^+(S)$.
\end{proof}

This corollary is the basis of an efficient algorithm for renaming
variables to convert a program to static single assignment form
(Figure \ref{fig:renaming}).
Due to the corollary, a pre-order (top down) traversal of the 
dominance tree achieves the required effect.

\begin{figure*}[p]
\small
\begin{tabbing}
\verb$  for each variable $$V$\verb$ do$ \\
\verb$      $$\mbox{C}(V) \leftarrow 0 $ \\
\verb$      $$\mbox{Version}(V) \leftarrow 0 $ \\
\verb$  end $ \\
\verb$  call $$\mbox{SEARCH}(\mbox{\em Entry})$ \\
\\
\verb$  $$\mbox{SEARCH}(X)$\verb$ :$ \\
\verb$      save current state of $$\mbox{Version}(V)$\verb$ for variables assigned in $$X$ \\
\\
\verb$      /* local processing */$ \\
\verb$      for each statement $$A$\verb$ in $$X$\verb$ do$ \\
\verb$          for each variable $$V$\verb$ used in an ordinary expression in $$A$\verb$ do$ \\
\verb$              replace use of $$V$\verb$ by $$V_i$, where $i = \mbox{Version}(V)$ \\
\verb$          end$ \\
\verb$          for each variable $$V$\verb$ assigned by $$A$\verb$ do$ \\
\verb$              $$\mbox{C}(V) \leftarrow \mbox{C}(V) + 1$ \\
\verb$              $$\mbox{Version}(V) \leftarrow \mbox{C}(V) $ \\
\verb$              replace def of $$V$\verb$ by $$V_i$, where $i = \mbox{Version}(V)$ \\
\verb$          end$ \\
\verb$      end$ \\
\\
\verb$      /* process $$\phi$\verb$-terms in successors */$ \\
\verb$      for each $$Y \in \mbox{Succ}(X)$\verb$ do$ \\
\verb$          $$j \leftarrow \mbox{WhichPred}(X,Y) $ \\
\verb$          for each $$\phi$\verb$-expression in $$Y$\verb$ do$ \\
\verb$              replace $$j$\verb$-th argument, $$V$\verb$, by $$V_i$\verb$, where $$i = \mbox{Version}(V)$ \\
\verb$          end$ \\
\verb$      end$ \\
\\
\verb$      for each $$Y \in \mbox{Children}(X)$\verb$ do$ \\
\verb$          call $$\mbox{SEARCH}(Y)$ \\
\verb$      end $ \\
\\
\verb$      restore entry state of $$\mbox{Version}(V)$\verb$ for variables assigned in $$X$ \\
\verb$  end $$\mbox{SEARCH}$
\end{tabbing}
\normalsize
\caption{Algorithm for renaming variables in reduction to SSA.
\label{fig:renaming}}
\end{figure*}

\end{document}
