limit check insertion

[Stephen Weeks]

> How about:
> 
>      V ([], n) = n
>      V (l :: p, n) = V (p, n - m)     if at(l) = Alloc(m)
>                      V (p, max(n, m)) if at(l) = LimitCheck(m)

Good.
 
> > Theorem: If A is correct for f, then f is limit check correct.
> 
> This is where I lose you.  What's the definition of limit check correct?

Sorry.  Replace "limit check correct" with "sound".

> So, the annotations are just a witness to the fact that the inserted
> limit-checks produce a sound function.

Yes.

> Overall comments: The one aspect I don't like is the fact that going from
> a function without limit checks to one with limit checks seems to require
> inserting new labels and changing the next function.  You need some
> additional requirement that the control-flow isn't significantly altered.

Agreed.  I would prefer to have limit checks as an annotation on the
function as well.

> You might also have simply have alloc : Label -> Nat and
> limitCheck: Label -> Nat and define
>      V ([], n) = n
>      V (l :: p, n) = V (p, max(n, limitCheck(l)) - alloc(l))
> That is, every block does a limit check (possibly zero) and then some
> allocation.  
>
> To get a limit check from ls, alloc, next, you need to produce a
> limitCheck that makes the function f = (ls, limitCheck, alloc, next)
> sound.

I like this, and would add one more thing, at least to the safety
part, and have the limit check insertion return

	limitCheck: label -> Nat option
	available: label -> Nat

so that we can easily check that limit check insertion has produced a
safe, and hence sound function.

> I also think that the next function needs to be carefully constructed.
> Note, I don't think that it is the "normal" control-flow function.  If a
> function does a limitCheck(m), then does a non-tail call, should the
> continuation be allowed to think that m bytes are available?  I wouldn't
> think so. 

Agreed.

> So, either there are a set of start labels (corresponding to
> the "real" start label and then all continuation and handler labels) or
> the start label is a dummy label with next(ls) being the real start label
> and all continuation and handler labels.

I prefer the latter, keeping the framework simple, and slightly
complicating how the IL is translated to a problem within the
framework.


I agree that there are other things that we need to worry about for
threads, space safety, etc., but would like to push them to the todo
for now.


I would still like to hear opinions on the short term fix of
restricting limit check coalescing to basic blocks.