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