Re: [tlaplus] TLC on the GPU

[tlaplus-google-group@xxxxxxxxxxx]

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.

Markus

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