关于并发程序中IORef操作重新排序的推理

Question

文档说：

在并发程序中，IORef操作可能会出现无序另一个线程，取决于底层的内存模型处理器体系结构。。。需要实施以确保内存操作的重新排序无法导致执行正确类型的代码错误的特别是在检查从IORef读取的值时，创建该值的内存写入必须发生在当前线程的观点。

我甚至不完全确定如何解析。杨说

换句话说，"我们对重新排序没有任何保证，除了你不会有任何类型的安全违规行为。"。。。最后一句话指出IORef不允许指向未初始化内存

所以。。。它不会打破整个哈斯克尔；帮助不大。关于记忆模型例子的讨论也给我留下了疑问(甚至西蒙·马洛似乎也有点惊讶)。

从文件中我似乎清楚的事情

1. 在线程中，atomicModifyIORef"从未被观察到发生在任何早期IORef操作之前，或发生在任何后期IORef运算之后"，即我们得到原子mod->原子mod->后面的部分排序。尽管如此，这里"从未被观察到"的措辞暗示了我没有预料到的诡异行为。

2. readIORef x可能在writeIORef y之前移动，至少在没有数据依赖的情况下是这样

3. 从逻辑上讲，我看不出像readIORef x >>= writeIORef y这样的东西是如何被重新排序的

我不清楚的是

• newIORef False >>= v-> writeIORef v True >> readIORef v是否总是返回True？

• 在maybePrint的情况下(来自IORef文档)，readIORef yourRef之前的readIORef myRef(可能还有seq或其他什么)是否会迫使重新排序成为障碍？

我应该有什么简单的心理模型？是不是有点像：

从单个线程的角度来看IORef操作的排序将显得理智而有序；但是编译器实际上可能会以这样一种方式重新排序操作并发系统中的某些假设；但是当线程atomicModifyIORef，没有线程会观察到对它的操作CCD_ 12出现在CCD_，反之亦然。

。。。？如果没有，上面的更正版本是什么？

如果你的回答是"不要在并发代码中使用IORef；使用TVar"，请用具体的事实和具体的例子说服我，说明你不能用IORef推理的事情。

Answer 1

我不了解Haskell并发性，但我对内存模型有所了解。

处理器可以按照自己喜欢的方式对指令进行重新排序：加载可能先于加载，加载可能先于存储，依赖的东西的加载可能先于它们所依赖的东西(a[i]可能首先加载数组中的值，然后加载对数组a的引用！)，存储可以相互重新排序。你根本不能把手指放在上面说"这两件事肯定会以特定的顺序出现，因为它们不可能被重新排序"。但为了让并发算法运行，它们需要观察其他线程的状态。这是线程状态以特定顺序进行的重要位置。这是通过在指令之间设置屏障来实现的，从而保证指令的顺序对所有处理器都是相同的。

通常(最简单的模型之一)，您需要两种类型的有序指令：不先于任何其他有序加载或存储的有序加载和根本不先于任何指令的有序存储，并保证所有有序指令对所有处理器都以相同的顺序出现。通过这种方式，您可以推断IRIW类型的问题：

Thread 1: x=1
Thread 2: y=1
Thread 3: r1=x;
r2=y;
Thread 4: r4=y;
r3=x;

如果所有这些操作都是有序加载和有序存储，则可以得出结果(1,0,0,1)=(r1,r2,r3,r4)是不可能的。事实上，线程1和2中的有序存储应该以某种顺序出现在所有线程中，并且r1＝1，r2＝0见证了在x＝1之后执行y＝1。反过来，这意味着线程4在不观察r3=1(在r4=1之后执行)的情况下永远无法观察r4=1(如果有序存储恰好以这种方式执行，则观察y==1意味着x==1)。

此外，如果加载和存储没有按顺序排列，处理器通常可以观察赋值的出现顺序：一个可能会看到x=1出现在y=1之前，另一个可能看到y=1出现在x=1之前，因此允许值r1、r2、r3、r4的任何组合。

这样就足够实现了：

订单装载：

load x
load-load  -- barriers stopping other loads to go ahead of preceding loads
load-store -- no one is allowed to go ahead of ordered load

订购商店：

load-store
store-store -- ordered store must appear after all stores
-- preceding it in program order - serialize all stores
-- (flush write buffers)
store x,v
store-load -- ordered loads must not go ahead of ordered store
-- preceding them in program order

