Haskell の同時実行性についてはわかりませんが、メモリ モデルについてはある程度知っています。
プロセッサは命令を好きなように並べ替えることができます: ロードはロードより先に進み、ロードはストアより先に進み、依存するもののロードはそれらが依存するもののロードより先に進みます (a[i] は最初に配列から値をロードし、次に、配列への参照 a!)、ストアは互いに並べ替えられます。「この 2 つのものは特定の順序で表示されることは間違いありません。順序を変更する方法はありません」とは簡単には言えません。しかし、並行アルゴリズムが機能するためには、他のスレッドの状態を監視する必要があります。これは、スレッドの状態が特定の順序で進むことが重要な場所です。これは、命令間にバリアを配置することによって実現されます。これにより、命令の順序がすべてのプロセッサに対して同じに見えることが保証されます。
通常 (最も単純なモデルの 1 つ)、2 種類の順序付き命令が必要です。他の順序付きロードまたはストアより先に進まない順序付きロードと、どの命令よりも先に進まない順序付きストアです。順序付けされたすべての命令は、すべてのプロセッサに対して同じ順序で表示されます。このようにして、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
これら 2 つのうち、IORef が順序付きストア ( atomicWriteIORef) を実装していることはわかりますが、順序付きロード ( atomicReadIORef) は見られません。これがなければ、上記の IRIW の問題について推論することはできません。ターゲット プラットフォームが x86 の場合、これは問題ではありません。そのプラットフォームでは、すべてのロードがプログラムの順序で実行され、ストアがロードより先に進むことはないためです (実際には、すべてのロードは順序付けられたロードです)。
アトミックな更新 ( atomicModifyIORef) は、いわゆる CAS ループ (値が a の場合、値がアトミックに b に設定されるまで停止しない比較と設定のループ) の実装のように思えます。アトミックな変更操作は、順序付けられたロードと順序付けられたストアの融合であり、そこにすべてのバリアがあり、アトミックに実行されることがわかります。プロセッサは、CAS のロードとストアの間に変更命令を挿入することはできません。
さらに、writeIORef は atomicWriteIORef より安価であるため、スレッド間通信プロトコルが許可する限り、writeIORef を使用する必要があります。はwriteIORefswriteIORef x vx >> writeIORef y vy >> atomicWriteIORef z vz >> readIORef tが他のスレッドに相互に現れる順序を保証しませんが、両方が前に現れるという保証がありますatomicWriteIORef- したがって、z==vz を見ると、現時点で x==vx と y を結論付けることができます。 ==vy であり、x、y、z へのストア後にIORef t がロードされたと結論付けることができます。これは他のスレッドによって観察できます。この後者のポイントでは、readIORef が順序付きロードである必要があります。これは、私が知る限り提供されていませんが、x86 では順序付きロードのように機能します。
通常、アルゴリズムについて推論するとき、x、y、z の具体的な値は使用しません。代わりに、割り当てられた値に関するいくつかのアルゴリズム依存の不変条件を保持する必要があり、証明することができます。たとえば、IRIW の場合のように、(0,1)=(r3,r4)スレッド 3 が を参照する場合、スレッド 4 が を参照しないことを保証でき(1,0)=(r1,r2)、スレッド 3 はこれを利用できます。これは、ミューテックスやロックを取得することなく、何かが相互に除外されることを意味します。
ロードが順序付けされていない場合、または順序付けられたストアが書き込みバッファをフラッシュしない場合 (順序付けられたロードが実行される前に書き込まれた値を可視化する要件) が機能しない例 (Haskell にはありません)。
z は、y が計算されるまで x を表示するか、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));
したがって、2 つのスレッドが x と y を設定し、y または x が計算されたかどうかに応じて、z を x または y に設定します。最初はすべて 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 yy が他のスレッドに表示される前に書き込まれた値を観察します。
ただし、ロードとストアが順序付けられている場合、スレッドは、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 に設定する必要があります。スレッド 1 が同時に z を x または y に設定しようとすると、単一の CAS が失敗する可能性があるため、ここでは CAS ループが必要です。
ここで重要なことは、「無関係な」ロードとストアがシリアル化されていない場合 (書き込みバッファーのフラッシュを含む)、そのような推論は不可能だということです。ただし、ロードとストアが順序付けられると、両方のスレッドがそれぞれの _will_take_in_the_future のパスを把握できるため、半分のケースで競合が解消されます。ほとんどの場合、x と y は大幅に異なる時間に計算されるため、y が x の前に計算される場合、スレッド 2 は z にまったく触れない可能性があります。(通常、「z に触れる」ということは、「cond_var z で待機しているスレッドを起動する」ことも意味する可能性があるため、メモリから何かをロードするだけの問題ではありません)