Merge branch 'three-eight' of linux:/r/c--/papers/dfopt into three-eight
authorJoao Dias <dias@cs.tufts.edu>
Mon, 26 Jul 2010 22:06:59 +0000 (18:06 -0400)
committerJoao Dias <dias@cs.tufts.edu>
Mon, 26 Jul 2010 22:06:59 +0000 (18:06 -0400)
paper/dfopt.tex

index 24429fd..c2e11e4 100644 (file)
@@ -751,10 +751,6 @@ As~described in \secref{checkpoint-monad},
 \hoopl~manages speculation with cooperation from the client.
 
 
-\paragraph{Cognitive costs of interleaving}
-
-\remark{I'm not entirely pleased with this subsection title}
-\simon{Me neither: nuke?}
 \seclabel{debugging-introduced}
 
 While it is wonderful that we can implement complex optimizations by
@@ -802,14 +798,12 @@ control cannot fall through to the next instruction).
 \item A label is closed on entry (because in \ourlib{} we do not allow
 control to fall through into a branch target), but open on exit.
 \item
-A~function call should be closed on exit,
-because control can flow from a call site to multiple points:
-for example, a~return continuation or an exception handler.
-(And~after optimization, distinct call sites may share a return
-continuation.)
-\simon{I think this is pretty confusing. A reader might well
-think that a call should be open on entry and exit, and it requires
-more explanation to say why not.}
+A~function call could, if the language being compiled is simple
+ enough, be open on entry and  exit.
+But if a function could return in multiple ways---for example by
+ transferring either to a normal return continuation or to an
+ exception handler---then a function call will have to be represented
+ by a node that is closed at exit.
 \end{itemize}
 % This taxonomy enables \ourlib{} to enforce invariants:
 % only nodes closed on entry can be the targets of branches, and only nodes closed
