Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc
> 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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] Nontermination in HOL-Corec_Examples on Epyc
>> 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. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
