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

Lars Hupel hupel at in.tum.de
Fri Jun 22 16:33:58 CEST 2018

> 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:


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.


More information about the isabelle-dev mailing list