在这两者中，我可以看到IORef实现了有序存储(atomicWriteIORef)，但我看不到有序加载(atomicReadIORef)，没有它你就无法解释上面的IRIW问题。如果您的目标平台是x86，这不是问题，因为所有加载都将在该平台上按程序顺序执行，并且存储永远不会提前加载(实际上，所有加载都是有序加载)。

在我看来，原子更新(atomicModifyIORef)似乎是所谓的CAS循环(compare-and-set循环，如果值为A，则在将值原子设置为b之前不会停止)的实现。您可以将原子修改操作视为有序加载和有序存储的融合，其中包含所有这些屏障，并以原子方式执行-不允许任何处理器在CAS的加载和存储之间插入修改指令。

---

此外，writeIORef比atomicWriteIORef便宜，因此您希望在线程间通信协议允许的情况下尽可能多地使用writeIORef。虽然writeIORef x vx >> writeIORef y vy >> atomicWriteIORef z vz >> readIORef t不能保证其他线程相对彼此出现writeIORef的顺序，但可以保证它们都会出现在atomicWriteIORef之前——因此，看到z==vz，您可以得出此时x==vx和y==vy的结论，并且您可以得出IORef t是在存储到x之后加载的，y，z可以被其他线程观察到。后一点要求readIORef是有序加载，据我所知，这并没有提供，但它将像x86上的有序加载一样工作。

在对算法进行推理时，通常不使用具体的x、y、z值。相反，一些与算法相关的赋值不变量必须保持，并且可以被证明——例如，在IRIW的情况下，如果线程3看到(1,0)=(r1,r2)，则可以保证线程4永远不会看到(0,1)=(r3,r4)，而线程3可以利用这一点：这意味着某些东西在不获取任何互斥或锁的情况下被相互排除。

---

一个示例(不在Haskell中)，如果未对加载进行排序，或者有序存储不刷新写缓冲区(要求在执行有序加载之前使写入值可见)，则该示例将不起作用。

假设z将显示x，直到计算出y，或者如果x也已经计算出，则显示y。不要问为什么，在上下文之外很难看到——这是一种排队——只需享受什么样的推理是可能的。

Thread 1: x=1;
if (z==0) compareAndSet(z, 0, y == 0? x: y);
Thread 2: y=2;
if (x != 0) while ((tmp=z) != y && !compareAndSet(z, tmp, y));

因此，两个线程设置x和y，然后将z设置为x或y，这也取决于是计算y还是x。假设最初所有都是0。转换为加载和存储：

Thread 1: store x,1
load z
if ==0 then
load y
if == 0 then load x -- if loaded y is still 0, load x into tmp
else load y -- otherwise, load y into tmp
CAS z, 0, tmp -- CAS whatever was loaded in the previous if-statement
-- the CAS may fail, but see explanation
Thread 2: store y,2
load x
if !=0 then
loop: load z -- into tmp
load y
if !=tmp then -- compare loaded y to tmp
CAS z, tmp, y  -- attempt to CAS z: if it is still tmp, set to y
if ! then goto loop -- if CAS did not succeed, go to loop

如果线程1load z不是有序加载，那么它将被允许在有序存储之前进行(store x)。这意味着无论z被加载到哪里(寄存器、缓存行、堆栈…)，该值都是在x的值可见之前存在的。查看这个值是没有用的-然后你就无法判断线程2达到了什么程度。出于同样的原因，你必须保证写缓冲区在执行load z之前被刷新-否则它仍然会显示为线程2看到x值之前存在的值的加载。这一点很重要，下面会很清楚。

如果线程2load x或load z不是有序加载，则它们可能在store y之前进行，并将观察到在y对其他线程可见之前写入的值。

但是，请注意，如果加载和存储是有序的，那么线程可以协商由谁来设置z的值，而不会冲突z。例如，如果线程2观察到x==0，则可以保证线程1稍后肯定会执行x==1，并且之后会看到z==0-因此线程2可以在不尝试设置z的情况下离开。

如果线程1观察到z==0，那么它应该尝试将z设置为x或y。因此，首先它将检查y是否已经设置。如果没有设置，将来会设置，所以尝试设置为x-CAS可能会失败，但前提是线程2同时将z设置为y，因此无需重试。类似地，如果线程1观察到y已被设置，则无需重试：如果CAS失败，则线程2已将其设置为y。因此，我们可以看到线程1根据要求将z设置为x或y，并且不会过多地争夺z。

