[isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc

[Lars Hupel]

>> So far it looks good, but we still need to test all of AFP.
> 
> I will do that today and report my findings.

The machine has been busy since yesterday running the distribution and
the AFP (except for slow) multiple times using different parameters.

The distribution is working fine.

But there are still (spurious) issues with some AFP sessions. With high
contention (a total of 64 worker threads at the same time, e.g. with
threads=2 and -j 32), some sessions will run into suspicious timeouts:

Timing Median_Of_Medians_Selection (2 threads, 25.039s elapsed time,
44.468s cpu time, 2.451s GC time, factor 1.78)
*** Timeout
Median_Of_Medians_Selection FAILED

The timeout for this session is 50 seconds. So I assume that this is
again a problem where the session itself runs through fine, but
something after that is not working well.

I'll send an update when I have more data points.