@@ -973,6 +967,8 @@ class `NonLocal n where
 \ourlib\ combines the client's nodes into
 blocks and graphs, which, unlike the nodes, are defined by \ourlib{}
  (\figref{graph}).
+\remark{Add to the figure: type LabelMap, addBlock, blockUnion (from
+ mapUnion)---squeeze in if there is room.}
 A~@Block@ is parameterized over the node type~@n@
 as well as over the same flag types that make it open or closed at
 entry and exit.
@@ -1117,12 +1113,11 @@ them
 with @BCat@ to produce a closed/closed block~@b@, which is
 added to the body of the result.
 
-The representation of @Graph@s is exposed to \hoopl's clients.\finalremark{This \P\ is a candidate to be cut.}
-\simon{Right.  If we don't talk about Blocks being exposed, why tackle Graphs? as it stands
-it's inconsistent. Moreover, the stuff that follows is a non-sequitur; needs a new para.}
 We~have carefully crafted the types so that if @BCat@ 
 is considered as an associative operator, 
 every graph has a unique representation.
+\finalremark{This \P\ is a candidate to be cut.}
+\simon{Right}
 %%  \simon{Well, you were the one who was so keen on a unique representation!
 %%  And since we have one, I think tis useful to say so. Lastly, the representation of
 %%  singleton blocks is not entirely obvious.}
@@ -1158,6 +1153,9 @@ to a client which representation to choose---or if the choice made a difference.
 
 \subsection{Labels and successors} \seclabel{nonlocal-class}
 
+\remark{Becomes ``Edges, labels, and successors.'' Absorbs ``3.4
+control-flow edges and program points}
+
 
 Although \ourlib{} is polymorphic in the type of nodes, 
 it~still needs to know how a node may transfer control from one
@@ -1717,83 +1715,73 @@ to insert infinitely many spills.
 
 
 
-\seclabel{rewrite-as-sequence}
-
 An~innovation of \hoopl\ is to build the choice of shallow or deep
-rewriting into each rewrite function, through the use of combinators.
-To~explain these combinators, 
-we model
-a~rewrite function of type @FwdRewrite m n f@ 
-as a potentially infinite sequence of functions of type
-\begin{code}
- forall e x . n e x -> f -> m (Maybe graph n e x).
-\end{code}
-When we apply a rewrite function to a node and a fact,
-we choose the first function in the sequence that returns $@Just@\;g$,
-and we recursively analyze and rewrite~$g$ using the remaining
-functions in the sequence. 
+rewriting into each rewrite function, through the use of the four
+combinators
+@mkFRewrite@, @thenFwdRw@, @iterFwdRw@, and @noFwdRw@ shown in
+\figref{api}. 
+Every rewrite function is made with these combinators,
+and its behavior is characterized by the answers to two questions:
+does the  function rewrite a~node, and if so, what rewrite function
+should be used to recursively analyze the replacement graph.
+To~answer these questions precisely, we offer a model of rewrite
+functions as an algebraic datatype:
 \begin{smallcode}
-rewrite :: FwdRewrite' n f -> -> n e x -> f
-        -> Maybe (Graph n e x, FwdRewrite' n f)
-rewrite rs node f = rew rs Just Nothing
- where
-  rew No     j n = n
-  rew (Mk r) j n =
-     case r node f of Nothing -> n
-                      Just g -> j (g, No)
-  rew (r1 `Then` r2) j n = rew r1 (j . add r2) (rew r2 j n)
-  rew (Iter r)       j n = rew r (j . add (Iter r)) n
-  add tail (g, r) = (g, r `Then` tail)
+data Rw a = Mk a | Then (Rw a) (Rw a) | Iter (Rw a) | No
 \end{smallcode}
-\vfil\break
-And here's the monadic version.
-Is this simpler than what we have?
+Using this model, we specify how a rewrite function works by
+giving a reference implementation.
+The code is in continuation-passing style;
+the first continuation~@j@ accepts a result where the graph is
+rewritten,
+and the second continuation~@n@ is the result when the graph is not
+rewritten.
 \begin{smallcode}
 rewrite :: Monad m => FwdRewrite m n f -> -> n e x -> f
         -> m (Maybe (Graph n e x, FwdRewrite m n f))
 rewrite rs node f = rew rs (return . Just) (return Nothing)
  where
-  rew No     j n = n
   rew (Mk r) j n = do mg <- r node f
                       case mg of Nothing -> n
                                  Just g -> j (g, No)
   rew (r1 `Then` r2) j n = rew r1 (j . add r2) (rew r2 j n)
   rew (Iter r)       j n = rew r (j . add (Iter r)) n
+  rew No             j n = n
   add tail (g, r) = (g, r `Then` tail)
 \end{smallcode}
-If~all functions in the sequence return @Nothing@, rewriting returns
-@Nothing@.
-The~model works because we needn't \emph{actually} check an infinite
-sequence of functions to see if they all return @Nothing@:
-even though the sequence in the model
-can be infinite, it has only finitely many distinct elements---and our
-implementation carefully avoids representing the infinite sequence.
-With~this model in mind, we can explain the combinators that \hoopl\
-provides for rewrite functions.
-
-A~function returned by @mkFRewrite@ returns a singleton sequence,
-which corresponds exactly to shallow rewriting.
-Rewriting can be made deep by making a sequence infinite;
-function
-\begin{code}
- `iterFwdRw :: FwdRewrite m n f -> FwdRewrite m n f
-\end{code}
-behaves on rewrite functions the way @cycle@ does on lists,
-repeating the elements infinitely often.
+Appealing to this model, we see that
+\begin{itemize}
+\item
+A~function returned by @mkFRewrite@ never rewrites a replacement
+graph---this behavior is shallow rewriting.
+\item
+When a~function @r1 `thenFwdRw` r2@ is applied to a node,
+if @r1@ replaces the node, then @r2@~is used to transform the
+replacement graph.
+And~if @r1@~does not replace the node, \hoopl\ tries~@r2@.
+\item
+When a~function @iterFwdRw r@ rewrites a node, then @iterFwdRw r@ is
+used to transform the replacement graph---this behavior is deep
+rewriting.
+But~if @r1@~does not replace the node, \hoopl\ returns @Nothing@.
+\item
+Finally, @noFwdRw@ never replaces a graph.
+\end{itemize}
 For~convenience, we~also provide the~function @`deepFwdRw@,
 which is the composition of @iterFwdRw@ and~@mkFRewrite@.
+\remark{maybe some of the real type signatures ought to be repeated?}
+
+%%  \begin{code}
+%%   `iterFwdRw :: FwdRewrite m n f -> FwdRewrite m n f
+%%  \end{code}
+
+%%  To try multiple rewrite functions in sequence,
+%%  provided they all use the same type of fact, \hoopl\ combines them with
+%%  \verbatiminput{comb1}
+%%  % defn thenFwdRw
+%%  Rewrite function @r1 `thenFwdRw` r2@ first does the rewrites of~@r1@,
+%%  then the rewrites of~@r2@.
 
