On 26/07/2010, at 1:35 PM, David Matthews wrote:
Gerwin Klein wrote:
Since the below I've run a few more experiments, and the theory does run fine with image built after less than 25min with the current svn trunk version of polyml on x86_64-darwin (5.4 Experimental). However, with the polyml-3.1-fixes version, it is still running after 45min with memory usage approaching 7.5GB and still raising. I'm not quite sure how to proceed. I don't think I'll want to run our production proofs on an experimental polyml version. How experimental/far away from release is the current trunk?
Just so I'm clear: the version that runs successfully is with the current SVN.
Yes, that's right.
Did you rebuild the compiler before you ran with that version (i.e. make compiler) or use the original compiler?
I checked out the svn trunk version from scratch, and did run "make compiler".
I suspect the problem has to do with the way the Poly/ML run-time system (RTS) manages memory. Currently, as the ML program uses more memory the RTS gets more memory from the system up to the various limits imposed. The limits are things like the swap size, the limit set by ulimit -d and on 32-bit architecture the size of the address space. The space the RTS uses for the heap has to be significantly more than the actual size that the ML program is currently using otherwise it would be constantly garbage-collecting.
The trouble is that this can leave no space left if the system needs to allocate memory for something else such as for malloc or for the stack for a new thread. I think I need to look at some way of keeping some space in reserve for these. It's a bit difficult because I don't think there's a way to find out how much space is left after extending the heap.
Can I do anything to help you debug this?
In the 64bit 5.3 version I noticed normal (< 2G) memory usage while it was processing everything and then a huge spike at the very end going up to > 7G (presumably at the commit call at the very end of the session, but can't really tell). Could there be a polyml reason for this or is it an Isabelle problem after all? I'd have expected memory usage to go up in Isabelle2009-2 slightly, but not by that much.
It's a bit difficult to provide good data at the moment, because I'm travelling and have only a low-bandwidth connection to my machine in the office, but I can produce more when I'm back mid Aug.
Cheers, Gerwin