Email Gateway (Aug 22 2022 at 09:51): Email Gateway (Aug 22 2022 at 09:51):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
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.
Email Gateway (Aug 22 2022 at 09:51):From: Gerwin Klein <Gerwin.Klein@nicta.com.au>
And the solution finds itself within minutes of hitting the send button: my setup looked like it was using the 64bit version of poly, but was actually running the 32bit version. Just forgot to set a path correctly.
Sorry for the spam.
Cheers,
Gerwin
Last updated: Apr 25 2024 at 04:18 UTC