[Agda] Agda interface generation memory consumption

Nils Anders Danielsson nad at Cs.Nott.AC.UK
Sat Feb 13 14:20:00 CET 2010


On 2010-02-10 21:02, Dan Doel wrote:
> However, loading the complete module still takes 75% of my 2 GB of RAM.

You are using a 64-bit OS, right? I get the following statistics on my
machine (with +RTS -s):

  11,657,136,764 bytes allocated in the heap
   2,504,549,644 bytes copied during GC
     201,036,388 bytes maximum residency (23 sample(s))
       2,065,840 bytes maximum slop
             563 MB total memory in use (4 MB lost due to fragmentation)

  Generation 0: 22198 collections,     0 parallel,  6.45s,  6.44s elapsed
  Generation 1:    23 collections,     0 parallel,  5.08s,  6.07s elapsed

  INIT  time    0.00s  (  0.04s elapsed)
  MUT   time   23.93s  ( 24.60s elapsed)
  GC    time   11.52s  ( 12.51s elapsed)
  EXIT  time    0.00s  (  0.00s elapsed)
  Total time   35.45s  ( 37.15s elapsed)

  %GC time      32.5%  (33.7% elapsed)

  Alloc rate    487,226,749 bytes per MUT second

  Productivity  67.5% of total user, 64.4% of total elapsed

Note that you can reduce the GC time substantially by tweaking the RTS
options. With -H600M (which sets the suggested heap size to 600M) I get
the following profile:

  11,657,299,432 bytes allocated in the heap
     705,164,488 bytes copied during GC
     145,201,216 bytes maximum residency (5 sample(s))
         938,080 bytes maximum slop
             584 MB total memory in use (4 MB lost due to fragmentation)

  Generation 0:    26 collections,     0 parallel,  2.66s,  2.67s elapsed
  Generation 1:     5 collections,     0 parallel,  1.29s,  1.30s elapsed

  INIT  time    0.00s  (  0.00s elapsed)
  MUT   time   25.20s  ( 25.77s elapsed)
  GC    time    3.95s  (  3.97s elapsed)
  EXIT  time    0.00s  (  0.01s elapsed)
  Total time   29.15s  ( 29.74s elapsed)

  %GC time      13.5%  (13.3% elapsed)

  Alloc rate    462,562,355 bytes per MUT second

  Productivity  86.5% of total user, 84.7% of total elapsed

If I use -H400M instead the total time is increased slightly, but the
total memory in use drops to ∼400MB. (You can also use -M to set a
maximum heap size, to avoid swapping.)

--
/NAD



More information about the Agda mailing list