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



I have posted (and seen postings) about this general type of thing here before,
but I am getting a more refined view of what seems to me to be a problem and want
to ask again and provide some data points.

I am running Isabelle 2016 under Ubuntu 14.04 LTS.  I am using the 64-bit
version on two similar machines, both of which are Intel(R) Core(TM)
i5-4670K CPU @ 3.40GHz (4 cores).  One machine has 24GB RAM, and I have
limited the ML heap to 16GB to avoid spamming other activities, and the other
machine has 16GB RAM, and I have limited the ML heap to 8GB for the same
reason.  The problem I am describing occurs on both machines, but for definiteness,
the screenshots I took today were done on the 16GB machine.

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.
During this period the CPU usage ranges anywhere from 100% to 400%, where 100%
means one core.  Based on previous postings, I would normally assume that it is
due to a major GC taking place, but also during these periods, the "Monitor"
window in JEdit does not receive any data updates from ML.  Once ML has come
back online, the Monitor window starts receiving data again, but it interpolates
the missing data by a line.  This makes it difficult to understand exactly what
is going on.  I don't really know whether there are any conditions under which
it is supposed to be the case that ML will stop sending data points to the
Monitor window, but it seems odd to me.  Of course, the long pause for an
unknown period is also frustrating, and in many cases I just terminate and
restart Isabelle, substituting the known wait for my theories to be reloaded and
rechecked for the unknown wait for ML to return.

For what it's worth, Isabelle memory use is limited, it is honoring the limits,
paging traffic is low, and CPU utilization is high, so it is not a thrashing
situation that is taking place.

I am attaching some screenshots that I took today when I let the sledghammering
run for awhile through multiple cycles of this behavior.

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.

The other windows are hard for me to interpret, due to the missing data.
For some reason, I didn't get a snapshot of the GC window, but the curves
are flat; not indicating the occurrence of major GC's like I would expect.
Again this might be due to missing data.

Could anyone comment on whether this behavior is considered "normal"?
I am suspicious of some kind of thread signalling/synchronization issue,
but not knowing anything about the actual implementation, can only speculate.

Thanks.

							- Gene Stark

Attachment: Screenshot from 2016-04-21 10:20:01.png
Description: PNG image

Attachment: Screenshot from 2016-04-21 10:20:16.png
Description: PNG image

Attachment: Screenshot from 2016-04-21 10:20:27.png
Description: PNG image

Attachment: Screenshot from 2016-04-21 10:20:37.png
Description: PNG image

Attachment: Screenshot from 2016-04-21 10:20:48.png
Description: PNG image



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