[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Diagnosing TLC Performance Issues
On 15.01.19 08:38, Hillel Wayne wrote:
> I'm currently teaching a class of people how to use TLA+. One thing we
> ran into is that TLC has poor performance on some machines. Running
> VARIABLE x
> Init== x =1
> Next==UNCHANGED x
> Will take either 0 seconds or around 10 seconds across computers. Times
> are consistent: if a computer takes 0 seconds, it takes 0 seconds on
> every run. I had everybody send me TLC logs and the only obvious
> difference I noticed is that the fast machines all had 12 cores, while
> the slow machines all had 8 cores. However, reducing the number of
> workers to 1 does not reduce the performance on the 12 core machines. So
> I don't think that's it, and I've hit a dead end.
can you check if you are affected by issue #227 ?