Hardware Memory Models 訳 - ARM/POWER Relaxed Memory Model

• 元記事
• ARM や POWER の Relaxed Memory Model
• Weak Ordering and Data-Race-Free Sequential Consistency へと続く

元記事

research!rsc: Hardware Memory Models (Memory Models, Part 1)

A long time ago, when everyone wrote single-threaded programs, one of the most effective ways to make a program run faster was to sit back and do nothing. Optimizations in the next generation of hardware and the next generation of compilers would make the program run exactly as before, just faster.

research.swtch.com

ARM や POWER の Relaxed Memory Model

Now let's look at an even more relaxed memory model, the one found on ARM and POWER processors. At an implementation level, these two systems are different in many ways, but the guaranteed memory consistency model turns out to be roughly similar, and quite a bit weaker than x86-TSO or even x86-TLO+CC.

The conceptual model for ARM and POWER systems is that each processor reads from and writes to its own complete copy of memory, and each write propagates to the other processors independently, with reordering allowed as the writes propagate.

• ARM や PORWER のようなさらにゆるいメモリモデルを見てみよう
• 実装レベルでは、これらの2つのシステムは多くの方針が違うが、メモリ一貫性モデルの保証はだいたい似通っていて、それは x86-TSO や x86-TLO+CC でさえよりも非常に弱い
• ARM と POWER システムのコンセプトは、それぞれのプロセッサは自身のメモリのコピーに読み込みや書き込みをし、それぞれの書き込みが他のプロセッサに独立して伝播し、書き込みが伝播するにつれ並び替えが許可される

Here, there is no total store order. Not depicted, each processor is also allowed to postpone a read until it needs the result: a read can be delayed until after a later write. In this relaxed model, the answer to every litmus test we’ve seen so far is “yes, that really can happen.”

• TSO はなく、それぞれのプロセッサーは結果が必要になるまで読み込みを遅らせることも許され、読み込みは後の書き込み後まで遅らせることができる
• この Relaxed モデルでは、私達がこれまでみてきたすべてのリトマステストの答えは “yes” となる

For the original message passing litmus test, the reordering of writes by a single processor means that Thread 1's writes may not be observed by other threads in the same order:

• リトマステストが通る元のメッセージについて、単一のプロセッサによる書き込みの並べ替えは、スレッド 1 の書き込みが他のスレッドによって同じ順序で観察されない可能性があることを意味する

In the ARM/POWER model, we can think of thread 1 and thread 2 each having their own separate copy of memory, with writes propagating between the memories in any order whatsoever. If thread 1's memory sends the update of y to thread 2 before sending the update of x, and if thread 2 executes between those two updates, it will indeed see the result r1 = 1, r2 = 0.

• ARM/POWER モデルにおいて、わたしたちはそれぞれが分けられたメモリコピーを持ち、どんな順番でもメモリ間で書き込みが伝播するスレッド 1 やスレッド 2 を考えることができる
• もしスレッド 1 のメモリが y のアップデートを x の更新を送る前に スレッド 2 へ送信し、スレッド 2 がそれらの 2 つの更新を実行した場合、r1 = 1, r2 = 0 の結果は確実に発生する。

This result shows that the ARM/POWER memory model is weaker than TSO: it makes fewer requirements on the hardware. The ARM/POWER model still admits the kinds of reorderings that TSO does:

• この結果は、ARM/POWER メモリモデルが TSO より弱いことを表し、これはハードウェアの要求が弱くする
• ARM/POWER モデルはまだ、TSO が行う並べ替えの種類を引き続き認める

On ARM/POWER, the writes to x and y might be made to the local memories but not yet have propagated when the reads occur on the opposite threads.

Here’s the litmus test that showed what it meant for x86 to have a total store order:

• ARM/POWER において x と y への書き込みはローカルメモリに対して行われることもあるが、反対のスレッドに読み込みが発生する時にはまだ伝播していない
• これは TSO を持つ x86 にとって何を意味するかを表すリトマステストである

On ARM/POWER, different threads may learn about different writes in different orders. They are not guaranteed to agree about a total order of writes reaching main memory, so Thread 3 can see x change before y while Thread 4 sees y change before x.

• ARM/POWER において、違うスレッドは、違う順番に違う書き込みを学習するかもしれない
• それらは、メインメモリに到達する書き込みの全順序について同意することが保証されない
• つまり、スレッド 3 は y の前に x の変更を確認でき、スレッド 4 は x の前に y の変更を確認できる

As another example, ARM/POWER systems have visible buffering or reordering of memory reads (loads), as demonstrated by this litmus test:

• もう一つの例として、ARM/POWER システムは、バッファリングかメモリ読み込みの並び替えを持つことがこのリトマステストによって実証された

Any sequentially consistent interleaving must start with either thread 1's r1 = x or thread 2's r2 = y. That read must see a zero, making the outcome r1 = 1, r2 = 1 impossible. In the ARM/POWER memory model, however, processors are allowed to delay reads until after writes later in the instruction stream, so that y = 1 and x = 1 execute before the two reads.

• 逐次一貫性のあるインターリーブは、スレッド 1 の r1 = x またはスレッド 2 の r2 = y で開始する必要がある
• その読み取りは必ずゼロが表示され、結果 r1 = 1、 r2 = 1 は不可能になる
• ただし、ARM/POWER メモリモデルのプロセッサは、命令の後半の書き込み後までに読み込みを遅らせることが許されているので、y = 1 と x = 1 は 2 つの読み込みの前に実行される

