Hardware Memory Models 訳 - Weak Ordering and Data-Race-Free Sequential Consistency

• 元記事
• ここまでで
• Adve と Hill の論文からいくつかの例を見てみよう
• 対比して、この 2 つのスレッドプログラムは競合がある
• 競合を避けるために

元記事

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

By now I hope you're convinced that the hardware details are complex and subtle and not something you want to work through every time you write a program. Instead, it would help to identify shortcuts of the form “if you follow these easy rules, your program will only produce results as if by some sequentially consistent interleaving.” (We're still talking about hardware, so we're still talking about interleaving individual assembly instructions.)

ここまでで

• ハードウェアの詳細は複雑で微妙であり、プログラムを書くたびに処理したいと思うものではないと確信したと思う
• 代わりに、”これらの簡単な規則に従えば、プログラムは、連続した一貫性のあるインターリーブによるかのようにしか結果を生成しない” という形式の近道を特定するのに役立つ
• （私たちはまだハードウェアについて話しているので、個々のアセンブリ命令をインターリーブすることについて話している）

Sarita Adve and Mark Hill proposed exactly this approach in their 1990 paper “Weak Ordering – A New Definition”. They defined “weakly ordered” as follows.

• Sarita Adve と Mark Hill は 1990 年の論文 “弱い順序付け - 新しい定義” を提案した
• 彼らは “弱い順序付け” を次のように定義した

Let a synchronization model be a set of constraints on memory accesses that specify how and when synchronization needs to be done.

Hardware is weakly ordered with respect to a synchronization model if and only if it appears sequentially consistent to all software that obey the synchronization model.

• 同期モデルを、同期をいつ、どのように行う必要があるかを指定するメモリアクセスの一連の制約とする
• ハードウェアは、同期モデルに従うすべてのソフトウェアに対して順番に一貫性があるように見える場合にのみ、同期モデルに関して弱く順序付けられる

Although their paper was about capturing the hardware designs of that time (not x86, ARM, and POWER), the idea of elevating the discussion above specific designs, keeps the paper relevant today.

• 彼らの論文は当時のハードウェア設計（x86、ARM、および POWER ではない）を捉えることに関するものだったが、特定の設計よりも議論を優先するという考えにより、今日の論文の関連性が保たれている

I said before that “valid optimizations do not change the behavior of valid programs.” The rules define what valid means, and then any hardware optimizations have to keep those programs working as they might on a sequentially consistent machine. Of course, the interesting details are the rules themselves, the constraints that define what it means for a program to be valid.

• 以前 “正しい最適化は正しいプログラムの振る舞いを変えない” と言った
• そのルールは有効な手段を定義し、ハードウェアの最適化では、これらのプログラムが逐次一貫性のあるマシン上で動作するように維持する必要がある
• もちろん、興味深い詳細はそのルールそのものであり、プログラムが有効であることの意味を定義する制約である

Adve and Hill propose one synchronization model, which they call data-race-free (DRF). This model assumes that hardware has memory synchronization operations separate from ordinary memory reads and writes. Ordinary memory reads and writes may be reordered between synchronization operations, but they may not be moved across them. (That is, the synchronization operations also serve as barriers to reordering.) A program is said to be data-race-free if, for all idealized sequentially consistent executions, any two ordinary memory accesses to the same location from different threads are either both reads or else separated by synchronization operations forcing one to happen before the other.

• Adve と Hill は、DRF と呼ばれる 1 つの同期モデルを提案した
• このモデルはハードウェアは普通のメモリの読み書きから分離したメモリ同期処理を行うことを前提とする
• 通常のメモリの読み書きは同期処理の間に並べ替えられるかもしれないが、それらを横切って移動することはできない（つまり同期処理は並び替えのバリアとしても機能する）
• プログラムは、すべての理想化された逐次一貫性のある実行について、data-race-free と言われ、異なるスレッドから同じ場所への 2 つの通常のメモリアクセスは、両方とも読み取りであるか、または一方が他方より先に発生することを強制する同期操作によって分離される

Let’s look at some examples, taken from Adve and Hill's paper (redrawn for presentation). Here is a single thread that executes a write of variable x followed by a read of the same variable.

Adve と Hill の論文からいくつかの例を見てみよう

• ここに、変数x へ書き込みをし、同じ変数を読み込むシングルスレッドがある

The vertical arrow marks the order of execution within a single thread: the write happens, then the read. There is no race in this program, since everything is in a single thread.

• 縦の矢印は書き込み後に読み込みをするシングルスレッドの実行順序を示す
• このプログラムはシングルスレッドであるので競合はない

In contrast, there is a race in this two-thread program:

対比して、この 2 つのスレッドプログラムは競合がある

Here, thread 2 writes to x without coordinating with thread 1. Thread 2's write races with both the write and the read by thread 1. If thread 2 were reading x instead of writing it, the program would have only one race, between the write in thread 1 and the read in thread 2. Every race involves at least one write: two uncoordinated reads do not race with each other.

