[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Diagnosing TLC Performance Issues

Hi Everyone,

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


Init ==  x = 1


Spec == Init /\ [][Next]_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.

I don't think I have enough data to diagnose the likely issues or file an informative bug report, so my goal here is to find out what else I should be looking for. Since these are other people's computers I can't do anything complicated or test stuff for more than five minutes at a time or so. The workshop goes the whole week, though, so I can try a few different short things. How can I get more data on what could be wrong here?

Some notes I have so far: