[isabelle] PolyML "Insufficient memory" exception while building images



Hello isabelle-users.

I've been struggling lately with fairly frequent "Insufficient memory" exceptions when trying to build heaps/images. The strange thing is that I don't seem to have run out of memory in any sense.

From reading the log, it looks a lot like PolyML ran out of something while trying to do its final cleanup before saving the session. In the session log, all the theories have been loaded already. There's also plenty more total memory available on this machine at the time of failure, so I don't think it's a fail-to-allocate problem. Perhaps PolyML has exhausted some fixed resource used while doing a shareCommonData or similar, such as stack space on some thread?

Finally, in the past I've noticed that the problem is slightly nondeterministic. If I delete a few heaps and try again, sometimes the process succeeds, usually after three or four attempts. This is not a lot of fun.

Does anyone have any idea what kinds of things might cause this problem, and where I should be looking? I've noticed that polyML itself has a number of command-line memory-debugging arguments, and I'm not sure what will happen if I try to convince Isabelle to pass them along.

I don't set any limits on PolyML's memory usage in my isabelle settings or via ulimit or similar. (There's a limit on Java's memory consumption, but that's not what's being hit here.)


Here are the last few ML statistics messages from the log of the failed session:

^LML_statistics = ^E^F:^Fnow=1410497588.77^Ftasks_ready=0^Ftasks_pending=0^Ftask
s_running=1^Ftasks_passive=0^Fworkers_total=4^Fworkers_active=1^Fworkers_waiting
=0^Ffull_GCs=4^Fpartial_GCs=1275^Fsize_allocation=548405248^Fsize_allocation_fre
e=292779660^Fsize_heap=3074088960^Fsize_heap_free_last_full_GC=18342268^Fsize_he
ap_free_last_GC=553199172^Fthreads_in_ML=1^Fthreads_total=7^Fthreads_wait_condva
r=4^Fthreads_wait_IO=0^Fthreads_wait_mutex=0^Fthreads_wait_signal=1^Ftime_CPU=43
6.427259^Ftime_GC=37.738374^Fuser_counter0=0^Fuser_counter1=0^Fuser_counter2=0^F
user_counter3=0^Fuser_counter4=0^Fuser_counter5=0^Fuser_counter6=0^Fuser_counter
7=0^E^E^F^E
^LML_statistics = ^E^F:^Fnow=1410497589.27^Ftasks_ready=0^Ftasks_pending=0^Ftask
s_running=1^Ftasks_passive=1^Fworkers_total=4^Fworkers_active=1^Fworkers_waiting
=0^Ffull_GCs=4^Fpartial_GCs=1275^Fsize_allocation=548405248^Fsize_allocation_fre
e=143978084^Fsize_heap=3074088960^Fsize_heap_free_last_full_GC=18342268^Fsize_he
ap_free_last_GC=553199172^Fthreads_in_ML=1^Fthreads_total=7^Fthreads_wait_condva
r=4^Fthreads_wait_IO=0^Fthreads_wait_mutex=0^Fthreads_wait_signal=1^Ftime_CPU=43
6.827284^Ftime_GC=37.738374^Fuser_counter0=0^Fuser_counter1=0^Fuser_counter2=0^F
user_counter3=0^Fuser_counter4=0^Fuser_counter5=0^Fuser_counter6=0^Fuser_counter
7=0^E^E^F^E


And the final few lines:

### Cannot present theory with skipped proofs: "InitLemmas"
### Cannot present theory with skipped proofs: "Invocations_R"
^LML_statistics = ^E^F:^Fnow=1410497589.57^Ftasks_ready=0^Ftasks_pending=0^Ftasks_running=0^Ftasks_passive=0^Fworkers_total=0^Fworkers_active=0^Fworkers_waiting=0^Ffull_GCs=4^Fpartial_GCs=1276^Fsize_allocation=528482304^Fsize_allocation_free=394241872^Fsize_heap=3075137536^Fsize_heap_free_last_full_GC=18342268^Fsize_heap_free_last_GC=532482744^Fthreads_in_ML=0^Fthreads_total=3^Fthreads_wait_condvar=0^Fthreads_wait_IO=0^Fthreads_wait_mutex=0^Fthreads_wait_signal=1^Ftime_CPU=437.319315^Ftime_GC=37.802378^Fuser_counter0=0^Fuser_counter1=0^Fuser_counter2=0^Fuser_counter3=0^Fuser_counter4=0^Fuser_counter5=0^Fuser_counter6=0^Fuser_counter7=0^E^E^F^E ^LTiming = ^E^F:^Fthreads=4^Felapsed=330.020^Fcpu=467.429^Fgc=37.442^Ffactor=1.42^E^E^F^E
val it = (): unit
ML> Exception- Fail "Insufficient memory" raised


Thanks for your time/thoughts,
    Thomas.




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.