cps & contification

[Stephen Weeks]

> It still seems to me that a solution to
>   Gamma = {ft |--> ft} V V_i R[ei] Gamma(fi)
> would give the right contification information, ...

You're getting closer to the way I like to think about these sorts of things.
Saying that "a solution to Gamma = F (Gamma)" would give the right information
is the same as saying that if Gamma satisfies a set of constraints, then the
transformation will be correct.  Usually, these constraints can be defined by a 
collection of forall conditions based on the entire program.  I'll give an
example of what I mean for contification below.  For another example, take a
look at one of our papers (http://www.star-lab.com/sweeks/papers/97-sas.ps).

We usually refer to these constraints as "safety" constraints.  They form a nice 
way of modularizing the reasoning about correctness between the analysis and the 
transformation.

> ... but if F is not monotone,
> then I don't know of any correct and efficient method of calculating it.
...
> Note: a solution to this does exist; Gamma = {l |--> l} will always be a
> solution.  Since there is an ordering on Gamma, then a least fixed point
> does exist as well, although not necessarily unique.

This last point does not follow.  Consider a simple lattice with four elements
L = {a, b1, b2, c} with the following ordering.
        c
       / \
      b1  b2
       \ /
	a
Let f: L -> L be the nonmonotone function defined by
	x	f(x)
	--	----
	a	c
	b1	b1
	b2	b2
	c	a
Then b1 and b2 are fixed points of f, but there is no least-fixed-point.  I'm
almost positive that there are analogous cases for the lattice REnv and
nonmonotone function that you define.

> What is currently in place will compute a fixed-point, but I guess not
> necessarily the least fixed-point; although the evidence seems to imply
> that it "small" enough to capture all the cases caught by the other
> analyses.  But I've spent enought time tweaking with it to know that there
> are probably some cases where it might miss something that the call-based
> analysis would catch.

So, the upshot is that we agree that your constraints will lead to a correct
transformation but that there are some times when your implementation does not
compute a small enough fixed point.  I would like to think some more about this
and see if we can think of the "right" order for REnv (it may be dependent on
the program) or another way of computing the analysis.

> True.  I've been puzzling why the existing continuation based analysis
> wasn't suffering from the same problem, because the fixed-point function
> there is very similar:
> 
> Label = Func
> RCont = Jump U {bot} U {top} ; squashed powerset domain with obvious join
> REnv = Label -> RCont        ; continuous function domain with pointwise join
> 
> Anal[<fun fi (<xij>*) = ei>*]
>   = fix (fn Gamma => {ft |--> top} V V_i R[ei] Gamma(fi)) 
> 
> R[k (f <xi>*)]p = {f |--> k}
> R[f <xi>*]p     = {f |--> p}
> 
> It finally hit me: in the new analysis, REnv is not a continuous function
> domain, so Gamma(fi) is not a continuous operation; that clearly keeps F
> from being a continuous function.  But in the old analysis, REnv was a
> continuous function domain, so Gamma(fi) is a continuous operation. 

I don't understand this last paragraph.  In both analyses, REnv is a complete
lattice of functions, ordered pointwise.  What does it mean for REnv to be a
continuous function domain?  I have a feeling we were brought up with different
terminology :-)  I think you're basically saying what I was about the fact that 
propagating RConts from one label to another causes nonmonotonicity in the new
analysis while it does not in the old analysis (recall that monotonicity is a
necessary condition for continuity).

Anyways, feel free to ignore my last paragraph if you think we're on the same
wavelength.

> In any event, it might not matter at all. Here are the results of the
> benchmarks, which are somewhat disappointing:

I wouldn't worry about the numbers as long as they don't hurt us.  We're still
missing lots of other CPS optimizations that might be triggered.  It's good to
get everything we can, just on general principles.

----------------------------------------

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)

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
	**  For all nontail calls (f, g, j) in N, either
		A(f) = Uncalled
		or A(f) in {Uncalled, Unknown, j}
	*** For all tail calls (f, g) in T, either 
		A(f) = Uncalled
		or A(g) in {Unknown, f, A(f)}

Note: You could express the safety constraints as a function F, and then say
	that a program is safe if it is a fixed point of the function.  But it
	doesn't really buy you anything until you have an ordering on analyses
	that turns them into a lattice and makes F monotone.

I claim that all of the strategies (call, cont, both, new, ...) we have looked
at have been producing safe analyses.  What we have been striving for is a safe
analysis that marks as many functions as possible as Uncalled (which is easy to
do) and marks as few functions as possible Unknown.

Here are some facts about safe analyses on (fm, T, N).

Define a path from f to g to be a sequence of (tail or nontail) calls from the
program where each callee equals the subsequent caller and the first caller is f
and the last caller is g.

1. If A(f) <> Uncalled and there is a path from f to g then A(g) <> Uncalled.
	Proof: by induction on the length of the path.
2. If there is a path from fm to f then A(f) <> Uncalled.
	Proof: follows from 1 and condition * of safety.
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.
4. If A(f1) in Jump and A(f2) in Jump and A(f1) <> A(f2)
	and there are paths of tail calls from f1 to g and f2 to g
   then A(g) in {Unknown} U Fun
	Proof: By fact 3.
5. If (f, g) in T and A(f) <> Uncalled and A(g) in Func - {f}
   then A(f) = A(g)
	Proof: By inspection of condition ***.

The continuation based analysis computes a map in
	Fun -> {Uncalled, Unknown} U Jump
Whenever it runs up against fact 4, it just maps a function to Unknown.

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.