[isabelle] Isabelle "pink out" for long periods · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Isabelle "pink out" for long periods

Email Gateway (Aug 22 2022 at 20:05):

From: "Eugene W. Stark" <isabelle-users@starkeffect.com>
Perhaps the biggest issue I have when using Isabelle (currently Isabelle2019) is that it will
relatively frequently get into a state in which JEdit can be used to edit the theory text,
but information from the prover is not forthcoming and panels (such as Output) that would
normally be displaying information are blank. The GUI goes into a "pink out" state, where
there is text highlighted in pink (which I believe means that it is scheduled for some processing)
and the right-hand gutter just to the left of the scrollbar has a solid pink color.
When this occurs, poly is compute-bound, sometimes just using 1 core and sometimes using more.

Once the system is in this state, it can persist for an indefinite period. Sometimes it clears
up and one can go back to work, but many other times it remains spammed for many, many minutes
and it is faster to restart than to wait, not knowing if or when it will come back to life.

At the moment of this writing, Isabelle is currently in such a state. I have tried in the past
to try to understand what it is doing, but I haven't been able to get information since usually
(before Isabelle2019) the "Monitor" panel also seemed to be spammed when in this state.
I just took another look try to find out what is happening, and this time I got apparently useful
information. There are an extremely large number (300K) of "tasks ready". The number is
dropping, but only 100 or so tasks are being completed per second, so it is taking a very long time.
A partial GC appears to be occurring every few seconds and full GCs are occurring infrequently,
if at all. My system is not thrashing: "iotop" shows very little disk activity and "top" shows
poly consuming 100% of one core at the moment.

I have attached screenshots of the Monitor panel displays. I have also pasted below some raw output
from the Protocol panel. In the time since I started writing this email (10 minutes or so),
the number of "tasks ready" has dropped by about 100K. So perhaps if I wait another hour the
system will become responsive again.

I think the issue is why the task queue would get spammed with so many tasks that are taking so
long to process in the first place. I note that I am a heavy user of "try", and the situation often
initiates when I have left "try" in the edit buffer for awhile. It seems like there should be
some kind of throttle on this, though.

(Note: OS is Ubuntu 16.04.)

<protocol function="ML_statistics" now="1561385035.83" tasks_ready="322810" tasks_pending="4674" tasks_running="2"
tasks_passive="45" tasks_urgent="4366" tasks_total="327531" workers_total="8" workers_active="4" workers_waiting="0"
full_GCs="127" partial_GCs="38252" share_passes="3" size_allocation="3191853168" size_allocation_free="2002137320"
size_code="4096" size_heap="6091177984" size_heap_free_last_full_GC="3202160" size_heap_free_last_GC="3196653272"
size_stacks="754991104" threads_in_ML="1" threads_total="13" threads_wait_condvar="3" threads_wait_IO="0"
threads_wait_mutex="8" threads_wait_signal="1" time_elapsed="73734.065202" time_elapsed_GC="3303.080842"
time_CPU="44446.104" time_GC="6294.34" user_counter0="0" user_counter1="0" user_counter2="0" user_counter3="0"
user_counter4="0" user_counter5="0" user_counter6="0" user_counter7="0"/>
Screenshot from 2019-06-24 10-24-24.png
Screenshot from 2019-06-24 10-24-42.png
Screenshot from 2019-06-24 10-24-54.png
Screenshot from 2019-06-24 10-25-05.png
Screenshot from 2019-06-24 10-25-17.png
Screenshot from 2019-06-24 10-25-42.png
Screenshot from 2019-06-24 10-25-53.png
Screenshot from 2019-06-24 10-26-05.png

Last updated: Apr 25 2024 at 20:15 UTC