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. Did you rebuild the compiler before you ran with that
version (i.e. make compiler) or use the original 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.
David
_______________________________________________
polyml mailing list
polyml@inf.ed.ac.uk
http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
