[isabelle-dev] Open Issues with JinjaThreads entry

Gerwin Klein gerwin.klein at nicta.com.au
Tue Oct 4 08:09:21 CEST 2011


On 04/10/2011, at 4:59 PM, Andreas Lochbihler wrote:

>>> the traditional isatest's AFP-Test did not report any failures the last few days,
>>> but the emerging testboard infrastructure mentions failures over the last few versions, and the current tips
>>> 
>>> 76aec35b4898934df700ee54ce4d8fb7b99b0388:AFP,fa3715b35370fd27bc9e6bd03fad4a34b0724af3:Isabelle
>>> 
>>> still seem to be broken.
>>> 
>>> For people involved in this issue, here is a more detailed report:
>>> 
>>> http://isabelle.in.tum.de/reports/Isabelle/report/37c2d104871b443f8b6dbd0a8b8b0314
>> 
>> The report just ends with "Interrupt". Is it possible that this is a time-out or similar?
> I would not call it broken - it's just lack of resources. It important line in the log is
> 
> Run out of store - interrupting threads

Ah, didn't spot that. This indeed is the usual out of memory problem.


> The tail of the output log tells me that the interrupt occured when one of the huge locales get opened. On my local machine, JinjaThreads requires to build in single-threaded mode about 12G of memory plus a few more when the heap image is written.

Yes, I can confirm that: our server logs show a spike each night at around 12G. The test runs with -M 1 -q 0 -p 0 for JinjaThreads. 

Interesting to see that the spike is for opening the locale. This is one of the things that might hit us as well.

Cheers,
Gerwin




More information about the isabelle-dev mailing list