[isabelle-dev] Isabelle_10-Sep-2013 (fwd)

[Makarius]

Another copy without the attachment, which did not get past the mailing 
list server.


 	Makarius

---------- 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
   IsaFoR a44e26d6605e
   Isabelle a49ce8d72a44
   AFP 4e87a0fc2528

   ML_PLATFORM="x86-darwin"
   ML_HOME="/Volumes/Macintosh_HD/Users/makarius/lib/polyml/polyml-svn/x86-darwin"
   ML_SYSTEM="polyml-5.5.1"
   ML_OPTIONS="--minheap 500 --gcthreads 4 --debug=sharing"

This produces the following information about the sharing phase of GC (attached 
file).

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.


 	Makarius