[Agda] Agda memory leaks?

[Wolfram Kahl]

While I am thoroughly enjoying the fact
that already Agda-2.3.0 can handle much more complex typechecking tasks
than before, I am now hitting RAM limitations again,
and I am therefore getting curious also about one strange effect I observe:

I start Agda-2.3.0 from a terminal, for example with:

  agda +RTS -S -K256M -H12G -M12G -RTS ...

I am watching using htop, and by the time the heap is all used
for the first time and the first modules are ``Finished''
(about 20 seconds later),
both VIRT and RES are 12.5G, which I consider reasonable.

However, 20 minutes later, I have VIRT=14.3G and RES=14.2G.

Does anybody know what these two additional gigabytes are?
Could these be FFI data that are not free'd properly?


In another run with the development version (with -H10G -M10G),
it took 7:05 minutes before it first encountered a module where
it allocated all heap before a generation-0 collection;
at that time, RES finally caught up with VIRT,
which in turn had already slowly grown from the initial 10.4G to 10.6G.
(Many modules had been Finished by then.)
Both RES and VIRT kept growing, albeit not very much;
at the end (after 70 minutes) I had VIRT = 10.69G and RES = 10.66G.

I extracted the timeline of this by taking ps snapshots every 5 seconds,
and removed lines where neither VIRT nor RES had changed
(and removed the first two columns to make it more e-mail friendly).
The result is attached below, first for 2.3.1.1 (from last week),
and then for the same run in 2.3.0.
(The main part of the 2G spike in that 2.3.0 run interestingly comes
 at a time when there appear to be only intense type checking
 and two gen-0 collections.)

>From these numbers, this appears to be almost negligible
in the development version;
however, I also see significant VIRT and RES growth beyond the -M limit
with the development version inside Emacs
in long sessions with repeated typechecking.

Does anybody have an idea what is going on here?


Wolfram


================== Agda-2.3.1.1 ==================
  0.0  1.3 10704976 227412 pts/72 R+  22:42   0:00 agda-2.3.1.1
  105  2.5 10735696 422228 pts/72 R+  22:42   0:05 agda-2.3.1.1
  102  3.9 10761296 653568 pts/72 R+  22:42   0:10 agda-2.3.1.1
  102 19.6 10761296 3216480 pts/72 R+ 22:42   0:15 agda-2.3.1.1
  101 27.9 10795088 4583616 pts/72 R+ 22:42   0:20 agda-2.3.1.1
  101 28.1 10795088 4610808 pts/72 R+ 22:42   0:25 agda-2.3.1.1
  101 28.1 10795092 4611208 pts/72 R+ 22:42   0:30 agda-2.3.1.1
  101 28.3 10821716 4637596 pts/72 R+ 22:42   0:35 agda-2.3.1.1
  100 28.3 10821716 4637596 pts/72 R+ 22:42   0:40 agda-2.3.1.1
  100 28.3 10821716 4637596 pts/72 R+ 22:42   0:45 agda-2.3.1.1
  100 28.3 10821716 4637832 pts/72 R+ 22:42   0:50 agda-2.3.1.1
  100 28.3 10821908 4637832 pts/72 R+ 22:42   0:55 agda-2.3.1.1
  100 28.3 10821716 4637932 pts/72 R+ 22:42   1:00 agda-2.3.1.1
  100 43.7 10879060 7172252 pts/72 R+ 22:42   1:05 agda-2.3.1.1
  100 43.7 10879060 7172252 pts/72 R+ 22:42   1:10 agda-2.3.1.1
  100 43.7 10879060 7172252 pts/72 R+ 22:42   1:15 agda-2.3.1.1
  100 43.8 10879252 7172516 pts/72 R+ 22:42   1:20 agda-2.3.1.1
  100 43.8 10879060 7172488 pts/72 R+ 22:42   1:25 agda-2.3.1.1
 99.8 43.9 10901780 7195044 pts/72 R+ 22:42   2:50 agda-2.3.1.1
 99.8 43.9 10901588 7195016 pts/72 R+ 22:42   2:55 agda-2.3.1.1
 99.8 43.9 10901588 7195024 pts/72 R+ 22:42   3:05 agda-2.3.1.1
 99.9 46.3 11060308 7584752 pts/72 R+ 22:42   3:15 agda-2.3.1.1
 99.9 46.3 11060308 7585016 pts/72 R+ 22:42   3:25 agda-2.3.1.1
 99.9 46.3 11060500 7585280 pts/72 R+ 22:42   3:55 agda-2.3.1.1
 99.9 46.3 11060308 7585252 pts/72 R+ 22:42   4:00 agda-2.3.1.1
  100 46.3 11060308 7585256 pts/72 R+ 22:42   4:41 agda-2.3.1.1
  100 47.5 11060308 7780084 pts/72 R+ 22:42   5:06 agda-2.3.1.1
  100 47.5 11060308 7780120 pts/72 R+ 22:42   5:31 agda-2.3.1.1
  100 51.2 11060308 8395768 pts/72 R+ 22:42   5:56 agda-2.3.1.1
  100 53.3 11060308 8736592 pts/72 R+ 22:42   6:01 agda-2.3.1.1
  100 53.3 11060308 8736636 pts/72 R+ 22:42   6:16 agda-2.3.1.1
  100 55.0 11060308 9020960 pts/72 R+ 22:42   6:46 agda-2.3.1.1
  100 55.6 11145300 9105780 pts/72 R+ 22:42   6:51 agda-2.3.1.1
  100 55.6 11145492 9106044 pts/72 R+ 22:42   6:56 agda-2.3.1.1
  100 55.6 11145300 9106016 pts/72 R+ 22:42   7:01 agda-2.3.1.1
  100 67.8 11145300 11108452 pts/72 R+ 22:42   7:06 agda-2.3.1.1
  100 67.8 11145300 11108544 pts/72 R+ 22:42   7:21 agda-2.3.1.1
  100 67.8 11145492 11108544 pts/72 R+ 22:42  10:27 agda-2.3.1.1
  100 67.8 11145300 11108544 pts/72 R+ 22:42  10:32 agda-2.3.1.1
  100 68.1 11198548 11161560 pts/72 R+ 22:42  12:37 agda-2.3.1.1
 99.9 68.1 11198548 11161796 pts/72 R+ 22:42  13:07 agda-2.3.1.1
  100 68.1 11198548 11161800 pts/72 R+ 22:42  17:38 agda-2.3.1.1
  100 68.1 11198548 11161812 pts/72 R+ 22:42  27:30 agda-2.3.1.1
  100 68.1 11198548 11162660 pts/72 R+ 22:42  28:10 agda-2.3.1.1
  100 68.1 11198548 11162664 pts/72 R+ 22:42  49:24 agda-2.3.1.1
 99.9 68.2 11212884 11176764 pts/72 R+ 22:42  62:56 agda-2.3.1.1
 99.9 68.2 11212884 11177000 pts/72 R+ 22:42  63:31 agda-2.3.1.1
 99.9 68.2 11212884 11177000 pts/72 R+ 22:42  69:47 agda-2.3.1.1

