#include <atomic>
#include <thread>
#include <assert.h>
std::atomic<bool> x,y;
std::atomic<int> z;
void write_x()
{
x.store(true,std::memory_order_seq_cst); // 1
}
void write_y()
{
y.store(true,std::memory_order_seq_cst); // 2
}
void read_x_then_y()
{
while(!x.load(std::memory_order_seq_cst)); // 3
if(y.load(std::memory_order_seq_cst)) // 4
++z;
}
void read_y_then_x()
{
while(!y.load(std::memory_order_seq_cst)); // 5
if(x.load(std::memory_order_seq_cst)) // 6
++z;
}
int main() {
x=false;
y=false;
z=0;
std::thread a(write_x);
std::thread b(write_y);
std::thread c(read_x_then_y);
std::thread d(read_y_then_x);
a.join();
b.join();
c.join();
d.join();
assert(z.load()!=0);
}
In the book C++ Concurrency in Action, the author gives this example when talking about suquential consistency, and says assert can never fire, because
either [1] or [2] must happen first...and if one thread sees x==true and then subsequently sees y==false, this implies that the store to x occurs before the store to y in this total order.
I understant there is a global total order with all sequentially consistent atomic operations, and if one thread sees x == true, that means operation 1 synchronozies with operation 3, and also happens before 3, but my question is if that thread subsequently sees y == false, why it implies 1 happens before 2? is it possible that operation 2 happens before 1 but operation 4 doesn't see that value change?
is it possible that operation 2 happens before 1 but operation 4 doesn't see that value change?
It is important to be careful about the terminology here. What you refer to here as "happens before" is not the happens-before relation used in the description of the memory model. What you mean here is occurs before in the total order of sequentially-consistent operations.
Suppose we write X < Y to mean that operation X occurs before operation Y in that total order. You consider the case 2 < 1. In order for 4 to observe the value before the store we also need 4 < 2. There is also a condition that 3 observes the stored value, otherwise 4 is never reached, so also 1 < 3. Lastly we have that 3 is sequenced-before 4 and the total order must be consistent with that, so also 3 < 4.
All in all:
2 < 1
4 < 2
1 < 3
3 < 4
If you now try to create a total order of 1, 2, 3, 4 satisfying these conditions, you will see that it can't work. For a proof see that 2 < 1 and 1 < 3 imply 2 < 3, which together with 3 < 4 implies 2 < 4. That contradicts 4 < 2.
There is no total order satisfying the conditions and therefore this is not a possible outcome. 4 must be seeing the value after the store which is in fact what the chain I used above deduced as 4 < 2. (If you check carefully replacing the condition 4 < 2 with 2 < 4 in the above does not yield any other contradictions and so you can also find a total order actually satisfying them all.)