另一方面，线程2可以检查是否已经计算了x。如果不是，那么设置z将是线程1的工作。如果线程1计算了x，那么需要将z设置为y。这里我们确实需要一个CAS循环，因为如果线程1试图同时将z设置成x或y，单个CAS可能会失败。

这里重要的一点是，如果"不相关"的加载和存储没有序列化(包括刷新写缓冲区)，那么就不可能进行这样的推理。然而，一旦对加载和存储进行了排序，两个线程就可以计算出它们各自的路径_will_take_in_the_future，这样就可以在一半的情况下消除争用。大部分时间x和y将在明显不同的时间计算，因此如果y在x之前计算，线程2很可能根本不会接触z。(通常，"触摸z"也可能意味着"唤醒在cond_var z上等待的线程"，因此这不仅仅是从内存加载东西的问题)

Answer 2

1. 在线程内，从未观察到发生atomicModifyIORef"在任何早期IORef操作之前，或在任何后续IORef之后运算"，即我们得到原子之上的东西的偏序mod->原子mod->之后的东西。尽管如此，措辞"观察到"这暗示了我没有的诡异行为预期

"从不被观察到"是讨论内存重新排序问题时的标准语言。例如，CPU可以在必要的时候更早地发出对存储器位置的推测性读取，只要该值在执行读取(早期)和应该执行读取(按程序顺序)之间不发生变化。这完全取决于CPU和缓存，但它从未暴露给程序员(因此，类似"从未被观察到"的语言)。

1. readIORef x可能会在writeIORef y之前移动，至少在没有数据依赖项

真实

1. 从逻辑上讲，我看不出readIORef x>>=writeIORef y可以重新排序

正确，因为该序列具有数据依赖关系。要写入的值取决于第一次读取返回的值。

对于其他问题：newIORef False >>= v-> writeIORef v True >> readIORef v将始终返回True(其他线程没有机会访问此处的ref)。

在myprint示例中，面对未来GHC和各种CPU架构中添加的新优化，您几乎无法确保这一点可靠运行。如果你写：

writeIORef myRef True
x <- readIORef myRef
yourVal <- x `seq` readIORef yourRef

尽管GHC 7.6.3产生了正确的cmm(可能还有asm，尽管我没有检查)，但没有什么可以阻止具有宽松内存模型的CPU将readIORef yourRef移动到所有myref/seq之前。唯一100%可靠的防止它的方法是使用内存围栏，而GHC没有提供。(爱德华的博客文章确实介绍了你现在可以做的其他一些事情，以及你为什么不想依赖它们)。

我认为你的心理模型是正确的，但重要的是要知道，并发操作引入的可能明显的重新排序可能是非常直观的。

编辑：在cmm级别，上面的代码片段如下(简化的伪代码)：

[StackPtr+offset] := True
x := [StackPtr+offset]
if (notEvaluated x) (evaluate x)
yourVal := [StackPtr+offset2]

因此，可能会发生一些事情。GHC目前不太可能更早地移动最后一行，但我认为如果这样做看起来更优化的话，它可以。我更担心的是，如果您通过LLVM进行编译，LLVM优化器可能会用刚刚写入的值替换第二行，然后第三行可能是不存在的常量，这将使读取更有可能提前移动。不管GHC做什么，大多数CPU内存模型都允许CPU自己在没有内存屏障的情况下提前读取。

Answer 3

http://en.wikipedia.org/wiki/Memory_ordering用于非原子并发读取和写入。(基本上，当你不使用原子论时，只需看看目标CPU的内存排序模型)

目前，ghc可以被视为而不是为非原子(和命令式)加载和存储重新排序读取和写入。然而，GHC Haskell目前没有指定任何类型的并发内存模型，因此这些非原子操作将具有底层CPU模型的排序语义，正如我链接到上面的那样。

换句话说，目前GHC没有正式的并发内存模型，而且由于任何优化算法都倾向于编写一些等价模型，因此目前没有重新排序。

也就是说：你现在唯一能拥有的语义模型是"实现方式">

给我发封电子邮件！我正在为7.10修补原子，让我们尝试构建一些语义！

编辑：一些比我更了解这个问题的人在这里加入了ghc用户线程http://www.haskell.org/pipermail/glasgow-haskell-users/2013-December/024473.html。假设我在这条评论和我在ghc用户线程中说的任何话中都错了：)