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

Re: [tlaplus] TLC on the GPU

The search for strongly connected components (SCC) is the (scalability) bottleneck of TLC's liveness checking.  It would be interesting to find out how GPU-based SCC search algorithms such as [1,2] perform on TLA+ liveness graphs.  In previous work, we collected statistics about the shape of the average TLA+ liveness graph.  One could use these statistics to generate synthetic graphs in addition to the existing real-world graphs.


[1] https://dl.acm.org/doi/10.1145/3026937.3026941
[2] https://link.springer.com/chapter/10.1007/978-3-319-08867-9_20

On Feb 18, 2022, at 8:21 AM, Igor Konnov <igor.konnov@xxxxxxxxx> wrote:

I am joining this conversation a bit late. It seems to me that the main challenge with parallelizing explicit-state enumeration is that transition systems of concurrent and distributed algorithms do not have much locality.

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/FA267897-C49A-45C5-8D22-FCFAB9B1F6F4%40lemmster.de.