contification paper

[Matthew Fluet]

> > - I assume that sticking to the level of detail that Steve used in the
> > messages to John Reppy would be good: i.e., drop the HandlerPush and
> > HandlerPop declarations, don't worry about the globals and datatypes, etc. 
> > Also, introduce mutual recursion among continuation delclarations. 
> 
> Sounds good to me.  If it's not too bad, I wouldn't mind seeing handler push and 
> pop, because I think it's neat how MLton handles handlers.  I've not seen it
> done that way before.  But that probably belongs in a separate paper that
> describes the CPS IL, handler inference, and the raise-to-jump optimization.

Looking at the outline, I think we'll be good on length without bringing
in handlers.  And, they are completely transparent to the analyses, so I
don't think they add much in this context.

> > An analysis A is cyclic if
> >  there exists f0, ..., fn in Fun such that fi_1 = A(fi) and f0 = fn.
> > An analysis A is acyclic if A is not cyclic.
> > 
> > I've also got a proof that any minimal safe analysis is acyclic.  This
> > proof motivates the additional minimality requirement on Uncalled
> > functions: any cycle in an analysis should really have all those functions
> > as Uncalled.
> 
> Since you have that proof, perhaps the framework would be simpler to understand
> if we just defined cyclic up front and imposed it as a condition of safety.
> After all, the whole idea is that safety is supposed to imply the transformation 
> can work.

Maybe.  I don't think there is a problem introducing acyclicity as a
condition on safety.  All of the analyses that we're considering are
obviously acyclic.  The only caveat is that the proof goes as follows: if
an analysis A has a cycle, then not(Reach(fi)) for all fi.  Therefore
Adom(fi) = Uncalled (where Adom is the safe, dominator based analysis).
By assumption, A was minimal, so Adom(fi) = Uncalled => A(fi) = Uncalled,
contradicting A(fi) = fi+1.  Therefore, there are no cycles and A is
acyclic.  (Note, we only use the safety of Adom, not acyclicity, although
Adom is acyclic by definition).

On the other hand, we really should be a little more precise about cycles.
For example, we could have the following:

fun fm () = ...
fun f () = ... K (g) ...
fun g () = ... f () ...

and A(f) = g, A(g) = K is safe, although not minimal, and not "acyclic" in
the sense that the transformation can't be performed.  I'll think a little
more about this and see if I can't hammer out something more precise.

> I'd like to see the transformation spelled out in more detail, including the
> call rewriting and the ordering.  Since the acyclicity gives us the ordering, I
> think we should be able to write a one pass recursive translation in a
> mathematical enough style.

Agreed.

> > - I think it is worth arguing that the resulting program is still
> > lexically scoped.  Is there anything else short of a full proof of
> > correctness that would be worth mentioning?
> 
> Maybe type correctness of resulting program.

I thought about this, but this will mean complicating the CPS IL a little.
On the other hand, it probably won't be too hard; a function contified in
another function doesn't change types at all; a function contified at a
continuation changes it's return type, but corresponding calls also
change.

> > 6. Results and Reality
> 
> Maybe the right thing to compare is the five analyses
> 
> 	none	call	cont	call+cont	dom
> 
> I'm wavering on including call+cont.

I agree.  The results there aren't much different than anywhere else.

> > - The runtimes aren't as impressive:
...
> 
> Is this for the dom based on A*/parent, right?  Should we instead report the
> dom based on ancestor, with a note that it's actually weaker due to the mutual
> recursion problem?

Yes, it is based on A*/parent.  The fact that the transformation accepts
any A* safe analysis doesn't affect the transformation that's done when
the dominator analysis uses ancestor (i.e., we won't be able to contify
those two functions in logic).  It's a trivial change to run the parent
analysis (I should just extend the contifyStrategy control) and get the
numbers there.

I'll make one other comment.  When run with the call analysis, the new
transformation is not identical to the old transformation.  Essentially,
this is another nesting issue: 

Eg.
fun g () = ...
fun f () = let fun L1 () = let in g () in L1 () end

Using the old transformation, contifying g in f yields:

fun f () = let fun L1 () = let fun g () = ... in g () in L1 () end

Using the new transformation, contifying g in f yields:

fun f () = let fun g () = ... ; fun L1 () = let in g () in L1 () end

Essentially, the old transformation just found the one outside call and
dropped the definition in the closest set of definitions.  The new
transformation know that g is to be contified in f, so it's added before
the original local functions of f.  There's no difference in runtimes
between the old and new transformations, and virtually no difference in
code size.

> It's weird that dom isn't consistently call.  We need to talk somewhere about
> the three rounds of contification and the fact that although dom will contify
> more than call on any given input, that after three rounds it doesn't matter.

That's not completely true.  There are plenty of examples where dom and
call both find no contifiable functions in the last round, but the number
of functions in the last round are different.  Even if we turned on the
dom analysis for the last round after two rounds of call, the intervening
optimizations might have made some of those functions uncontifiable; i.e.,
we missed our chance on one of the first two rounds.