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

[tlaplus] Current status of TLC multi-core scaling

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...


[1]: https://groups.google.com/g/tlaplus/c/D96Cop_EcN0/m/fh7pNcswBQAJ from a

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/60b08972-af6c-496c-a573-e90483553633n%40googlegroups.com.