-To try multiple rewrite functions in sequence,\remark{Horrendous page
-break will need fixing}
-provided they all use the same type of fact, \hoopl\ combines them with
-\verbatiminput{comb1}
-% defn thenFwdRw
-Rewrite function @r1 `thenFwdRw` r2@ first does the rewrites of~@r1@,
-then the rewrites of~@r2@.
-It~behaves on rewrite functions the way @++@~behaves on lists.
-Finally, 
-@noFwdRw@ is the identity of @thenFwdRw@, and it
-corresponds to an empty sequence of rewrite functions.
 %%  
 %%  
 %%  by using
@@ -1803,13 +1791,16 @@ corresponds to an empty sequence of rewrite functions.
 %%  \hoopl\ makes it easy for a client to combine multiple rewrite
 %%  functions that use the same fact:
 
-Our combinators satisfy the algebraic laws that you would expect, including
+Our combinators satisfy the algebraic laws that you would expect;
+for~example 
+@noFwdRw@ is a left and right identity of @thenFwdRw@.
+A~more interesting law is
 \begin{code}
   iterFwdRw r = r `thenFwdRw` iterFwdRw r
 \end{code}
-Unfortunately, this equation cannot be used to \emph{define}
+Unfortunately, this law cannot be used to \emph{define}
 @iterFwdRw@:
-if~we used this equation to define @iterFwdRw@, then when @r@ returned @Nothing@,
+if~we used this law to define @iterFwdRw@, then when @r@ returned @Nothing@,
 @iterFwdRw r@ would diverge.
 
 
@@ -2421,7 +2412,7 @@ the private function @arfGraph@, which is short for ``analyze and rewrite
 forward graph:''
 \begin{smallfuzzcode}{15.1pt}
 `arfGraph
- :: forall m n f e x. (FuelMonad m, NonLocal n)
+ :: forall m n f e x. (CkpointMonad m, NonLocal n)
  => FwdPass m n f    -- lattice, transfers, rewrites
  -> MaybeC e [Label] -- entry points for a closed graph
  -> Graph n e x      -- the original graph
@@ -2592,9 +2583,8 @@ fixed points.
 \seclabel{block-impl}
 
 Extended fact transformers compose nicely.
-For example, @block@ is implemented thus: \simon{we don't need the foralls? save a line}
-\simon{How can block have no Monad m constraint, while cat does?}
-%\ifpagetuning\par\vfilbreak[1in]\fi  % horrible page break
+For example, @block@ is implemented thus:
+% we need the foralls
 \begin{smallcode}
   `block :: forall e x .
             Block n e x -> f -> m (DG f n e x, Fact x f)
@@ -2607,10 +2597,10 @@ The composition function @cat@ feeds facts from one extended fact
 transformer to another, and it splices decorated graphs.
 It~has a very general type:
 \begin{smallcode}
