Joh*_*ger 12 c language-lawyer
最近一个问题的 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 不会限制程序表现出一致的执行。我在这里错过了什么吗？
显然，没有人有足够的兴趣和足够的信心来写答案，所以我想我会继续。
\n\n\n难道这个论点有致命的缺陷吗？
\n
在某种程度上，论文中引用的证明旨在证明符合标准的 C 实现不允许执行问题中描述的源到源转换，或者等效的，是的，证明是有缺陷的。问题中提出的反驳是合理的。
\n评论中有一些关于如何将反驳视为在未定义行为的情况下归结为允许的任何事情的讨论。这是一个有效的观点，并且绝不会削弱这个论点。然而，我认为这是不必要的简约。
\n同样，论文证明的关键问题在这里：
\n\n\n\n\n的加载
\na只能返回 0（ 的初始值a），因为\n存储a=1不会在它之前发生（因为它位于另一个尚未同步的线程中），并且非原子加载必须\n返回最新的写入发生在他们面前。
证明的错误在于，语言规范要求读取a必须返回“之前发生”的写入结果a，前提是程序不存在数据争用。这是整个模型的重要基础，而不是某种逃生舱口。如果实际上执行了读取，则该程序显然不会摆脱数据竞争a，因此在这种情况下该要求没有实际意义。线程 2 的读取a绝对可以观察到线程 1 的写入，并且有充分的理由假设在实践中有时可能会这样做。
从另一个角度来看，证明选择关注写入不发生在读取之前，但忽略了读取也不会发生在写入之前的事实。
\n考虑宽松的原子访问不会改变任何东西。在本文的三线程程序的实际执行中，实现（例如）推测性地执行x线程 2 中的宽松加载（假设它将返回 1），然后从由a写入的值中读取，这似乎是合理的。线程 1，结果执行存储到y。由于原子访问是使用宽松语义执行的，因此线程 3 的执行可以读取y1 的值（或推测它将这样做），从而执行对 的写入x。然后可以确认所有涉及的推测都是正确的，最终结果是 a = x = y = 1。“宽松”的内存顺序允许这种看似矛盾的结果是有意的。
\n\n对于 C11 实现来说，将原始三线程程序视为由线程 2' 和 3 组成的双线程程序是否确实有效？
\n
至少，论文的论点没有表明其他情况，即使我们在没有规范基础的情况下将数据竞争产生的 UB 范围解释为仅限于读取的值是否a是其初始值一个或由线程 1 写入的一个。
只要实现产生与抽象机所需行为一致的可观察行为，就获得了广泛的许可，可以按照自己的选择行事。正如规范所定义的那样，多个执行线程的创建和执行本身并不是程序可观察行为的一部分。因此，是的，执行建议的转换然后相应地表现的程序，或者表现得好像在写入和读取之间发生边缘之前的程序，不会与规范不一致。aa
根据最近的替代答案并考虑到对此的评论，在这个答案中加入一些关于这个和这个如何得出不同结论的评论似乎是合适的。
\n主要争议
\n另一个答案总结了本文分析的关键特征：
\n\n\n因此，对“竞赛”（以及因此“未定义的行为”）的检查仅在“一致执行”上进行，而不是在“候选执行”上进行。
\n
另一个答案似乎赞同这种方法，显然接受过滤掉候选执行而不考虑 UB 的影响是有效的。它没有提供一般的理由，但在示例程序的情况下，它声称它是由规范的规则证明的，即通过哪些评估可以看到哪些副作用（5.1.2.4/19）。
\n反对意见一：UB的规格不容忽视
\n另一个答案引用的规则并不表示比表明程序行为未定义的规则有任何优先级，也不与规范对具有 UB 的程序没有任何要求的定义相矛盾。
\n在实践中，解释 UB 规范的既定惯例是 UB 确实具有其定义所述的后果。规范中任何需要特定程序行为的规定都适用于具有 UB 的程序。\n指定程序行为的规则的存在并不提供任何理由忽略明确指定程序行为为未定义的规则。事实上恰恰相反。
\n侧面考虑：证明 UB
\n这个问题是在如何证明一个程序具有 UB 的讨论中出现的。如果人们根据规范对程序进行推理，并得出诸如 5.1.2.4/24 之类的规定，指定该程序具有 UB，那么这是否不会破坏得出该结论的推理链？
\n是和不是。我们可以观察到，首先进行这样的推理链必然始于程序已定义行为的假设。如果这允许人们根据某种明确的规范得出程序具有 UB 的结论，那么这与最初的假设相矛盾，通过矛盾证明 UB （如果不是直接证明的话）。
\n或者，也可以依赖第 4/2 段，其中除其他事项外，
\n\n\n未定义的行为是通过省略任何明确的行为定义来表示的
\n
因此，即使有人通过矛盾来拒绝证明的有效性，在这种情况下，人们也会仅仅因为规范没有提供程序行为的任何连贯定义而留下 UB。
\n反对意见 2：“一致执行”并不是 C 语言规范允许的唯一执行方式
\n考虑这个更简单的程序：
\nints a且b最初为 0。a = 1;b = a;按照本文的方法，我们从一致执行列表中排除任何线程 2 的读取a观察到非 0 值的执行，以及任何最终值a不为 1 的执行。这样就只剩下一个一致执行执行，但是当分析该执行的数据竞争时，我们发现其中涉及a. 现在怎么办？
语言规范对包含数据竞争的程序的行为没有任何要求，因此我们必须重新考虑之前的排除：允许所有候选执行（即，它们与语言规范一致），即使是那些与语言规范不一致的程序。纸。
\n但这篇论文的一致执行有何意义呢？如果在某些情况下仍然允许不一致的执行，那么我们基于什么基础将所有此类执行排除在程序是否包含数据竞争的分析之外？事实上，我们确实希望从该分析中排除许多候选执行，但我认为我们不能证明排除那些需要首先假设不存在数据竞争的执行。
\n反对意见3：论文的解释与现实世界的期望和行为不一致
\n本文和另一个答案假设，由于示例程序的线程 1 中的非原子存储与线程 2a中的负载没有发生之前关系a，因此需要实现以防止负载观察存储。正如前面的反对意见所示，这显然是不真实的，但这甚至不是一个合理的期望。
实际实践和一般期望是，非原子访问遵循机器的自然存储行为，不需要除此之外的任何特别注意，包括在多线程程序中。在没有数据竞争的程序中，所需的内存行为（包括非原子访问）预计将通过原子操作和其他同步操作的正确实现来保证，而对非原子访问的处理没有任何额外要求。例如，这是 5.1.2.4/19 的根本基础。
\n将未定义的行为归因于数据竞争的目的正是为了减轻实现在具有数据竞争的程序中满足这些规定的负担。（毫无疑问，具体是关于对 racy 对象的访问，但委员会更喜欢使用现有的工具，例如 UB，有时甚至用大画笔进行绘制。）这就是我在说自由种族是基础，或者说其他条款取决于此。是的，它们在技术意义上是偶然的，因为一切都取决于程序具有定义的行为，但这是委员会实现其目标的方法，使程序在存在数据竞争的情况下免于承担义务。
\n因此，在不首先考虑是否存在数据争用的情况下应用 5.1.2.4/19 或内存模型的其他规则是错误的。这篇论文颠倒了这种关系。
\n反对意见 4：这篇论文因此产生了自己的问题
\n该论文的作者声称在 C 内存模型中发现的至少一些缺陷取决于他们的模型处理数据竞争的方法。一个常见的主题是，包含数据竞争的执行据称比不包含数据竞争的类似执行提供的一致性执行要少，并且这使得各种源到源的翻译无效，而作者声称（我同意）本应是有效的。
\n但这些都是人为的问题，可以通过纠正模型来解决，以便它以某种方式集成数据竞争的处理，从而导致预测与我们似乎都同意的预期行为相匹配。与我们的期望一致是我们判断正式模型（例如本文的模型）的主要标准之一。按照这些思路修正的模型在形式化方面会更加混乱，我预计它会更弱，但这只是反映了现实：C 内存模型比论文的形式化更弱。
\nSEQ 执行的结束示例
\n结合另一个允许（或应该）执行程序 SEQ 的示例问题进行了一些讨论，并产生最终状态 a=1 \xe2\x88\xa7 x=y=1。这是一个：
\n| 线程1 | 线程2 | 线程3 |
|---|---|---|
1.1 存储 1 中a（非原子） | 2.1 从x（宽松）加载 1 2.2 从（非原子）加载1 2.3 将 1 存储在 y 中（宽松） a | y3.1 从（放松）加载 1 3.2 将 1 存储到 x（放松） |
这里发生之前关系的完整列表是
\n我注意到存在一个happens-before循环，但是内存模型并不禁止它。每个原子读取都会映射到在其之前发生的相应原子写入，并写入读取的值。存在冲突的读取和写入a，并且没有发生之前的关系，因此（这就是我们与本文不同的地方）程序行为是未定义的，因此 2.2 是允许的（与任何其他内容一样）。
| 归档时间： |
|
| 查看次数： |
357 次 |
| 最近记录： |