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.