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)
1  2 
paper/dfopt.tex

diff --combined paper/dfopt.tex
@@@ -637,9 -637,9 +637,9 @@@ As~a concrete example, we show constan
  folding. 
  On the left we show a basic block; in the middle we show
  facts that hold between statements (or \emph{nodes}) 
 -in the block; and at
 +in the block; and on
  the right we show the result of transforming the block 
 -based on the assertions:
 +based on the facts:
  \begin{verbatim}
        Before        Facts        After
            ------------{}-------------
@@@ -707,8 -707,8 +707,8 @@@ replaces the node @x:=e@ with a no-op
  
  \seclabel{simple-tx}
  \paragraph{Interleaved transformation and analysis.}
 -Our first example \emph{interleaves} analysis (constant propagation) 
 -and transformation (constant folding).
 +Our first example \emph{interleaves} analysis and transformation.
 +% constant propagation is a transformation, not an analysis
  Interleaving makes it far easier to write effective analyses.
  If, instead, we \emph{first} analyzed the block
  and \emph{then} transformed it, the analysis would have to ``predict''
@@@ -751,10 -751,6 +751,6 @@@ As~described in \secref{checkpoint-mona
  \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 +798,12 @@@ control cannot fall through to the nex
  \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
@@@ -886,7 -880,7 +880,7 @@@ data `Node e x wher
  
  The type of a node specifies \emph{at compile time} whether the node is open or
  closed on entry and exit. Concretely,
 -the node type constructor has kind @*->*->*@, where the two type parameters
 +the type constructor for a node has kind @*->*->*@, where the two type parameters
  are type-level flags, one for entry and one for exit.
  Such a type parameter may be instantiated only with type @O@~(for
  open) or type~@C@ (for closed).
@@@ -973,6 -967,8 +967,8 @@@ class `NonLocal n wher
  \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.
@@@ -1062,7 -1058,7 +1058,7 @@@ the type @MaybeO O a@ is isomorphic to~
  the type @MaybeO C a@ is isomorphic to~@()@.
  \item 
  The \emph{body} of the graph is a collection of  closed/closed blocks.  
 -To~facilitate traversal of the graph, we represent a body as a finite
 +To~facilitate traversal of the graph, we represent the body as a finite
  map from label to block. 
  \simon{{\tt LabelMap} not defined in Fig 2}
  \item 
  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 +1153,9 @@@ to a client which representation to cho
  
  \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 +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
  %%  \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 +2412,7 @@@ the private function @arfGraph@, which 
  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 +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 +2597,10 @@@ The composition function @cat@ feeds fa
  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 +2695,8 @@@ Function @graph@ is much like @block@, 
  \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 +3148,7 @@@ comparison with a library using a mutab
  \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 +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}
@@@ -3248,7 -3238,7 +3238,7 @@@ so when implemented in \hoopl
  
  \paragraph{Examining the API}
  
 -We hope the our presentation of the API in \secref{api} speaks for
 +We hope that our presentation of the API in \secref{api} speaks for
  itself,
  but there are a couple of properties we think are worth highlighting.
  First, it's a good sign that the API provides many higher-order
@@@ -3305,13 -3295,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.
  
  
  
@@@ -3493,7 -3483,7 +3483,7 @@@ a client wanted one set o
  unique names for labels and a different set for registers?
  Moreover, a client might want a rewrite to perform other actions
  entirely that could not be anticipated by \hoopl{}.
 -For exampe, in order to judge the effectiveness of an optimization,
 +For example, in order to judge the effectiveness of an optimization,
  a client might want to log how many rewrites take place, or in what
  functions they take place.
  As~a more ambitious example, \citet{runciman:increasing-prs} describes
@@@ -3517,22 -3507,22 +3507,22 @@@ fuel is exhausted. This would leave th
  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