Hardware Memory Models 訳 - Sequential Consistency

• 元記事
• 逐次一貫性
• レスリーランポートの 1979年の論文は逐次一貫性のコンセプトを紹介した
• 現在では、ハードウェアだけでなくプログラミング言語でも逐次一貫性が保証されることが話題になっている
• 先ほど「このプログラムは0を表示できるのか」という質問をした
• サンプルプログラムの実行結果について質問することをリトマステストという
• このリトマス試験の実行が逐次一貫である場合、インターリーブのパターンは 6 つだけ
• この図は逐次一貫性のあるマシンのモデルであるが、方法はこれだけではない
• x86 Total Store Order へ続く

元記事

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

Sequential Consistency

逐次一貫性

Leslie Lamport's 1979 paper “How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs” introduced the concept of sequential consistency:

The customary approach to designing and proving the correctness of multiprocess algorithms for such a computer assumes that the following condition is satisfied: the result of any execution is the same as if the operations of all the processors were executed in some sequential order, and the operations of each individual processor appear in this sequence in the order specified by its program. A multiprocessor satisfying this condition will be called sequentially consistent.

レスリーランポートの 1979年の論文は逐次一貫性のコンセプトを紹介した

• マルチプロセスプログラムを正しく実行するマルチプロセッサ・コンピュータの作り方
• マルチプロセスアルゴリズムの正確性は次の条件が満たされることを前提とする
• すべてのプロセッサの操作による実行結果は、順序が変わらないこと
• 個々のプロセッサの演算の順序は、プログラムにより指定された順序で表示されること
• マルチプロセッサがこの条件を満たすことを`逐次一貫性`と呼ぶ

Today we talk about not just computer hardware but also programming languages guaranteeing sequential consistency, when the only possible executions of a program correspond to some kind of interleaving of thread operations into a sequential execution. Sequential consistency is usually considered the ideal model, the one most natural for programmers to work with. It lets you assume programs execute in the order they appear on the page, and the executions of individual threads are simply interleaved in some order but not otherwise rearranged.

現在では、ハードウェアだけでなくプログラミング言語でも逐次一貫性が保証されることが話題になっている

• プログラムの実行が、スレッド操作のある種のインターリーブによる順次実行にのみ対応する場合、順次的整合性は通常、理想的なモデルであり、プログラマにとって最も自然なモデルであると考えられている
• このモデルでは、プログラムはページ上に表示されている順番に実行され、個々のスレッドの実行は単に何らかの順番でインターリーブされているだけで、それ以外に再配置されていないと仮定することができる

One might reasonably question whether sequential consistency should be the ideal model, but that's beyond the scope of this post. I will note only that considering all possible thread interleavings remains, today as in 1979, “the customary approach to designing and proving the correctness of multiprocess algorithms.” In the intervening four decades, nothing has replaced it.

• 逐次一貫性が理想的なモデルであるべきかという疑問は当然あるかもしれないが、それはこの記事の範囲外とする
• 筆者は 1979 年当時と変わらず、すべての可能なスレッドのインターリーブを考慮することが「マルチプロセスアルゴリズムの設計と正しさを証明するための慣習的なアプローチ」であることだけを記しておく
• この40年間、これに取って代わるものは何もなかった

Earlier I asked whether this program can print 0:

To make the program a bit easier to analyze, let's remove the loop and the print and ask about the possible results from reading the shared variables:

先ほど「このプログラムは0を表示できるのか」という質問をした

• この問題を簡単にするため、ループとプリントを取り除き、共有変数を読み取ることで起こりうる結果について考えてみる

We assume every example starts with all shared variables set to zero. Because we're trying to establish what hardware is allowed to do, we assume that each thread is executing on its own dedicated processor and that there's no compiler to reorder what happens in the thread: the instructions in the listings are the instructions the processor executes. The name rN denotes a thread-local register, not a shared variable, and we ask whether a particular setting of thread-local registers is possible at the end of an execution.

• すべての共有変数がゼロに設定された状態で開始されると仮定する
• 我々はハードウェアが許可されるを確立しようとしているので、各スレッドはそれ自身の専用プロセッサで実行され、スレッドの内容を並べ替えるコンパイラは存在しないと仮定する
• リスト内の命令はプロセッサが実行する命令である
• rNという名前は、共有変数ではなくスレッドローカルレジスタを示します。実行の最後に、スレッドローカルレジスタの特定の設定が可能かどうかを確認する

