possible memory leak

[msaaltink]

There seems to be a memory leak in the interpreter.

type T = [100][8]

init: T
init = [0 .. 99]

step: T -> T
step v = v + (v <<< 1)

f: {n} (fin n) => T -> T
f v = vs @ `n where vs = [v] # [step x | x <- vs]

f1 = f`{10^^5}

If I run f1 init in the interpreter, each successive time I execute it the cryptol memory used increases by several Gb. The jump in memory size appears to occur just before the result is printed, and the memory does not drop afterwards the way it does when I try other computations that consume lots of memory. Equally strangely, the REPL gets less responsive after one or two of the computations, even though there's still lots of free memory, but perhaps that's a red herring.

This is probably related to the discussion of #810. As in that issue, if I change the accumulator type in the comprehension to be flat (that is [800]), this problem disappears.

[robdockins]

Some profiling reveals that the space usage is primarily due to a single call to memoMap inside the (+) primitive. This point-wise memoizes the results of the addition in the step function. If I remove the memoization step, the memory usage becomes basically constant... at the cost making the algorithm take exponential time.

Unfortunately, because of the way memoization works at the moment, a long chain of additions like this retains the memo maps for each of the intermediate steps along the way and results in this space leak. I think this is because right now there's no way to check if we have memoized the entire range of a sequence, so we have to retain the previous maps indefinitely in case we probe a location we haven't seen before (even if this eventually becomes impossible).

Two thoughts. First, I don't know offhand a great way to solve this problem, but maybe we can find a way to do memoization that allows the memoized map to eventually become garbage. Second, I'm surprised because it seems like the garbage collector never recognizes these chains of memo maps as garbage, even if we run some other computations at the REPL; I don't understand why that is the case.

[robdockins]

Additional note: I also notice the REPL slowdown. It's a general symptom I've noticed at the REPL after running a computation that consumes a lot of memory. I've never really understood why it happens, but maybe it has something to do with GC pauses.

[robdockins]

Interesting, it seems like this was easier to fix than I expected. Commit 3f66dbf adds the ability for memoized maps to pay attention to their length and notice when they have been forced at that many unique locations; in that case, they discard the underlying computation they are memoizing and allow the garbage collector to reclaim the space. This allows the linked program to run in approximately constant space.

I still don't understand why memory is not being reclaimed after more computations are run.

[robdockins]

Computations on the "packed" accumulator are faster than the unpacked one, but #1136 has solved the accumulating space leak problem, so I think we can close this.