c++11 atomic ordering: extended total order memory_order_seq_cst for locks

atomic, c++, c++11, multithreading

Solution

What does it mean by "always"?

Always means that there exists a total order `S+l` on `seq_cst ops U lock ops` that is consistent with `happens-before` and `S`.

Why is that

Fact 1: `S` is a total order consistent with `HB`.

Fact 2: Lock operations are ordered in the `HB` partial order, because they are acquire/release operations.

Fact 3: There are no cycles in `HB`.

Lemma 1: There are no cycles in `S' = S union HB`.

Proof: If there were any cycles in `S'`, they would be in the form `Aop1 <S Aop2 <HB Aop1`, because any two atomic operations are comparable in `S` and happens-before is transitive. That would contradict with Fact 1. QED

Conclusion: Because for each partial order (= without cycles) there exists its extension to total order (cf. topological sorting), there is a total order extending `S'`. So you just pick atomics and lock operations from it and get `S+l`.

But in some general implementation that wasn't designed for it, I don't see that S can be extended so.

Such an implementation would not satisfy `mem_order_seq_cst` requirements.

Problem

from c++11 29.3-p3: There shall be a single total order S on all memory_order_seq_cst operations, consistent with the "happens before" order and modification orders for all affected locations, such that each memory_order_seq_cst operation B that loads a value from an atomic object M observes either one of the following values: -- the result of the last modification A of M that precedes B in S, if it exists, or -- if A exists, the result of some modification of M in the visible sequence of side effects with respect to B that is not memory_order_seq_cst and that does not happen before A, or -- if A does not exist, the result of some modification of M in the visible sequence of side effects with respect to B that is not memory_order_seq_cst. [ Note: Although it is not explicitly required that S include locks, it can always be extended to an order that does include lock and unlock operations, since the ordering between those is already included in the "happens before" ordering. --end note ] In the last note, what does it mean by "always"? I can understand that any certain implementation can be designed to support such an extended S. But in some general implementation that wasn't designed for it, I don't see that S can be extended with the described properties. Does it mean an extended order that also satisfies the same visibility properties here? I had sent this question to comp.std.c++ but got no answers there. http://groups.google.com/group/comp.std.c++/browse_frm/thread/5242fa70d0594d1b#

Original source