-  cat :: forall m e a x f f1 f2. Monad m 
-      => (f  -> m (DG f n e a, f1))
-      -> (f1 -> m (DG f n a x, f2))
-      -> (f  -> m (DG f n e x, f2))
+  cat :: forall e a x f1 f2 f3. 
+         (f1 -> m (DG f n e a, f2))
+      -> (f2 -> m (DG f n a x, f3))
+      -> (f1 -> m (DG f n e x, f3))
   `cat ^ft1 ^ft2 f = do { (g1,f1) <- ft1 f
                      ; (g2,f2) <- ft2 f1
                      ; return (g1 `dgSplice` g2, f2) }
@@ -2705,8 +2695,8 @@ Function @graph@ is much like @block@, but it has more cases.
 \subsection{Analyzing and rewriting nodes} \seclabel{arf-node}
 
 The @node@ function is where we interleave analysis with rewriting:
-\remark{Implementation of rewriting is finally revealed---needs to be earlier}
-\simon{need defn of FwdGraphAndTail. Why not combine it with the Maybe?}
+\simon{NR: FwdGraphAndTail can be expunged and replaced with a simple pair
+type}
 \smallfuzzverbatiminput{15.1pt}{node}
 % defn ShapeLifter
 % defn singletonDG
@@ -3158,7 +3148,7 @@ comparison with a library using a mutable control-flow graph
 \cite{ramsey-dias:applicative-flow-graph}. 
 
 Although thorough evaluation of \hoopl's performance must await
-future work, we can identify some design decisions that affect
+future work, we can identify some design decisions that might affect
 performance. \simon{I think it's highly speculative whether these issues
 are anywhere near the high-order bit of performance.  Candidate for cutting
 if you ask me.}
@@ -3206,7 +3196,7 @@ performance.
 In summary, \hoopl\ performs well enough for use in~GHC,
 but there is much we don't know. Systematic investigation
 is indicated.
-
+\remark{We have no evidence that any of the above actually affects performance}
 
 
 \section{Discussion}
@@ -3305,13 +3295,13 @@ Because of this separation of concerns,
 we believe our implementation will be much easier to maintain than
 anything that preceded~it.
 
-Another good sign is that we have been able to make substantial
-changes in the implementation without changing the API.
-For example, in addition to ``@concatMap@ style,'' we have also
-implemented @arfGraph@ in ``fold style'' and in continuation-passing
-style.
-Which style is preferred is a matter of taste, and possibly
-a matter of  performance.
+%%  Another good sign is that we have been able to make substantial
+%%  changes in the implementation without changing the API.
+%%  For example, in addition to ``@concatMap@ style,'' we have also
+%%  implemented @arfGraph@ in ``fold style'' and in continuation-passing
+%%  style.
+%%  Which style is preferred is a matter of taste, and possibly
+%%  a matter of  performance.
 
 
 
@@ -3517,22 +3507,22 @@ fuel is exhausted. This would leave the user free to use a more
 exotic fuel monad, such as one supporting several supplies of fuel for
 different sorts of rewrites.  
 
-\simon{These next two paras are incomprehensible. Cut?}
-Of the many varied implementations we have tried,
-we have space only to raise a few questions, with even fewer answers.
-%
-An~earlier implementation of @fixpoint@ stored the
-``current'' @FactBase@ in a monad; we~find it easier to understand and
-maintain the code that passes the current @FactBase@ as an argument.
-Among @concatMap@ style, fold style, and continuation-passing style, 
-which is best?
-No~one of these styles makes all the code easiest to read
-and understand: @concatMap@ style is relatively straightforward throughout;
-fold~style is similar overall but different in detail;
-and continuation-passing style is clear and elegant to those who
-like continuations, but baffling to those who don't.
-
-Which value constructors should be
+%%  \simon{These next two paras are incomprehensible. Cut?}
+%%  Of the many varied implementations we have tried,
+%%  we have space only to raise a few questions, with even fewer answers.
+%%  %
+%%  An~earlier implementation of @fixpoint@ stored the
+%%  ``current'' @FactBase@ in a monad; we~find it easier to understand and
+%%  maintain the code that passes the current @FactBase@ as an argument.
+%%  Among @concatMap@ style, fold style, and continuation-passing style, 
+%%  which is best?
+%%  No~one of these styles makes all the code easiest to read
+%%  and understand: @concatMap@ style is relatively straightforward throughout;
+%%  fold~style is similar overall but different in detail;
+%%  and continuation-passing style is clear and elegant to those who
+%%  like continuations, but baffling to those who don't.
+
+Which value constructors should be\simon{still incomprehensible.  cut?}
 polymorphic in the shapes of their arguments, and which should be
 monomorphic?
 We~experimented with a polymorphic