[isabelle-dev] >>> SCHEDULER: disposed 4 dead worker threads

Christian Urban christian.urban at kcl.ac.uk
Sun Dec 15 01:42:47 CET 2013

Sorry about being a harbinger of bad news. But
this message about dead worker threads shows up 
pretty frequently with me. Though it has not caused
any problems I am aware of. My guess is that I notice this
message already for at least a year. It is in fact 
so frequent that I assumed this is normal behaviour 
of Isabelle. 

I just tried it out with tree different theories, with
Isabelle-2013-1 and also Isabelle-2013-2; in all 
instances I got a message like

 > isabelle build -c -v -d . Slides1

 Started at Sun 15 Dec 2013 11:25:22 EST (polyml-5.5.1_x86-darwin on Christians-MacBook-Air-2.local)
 ML_OPTIONS="-H 500"

 >>> SCHEDULER: disposed 4 dead worker threads
 Timing RC (4 threads, 372.740s elapsed time, 1161.691s cpu time, 111.615s GC time, factor 3.12)
 Finished RC (0:06:41 elapsed time, 0:20:03 cpu time, factor 3.00)
 Running Slides1 ...
 Slides1: theory Slides1
 Timing Slides1 (4 threads, 1.143s elapsed time, 1.706s cpu time, 0.016s GC time, factor 1.49)
 Document at /Users/cu/Repos/rc/slides1.pdf
 Finished Slides1 (0:00:14 elapsed time, 0:00:15 cpu time, factor 1.07)
 Finished at Sun 15 Dec 2013 11:32:23 EST
 0:07:01 elapsed time, 0:20:34 cpu time, factor 2.93

This seems to me all reproducible, although with a
fourth theory I tried I do not get this message.

If I can provide any further debugging information,
please let me know.

Best wishes,

On Friday, December 13, 2013 at 14:44:28 (+0100), Makarius wrote:
 > On Wed, 11 Dec 2013, Tobias Nipkow wrote:
 > > I just saw the above message for the first time, when building HOL-IMP. 
 > > Should this worry me?
 > Incidently I had seen the same on the same day, and asked myself the same 
 > question.  It did not come back later, though.
 > These sporadic incidents might be a problem in the session shutdown phase, 
 > i.e. a misunderstanding of Isabelle/ML vs. Poly/ML.  If it happens more 
 > frequently, I will have to look again.
 >  	Makarius
 > _______________________________________________
 > isabelle-dev mailing list
 > isabelle-dev at in.tum.de
 > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


More information about the isabelle-dev mailing list