我不知道 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 证明 y=1 在 x=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
如果您的目标平台是 x86,这不是问题,因为所有加载都将在该平台上按程序顺序执行,并且存储永远不会先于加载(实际上,所有加载都是有序加载)。
atomicModifyIORef
在我看来,原子更新(您可以将原子修改操作视为有序加载和有序存储的融合,所有这些障碍都在那里,并以原子方式执行 - 不允许处理器在 CAS 的加载和存储之间插入修改指令。
此外,writeIORef 比 atomicWriteIORef 便宜,因此您希望在线程间通信协议允许的范围内尽可能多地使用 writeIORef。虽然writeIORef x vx >> writeIORef y vy >> atomicWriteIORef z vz >> readIORef t
不保证 writeIORefs 相对于其他线程出现的顺序,但可以保证它们都将出现在之前atomicWriteIORef
- 所以,看到 z==vz,你可以在这一刻得出结论 x==vx 和 y ==vy,你可以断定IORef t是在存储到x、y、z之后加载的,其他线程可以观察到。后一点要求 readIORef 是一个有序负载,据我所知没有提供,但它会像 x86 上的有序负载一样工作。
通常,在推理算法时,您不会使用 x、y、z 的具体值。相反,一些与分配值有关的算法相关的不变量必须保持,并且可以被证明——例如,在 IRIW 的情况下,您可以保证线程 4 永远不会看到(0,1)=(r3,r4)
,如果线程 3 看到(1,0)=(r1,r2)
,并且线程 3 可以利用这一点:这意味着某些东西在没有获得任何互斥锁或锁的情况下被相互排除。
一个示例(不在 Haskell 中),如果加载未排序,或者有序存储不刷新写入缓冲区(要求在有序加载执行之前使写入值可见),则该示例将不起作用。
假设,z 将显示 x,直到 y 被计算,或者 y,如果 x 也被计算。不要问为什么,在上下文之外不是很容易看到 - 它是一种队列 - 只是享受什么样的推理是可能的。
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 的线程”,因此这不仅仅是从内存中加载某些内容的问题)