• スレッド 2 はスレッド 1 に関係なく x に書き込みをする
• スレッド 2 の書き込みは、スレッド 1 による書き込みと読み込みの両方において競合がある
• スレッド 2 が書き込みの代わりに読み込みだったら、スレッド 1 の書き込みとスレッド 2 の読み込みにおいて、このプログラムの競合は 1 つになる
• 競合は少なくとも 1 つの書き込みがある場合に発生する
• 2つの間に読み込みだけであれば競合は発生しない

To avoid races, we must add synchronization operations, which force an order between operations on different threads sharing a synchronization variable. If the synchronization S(a) (synchronizing on variable a, marked by the dashed arrow) forces thread 2's write to happen after thread 1 is done, the race is eliminated:

競合を避けるために

• 異なるスレッド間でシェアしている同期変数を処理するのに強制的に順序付ける同期演算を追加しなくてはならない
• 同期の S(a)（点線でマークした変数を同期すること）は強制的にスレッド 1 が終わったあとにスレッド 2 の書き込みを発生させ、競合は排除される

Now the write by thread 2 cannot happen at the same time as thread 1's operations.

• スレッド 2 の書き込みはスレッド 1 の処理と同じタイミングで発生しない

If thread 2 were only reading, we would only need to synchronize with thread 1's write. The two reads can still proceed concurrently:

• もしスレッド 2 が読み込みだけだった場合、スレッド 1 の書き込みを同期するだけですみ、2 つの読み込みは引き続き同期的に実行できる

Threads can be ordered by a sequence of synchronizations, even using an intermediate thread. This program has no race:

• スレッドは中間のスレッドであっても、同期の順番によって順序付けされる
• これは競合のないプログラムである

On the other hand, the use of synchronization variables does not by itself eliminate races: it is possible to use them incorrectly. This program does have a race:

• 一方で、同期変数を使っても競合が解消されず、間違った使い方をする可能性がある
• 次のプログラムは競合がある

Thread 2's read is properly synchronized with the writes in the other threads—it definitely happens after both—but the two writes are not themselves synchronized. This program is not data-race-free.

• スレッド 2 の読み込みはきちんと、他のスレッドの書き込みで同期されている
• それは間違いなく両方のあとに起こる
• しかし、2 つの書き込みはそれぞれのスレッドには同期されていないので、このプログラムは data-race-free ではない

Adve and Hill presented weak ordering as “a contract between software and hardware,” specifically that if software avoids data races, then hardware acts as if it is sequentially consistent, which is easier to reason about than the models we were examining in the earlier sections. But how can hardware satisfy its end of the contract?

• Adve と Hill は “ソフトウェアとハードウェア間の契約” として弱い順序付けを提示した
• 具体的には、ソフトウェアがデータ競合を避ける場合、ハードウェアは逐次一貫性があるかのように振る舞う
• これは、前のセクションで検討したモデルよりも簡単に推論できる

Adve and Hill gave a proof that hardware “is weakly ordered by DRF,” meaning it executes data-race-free programs as if by a sequentially consistent ordering, provided it meets a set of certain minimum requirements. I’m not going to go through the details, but the point is that after the Adve and Hill paper, hardware designers had a cookbook recipe backed by a proof: do these things, and you can assert that your hardware will appear sequentially consistent to data-race-free programs. And in fact, most relaxed hardware did behave this way and has continued to do so, assuming appropriate implementations of the synchronization operations. Adve and Hill were concerned originally with the VAX, but certainly x86, ARM, and POWER can satisfy these constraints too. This idea that a system guarantees to data-race-free programs the appearance of sequential consistency is often abbreviated DRF-SC.

• Adve と Hill は、ハードウェアは “DRF によって弱く順序付けられている” ことを証明した
• つまり、特定の最小要件を満たしていると、逐次一貫した順序であるかのように、データ競合のないプログラムを実行するということである
• 詳細については触れないが、ポイントは Adve と Hill の論文の後に、ハードウェア設計者はクックブックのレシピを得たことである
• これらのことを行うと、ハードウェアは、競合のないプログラムに逐次一貫性があると断言できる
• 実際に、ほとんどのリラックスハードウェアは、同期操作の適切な実装を前提として、このように動作するしそれはいまも続いている
• Adve と Hill はもともと VAX に関心があったが、x86 、ARM、POWER もこれらの制約を満たした
• システムが逐次一貫性のある競合のないプログラムを保証するというこの考えは、省略して DRF-SC と呼ばれる

DRF-SC marked a turning point in hardware memory models, providing a clear strategy for both hardware designers and software authors, at least those writing software in assembly language. As we will see in the next post, the question of a memory model for a higher-level programming language does not have as neat and tidy an answer.

• DRF-SC はハードウェア設計者やソフトウェアを書く人（少なくともアセンブリ言語を書くソフウェアをエンジニア）へ明確な戦略を提供し、ハードウェアメモリモデルにおけるターニングポイントになった
• 次の投稿で説明するように、高水準プログラミング言語のためのメモリモデルの問題には、きちんと整理された答えは存在していない

The next post in this series is about programming language memory models.

• このシリーズの次の投稿はプログラミング言語メモリモデルである