I'm using TLC to analyze a spec on a machine with 64 cores, and I'm seeing significantly diminishing returns when adding new cores (a few percent speed-up going from 10 to 60 workers), and I'd like to know what the state of the art options for scaling TLC (obviously, I will profile my model).
Searching the mailing list archives, I found a discussion from a couple of years ago [1] where it was suggested to use OffHeapDiskFPSet, but the state queue implementation was still mentioned as a bottleneck. The 1.6.0 release notes also mentioned ByteArrayQueue, switching to which yielded a 30% speedup with many cores. Is using these two the best I can do today? Is there anything else on the horizon that might improve scaling.
Also, have you considered documenting the options to switch the fingerprint/queue implementations in current-tools.pdf? They were not easy to find otherwise. I'm happy to send a PR...
Best,
Ognjen
[1]:
https://groups.google.com/g/tlaplus/c/D96Cop_EcN0/m/fh7pNcswBQAJ from a