[isabelle-dev] Isabelle_10-Sep-2013 (fwd)
makarius at sketis.net
Fri Sep 13 20:59:27 CEST 2013
Another copy without the attachment, which did not get past the mailing
---------- Forwarded message ----------
Date: Fri, 13 Sep 2013 20:48:54 +0200 (CEST)
From: Makarius <makarius at sketis.net>
To: David Matthews <dm at prolingua.co.uk>
Cc: René Thiemann <rene.thiemann at uibk.ac.at>, isabelle-dev at in.tum.de
Subject: Re: [isabelle-dev] Isabelle_10-Sep-2013
On Fri, 13 Sep 2013, David Matthews wrote:
> I think the exception may be occurring with PolyML.shareCommonData. This
> needs memory outside the heap to hold some tables. If there is a lot of live
> data in the heap these tables can be large and if the heap is taking up most
> or all of the available virtual memory, a particular problem in 32-bit mode,
> you may get the above message and exception. Is that possible in this case?
> It is safe to handle the exception and continue; it's just that the sharing
> process will not be complete so that the heap will be bigger than it might
> otherwise be.
I've made my own tests with the following setup:
Poly/ML SVN 1848
ML_OPTIONS="--minheap 500 --gcthreads 4 --debug=sharing"
This produces the following information about the sharing phase of GC (attached
Moreover, I have instrumented the C++ sources of polyml to figure out which of
the 5 places of "Insufficient memory" are relevant here: it is the one in
polyml/libpolyml/sharedata.cpp (line 882):
raise_exception_string(taskData, EXC_Fail, "Insufficient memory");
If you say that we can just absorb an exception Fail "Insufficient memory" in
ML, we can do that on the Isabelle/ML side as a workaround.
More information about the isabelle-dev