Re: [isabelle] ML goes "incommunicado" for minutes at a time during sledgehammering



On Thu, 21 Apr 2016, Eugene W. Stark wrote:

The problem is that, during sledgehammering using "try" it seems that ML will go "incommunicado" for minutes at a time, and it is hard to figure out why.

On the snapshot from the "Heap" window, you can see spikes in memory usage, leading to what appears to be a major GC. Upon completion of the major GC, the "freeze" sets in, and no data is sent to the monitor for several minutes. When the data resumes, the heapsize is much lower, but quickly spikes up to the max and the cycle repeats. Because there is no data during the freeze period, it is difficult to tell what is going on, but I have to wonder what it is doing during those 3+ minutes when there is only a short spike of computing activity that takes place before it starts again.

Could anyone comment on whether this behavior is considered "normal"?

It sounds indeed like a normal consequence of a situation where the ML heap is under high pressure: tons of data produced and the GC + heap compaction phases trying to reclaim memory.

When the Poly/ML runtime system performs such GC-related operations, all ML threads are stopped. The Monitor data is produced by such a regular ML thread, so nothing will be reported during that time.


I am suspicious of some kind of thread signalling/synchronization issue, but not knowing anything about the actual implementation, can only speculate.

From the description of the problem, it does not really look like that.
Although there is always a possibility for something really strange going on.


In conclusion, my guess from a distance is that "sledgehammer" or "try" produce more data than expected, potentially due to unusually big theories. You could also try to reset the machine-learning information in $ISABELLE_HOME_USER/mash_state.


Since you are using 64bit Poly/ML with substantial amounts of heap space, the question is what makes the theories so big that this is required. Even the biggest applications on AFP still fit into the small memory model of 32bit with 3.5 GB heap. There is a penalty of approx. factor 2 in memory requirements, when switching from 32bit to 64bit.


	Makarius





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