Comment by pron
16 hours ago
> I think we can increase the TLC model checker throughput to 1 billion states per minute (1000x speedup) by writing a bytecode interpreter.
Truffle [1] can convert an interpreter to a JIT compiler -- there's no need to invent bytecode, and instead of an interpreter you get compilation to native, and it's easy to add intrinsics in Java; optimisations can be added gradually over time. This would probably be the most effective strategy, even in general, and certainly compared to cost.
[1]: https://www.graalvm.org/latest/graalvm-as-a-platform/languag...
That's very neat! I will look at Truffle. The TLA+ interpreter is definitely "weird" in that it does this double duty of both evaluating a predicate while also using that same predicate to extract hints about possible next states. I wonder how well this highly unusual side-effectful pattern can be captured in Truffle.
Edit: okay the more I look into GraalVM the more impressed I am. I will have to sit down and really go through their docs. Oracle was actually cooking here.