Hi,
I’m running into problems with large heap sizes on 64bit Darwin.
The machine I’m running on has 32GB physical memory, and runs out of polyml
memory on sessions that take about 12GB on 64bit Linux. The error message is
val it = (): unit
ML> Exception- SysErr ("Cannot allocate memory", SOME ENOMEM) raised
(This is from an Isabelle build of the image CBaseRefine in
https://github.com/seL4/l4v/tree/master/proof)
The initial heap size was specified as “-H 2000”. Playing around with that
option, I got for instance for “-H 8000” the message:
"Value of -H option is too large"
I’m getting the same for trying to increase —maxheap. The same -H 8000 option
on a 64-bit Linux machine works fine.
The check that throws this error seems to be:
libpolyml/mpoly.cpp:177
// Check that the number of kbytes is less than the address space.
// The value could overflow when converted to bytes.
if (result >= ((POLYUNSIGNED)1 << (SIZEOF_VOIDP*8 - 10)))
Usage("Value of %s option is too large\n", arg);
As far as I can see, config sets the value of SIZEOF_VOIDP to 8 on both
platforms, so I’m a bit mystified why one works and the other doesn’t.
The polyml version is 5.5.2 (-3 in the Isabelle distribution, but same problem
for vanilla 5.5.2).
Any ideas?
Cheers,
Gerwin
________________________________
The information in this e-mail may be confidential and subject to legal
professional privilege and/or copyright. National ICT Australia Limited accepts
no liability for any damage caused by this email or its attachments.
_______________________________________________
polyml mailing list
[email protected]
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
