> 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
