[saagarjha]

Yeah, this stuff is hard even before you bring memory ordering into the picture. What's worse, checks such as thread sanitizer will not catch it, since it's not a simple data race. Proving functional invariants about multithreaded code requires a different class of tools.

[chc4]

Funnily enough, ARM has another difference here on top of just having a non-TSO memory model: LL/SC atomics solve the ABA problem, because the word holding the queue head has been written to and the store-conditional fails, even though the contents of the memory will be the same at the end. Which makes sense once you say it and some docs about LL/SC will mention that, but also reading various lockfree data structure papers I've basically never seen talked about (probably because LL/SC progress guarantees are kinda scuffed)

[gpderetta]

the issue with LL/SC is that it is hard to expose to higher level languages than assembler. What you can do within an LL/SC section without causing it to spuriously fail is very much architecture dependent and you need full control of the load and stores within it. Exposing it to compiler optimizations won't work reliably.

So in practice LL/SC, in higher level languages, is used to implement CAS, XCHG and other atomic primitives which don't allow taking advantage of the ABA resistance. As an additional downside, you get a weak CAS that you always need to call in an loop.

[saagarjha]

It would be nice if compilers can lower this back to LL/SC if that’s what you actually wanted.

[saagarjha]

Tired: deadlocks

Wired: livelocks

[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?