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

Makarius makarius at sketis.net
Sun Jun 24 23:27:15 CEST 2018


On 23/06/18 19:16, Makarius wrote:
> 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).

Which HD product is actually /dev/sda on the new hardware?

I don't have root access to query it e.g. via "sudo lshw -class disk
-class storage".


	Makarius



More information about the isabelle-dev mailing list