[redixhumayun]

Are there tools out there that can prove semantic invariants in multi-threaded code? I don't understand how there can be automated tools around it at all because how would that even be possible?

[jeffreygoesto]

TLA+ comes to mind

[0] https://www.learntla.com/index.html

[kangda123]

There are model checkers such as nidhugg (C++), dscheck (ocaml). They take a test case and reach all possible terminal states by trying different interleavings.

Crucially, they don’t have to try all interleavings to reach all terminal states, making the enumeration quite fast.

[maxbond]

Rust comes to mind.

[redixhumayun]

How would Rust solve this problem?

[maxbond]

All I meant was that it "proves semantic invariants in multi-threaded code," which proves the concept.

[kaba0]

No data races is just a very tiny subset of semantic invariants, though.

[redixhumayun]

I assumed what the poster above meant was that Rust can take care of more than just data races. Specifically Rust can solve the ABA problem somehow?

[maxbond]

Rust won't solve the ABA problem, no. You'd be in unsafe Rust if you were writing something that could encounter the ABA problem.

You wondered out loud how it was even possible to do that kind of analysis, and that's where my mind went. Evidently people think it's a bad take. That's as deep as it goes.