I love this. This is great to read if you are trying to use TLA+ for something.
In a different vein, another thing TLA+ isn't great at is modeling atomics and in particular weak-memory semantics or anything that's not sequentially consistent. If you translate your algorithm to pcal, it will run as if it was sequentially consistent. If you need to model non-sequential-consistency, then that needs to be spelled out with explicit logic to TLA+, which is probably too complicated and error-prone to do by hand. The C/C++/Rust memory models permit a lot of wacky stuff. I imagine you need to add read caches and writeback buffers for each variable with cache-flushing instructions at appropriate points, but maybe there is a more elegant way to do it.
If you use rust, miri and loom both have analyzers that can check some non-sequentially-consistent behavior (and loom doesn't actually implement sequential-consistency at all).
For C++ GenMC is probably the state of the art for this: <a href="https://plv.mpi-sws.org/genmc/" rel="nofollow">https://plv.mpi-sws.org/genmc/
singron · · focus · HN ↗
In a different vein, another thing TLA+ isn't great at is modeling atomics and in particular weak-memory semantics or anything that's not sequentially consistent. If you translate your algorithm to pcal, it will run as if it was sequentially consistent. If you need to model non-sequential-consistency, then that needs to be spelled out with explicit logic to TLA+, which is probably too complicated and error-prone to do by hand. The C/C++/Rust memory models permit a lot of wacky stuff. I imagine you need to add read caches and writeback buffers for each variable with cache-flushing instructions at appropriate points, but maybe there is a more elegant way to do it.
If you use rust, miri and loom both have analyzers that can check some non-sequentially-consistent behavior (and loom doesn't actually implement sequential-consistency at all).
anonymousDan · · focus · HN ↗
There's also RustMC for Rust.