cps & contification

[Matthew Fluet]

> Here is my attempt at defining "safety" constraints for contification.
> 
> Abstractly, a program consists of a main function and a set of tail and nontail
> calls.  A tail call consists of a caller and a callee.  A nontail call consists
> of a caller, callee, and jump.
> 
> 	j in	Jump
> 	f in	Fun
> 		TailCall = Fun x Fun
> 		NonTailCall = Fun x Fun x Jump
> 	p in	Program = Fun x P(TailCall) x P (NonTailCall)

Just to make sure I have the terminology correct:

(f,g) in TailCall corresponds to something like:

fun f (...)
  = let
      fun L_1 (...)
        = g(...)
      fun L_2 (...)
        = ...
    in
      case 
        of true => L_1 | false => L_2
    end

I.e., the caller is f and the callee is g, with no notion that g is
really being called in L_1? or even deeper lexical nesting?

Second question, relating to the safety constraints below, is it possible
for a local function to be unused?  If so, then although g is
called in L_1, it may not be the case that g is really called by f.


(f,g,j) in NonTailCall corresponds to something like:

fun f (...)
  = let
      fun L_1 (...)
        = ...
      fun L_2 (...)
        = L_1(g(...))
    in
      ...
    end

Again, no notion that g is really being called in L_2, although it is
returning to the continuation L_1?  How about the possibility that L_2 is
never called; in which case does g really ever return to L_1?

> An analysis is a map from functions to the continuation that they return to.
> 
> 	A in Fun -> {Uncalled, Unknown} U Jump U Fun
> 
> Here is the intended meaning of A.
> 
> 	A(f)		meaning
> 	--------	------------------------------------------------
> 	Uncalled	f is never called during evaluation of the program
> 	Unknown		f may returns to different places
> 	j		f always returns to continuation j
> 	g		f always returns to function g
> 
> I now define a sufficient condition, called "safe", on an analysis in order for
> the contification transformation to be correct.
> 
> An analysis A is safe for program p = (fm, T, N) if 
> 	*   A(fm) = fm

Does        A(fm) = Unknown
make more sense?  I wouldn't think that the interpretation that the main
function fm always returns to fm is what we want to say; because the next
step would be to say that if A(g) = f in Fun, then g is contifiable in f.

> 	**  For all nontail calls (f, g, j) in N, either
> 		A(f) = Uncalled
> 		or A(g) in {Uncalled, Unknown, j}
> 	*** For all tail calls (f, g) in T, either 
> 		A(f) = Uncalled
> 		or A(g) in {Unknown, f, A(f)}

Assuming an exclusive or, if A(f) <> Uncalled, why can A(g) = Uncalled in
non-tail calls but not in tail calls.  This ties back to the question I
asked above, about whether local-functions can be unused.  If they can be
unused, then it seems that both calls could have A(g) = Uncalled.  On the
other hand, if local functions are always used, then in non-tail calls,
maybe we can have A(g) in {Unknown, j}.

> 3. If A(f) in Jump and there is a path of tail calls from f to g
>    then A(g) in {Unknown, A(f)} U Fun
> 	Proof: by induction on the length of the path.

Does this fact depend on A(f) in Jump, or just A(f) <> Uncalled?  

> So, my gut feeling is that we can do a two step algorithm:
> 
> 1. Run the continuation based analysis.
> 	For anything that's marked Uncalled or is in Jump, we can leave it at
> 	that. 
> 2. For all functions that are marked Unknown, we need to run a second analysis
> 	that determines if they can be contified within another function.  To 
> 	me this feels like doing some kind of scc or dominator calculation on
> 	the graph of tail calls, but I don't quite see it yet.

I agree that there is a graph feel to this problem, but I don't see it yet
either.