This kind of question about execution results for a sample program is called a litmus test. Because it has a binary answer—is this outcome possible or not?—a litmus test gives us a clear way to distinguish memory models: if one model allows a particular execution and another does not, the two models are clearly different. Unfortunately, as we will see later, the answer a particular model gives to a particular litmus test is often surprising.

サンプルプログラムの実行結果について質問することをリトマステストという

• リトマステストは、この結果が可能か不可能かという二値的な答えを持つので、あるモデルが特定の実行を許し、別のモデルが許さない場合、その2つのモデルは明らかに異なるという、メモリモデルを区別する明確な方法である
• 残念ながら、あるモデルが特定のリトマステストに対して出す答えは意外なものであることが多い

If the execution of this litmus test is sequentially consistent, there are only six possible interleavings:

このリトマス試験の実行が逐次一貫である場合、インターリーブのパターンは 6 つだけ

Since no interleaving ends with r1 = 1, r2 = 0, that result is disallowed. That is, on sequentially consistent hardware, the answer to the litmus test—can this program see r1 = 1, r2 = 0?—is no.

• r1 = 1、r2 = 0 で終わるインターリーブはない
• つまり、逐次一貫性のあるハードウェア上では、このプログラムは r1 = 1、r2 = 0 がありうるかというリトマステストの答えは「いいえ」である

A good mental model for sequential consistency is to imagine all the processors connected directly to the same shared memory, which can serve a read or write request from one thread at a time. There are no caches involved, so every time a processor needs to read from or write to memory, that request goes to the shared memory. The single-use-at-a-time shared memory imposes a sequential order on the execution of all the memory accesses: sequential consistency.

• 逐次一貫性のための良いメンタルモデルは、下図のように同じシェアドメモリに直接つながる全プロセッサをイメージすることで、これらは 1 度に 1 スレッドからリクエストを読み書きすることができる
• キャッシュは考慮しないので、毎回プロセッサはメモリから読み込みメモリへ書き込むたびに、そのリクエストは共有メモリへ送られる
• 全ての読み書きはシーケンシャルに行われる

(The three memory model hardware diagrams in this post are adapted from Maranget et al., “A Tutorial Introduction to the ARM and POWER Relaxed Memory Models.”)

• この投稿の 3 つのメモリモデルハードウェアの図は、次のドキュメントから引用している
• “A Tutorial Introduction to the ARM and POWER Relaxed Memory Models.”

This diagram is a model for a sequentially consistent machine, not the only way to build one. Indeed, it is possible to build a sequentially consistent machine using multiple shared memory modules and caches to help predict the result of memory fetches, but being sequentially consistent means that machine must behave indistinguishably from this model. If we are simply trying to understand what sequentially consistent execution means, we can ignore all of those possible implementation complications and think about this one model.

この図は逐次一貫性のあるマシンのモデルであるが、方法はこれだけではない

• 実際のところ、複数の共有メモリモジュールとキャッシュを使用して逐次一貫性のあるマシンを構築し、メモリフェッチの結果を予測することもできる
• ただし、逐次一貫性があるということは、マシンがこのモデルとは区別なく動作する必要があることを意味する
• 逐次一貫性についての理解を簡単にするためには、複雑性を全て無視して、この一つのモデルについて考えるのがよい

Unfortunately for us as programmers, giving up strict sequential consistency can let hardware execute programs faster, so all modern hardware deviates in various ways from sequential consistency. Defining exactly how specific hardware deviates turns out to be quite difficult. This post uses as two examples two memory models present in today's widely-used hardware: that of the x86, and that of the ARM and POWER processor families.

• プログラマにとって残念なことに、ハードウェアがプログラムをより早く実行するため、厳密な逐次一貫性を放棄すると、最新のハードウェアはすべて、様々な方法で逐次一貫性から逸脱してしまう
• また、特定のハードウェアがどのように逸脱しているかを明確に定義することはとても難しい
• この投稿は今現在広くハードウェアで使われている 2 つのメモリモデルを 2 つの例としてとりあげる
• x86
• ARM、POWER

x86 Total Store Order へ続く