Hi,
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.
Since Apalache was mentioned in this thread, there is probably a way to exploit GPUs for speeding up symbolic model checking. The main SMT encoding that is implemented in Apalache is almost propositional, with the exception being made for integers and string constants [1]. So instead of translating a TLA+ spec to SMT, we could translate it to SAT. (If we fix the bit width, we can translate integers by bit blasting.) That would let us run a GPU-enabled SAT solver such as ParaFROST [2].
Apalache was designed with alternative encodings in mind. For instance, we are currently experimenting with SMT arrays, and this required well-isolated changes in the rewriting rules. So this all sounds nice in theory. In practice an alternative encoding would require at least 6 months of devoted work. If somebody is looking for an internship on this topic at Informal Systems [3] or wants to do it as part of their research, please let me know. It is much easier to extend Apalache than to write a new model checker for TLA+ from scratch.
PS: Alex, thanks for the kind words about Apalache :)
[1] TLA+ model checking made symbolic:
https://dl.acm.org/doi/10.1145/3360549
[2]
https://github.com/muhos/ParaFROST
[3]
https://informal.systems/
Best regards,
Igor
> To view this discussion on the web visit
https://groups.google.com/d/msgid/tlaplus/CABW84KxsSaMQR-SHfWipAYa3pbW8BJBv6NRBV2u11XEqxsMLYw%40mail.gmail.com.