================== Agda-2.3.0 ==================
  107  3.3 10743052 544776 pts/5 R+   22:35   0:04 agda
  103  3.5 10764556 578188 pts/5 R+   22:35   0:09 agda
  102 11.0 10764556 1809220 pts/5 R+  22:35   0:14 agda
  101 38.2 10764556 6293260 pts/5 R+  22:35   0:19 agda
  101 61.4 10764556 10109908 pts/5 R+ 22:35   0:24 agda
  101 69.3 11438348 11397772 pts/5 R+ 22:35   0:29 agda
  100 69.3 11438348 11398300 pts/5 R+ 22:35   0:39 agda
  100 69.3 11438588 11398668 pts/5 R+ 22:35   1:39 agda
  100 69.3 11438396 11398672 pts/5 R+ 22:35   1:44 agda
  100 69.3 11438588 11398672 pts/5 R+ 22:35   2:04 agda
  100 69.3 11438396 11398776 pts/5 R+ 22:35   2:09 agda
  100 69.3 11438588 11398776 pts/5 R+ 22:35   2:29 agda
  100 69.3 11438396 11398776 pts/5 R+ 22:35   2:34 agda
  100 69.3 11438396 11398780 pts/5 R+ 22:35   4:04 agda
 99.8 69.3 11438396 11398784 pts/5 R+ 22:35   4:24 agda
 99.8 69.3 11438396 11398784 pts/5 R+ 22:35   5:14 agda
 99.8 76.6 12650812 12610436 pts/5 R+ 22:35   5:19 agda
 99.8 80.4 13270332 13230484 pts/5 R+ 22:35   5:24 agda
 99.9 80.4 13270524 13230748 pts/5 R+ 22:35   5:54 agda
 99.9 80.4 13270332 13230720 pts/5 R+ 22:35   5:59 agda
 99.9 80.4 13270332 13230720 pts/5 R+ 22:35  15:50 agda
 99.9 80.4 13270332 13230732 pts/5 R+ 22:35  26:26 agda
 99.9 80.4 13270332 13230736 pts/5 R+ 22:35  26:31 agda
 99.9 80.4 13270332 13230736 pts/5 R+ 22:35  29:06 agda
 99.9 80.4 13270332 13230696 pts/5 R+ 22:35  29:11 agda
 99.9 80.4 13270332 13230600 pts/5 R+ 22:35  32:01 agda
 99.9 80.4 13270332 13230608 pts/5 R+ 22:35  32:16 agda
 99.9 80.4 13270332 13230572 pts/5 R+ 22:35  33:02 agda
 99.9 80.4 13270332 13230508 pts/5 R+ 22:35  37:47 agda
 99.9 80.4 13270332 13230460 pts/5 R+ 22:35  38:47 agda
 99.9 80.4 13270332 13230396 pts/5 R+ 22:35  42:57 agda
 99.9 80.4 13270332 13229880 pts/5 R+ 22:35  50:58 agda
 99.9 80.4 13270332 13228056 pts/5 R+ 22:35  52:58 agda
 99.9 80.4 13270524 13228056 pts/5 R+ 22:35  58:14 agda
 99.9 80.4 13270332 13228068 pts/5 R+ 22:35  58:19 agda
 99.9 80.4 13270332 13228068 pts/5 R+ 22:35  79:56 agda
 99.9  0.0      0     0 pts/5    R+   22:35  80:01 agda