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?
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.
So formal methods may be used for extremely critical parts of systems (eg; safety critical systems or in embedded where later fixes cannot be readily rolled out) but they fail to make inroads in most other development because it's a lot of extra work.
But yeah, that's basically the answer to the conformance problem for these sort of lightweight formal methods. Trace validation or model-based testing.
[0] https://buttondown.com/hillelwayne/archive/requirements-chan...)
0. https://conf.tlapl.us/2020/11-Star_Dorminey-Kayfabe_Model_ba...
Damn. Happened a 10 minute drive from my house and I didn't even know about it.
TLA+ is on the infinite bucket list for me. I'm sure like many others, I know the value of learning and applying formal verification, but it feels impenetrable knowing really how to jump in.
It surely did produce a fancy, mathy PDF which I proudly shown and explained to my team, but honestly, a little duck-talking would have permitted to find the same bug without TLA+
For aome context, it's a CRUD api + web interface for external clients, nothing too complicated, and I really wanted to try TLA+ in real life
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...
A few years ago I tried making some contributions to the TLC codebase. It was definitely "academic code," lacking tests, reinvesting basic structured instead of using them from libraries, and largely the work of a single contributor with seemingly no code reviews for commits. I was motivated to try to help improve things and wanted to get a sense for what that would be like by sending a small PR to get a feeling for working with the code owners. They basically stonewalled me. It was odd.
Modeling languages are useful to check the correctness of an algorithm during development. During development, a model can also serve as a specification for the actual implementation. This requires that your the modeling language is readable to a broad range of developers, which TLA+ is not. We have been experimenting with FizzBee (fizzbee.io) which looks promising in this regards.
When you go to prod, you really want to test your actual implementation, not a model of it. For this you want something like https://github.com/awslabs/shuttle (for Rust), or https://github.com/cmu-pasta/fray (for Java). Or use something custom.
femto2151•3h ago