Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Atomics and Concurrency

redixhumayun.github.io

Post reply on HN
Print view View original

11–20 of 52 posts

Re: Atomics and Concurrency

#11

Post by kangda123 »

redixhumayun wrote: post #5
saagarjha wrote: post #4

Earlier quoted context omitted.

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.

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.

Re: Atomics and Concurrency

#14

Post by saagarjha »

chc4 wrote: post #9
saagarjha wrote: post #4

Earlier quoted context omitted.

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.

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…

Tired: deadlocks

Wired: livelocks

Re: Atomics and Concurrency

#15

Post by kaba0 »

maxbond wrote: post #12
redixhumayun wrote: post #10

Earlier quoted context omitted.

How would Rust solve this problem?

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

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

Re: Atomics and Concurrency

#16

Post by gpderetta »

IMHO that the graph in the Memory Barrier section is misleading [1]. It has the barriers spanning across threads, but that's not the right mental model. Something like this is more correct (note the additional barriers after the store and before the load to match seq_cst semantics):

  Thread 1                Memory                  Thread 2
  ---------               -------                 ---------
  |                          |                          |
  |   write(data, 100)       |                          |
  | -----------------------> |                          |
  |                          |                          |
  | ====Memory Barrier====== |                          |
  |   store(ready, true)     |                          |
  | -----------------------> |                          |
  | ====Memory Barrier====== |                          |
  |                          |                          |
  |                          | ===Memory Barrier======= |
  |                          |   load(ready) == true    |                   
  |                          |
I.e. barriers prevent reordering of operations within a thread, not across threads. It also makes immediately obvious why the seq_cst ordering of both the thread 1 atomic store and the thread 2 atomic load can be relaxed: The last barrier in Thread 1 does not prevent any reordering in this example, hence it can be omitted, leaving only the barrier before the store making it a release operation. Similarly, we can omit the barrier before the first load in thread 2, leaving only the barrier after, making it an acquire operation.

[1] well, it is showing the effect of sequential consistency as opposed to acquire-release, so a logical barrier spanning threads is not necessarily wrong, but then you would still need to show a barrier before the last store and the first load.

Re: Atomics and Concurrency

#17

Post by gpderetta »

chc4 wrote: post #9
saagarjha wrote: post #4

Earlier quoted context omitted.

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.

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…

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.

Re: Atomics and Concurrency

#18

Post by el_pollo_diablo »

There are many problems with this concurrent queue. Here are a few I found in a cursory reading.

In order to enqueue an element, you have to change two atomic pointers: tail->next and tail. That cannot be done atomically.

enqueue() assumes that the queue is not empty.

enqueue() happily overwrites current_tail->next even if it is not null (which may happen if some other producer has enqueued something since we read current_tail).

Then there is the old-time favourite ABA problem.

By the way, when used in a loop, compare_exchange_weak is preferred to compare_exchange_strong, and there is no need to reload the atomic every time: compare_exchange_* do that for you by updating the argument containing the expected value.

Re: Atomics and Concurrency

#19

Post by redixhumayun »

gpderetta wrote: post #16

IMHO that the graph in the Memory Barrier section is misleading [1]. It has the barriers spanning across threads, but that's not the right mental model. Something like this is more correct (note the additional barriers after the store and before the load to match seq_cst semantics): Thread 1 Memory Thread 2 --------- ------- --------- | | | | write(data, 100) | | | -----------------------> | | | | | | ====Memory Barr…

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

```

  Thread 1                Memory                  Thread 2
  ---------               -------                 ---------
  |                          |                          |
  |   write(data, 100)       |                          |
  | -----------------------> |                          |
  |                          |                          |
  | ====Memory Barrier====== |                          |
  |   store(ready, true)     |                          |
  | -----------------------> |                          |
  | ====Memory Barrier====== |                          |
  |                          |                          |
  | ====Memory Barrier====== |                          |
  |   store(not_ready, true) |                          |
  | -----------------------> |                          |
  | ====Memory Barrier====== |                          |
  |                          |                          |
  |                          | ===Memory Barrier======= |
  |                          |   load(ready) == true    |                   
  |                          |
```

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?

Re: Atomics and Concurrency

#20

Post by redixhumayun »

kaba0 wrote: post #15
maxbond wrote: post #12

Earlier quoted context omitted.

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

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

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?
Post reply on HN