Although both the ARM and POWER memory models allow this result, Maranget et al. reported (in 2012) being able to reproduce it empirically only on ARM systems, never on POWER. Here the divergence between model and reality comes into play just as it did when we examined Intel x86: hardware implementing a stronger model than technically guaranteed encourages dependence on the stronger behavior and means that future, weaker hardware will break programs, validly or not.

• ARM や POWER メモリモデルはこの結果を許容するが、Maranget らの 2012 年の論文は、ARM システムでのみ経験的に再現し、POWER では再現しないと報告された
• ここで、インテル x86 を調べたときと同じように、モデルと現実の間の相違が生じる
• 技術的に保証されているよりも強力なモデルを実装するハードウェアは、より強力な動作への依存を促進し、将来、より弱いハードウェアが有効かどうかに関係なくプログラムを破壊することを意味する

Like on TSO systems, ARM and POWER have barriers that we can insert into the examples above to force sequentially consistent behaviors. But the obvious question is whether ARM/POWER without barriers excludes any behavior at all. Can the answer to any litmus test ever be “no, that can’t happen?” It can, when we focus on a single memory location.

Here’s a litmus test for something that can’t happen even on ARM and POWER:

• TSO システムのように、ARM と POWER は強制的に逐次一貫性の振る舞いを上記の例に差し込むことができるバリアを持つ
• しかい明らかな問題は、バリアのない ARM/POWER が振る舞いを排除するか
• リトマステストに対する答えとして、”no、そんなこと起こり得ない” ということがあるか？単一のメモリ位置に焦点を当てると、それが可能となる
• これは ARM / POWER でも起こり得ないリトマステストである

This litmus test is like the previous one, but now both threads are writing to a single variable x instead of two distinct variables x and y. Threads 1 and 2 write conflicting values 1 and 2 to x, while Thread 3 and Thread 4 both read x twice. If Thread 3 sees x = 1 overwritten by x = 2, can Thread 4 see the opposite?

• このリトマステストは前のと似ているが、両方のスレッドが 2 つの異なる変数 x と y ではなく、単一の変数 x に書き込みを行っている
• スレッド 1 と 2 は競合する値 1 と 2 を x に書き込むが、スレッド 3 とスレッド 4 は両方とも x を 2 回読み取る
• スレッド 3 が x = 1 が x = 2 によって上書きされたことを確認した場合、スレッド 4 は反対のことを確認できるか？

The answer is no, even on ARM/POWER: threads in the system must agree about a total order for the writes to a single memory location. That is, threads must agree which writes overwrite other writes. This property is called called coherence. Without the coherence property, processors either disagree about the final result of memory or else report a memory location flip-flopping from one value to another and back to the first. It would be very difficult to program such a system.

• その答えはARM/POWER でも no である
• システムのスレッドは、単一のメモリロケーションに書き込みのために全順序について合意する必要がある
• このプロパティはコヒーレンスと呼ばれる
• コヒーレンスプロパティなしに、プロセッサは、メモリの最終結果について意見が一致しないか、ある値から別の値にフリップフロップして最初の値に戻るメモリ位置を報告する
• このようなシステムをプログラムすることは非常に難しいことである

I'm purposely leaving out a lot of subtleties in the ARM and POWER weak memory models. For more detail, see any of Peter Sewell's papers on the topic. Also, ARMv8 strengthened the memory model by making it “multicopy atomic,” but I won't take the space here to explain exactly what that means.

• ARM および POWER の弱いメモリモデルでは、多くの微妙な点を意図的に省略している
• より詳細をみるためには、 Peter Sewell's papers on the topic などをみてください
• ARMv8 は  strengthened the memory model にある、メモリモデルを「マルチコピー アトミック」にすることで強化したが、それが何を意味するのかを正確に説明するためにここでスペースを取らない

There are two important points to take away. First, there is an incredible amount of subtlety here, the subject of well over a decade of academic research by very persistent, very smart people. I don't claim to understand anywhere near all of it myself. This is not something we should hope to explain to ordinary programmers, not something that we can hope to keep straight while debugging ordinary programs. Second, the gap between what is allowed and what is observed makes for unfortunate future surprises. If current hardware does not exhibit the full range of allowed behaviors—especially when it is difficult to reason about what is allowed in the first place!—then inevitably programs will be written that accidentally depend on the more restricted behaviors of the actual hardware. If a new chip is less restricted in its behaviors, the fact that the new behavior breaking your program is technically allowed by the hardware memory model—that is, the bug is technically your fault—is of little consolation. This is no way to write programs.

• 押さえておきたい重要なポイントは 2 つ
• まず、ここには信じられないほどの微妙な点があり、非常に粘り強く、非常に頭の良い人々による 10 年をはるかに超える学術研究のテーマがある
• 私はそれのほとんどすべてを自分で理解しているとは主張しない
• これは、普通のプログラマーに説明したいことではなく、普通のプログラムをデバッグしている間、正しさを保つことが期待できるものでもない
• 2 つ目に、許可されていることと観察されていることの間のギャップは、不幸な将来の驚きをもたらす
• 現在のハードウェアが許可されているすべての動作を示していない場合（特に、そもそも何が許可されているかを判断するのが難しい場合）
• 必然的に、実際のハードウェアのより制限された動作に誤って依存するプログラムが作成される
• 新しいチップの動作の制限が緩和されている場合、プログラムを壊す新しい動作がハードウェアメモリモデルによって技術的に許可されているという事実（つまり、バグは技術的にはユーザーの責任である）は、ほとんど慰めにはならない
• これはプログラムを書く方法ではない

Weak Ordering and Data-Race-Free Sequential Consistency へと続く