cps & contification

[Stephen Weeks]

> One minor modification: C(A'') <= A'',
> because a function g which only appears once as a nontail callee will have
> C(A'')(g) = j <= A''(g) = Unknown.
> Result still holds because A'' is a prefixed point (rather than a fixed
> point).

Makes sense.

> With barnes-hut, note that -contify both resulted in a program with 7
> top-level functions, while -contify new resulted in a program with 9
> top-level functions.  This seems surprising to me -- the extra
> contification seems to have inhibited some other simplification from
> removing functions.  Whatever else went on, the running times were hurt by
> -contify new.

My best guess is inlining got turned off because of larger functions.

> I was also able to verify that all functions determined call_cont
> contifiable were determined uncalled by the new analysis; the one function
> determined call contifiable was determined uncalled by both the cont & new
> analyses.

So the upshot is that on all the examples, the new analysis is at least as
precise as call based, continuation based, or both, right?  And we believe that
will always hold, right?

> I was thinking about trying to prove that the analysis A is the least safe
> analysis under the RCont ordering extended pointwise to analyses.  But
> this won't work, because of nesting of functions:
...
> It seems like for tail calls (f, g) in T, we want to favor A(g) = A(f)
> over A(g) = f.

Yep.  There is probably some (program dependent) ordering that we could make up, 
but it doesn't seem worth the trouble to me, given the following theorems.

> On the other hand, there are some interesting properties that can be
> shown.  If B is a safe analysis and B(f) = Uncalled, then A'(f) =
> Uncalled and A(f) = Uncalled.  Likewise, if B is a safe analysis and B(f)
> = j in Jump, then A'(f) <= j and A(f) <= j.

I like these, and would like to add one more.
	If B is safe and B(f) = g then A(f) <> Unknown

Here's a concise summary of those theorems that captures minimality
	If B is safe and B(f) <> Unknown then A(f) <> Unknown

If this is indeed (or can be made) true, then I'm happy calling A minimal.

> However, I did discover one "bug" in the definition of Edge, which would
> have prevented any proof of minimality (for some reasonable definition).
...
> 
> The solution is to change the definition of Edge to the following:
>         Edge = {(Root, fm)}
>                U {(Root, f) | A'(f) <> Unknown}
>                U {(f, g) | (f, g) in T and A'(f) <> Uncalled
>                                        and A'(g) = Unknown}
>                U {(Root, g) | (f, g, j) in N and A'(f) <> Uncalled 
>                                              and A'(g) = Unknown}
> 
> Only minor changes to the proofs of safety and connectivity.

Makes sense.  It might be simpler to just remove all nodes from the graph that
have A'(f) = Uncalled.

> Also, I was considering a slightly different definition of A:
> 
> A(f) = if parent(f) = Root
>          then A'(f)
>          else the ancestor g of f such that parent(g) = Root
> 
> It's equivalent to the original definition, but I thought that less
> branches in the definition might simplify a proof of minimality.  It also
> shows a little more clearly when we fall back to the A' analysis.

I don't think it makes much difference, but I'm happy either way.

> Here's an updated contify.fun with the new analysis.  I checked into logic
> a little more (tweaking checkDominators to run just before contify and
> print out the call graph was useful, rather than tracing 47 functions by
> hand), and it looks pretty clear that the mutual recursion can't be
> moved into the local functions.

Can you send the graph?  You know about dot, right?