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 _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
