Many programming languages today have happens-before
relation and release+acquire
synchronization operations.
Some of these programming languages:
- C/C++11: happens-before, release+acquire
- Rust and Swift adopted the C/C++ memory model in its entirety — so they have that too.
- Java: happens-before, release+acquire.
I would like to know if release+acquire
can violate happens-before
:
- if it's possible, then I would like to see an example
- if it's impossible, then I would like to get simple and clear explanations why
What is release+acquire
and happens-before
Release/acquire
establishes happens-before
relation between different threads: in other words everything before release
in Thread 1
is guaranteed to be visible in Thread 2
after acquire
:
\ Thread 1 /
\ -------- /
\ x = 1 / Everything
\ y = 2 / here...
\ write-release(ready = true) /
└───────────────────────────┘
|
└─────────────┐ (happens-before)
V
┌─────────────────────────┐
/ Thread 2 \
...is visible to / -------- \
everything / read-acquire(ready == true) \
here / assert(x == 1) \
/ assert(y == 2) \
More than that, happens-before
is a strict partial order.
This means it is:
- transitive:
Thread 2
is guaranteed to see not only writes made byThread 1
, but also all writes by other threads thatThread 1
saw - asymmetric: either
a
happens-beforeb
, orb
happens-beforea
, both isn't allowed
Why I think that release/acquire
might break happens-before
As we know from IRIW litmus test, release/acquire
could cause two threads to see writes from different threads in different order (for C++ see also the last example here, and these two examples from gcc wiki):
// Thread 1
x.store(1, memory_order_release);
// Thread 2
y.store(1, memory_order_release);
// Thread 3
assert(x.load(memory_order_acquire) == 1 && y.load(memory_order_acquire) == 0)
// Thread 4
assert(y.load(memory_order_acquire) == 1 && x.load(memory_order_acquire) == 0)
Here both assert
s can pass, which means that Thread 3
and Thread 4
see writes to x
and y
in different order.
As I understand, if it were ordinary variables, then this would violate the asymmetry property of happens-before.
But because x and y are atomics it's OK.
(BTW I am not sure about that)
Nate Eldredge demonstrated in his answer that this IRIW example is OK.
But I still have a sneaking suspicion that there might be something similar to IRIW which would cause Thread 3
and Thread 4
to see regular writes to happen-before in different order — this would break happens-before (it wouldn't be transitive anymore).
Note1
In cppreference there is also this quote:
The implementation is required to ensure that the happens-before relation is acyclic, by introducing additional synchronization if necessary (it can only be necessary if a consume operation is involved, see Batty et al)
The quote hints that there might be cases when happens-before
is violated and which require additional synchronization ("acyclic" means that happens-before forms a directed acyclic graph, which is equivalent to saying "strict partial order").
If it's possible I would like to know what are these cases.
Note2
Since java allows data races, I'm also interested in cases when happens-before
is violated only in presence of data races.
Edit 1 (03 Nov 2021)
To give you an example, here is a explanation why sequentially consistent (SC) atomics cannot violate happens-before
.
(A similar explanation for release/acquire atomics would be an answer to my question).
By "violate happens-before
" I mean "to violate axioms of happens-before
, which is a strict partial order".
Strict partial orders correspond directly to directed acyclic graphs (DAGs).
Here is an example of a DAG from wiki (note that it has no cycles):
Let's show that with SC atomics happens-before
graph stays acyclic.
Remember that SC atomics happen in a global order (the same for all threads), and:
- the order is consistent with the order of actions within each thread
- every SC atomic read sees the latest SC atomic write in this total order to the same variable
Look at this happens-before
graph:
Thread1 Thread2 Thread3
======= ======= =======
│ │ │
W(x) │ │
↓ │ │
Sw(a) ┐ │ W(y)
│ │ │ ↓
│ └> Sr(a) ┌ Sw(b)
│ ↓ │ │
│ Sr(b)<─┘ │
│ ↓ │
│ R(x) │
│ ↓ │
│ R(y) │
│ │ │
V V V
On the graph:
- time flows downwards
W(x)
andR(x)
are regular actions: write and read ofx
Sw(a)
andSr(a)
are SC atomics: write and read ofa
- within each thread actions happen in a program order (aka
sequenced-before order
in C++): in the order they go in the code - between threads
happens-before
is established by SC atomics
Note that arrows on the graph always go downwards
=> the graph cannot have cycles
=> it's always a DAG
=> happens-before
axioms cannot be violated
The same proof doesn't work for release/acquire
atomics because (as far as I understand) they don't happen in a global order => a HB arrow between Sw(a)
and Sr(a)
might go upwards => a cycle is possible. (I'm not sure about that)