Termination...

[Chris]

In today's seminar, we talked about termination of the polymorphic
splitting analysis. Upon further reflection, I think my last example
program might cause the analysis to not terminate:

let^1 f = lambda g. let^2 y = (g^3 g^3)
in y
in (f f)

I stated at the end of the seminar that the only way to extend the
contour was by having a let lexically within the "argument" of the
let, or within e1 in the following:

let x = e1 in e2

However, I no longer believe that to be true.

Instead, I believe that the only way to extend the contour is to
evaluate a let within the "argument" of a let - lexically or not.

In this static analysis, we consider flow rather than evaluation: So
to extend a contour, a let must flow to the argument of another let.

In the above program, let^2 flows to itself. When we find the flows
of let^1, we start by finding the flow of it's argument, which is the
closure created with the single lambda term, the empty environment,
and the contour k_0,label^1. Since we have a value for its argument,
we find the flow of the let's body. So we find the flow of the
application, which is the single closure we have applied to itself.
Since we have values for both the function and the argument - both are
the closure - we find the flow of the body of the lambda, which is
let^2.

We now continue by finding the flow of the argument of let^2, with
contour k_0,label^2. We end up finding the flow of applying the
closure to itself again - with a different contour. We progress again
until we need to find the flow of the argument of let^2, this time
with contour k_0,label^2,label^2.

Clearly we have omega here, but not so clear, each time we recurse, we
add label^2 to the contour, slowly growing its size. Since we are
continually seeing new contours, we continue finding the flow for the
new contours.

I have glossed over some of the details here, but I don't see how this
analysis terminates for certain - yet admittedly pathological -
programs.

This is not the main point of the paper - they don't prove termination
or even make a claim towards it. However, I do find it interesting
that this static analysis does not guarantee termination. It would be
easy to add - just bound the length of the contour much as k-CFA does;
however, that would hurt precision - and they do make a (implied)
claim that their analysis is more precise than k-CFA (for low values
of k).

If anyone is interested in continuing this discussion, please let me
know and I will cover this again at the beginning of next week's
seminar.

Chris

[Shuying Liang]

Very interesting and hard example! 

I have a few questions: 

1. As I walked it through,  I find when it progressed to evaluate the let^2 's argument of (g g), 

should 

the env: 

g maps to (k0 label^1)

the store

[ <g, k_0 label 1> maps to closure( (lambda g ...), env_0, (k0 label^1))

the contour: (k_0, label^1, label^2)

If the above components are right, then in the evaluation, how are we supposed to find g's value?

2. It seems to me that it will terminate in the sense that the g is always evaluated to the closure what the f was evaluated to, and then when applying the g to g, it uses the contour from the closure to extend g, which will not extend the contour with more and more label^2... 

3. Does static analysis always/necessary  have to be proved  for this Omega or the like to terminate to make a strong paper, or for the sake of theoretical aspect? 

Thanks for any comment or correction from the group!

Shuying

[Chris]

1. I'm not sure I understand your question, but here's my best guess.
We don't explicitly have a store, but we do have a "flow analysis" F
that acts like a store.
This flow analysis F maps <g, k_0 label^1> to the closure <(lambda
g ...), env_0, (k0 label^1)>.
To look up the values that can flow to g in the current environment/
context, we look up the contour matching g in the env:
env(g) = (k_0 label^1)
Now using this contour, we look up the values bound to g and the
contour in the flow analysis (store):
F(g, k_0 label^1) = <(lambda g ...), env_0, (k0 label^1)>
Now we have the closure bound to g in the current environment.

2. This is a point I glossed over. However, you might be right. As
far as I can tell at the moment, g is always bound to the same
closure; however, my argument for nontermination is based on the idea
that if we reach the same program point (calling g) with a different
contour, we must continue evaluation.

3. Any static analysis without a proof of termination has limited
use. If you run a program through it, and it's taking a long time,
how do you know if it hit an exponential or if it hit an infinite
loop? There is no way to tell. That said, this paper is successful
in showing that for common (Scheme) programming idioms this analysis
halts and is better than other approaches from the mid 90's. I
consider this discussion of termination to be interesting but not
fatal to the main points of the paper. The biggest impact
nontermination could have on this paper is to cause us to question how
well this analysis preforms when termination is guaranteed. If we
must change the analysis so that we guarantee termination, that change
will most likely reduce the precision of the analysis. If we reduce
the precision of the analysis, how well does it preform now?

Chris

[Shuying Liang]

On Thu, Jan 26, 2012 at 2:02 PM, Chris <cwe...@cs.utah.edu> wrote:

1.  I'm not sure I understand your question, but here's my best guess.
 We don't explicitly have a store, but we do have a "flow analysis" F
that acts like a store.
 This flow analysis F maps <g, k_0 label^1> to the closure <(lambda
g ...), env_0, (k0 label^1)>.
 To look up the values that can flow to g in the current environment/
context, we look up the contour matching g in the env:
 env(g) = (k_0 label^1)
 Now using this contour, we look up the values bound to g and the
contour in the flow analysis (store):
 F(g, k_0 label^1) =  <(lambda g ...), env_0, (k0 label^1)>
 Now we have the closure bound to g in the current environment.

Yes.
But when we evaluate the (g g), the contour is not (k0 label^1), it is (k0, label^1, label^2)
because the evaluation of let argument is performed in the extended contour, which is label^2 : (k0, label^1), and the reference of g will use this contour to construct program point for F in the function application rule, which ends up finding nothing...

2. This is a point I glossed over.  However, you might be right.  As
far as I can tell at the moment, g is always bound to the same
closure; however, my argument for nontermination is based on the idea
that if we reach the same program point (calling g) with a different
contour, we must continue evaluation.

Is it also to say that if the contour is changing all the time, we never reach the fixed point?

Thanks,
--Shuying