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

user17732522
  • 53,019
  • 2
  • 56
  • 105
codesavesworld
  • 587
  • 3
  • 10
  • FYI, this is the IRIW litmus test. `acq_rel` or weaker doesn't guarantee that all threads can agree on the order of 2 stores (other than the threads doing the stores; store-forwarding makes your own stores visible instantly). But only some PowerPC machines can actually violate it in real life ([Will two atomic writes to different locations in different threads always be seen in the same order by other threads?](https://stackoverflow.com/a/50679223) explains the mechanism in PowerPC), although some other ISAs have allowed it on paper. – Peter Cordes Aug 28 '22 at 20:54
  • @PeterCordes When Peter writes `acq_rel` he means acq or rel as applicable *not* specifically ops that are acq _and_ rel, which are only RMW ops. (I think that's better made explicit.) – curiousguy Oct 06 '22 at 15:19
  • 1
    @curiousguy: Well I did want to *include* RMW operations with `acq_rel`, `acquire`, `release`, or `relaxed` as part of what I was talking about with anything weaker than seq_cst. I wrote it that way because I consider `acq_rel` stronger than `acquire` or `release`. But yes, also pure load / pure store without seq_cst are important, too, and you can't use `acq_rel` with `.load` or `.store`. – Peter Cordes Oct 06 '22 at 15:22

1 Answers1

6

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

user17732522
  • 53,019
  • 2
  • 56
  • 105
  • is it possible that 2 < 4, so total order is 2 1 3 4, but 4 doesn't observe that stored value? and if there is a global totoal order, occurs before in the total order and happens before don't refer to the same thing ? – codesavesworld Aug 28 '22 at 03:25
  • @codesavesworld No, if a load happens after a store to the same variable in the total order, then the load must observe the value stored by that store (or a store inbetween the two). Yes, the total order and _happens-before_ are separate, but `seq_cst` operations are at the same time acquire/release operations and therefore introduce _synchronizes-with_ relations as you mentioned, which in turn imply _happens-before_ relations between operations in the threads. But these are only really important when talking about reads/writes other than the seq_cst operations. – user17732522 Aug 28 '22 at 03:33
  • so if operation A in thread a happens before operation B in thread b (through synchronizes-with), is it right to say A occurs before B in total order? – codesavesworld Aug 28 '22 at 03:43
  • @codesavesworld (Assuming `A` and `B` are seq_cst operations, otherwise they are not part of the total order at all:) Almost yes. The standard requires this to be true only if A _strongly happens before_ `B`, see [\[atomics.order\]/4](https://eel.is/c++draft/atomics.order#4.sentence-2). This seems to allow more efficient implementation on some architectures (see [note](https://eel.is/c++draft/atomics.order#note-4)). _Strongly happens before_ is a slightly stronger requirement than just _happens before_. See [\[intro.races\]/12](https://eel.is/c++draft/intro.races#12) for a definition. – user17732522 Aug 28 '22 at 03:49