Parallel model checker implementation

[wwl020]

Hi all, thank you for maintaining this great project! I have a question about the status of the parallel model checker implementation. It seems that the parallel model checker has been implemented in the "ik/multicore" branch in 2020 but it has not been merged into the main branch so far.

After reading related pull requests and issues about this feature, I realized that the parallel model checker will not be merged into the main branch (#2275 (comment)). Do you mind sharing some insights behind this decision? Is it because the performance improvement is not significant or the implementation is not stable enough? Thank you!

[konnov]

Hi @wwl020!

True. I have spent quite a bit of time on that. The resulting solution was hard to understand and maintain, so we have decided that it was not worth the effort. In practice, using GNU parallel delivers as good results as more sophisticated solutions. For example, here is the way to parallelize symbolic search:

https://protocols-made-fun.com/specification/modelchecking/tlaplus/apalache/2024/11/03/ben-or.html#43-unexpected-perk--parallel-search

Similar to that, we can parallelize checking of inductive invariants by splitting over invariant indices:

https://apalache-mc.org/docs/apalache/tuning.html#invariant-filter