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

[Lars Hupel]

> 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

Here are the offending sessions:

Dict_Construction
Hidden_Markov_Models
Median_Of_Medians_Selection
Mason_Stothers

They fail spuriously (except for the last one, which fails reproducibly)
when running with a total of 64 or even 128 worker threads:

./isabelle/bin/isabelle build -cbv -a -d afp-devel/thys/ -X slow -o
threads=2 -j 32

./isabelle/bin/isabelle build -cbv -a -d afp-devel/thys/ -X slow -o
threads=4 -j 32

None of this happens when using a total of just 32 worker threads.

Makarius, David, this probably requires another round of analysis.

Isabelle/b6e48841d0a5
AFP/00e13b87d199