"I think we can increase the TLC model checker throughput to 1 billion states per minute (1000x speedup) by writing a bytecode interpreter. C"
I never used TLC with a large model, but I bet making the tool faster would make it more useful to lots of people.
I wonder what the speedup would be if the code targeted a GPU?
Agreed.
But I wonder if the logic of model checking is actually amenable to vectorization. I suspect not really, even for something basic like checking safety properties where you could try to shard the state space across cores. There is still likely to be some synchronization that is needed that eliminates the benefits. A cheaper way to test it would be to look to vectorize on the CPU first.
For a pure hardware based speedup, if there is effort to transcompile TLA+ specs to C++, there could then be a further step to transcompile that to say Verilog and try to run the model checking on an FPGA. That _might_ pay off.
Even 10x speedup would be amazing. Just imagine current 1min check would be performed in 6s.
There is a strong Jevons Paradox effect at play here though, people generally have a set amount of wall-clock time (1 minute, 10 minutes, etc.) they budget to check their model and then find the largest model that fits within that wall-clock time. So really this just increases the size of the state space people will explore, which might be the difference between checking, say, 3 vs. 5 nodes in a distributed system.
For TLA it's even worse. Increasing node counts makes the spec immediately more "correct", at least it feels like that xdd.