dm at prolingua.co.uk
Fri Aug 31 11:40:41 CEST 2012
On 31/08/2012 05:21, Christian Sternagel wrote:
> On 08/31/2012 12:44 PM, Gerwin Klein wrote:
>> On 31/08/2012, at 1:25 PM, Christian Sternagel <c-sterna at jaist.ac.jp>
>>> Well, it almost worked now ;).
>>> even without -b all my memory was wasted and just as swapping started
>>> in earnest I got an error message, i.e., I have to adapt JinjaThreads
>>> to some previous changes.
>>> Still, I am nowhere close to the 3-4 GB RAM usage that seem to be
>>> possible. Maybe the reason is that I'm on x86_64?
>> Yes, that'll be it. Memory usage on x86_64 is almost twice that of the
>> 32bit version (which makes sense if you think about it).
> Now that you mention it ... ;)
> With TypeComp adapted (only minor changes) JinjaThread succeeded while
> using 6-8 GB RAM (which magically corresponds to the 3-4 GB on an i386 ;)).
If you're using Poly/ML 5.5 from SVN it could well be worth setting the
maximum heap size to about 80% of the available memory e.g.
Basically, choose the largest value that will avoid swapping on your
machine with whatever else you have running. Commit 1579 has reduced
the default maximum (without any --maxheap option) from 100% of the
memory to 80%.
The new heap sizer in 5.5 will detect swapping and reduce the heap
accordingly but it cannot know exactly how much memory is required by
the operating system and anything else you are running so it requires
some swapping activity to know it is at the limit.
The experiments Makarius and I were doing on x86_32 were on machines
that had at least 4G of real memory so swapping was not an issue. The
limit was imposed by the address length and/or the operating system.
Effectively the OS was setting a value for --maxheap below the memory size.
More information about the isabelle-dev