removed verbiage about soundness and termination. just the bare facts remain
authorNorman Ramsey <nr@cs.tufts.edu>
Thu, 10 Jun 2010 01:39:23 +0000 (21:39 -0400)
committerNorman Ramsey <nr@cs.tufts.edu>
Thu, 10 Jun 2010 01:39:23 +0000 (21:39 -0400)
paper/dfopt.tex

index 68f28f7..27c8deb 100644 (file)
@@ -2090,44 +2090,46 @@ that is, \mbox{@`transfer n f@ $\sqsubseteq$ @transfer g f@}.
 For example, if the analysis says that @x@ is dead before the node~@n@,
 then it had better still be dead if @n@ is replaced by @g@.
 \item 
-To ensure termination, a transformation that uses deep rewriting
-must not return replacement graphs which 
-contain nodes that could be rewritten indefinitely.
+%  To ensure termination, 
+A transformation that uses deep rewriting
+must not return a replacement graph which
+contains a node that could be rewritten indefinitely.
 \end{itemize}
-Without the conditions on monotonicity and consistency,
-our algorithm will terminate, 
-but there is no guarantee that it will compute
-a fixed point of the analysis.  And that in turn threatens the
-soundness of rewrites based on possibly bogus ``facts''.
-
-However, when the preconditions above are met,
-\begin{itemize} 
-\item
-The algorithm terminates.  The fixed-point loop must terminate because the 
-lattice has no infinite ascending chains. And the client is responsible
-for avoiding infinite recursion when deep rewriting is used.
-\item 
-The algorithm is sound.  Why? Because if each rewrite is sound (in the sense given above), 
-then applying a succession of rewrites is also sound.
-Moreover, a~sound analysis of the replacement graph
-may generate only dataflow facts that could have been
-generated by a more complicated analysis of the original graph.
-\end{itemize}
-
-\finalremark{Doesn't the rewrite have to be have the following property:
-for a forward analysis/transform, if (rewrite P s) = Just s',
-then (transfer P s $\sqsubseteq$ transfer P s').
-For backward: if (rewrite Q s) = Just s', then (transfer Q s' $\sqsubseteq$ transfer Q s).
-Works for liveness.
-``It works for liveness, so it must be true'' (NR).
-If this is true, it's worth a QuickCheck property!
-}%
-\finalremark{Version 2, after further rumination.  Let's define
-$\scriptstyle \mathit{rt}(f,s) = \mathit{transform}(f, \mathit{rewrite}(f,s))$.
- Then $\mathit{rt}$ should
-be monotonic in~$f$.  We think this is true of liveness, but we are not sure
-whether it's just a generally good idea, or whether it's actually a 
-precondition for some (as yet unarticulated) property of \ourlib{} to hold.}%
+%%  Without the conditions on monotonicity and consistency,
+%%  our algorithm will terminate, 
+%%  but there is no guarantee that it will compute
+%%  a fixed point of the analysis.  And that in turn threatens the
+%%  soundness of rewrites based on possibly bogus ``facts''.
+Under these conditions, the algorithm terminates and is
+sound.
+%%  
+%%  \begin{itemize} 
+%%  \item
+%%  The algorithm terminates.  The fixed-point loop must terminate because the 
+%%  lattice has no infinite ascending chains. And the client is responsible
+%%  for avoiding infinite recursion when deep rewriting is used.
+%%  \item 
+%%  The algorithm is sound.  Why? Because if each rewrite is sound (in the sense given above), 
+%%  then applying a succession of rewrites is also sound.
+%%  Moreover, a~sound analysis of the replacement graph
+%%  may generate only dataflow facts that could have been
+%%  generated by a more complicated analysis of the original graph.
+%%  \end{itemize}
+%%  
+%%  \finalremark{Doesn't the rewrite have to be have the following property:
+%%  for a forward analysis/transform, if (rewrite P s) = Just s',
+%%  then (transfer P s $\sqsubseteq$ transfer P s').
+%%  For backward: if (rewrite Q s) = Just s', then (transfer Q s' $\sqsubseteq$ transfer Q s).
+%%  Works for liveness.
+%%  ``It works for liveness, so it must be true'' (NR).
+%%  If this is true, it's worth a QuickCheck property!
+%%  }%
+%%  \finalremark{Version 2, after further rumination.  Let's define
+%%  $\scriptstyle \mathit{rt}(f,s) = \mathit{transform}(f, \mathit{rewrite}(f,s))$.
+%%   Then $\mathit{rt}$ should
+%%  be monotonic in~$f$.  We think this is true of liveness, but we are not sure
+%%  whether it's just a generally good idea, or whether it's actually a 
+%%  precondition for some (as yet unarticulated) property of \ourlib{} to hold.}%
 
 %%%%    \simon{The rewrite functions must presumably satisfy
 %%%%    some monotonicity property.  Something like: given a more informative