limit check insertion
Matthew Fluet
fluet@CS.Cornell.EDU
Mon, 22 Oct 2001 20:16:18 -0400 (EDT)
> 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.
Nat or Nat option on limitCheck doesn't really matter. Until we care
about threads, I would say that limitCheck(l) = SOME 0 is basically
equivalent to limitCheck(l) = NONE, so a simple Nat suffices. But no big
deal either way.
The limit check insertion returning both it's limit check's and the
witness is good.
> > 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.
Fine by me. It's just going to turn into a graph problem, so a single
root is probably the way to go.
> I would still like to hear opinions on the short term fix of
> restricting limit check coalescing to basic blocks.
Meaning, let alloc(l) = sum of allocations in the block and setting
limitCheck(l) = alloc(l)?
Sounds cheap and quick (to write); I guess we need to see how it plays out
in practice to determine how quickly we need to move to something else.
I've got no objections to it.