limit check pushed inside loop

[Stephen Weeks]

> Talking with Suresh yesterday about the discussion on n-byte limit checks
> pushed inside loops, we were wondering if this aggressive coalescing of
> limit checks violates safe-for-space.  

In short, I don't think so.  To explain why, I think we need to agree on what
space safety means.  Here is my definition.

Let's imagine all programs take a single natural number as input.  Suppose the
semantics of the language specifies some imaginary ideal of max memory usage for
every program.  I.E., assume we have a function

	Ideal: Program x Nat -> Nat

Now, suppose we build an implementation that has an actual max memory usage for
every program.  I.E., our implementation implies a function

	Actual: Program x Nat -> Nat

Define Actual to be safe-for-space with respect to Ideal if
  for all programs P
  there exists a constant c such that 
  for all inputs n
     Actual(P, n) < Ideal(P, n) * c 

Hopefully this definition makes sense.

> I've got one extreme case which I
> think does, although it is certainly up for debate as to whether or not it
> could be turned into a real case to worry about.
...
> fun f 0 = true
>   | f n = g 1
> and g  0 = false
>   | g  n = f 1
> 
> val _ = let
> 	  val x = Bool.toString (f 2)
> 	in 
> 	  print (concat["f(2) = ",
> 			"",            \
> 			"",             \
> 			...,             - n instances of the empty string
> 			"",             /
> 			"",            /
> 			x])
> 	end
> 
> At the top of the (non-allocating, non-terminating) f-g loop, there is a
> limitCheck for (24 + 12 * n) bytes; I guess that constant sized lists are
> just allocated all at once, not consed.  For any n, this program
> shouldn't terminate, but for a fixed heap of 4k (can't get any smaller
> with page sizes), n=283 runs but n=284 exits with an out of memory error.

The reason why this does not violate space safety is that the program is
varying, and the definition allows me to pick the constant based on the program.
Note that the definition is not

  there exists a constant c such that
  for all programs P
  for all inputs n
     Actual(P, n) < Ideal(P, n) * c 

> So, the potential might be there for those loop limit checks to change
> behavior.  

For any implementation, it will be the case that shrinking the fixed heap size
below a certain point will cause the program to run out of memory.  Just because
there is another implementation that could run in a smaller heap does not mean
the original implementation is not safe for space.   A definition of safe for
space based on quantifying over other implementations seems unreasonable to me.


There are variants of your example which are more evil.  However, none cause
space safety to be violated, at least by the above definition.  Here's one.

fun f 0 = true
  | f n = g(n + 1)
and g  0 = false
  | g  n = f(n - 1)

val _ = let
	   val b = f 13
	   val a = Array.array(1000, b)
	in
	   if Array.sub(a, 0)
	      then raise Fail "yes"
	   else raise Fail "no"
	end

In this program, the array allocation limit check is moved into the loop,
because the size of the array is a compile-time constant.  So, we only need to
change the length of the array to, say 1000000000, to cause the program to
require tons more memory.  But, that is still changing the program, and so falls 
prey to the constant depending on the program argument I gave above.  Trust me
-- I feel sleazy at this point.

One might try changing the program to

fun f 0 = true
  | f n = g(n + 1)
and g  0 = false
  | g  n = f(n - 1)

val _ = let
	   val n = valOf(Int.fromString(hd(CommandLine.arguments())))
	   val b = f 13
	   val a = Array.array(n, b)
	in
	   if Array.sub(a, 0)
	      then raise Fail "yes"
	   else raise Fail "no"
	end

But then, the array size is not known at compile time and is not pushed into the 
loop.

So, it looks like I sleaze out, according to my definition.  However, I really
don't like my first example.  The easiest fix I can think of is to put some
limit (say, 1K) on the array size limit check that can be moved away from the
array allocation.  Then, it will really be the case that you can only create
large limit checks with large programs, which seems ok to me.