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

最近一个问题的 OP添加了一条评论，链接了一篇题为C11 内存模型中的通用编译器优化无效以及我们可以做些什么的论文，这显然是在 POPL 2015 上提出的。除其他外，它声称展示了几个从所谓的“C11 内存模型”的规范中得出的意外和违反直觉的结论，我认为主要由C11 语言规范第 5.1.2.4 节的规定组成。

这篇论文有点冗长，但出于这个问题的目的，我将重点放在第二页上对“SEQ”方案的讨论。这涉及一个多线程程序，其中...

• a是非原子的（例如， an int），
• x并且y是原子的（例如，_Atomic int），并且
• a, x, 和y所有最初都有价值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);

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

首先，请注意没有发生负载的执行（第 2 节术语中的一致执行）a。我们通过矛盾来证明这一点。假设有一个执行，其中a发生了负载。在这样的执行中， 的加载a只能返回0（ 的初始值a），因为存储a=1不会在它之前发生（因为它位于尚未与之同步的不同线程中）并且非原子加载必须返回最新的写入发生在他们面前。因此，在这次执行中 store toy不会发生，这反过来意味着加载y无法返回1并且 store tox也不会发生。然后，x无法读取1，因此a不会发生的负载。因此，该程序不活泼：由于a在任何执行中都不会发生的加载，因此不会有对同一非原子变量的访问冲突的执行。我们得出结论，唯一可能的最终状态是a=1 ? x=y=0。

（问题1）但是这个论点不是有致命的缺陷吗？

的负载a只能返回 0的断言受制于a实际读取的假设，该参数旨在反驳。但在那种情况下，正如论文所观察到的，线程 1 中的存储到线程和线程 2 中的加载之间没有发生之前的关系。这些是冲突访问，既不是原子访问，一个是写入。因此，根据第 5.1.2.4/25 段，该程序包含导致未定义行为的数据竞争。由于行为未定义，因此无法对线程 2从加载的值得出任何结论，特别是不能从规范中得出加载必须返回的结论。其余的论点随后崩溃。aaa0

尽管论文声称该论证表明该程序不包含数据竞争（“不活泼”），但实际上这不是论证的结果，而是一个隐藏的假设。只有与 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 不会限制程序表现出一致的执行。我在这里错过了什么吗？