undefined

points

[-]

Yeah, the last time I had to check anything regarding memory orderings, I wrote a custom analyzer for that problem. It's...not easy. The state space is enormous too, so even with compiled code I had to take some shortcuts and prove parts of the problem by hand.

by kccqzy2 hours ago|

prev|

[-]

I think the style guides I’ve seen only permit acquire/release memory orders for locks, and relaxed for simple counters. Anything more complicated including lockless hashtables or RCU, using seq_cst is required by the style guide.

The restriction is a good thing because there are very few humans who can reason about acquire/release semantics in situations other than locks.

by senderista1 hours ago|

parent|

[-]

Which style guides? That makes no sense to me because 1) if you're writing a lock-free algorithm/data structure you presumably both know what you're doing and care a lot about performance, 2) many lock-free algorithms don't even require any seq_cst operations (or equivalent fences), and 3) weak memory orderings can be essential to getting acceptable performance in critical paths.

I would also note that aside from formal methods, LLMs are absolutely not trustworthy but the top frontier models can reason to some degree about weak memory orderings, and can at least find concurrency bugs which can be later confirmed by human expert review (preferably after eliminating false positives via adversarial LLM review of the findings).

by kccqzy1 hours ago|

parent|

[-]

The well-known C++ Core Guidelines say this:

> Atomic variables can be used simply and safely, as long as you are using the sequentially consistent memory model (memory_order_seq_cst), which is the default.

That’s from https://isocpp.github.io/CppCoreGuidelines/CppCoreGuidelines

A lot of companies’ in-house guidelines then say you are allowed to use acquire/release if you are implementing a lock, relaxed if are implementing a counter.

This IMO probably reflects most companies’ distrust in their own developers to develop lock free data structures.

by ahelwer3 hours ago|

prev|

[-]

This is true, and it falls into the "possible but not ergonomic" category for modeling systems like this in TLA+. Concurrent programs reading & writing to shared variables can be reordered at two levels: the compiler, and then the CPU. Specifying this in TLA+ is possible but difficult, and your conventional TLA+ specification will assume things happen in a linear order within each thread, and are interleaved arbitrarily between threads. In other words by default PlusCal works like there is both a barrier and memory fence between each action. Even with strong memory semantics like x86-TSO, specifying something like the action of the store buffer (where a core writes a value and can read the updated value but its write is not yet visible to other cores) requires actually writing your own tiny implementation of x86-TSO; there isn't one already defined as a library you can easily use.

I've been thinking lately about how to make this more ergonomic, as I've been getting into lock-free algorithms and would like to be able to specify them nicely in TLA+.