[isabelle-dev] AFP: Session AVL-Trees broken

[Gerwin Klein]

On 08/11/2012, at 8:50 AM, Lukas Bulwahn <bulwahn at in.tum.de> wrote:

> On 11/07/2012 10:41 PM, Gerwin Klein wrote:
>> I can see no reason why any of these would have to time out, and they don't on other machines (I've only tried some, though, not all).
>> 
>> Could it be an artefact of time measurement on macbroy 2 or something like that? Too many jobs in parallel? It doesn't seem to be very deterministic either, there are different sessions failing at different times.
> I can confirm that the AVL-Tree certification errors are real and the timeouts occur nondeterministically even on my laptop, when running "afp_build -A".

Interesting, is your laptop swapping when the sessions fail? My guess is that this is a symptom of the machine being overloaded.

When I was testing, I was running sessions one at a time, not in parallel, so I wouldn't have seen any issues with too many parallel jobs or similar.

Does anyone know what the timeout measures? Elapsed real time or time spent on that session?

The solution may be to just increase timeouts. On the other hand, this whole thing used to work just fine and started to go haywire 2012-10-19, then the log files are cut off in the middle at HOL-Probability (probably nonterminating, I guess these sessions should get a timeout too, the old setup was cumulative), HOL-Probality worked on 2012-10-26 (but then timeouts), then again stuck at HOL-Probability, and since 2012-10-28 mostly timeouts.

Also: 13h elapsed time for 4:50h cpu time on 2012-10-30 and 9h elapsed time for 5:26h cpu time yesterday. These should be the other way around. It definitely looks like the machine is way overloaded. 

The afp test assumes it has the machine to itself and runs at 6:28 in the morning. It should be finished after about 3h. 

Looking at isatest logs, it looks like that test now reaches long into that time (mac-poly64-M8-2012-11-07-macbroy2 finished 7:32 and mac-poly-M8-2012-11-07-macbroy2 at 9:14, mac-poly-M4-2012-11-07-macbroy2 at 8:28). These seem to be starting way later than usual. 

I can either move the afp test to later, or whoever now feels in charge of isatest should have a look at moving that back to an earlier time. E.g. on 2012-10-15 when afp-test was still fine, mac-poly64-M8-2012-10-15-macbroy2 finished at 4:11 am.

Cheers,
Gerwin