[isabelle-dev] Isabelle_10-Sep-2013

[David Matthews]

On 13/09/2013 11:08, René Thiemann wrote:
>> I would suggest trying with the --stackspace option e.g.
>> ML_OPTIONS='--stackspace 500'
>> The Fail exception with "Insufficient space" arises in a number of places such as when trying to fork a thread.  This requires memory outside the ML heap.  The stackspace option keeps some space free from the ML heap for these purposes.
>
> I tried it, but the setting was not high enough: then even earlier sessions crash with a new
> 'Run out of store - interrupting threads' error message. This also happens if I set stackspace to 1500,
> but it succeeded with 5000. However, then still afterwards I get the usual
>
> poly(6820,0xb09a5000) malloc: *** mmap(size=16777216) failed (error code=12)
> *** error: can't allocate region
>
> error as before, if I use minheap=1000, or drop the minheap parameter.
>
>> I would guess that this is when running the X86/32 version rather than X86/64.
>
> Yes, I use the 32-bit mode. I will later run some tests when using the 64-bit mode.
>
> Here is my current setup:
>
> ISABELLE_BUILD_OPTIONS=""
>
> ML_PLATFORM="x86-darwin"
> ML_HOME="/Users/rene/.isabelle/contrib/polyml-5.5.0-3/x86-darwin"
> ML_SYSTEM="polyml-5.5.0"
> ML_OPTIONS="--minheap 1000 --stackspace 5000"
>

You definitely don't want a value as large as 5000.

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.

Regards,
David