I wrote a little bit about extendible hash tables and put some effort into creating visualisations around them. Mostly because this is something I struggle with when learning about a new topic - how to "see" what's happening
Honestly, now that I look back at it having written it a couple of weeks ago, it doesn't feel that long. But, writing it felt incredibly wrong because I was encountering memory models for the first time.
I think for someone who has no exposure to it before, its quite dense (perhaps long wasn't the best choice of wording)
Also, I've been meaning to read The Art of Multiprocessor Programming. I've heard great things about it!
You shouldn't feel bad about it - the blog is going to have its audience, so don't worry about it. That said, the topic is incredibly complex and to understand it fully requires intimate knowledge of the CPU microarchitectural details and design. So, technically speaking even the links from the comment you're replying to are providing a shallow although somewhat longer introduction. Programming languages only provide an abstraction for these very real things happening in the silicon so that's about as far as they can go by providing the sufficient amount of details. The real meat is down the rabbit hole of the CPU and memory subsystem design and if you want to go there I'd suggest the yt lectures from ETH Zurich on the topic of computer architectures and design (can find the link later).
That concurrent queue is only there to illustrate usage of CAS in a data structure. I think having an actual implementation of a concurrent queue along with handling the ABA problem might be an entirely separate post.
I added in a note about the ABA problem but perhaps you're seeing a cached version of the post.
Hey, so I'm curious why having memory barriers span across threads is the wrong mental model.
Assuming that the memory barrier is syncing across a single variable (in this case ready), why would it be correct to think of it as two separate barriers? If it were correct to think of it as two separate barriers on two separate threads, wouldn't there need to be some form of synchronization or linkage between the two barriers themselves so that memory barriers can be coupled together?
For instance, if I had release-acquire models on two variables, ready and not_ready, using separate barriers as representation might look something like this
Now, how does the processor know which memory barriers are linked together? I ask because without understanding which barriers are linked together, how is instruction re-ordering determined?
The linking of barriers in pair is really just a mental model, not (usually) what happens at the hardware level. In fact in the C++ memory model the synchronizes-with relationship is load and stores, not barriers, which indirectly affect the properties of load and stores around them. That's another reason why I don't really like the memory barrier model and I prefer to think in terms of happens-before dependency graphs.
edit: AFAIK, seq_cst ordering (as opposed to acq_rel) is only relevant when you have more than two threads and you care about things like IRIW. In this case acquires and releases are not enough to capture the full set of constraints, although at the hardware level it is still everything local.
edit2: I guess the missing bit is that beyond the hardware fences you have the hardware cache coherency protocol that makes sure that a total order of operations always exist once load and stores reach the coherence fabric.
>I guess the missing bit is that beyond the hardware fences you have the hardware cache coherency protocol that makes sure that a total order of operations always exist once load and stores reach the coherence fabric.
Modern processors are out-of-order execution beasts. A barrier within a thread serves to enforce some ordering within that thread - that a store will occur after another store, and that a load will occur before another load. Threads know nothing of each other.
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?
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.
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.
The ABA problem is a false-positive execution of a CAS speculation on a shared memory location.
It is very easy to create an ABA problem in safe Rust. Data race free sequential consistency, which Rust has, is almost completely orthogonal to the ABA problem.
This is an area of active PLT research, we haven't come anywhere close to addressing the problem in the general case.
I suspect we'll be seeing all kinds of bugs caused by a generation of programmers thinking everything has guard rails in Rust because "safety", so they can turn their brain off and not think. In reality, those promises of safety largely disappear when threads, files, signals, and networks are involved.
At the end of the day, your programs run on computers which exist in the physical world. The abstractions are mostly isomorphic, but it's at the margins where the abstractions aren't isomorphic that all the interesting things happen.
> The ABA problem is a false-positive execution of a CAS speculation on a shared memory location.
In safe Rust, if I have a mutable reference to Foo, and Foo contains a shared reference to Bar, then no other thread has a mutable reference to Foo or Bar. So no other thread will make a CAS on my reference to Bar, or drop Bar and then allocate something at the same memory address, etc.
You could have some higher level ABA problem I suppose, where you acquire a lock, read a value, give up the lock, and then make spurious assumptions about what happens while you've let the lock go. But that's obviously not what we're talking about if we're talking about CAS. (ETA: or if these were application level references, eg indices into a list.)
If we're going to implement a lockfree data structure, we're going to need unsafe Rust to hand-roll interior mutability. Because we're going to be sharing mutable state. Which isn't allowed in safe Rust.
I guess? I've only ever heard about the ABA problem in reference to pointers, eg in the context of lockfree queues. Maybe that's my ignorance. (Which is why I addressed shared references in my comment.)
Yes, if you don't hold a lock on a value, or exert some kind of control at the API level (eg making it monotonic so your CAS will work), you can't make assumptions about it. I think you'll find that Rust developers understand that concept about as well as any other community of concurrent developers.
But yes, granted, the semantic information about these integers isn't represented in Rust's type system, and won't be caught by it's static analysis.
Can you share more about how you are prompting to disable sycophancy?