Skip to content

Spurious "Heap exhausted" with same (or close) `+RTS -H` and `-M` arguments

Summary

Calling Agda with the same size as arguments of the RTS flags -H and -M reports Heap exhausted long before the live heap reaches that size.

This even happens if the -H size is only a little below the -M size.

Steps to reproduce

(I installed GHC-9.8.1 using ghcup.)

cabal get https://hackage.haskell.org/package/Agda-2.6.4.2/candidate/Agda-2.6.4.2.tar.gz
cd Agda-2.6.4.2
cabal install -f +optimise-heavily -f +enable-cluster-counting

wget -O agda-stdlib.tar.gz https://github.com/agda/agda-stdlib/archive/v2.0.tar.gz
tar -xzf agda-stdlib.tar.gz
cd agda-stdlib-2.0
cabal install

# Repeat from here for more experiments with different `-H_ -M_`:
make clean
GenerateEverything # silent, fraction of a second.
time agda +RTS -S -H3.2G -M3.2G -RTS -i src -i . Everything.agda

Result:

    Alloc    Copied     Live     GC     GC      TOT      TOT  Page Flts
    bytes     bytes     bytes   user   elap     user     elap
  4844080    309096    484256  0.056  0.056    0.080    0.079    0    0  (Gen:  0)
Checking Everything (/var/tmp/kahl/Agda/agda-stdlib-2.0/Everything.agda).
 Checking Algebra (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Algebra.agda).
  Checking Algebra.Core (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Algebra/Core.agda).
   Checking Level (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Level.agda).
  Checking Algebra.Definitions (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Algebra/Definitions.agda).
187690672   6016408   6756640  0.035  0.035    0.295    0.293    0    0  (Gen:  1)
   Checking Relation.Binary.Core (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Relation/Binary/Core.agda).
    Checking Data.Product.Base (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Data/Product/Base.agda).
     Checking Function.Base (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Function/Base.agda).
585794240  10800232  14586976  0.032  0.032    0.847    0.845    0    0  (Gen:  0)
   Checking Relation.Nullary.Negation.Core (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Relation/Nullary/Negation/Core.agda).
    Checking Data.Bool.Base (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Data/Bool/Base.agda).
     Checking Data.Unit.Base (/var/tmp/kahl/Agda/agda-stdlib-2.0/src/Data/Unit/Base.agda).
 98277808   6409384   8465232  0.022  0.022    0.979    0.976    0    0  (Gen:  1)
agda: Heap exhausted;
agda: Current maximum heap size is 3435970560 bytes (3276 MB).
agda: Use `+RTS -M<size>' to increase it.
    22808     16472    110552  0.000  0.000    0.980    0.977    0    0  (Gen:  1)
     1784                      0.000  0.000

     876,631,392 bytes allocated in the heap
      23,551,592 bytes copied during GC
       8,465,232 bytes maximum residency (3 sample(s))
         156,848 bytes maximum slop
            3330 MiB total memory in use (0 MiB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0         2 colls,     0 par    0.089s   0.089s     0.0444s    0.0564s
  Gen  1         3 colls,     0 par    0.057s   0.057s     0.0190s    0.0350s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.002s  (  0.002s elapsed)
  MUT     time    0.832s  (  0.829s elapsed)
  GC      time    0.146s  (  0.146s elapsed)
  EXIT    time    0.001s  (  0.000s elapsed)
  Total   time    0.981s  (  0.977s elapsed)

  Alloc rate    1,053,786,024 bytes per MUT second

  Productivity  84.8% of total user, 84.9% of total elapsed


real    0m1.075s
user    0m0.678s
sys     0m0.400s

Expected behavior

What do you expect the reproducer described above to do?

Something close to the following, produced with -H3G -M3.2G

[...]
181852688  12500976 1694569456  0.015  0.015  646.040  644.610    0    0  (Gen:  0)
121336376  13558856 1283757016  0.045  0.045  646.167  644.736    0    0  (Gen:  1)
151690664  44427016 1330286952  0.076  0.076  646.378  644.947    0    0  (Gen:  0)
147730832  19051744 1303443600  0.067  0.067  646.551  645.120    0    0  (Gen:  0)
  5600976  19400152 1307901656  0.053  0.053  646.638  645.206    0    0  (Gen:  0)
 22498312     15656     93304  0.019  0.019  646.776  645.345    0    0  (Gen:  1)
      656                      0.000  0.000

 766,004,153,856 bytes allocated in the heap
  46,365,512,064 bytes copied during GC
   1,534,982,456 bytes maximum residency (56 sample(s))
       5,982,152 bytes maximum slop
            3385 MiB total memory in use (1 MiB lost due to fragmentation)

                                     Tot time (elapsed)  Avg pause  Max pause
  Gen  0      2732 colls,     0 par   104.382s  104.420s     0.0382s    0.9379s
  Gen  1        56 colls,     0 par   16.098s  16.099s     0.2875s    1.1602s

  TASKS: 4 (1 bound, 3 peak workers (3 total), using -N1)

  SPARKS: 0 (0 converted, 0 overflowed, 0 dud, 0 GC'd, 0 fizzled)

  INIT    time    0.002s  (  0.002s elapsed)
  MUT     time  526.294s  (524.823s elapsed)
  GC      time  120.480s  (120.519s elapsed)
  EXIT    time    0.001s  (  0.000s elapsed)
  Total   time  646.777s  (645.345s elapsed)

  Alloc rate    1,455,468,876 bytes per MUT second

  Productivity  81.4% of total user, 81.3% of total elapsed


real    10m45.618s
user    10m42.115s
sys     0m4.931s

Using -M3G alone without -H also succeeds.

Using -H3.1G -M3.2G also fails, after 1m48.564s.

Using -H4G -M4G also fails immediately.

Over two years ago, I was routinely using settings like -H3G -M3G without problems.

Environment

  • GHC version used: 9.8.1

Optional:

  • Operating System: Ubuntu 20.04.6 LTS
  • System Architecture: Intel(R) Core(TM) i7-8565U
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information