C sequential consistency and happens before relation-CodePudding

    #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?

CodePudding user response：

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:

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.)