#include <atomic>
#include <thread>
#include <cassert>
#include <chrono>
std::atomic<int> x {}, y {};
void write_x_and_y() {
x.store(1, std::memory_order_seq_cst); // 1
y.store(-1, std::memory_order_relaxed); // 2
}
void read_x_then_y() {
while(x.load(std::memory_order_seq_cst) not_eq 1); // 3
assert(y.load(std::memory_order_seq_cst) < 0); // 4
}
int main(int argc, char *argv[]) {
A: std::thread t1(write_x_and_y), t2(read_x_then_y);
t1.join();
t2.join();
goto A;
}
First, reordering is never considered. Because if 2 is reordered and it happens before 1, the relaxed-store 2 will be synchronized while operation 1 released. We can see that (A happens before B will be marked as A->B)
1 has not happened, 3 and 4 will never happen, so we can assume that 1 happens before 3. We have 1->3 and 1->4;t1 and t2, we have 1->2 and 3->4.So there are three global sequences left :
1->2->3->4;1->3->2->4;1->3->4->2.In S1 and S2, assertion in t2 is always correct. S3 is not a valid global sequence. My opinion is very simple, a relaxed-store is able to be shown in a global sequence only if some load-operations sees the value. In order S3, no one sees the result of y.store(-1), so 2 cannot be shown in the global sequence.
I asked ChatGPT. ChatGPT gave me a rigorous analysis, but the answer confused me.
ChatGPT thinks no rings can appear in a global sequence. But I cannot find a ring in 1->3->4->2, maybe ChatGPT means
|--------|
1->3->4->2
In this graph, it's impossible to go back to the starting node when we traversal from the starting node. And then ChatGPT said the definition of cycle in global sequence is different from the definition in Graph Theory. Finally, ChatGPT said you can list all orders and align them, if you find
Order O1 : 1->3->4->2
Order O2 : 1->2
2 comes after 4 in O1 but 2 comes before 4 in O2,
the sequence 1->3->4->2 is invalid??? I always feel that this method is very arbitrary and lacks rigorous basis.
In comments, you clarified that by "global sequence" you mean the total order S defined in atomics.order p4. This is clearly defined as an order on the seq_cst operations only. Your relaxed store #2 is not an element of this order at all. So the only possible ordering for S is 1 -> 3 -> 4.
a relaxed-store is able to be shown in a global sequence only if some load-operations sees the value
There is no such rule. A relaxed load or store will never appear in the global total order S, by its very definition.
The assert can certainly fail. In fact, it can fail even if you strengthen #2 to be seq_cst. In that case, 1 -> 3 -> 4 -> 2 is a perfectly valid ordering for S, because there is no rule that forbids it. It does not contain a "ring" (the more usual term is "cycle") because 2 does not have to precede any of the other operations - there is no rule which would require that it does.
I asked ChatGPT.
That's not typically helpful with questions like this. Showing your research effort in your question is encouraged, but asking ChatGPT isn't very productive, and telling us what it said does not contribute much of value to the question. Tell us what you tried in your efforts to solve the problem, not what a machine tried.
See also How can I handle questions which provide an MCVE or "what I tried" generated by ChatGPT?
ChatGPT gave me a rigorous analysis
No, it gave you nonsense that looks like a rigorous analysis.
but the answer confused me.
Because it is nonsense.