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

Makarius makarius at sketis.net
Sat Jun 23 19:16:24 CEST 2018


On 22/06/18 16:33, Lars Hupel wrote:
> 
> They fail spuriously (except for the last one, which fails reproducibly)
> when running with a total of 64 or even 128 worker threads:
> 
> 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

I am still in the process of exploring the situation (with new and old
hardware).

So far I have merely improved the overall session scheduling:
Isabelle/6984a55f3cba.


	Makarius




More information about the isabelle-dev mailing list