c - C11 内存模型真的与常见的优化冲突吗？

Question

a recent question的OP添加了一条评论，链接了一篇题为 Common Compiler Optimisations are Invalid in the C11 Memory Model and what we can do about it 的论文。 ，这显然是在 POPL 2015 上提出的。除其他外，它声称展示了从所谓的“C11 内存模型”的规范中得出的几个意想不到的和违反直觉的结论，我认为它主要由 section 5.1.2.4 的规定组成。 C11 语言规范。
这篇论文有点冗长，但出于这个问题的目的，我将重点放在第二页上对“SEQ”方案的讨论。这涉及一个多线程程序，其中...

a是非原子的(例如， int )，

x和 y是原子的(例如， _Atomic int )和

a , x , 和 y所有最初都有值(value) 0 ,

...然后发生以下情况(从伪代码音译):

主题 1

a = 1;

主题 2

if (atomic_load_explicit(&x, memory_order_relaxed))
    if (a)
        atomic_store_explicit(&y, 1, memory_order_relaxed);

主题 3

if (atomic_load_explicit(&y, memory_order_relaxed))
    atomic_store_explicit(&x, 1, memory_order_relaxed);

该论文提出了这样的论点:

First, notice that there is no execution (consistent execution inthe terminology of Section 2) in which the load of a occurs. We show thisby contradiction. Suppose that there is an execution in which a loadof a occurs. In such an execution the load of a can only return 0 (theinitial value of a) because the store a=1 does not happen before it(because it is in a different thread that has not been synchronisedwith) and non-atomic loads must return the latest write that happensbefore them. Therefore, in this execution the store to y does not happen,which in turn means that the load of y cannot return 1 and the storeto x also does not happen. Then, x cannot read 1, and thus the load of a doesnot occur. As a consequence this program is not racy: since the loadof a does not occur in any execution, there are no executions withconflicting accesses on the same non-atomic variable. We conclude thatthe only possible final state is a=1 ∧ x=y=0.

(问题1) 但是，这个论点不是有致命的缺陷吗？
断言 a的负载只能返回 0 的前提是 a实际上是阅读，该论证旨在反驳。但在这种情况下，正如论文所观察到的，在商店与 a 之间没有任何关系之前发生。在线程 1 和来自 a 的负载中在线程 2 中。这些是冲突访问，既不是原子访问，也不是写操作。因此，根据第 5.1.2.4/25 段，该程序包含导致未定义行为的数据竞争。由于行为未定义，因此无法对从 a 加载的值得出任何结论。通过线程 2，特别是，不能从规范中得出负载必须返回 0 的结论。 .其余的论点随后崩溃。
尽管该论文声称该论证表明该程序不包含数据竞争(“不活泼”)，但实际上这不是论证的结果，而是一个隐藏的假设。仅当与 5.1.2.4/25 不同，程序不包含数据竞争时，该论点才成立。
现在也许关键是上面的论点只考虑了“一致执行”，这是本文后面部分定义的术语。我承认在这一点上它对我来说有点深，但如果实际上将行为限制为一致的执行就足以支持 a 的负载的断言。必须返回0，那么看来已经不是(只是)我们说的C11内存模型的规则了。
这很重要，因为作者得出结论，源到源的翻译结合了线程 1 和 2 以产生......

线程 2'

a = 1;
if (atomic_load_explicit(&x, memory_order_relaxed))
    if (a)
        atomic_store_explicit(&y, 1, memory_order_relaxed);

... C11 内存模型不允许实现，因为它允许最终状态为 a = x = y = 1 的执行.这个和其他各种代码转换和优化是无效的，这是论文的主题。
(问题2) 但是对于 C11 实现来说，将原始的三线程程序视为由线程 2' 和 3 组成的双线程程序是否确实有效？
如果这允许“一致执行”的结果不能由原始程序的任何一致执行产生，那么我认为这只是表明 C11 不限制程序表现出一致的执行。我在这里错过了什么吗？

Answer 1

显然，没有人有足够的兴趣和信心来写答案，所以我想我会继续。

isn't that argument fatally flawed?

从论文中引用的证明旨在证明不允许符合标准的 C 实现执行问题中描述的源到源转换，或等效的， 是 ，证明有问题。问题中提出的反驳是合理的。
评论中有一些关于如何将反驳视为归结为在未定义行为的情况下允许的任何事情的讨论。这是一个有效的观点，绝不会削弱论点。但是，我认为这是不必要的简约。
同样，论文证明的关键问题在这里:

the load of a can only return 0 (the initial value of a) because thestore a=1 does not happen before it (because it is in a differentthread that has not been synchronised with) and non-atomic loads mustreturn the latest write that happens before them.

证明的错误是语言规范要求读取 a必须将写入结果返回到 a “之前发生过”的条件是程序没有数据竞争。这是整个模型的重要基础，而不是某种逃生舱口。如果实际上读取 a，该程序显然不是没有数据竞争的。已执行，因此在这种情况下要求没有实际意义。阅读 a线程 2 绝对可以观察线程 1 的写入，并且有充分的理由假设它在实践中有时可能会这样做。
换个角度来看，证明选择关注在读之前没有发生的写，但忽略了读也没有在写之前发生的事实。
考虑宽松的原子访问不会改变任何东西。在论文的三线程程序的实际执行中，该实现(例如)推测性地执行 x 的松弛负载是合理的。在线程 2 中假设它将返回 1，然后从 a 读取线程 1 写入的值，因此执行存储到 y .因为原子访问是用宽松语义执行的，线程 3 的执行可以读取 y 的值。为 1(或推测它会这样做)并因此执行写入 x .然后可以确认所有涉及的推测是正确的，最终结果 a = x = y = 1。这个看似矛盾的结果是有意为“放松”的内存顺序所允许的。

isn't it indeed valid for a C11 implementation to treat the originalthree-threaded program as if it were the two-threaded programconsisting of threads 2' and 3?

至少，论文的论点没有另外表明，即使我们——没有规范的基础——将数据竞争引起的 UB 的范围解释为仅限于是否从 a 读取的值。是它的初始值还是线程 1 写入的值。
只要实现产生与抽象机器所需的行为一致的可观察行为，就可以获得广泛的许可来按照他们的选择行事。多个执行线程的创建和执行本身并不是程序可观察行为的一部分，正如规范所定义的那样。因此，是的，一个程序执行了建议的转换，然后执行了相应的操作，或者一个程序的行为就像在写入 a 之间的边缘之前发生了发生一样。以及来自 a 的阅读, 不会与规范不一致。