Andreas, How much real memory do you have on this machine? I would not expect that the size of the live data or the CPU time will have changed much, indeed I would have expected the CPU time to have reduced. There has, though, been a major change in the garbage-collector and in the way that the heap is allocated.
In languages with a GC the size of the heap effectively determines the amount of time the program spends garbage-collecting. With a small heap the program needs to garbage-collect more frequently and since the cost of each GC depends largely on the amount of live data the total GC time goes up. Poly/ML increases the total size of the heap as the amount of live data goes up but working out how to do this is largely down to heuristics. The big problem occurs if the heap size reaches the size of the available main memory because at that point GC results in a very significant increase in paging activity.
The GC in SVN has been extensively re-worked to allow for multi-threading the GC and there were various other changes. Multi-threading is off by default but if anyone wants to experiment with it there is a run-time option --gc-threads=N which sets the number of GC threads. Zero means use as many threads as there are processors. As part of these changes the way the -H option works has changed. If you are providing a -H option try providing a smaller value than you did with 5.4.1.
Determining the optimal heap size is an open research topic and I'm planning to look into this in more detail. Let me know how you get on and if there's still a problem I'll investigate.
Regards, David
On 16/11/2011 09:04, Andreas Lochbihler wrote:
Hi all,
when I build a large session in Isabelle2011-1 (to be precise, an extension of of JinjaThreads in the Archive of Formal Proofs) with PolyML 5.4.1, this takes 1:51h. While running the session, polyml requires 12GB of memory (VmSize in /proc/<PID>/status). The final call to PolyML.shareCommonData before writing the heap image consumes 17GB of memory.
I now ran the same session with the SVN version 1352 of PolyML. Then, it takes 2:35h, 16GB for the session and 21GB for sharing common data. What is happening there? Have other people experienced a similar surge in memory usage and runtime?
Thanks for any hints, Andreas