uDiary

◆ TSO と store forwarding

追記:まとめというか、続きが2006-09-22 にあります。

http://www.nminoru.jp/~nminoru/diary/2006/08.html#2006-08-11

nminoru さんのところに押しかけていって、議論を迷走させてしまった件について。 私の議論スキルの無さが露呈してしまったと思います。 この件について、私は、 きちんと人に説明できるほどには十分理解していなかったというべきかも知れません。

本来の争点からずれたところで話を長引かせてしまい、かつ、 いくつか誤ったことを言ってしまうという痛い間違いも犯してしまいました。 我ながら議論が出来ていない。 また、きちんと文献にあたっていれば防げたはずの間違いをしている点は、 不誠実だったと思う。 こんなことにつき合わせてしまい、nminoru さんには申し訳ないことをしました。

問題点：Store forwarding は load - load 間の追い抜きを発生させるか。

問題となったのは、TSO (Total Store Ordering) で、かつ、 Store forwarding を採用しているシステムの場合、 後続の load が先行する load を追い越してしまうケースがあるのではないかという話。

プロセッサ 1        プロセッサ 2
1: Store [x] = 1    4: Store [y] = 1
2: Load r1 = [x]    5: Load r3 = [y]
3: Load r2 = [y]    6: Load r4 = [x]

上の例は nminoru さんの挙げられたものを借りてきました。 Store forwarding を行うシステム上でこれらの命令列を実行した場合、 r1 = r3 = 1 で、かつ、r2 = r4 = 0 という結果が得られる場合があります。

結論からいうと、これはなんら TSO に違反していません。 1: の store は、プロセッサ 1　上で実行された時点では Store buffer に格納されるだけであって、ただちには global visible になりません。 後続の 2:, 3: の load は、1: の store が global visible になるのを またずに実行可能。また、load は実行された時点で global visible になります。 *1

つまり、 プロセッサ 1 の memory operation は　2: → 3: → 1: の順で global visible になったのです。 （これが唯一の解ではなく、プロセッサ２が 5: → 6: → 4: でもいい）

私は、これで話が尽きていると思っていた（いまも思っている）ので、 これに対する反論にあまりきちんと対処できていませんでした。

反論：3: → 1: → 2: でないとおかしい。

これに対し、nminoru さんは、global visible になった順序は 3: → 1: → 2: だったと考えるほうが自然だと言われました。 2: の load は、1: の store 値を受け取っているのだから、 1: が global visible になった後に置かれるべきであるということでしょう。

こう考えると、3: の load が 1:, 2: の両方を追い抜かしたと 考えなくてはならなくなります。1: を追い越すのだけならまだしも、 2: を抜かすというのは TSO に違反しています。 本当にこのように考える必要があるのでしょうか？

追記：こう考えるためには、Store 値が global visible になるのと、local visible になるのが同時であるという類の追加規則を仮定する必要があります。 なぜ、勝手に規則を追加するの？ 既に矛盾のない体系に、あらたな仮定を追加することによって矛盾を引き起こしていますよ。

この案の欠点は、

1. 2: が 1: を追い越したという自然な解釈を採用すればすべて解決するのに、それをしていない点。
2. それにより、load が load を追い越すケースが存在するという例外規則を必要としている点。
3. その例外規則だけではハンドリングしきれないケースが存在する点。
4. （追加）2: は 1: よりも後に global visible になる筈だという暗黙の規則を、どこからともなく持ち出している。

あたりでしょうか。 とくに、３番目がクリティカルなんじゃないかと思うのですが。

これは、命令列をちょっと変更すると明らかになります。

1: Store [x] = 1
2: Load r1 = [x]
3: if (r1 == 1) {Load r2 = [y]}

こうすれば、nminoru さん的世界観でも、3: は 2: を抜かせなくなりますが、 これでも r1 = r3 = 1 で、かつ、r2 = r4 = 0 という結果は得られるはずです。

仕様書には、たしかに、Sigle port memory に memory transaction が到達したところで memory order が観測されると書いてあります (SPARC-V8 の場合) が、ここでいう memory transaction は、 純粋に仮想的なものであって、 実システムにおけるどのような処理に相当するのかは自明ではありません。 （Model に反しない限り、どのようにインプリしてもかまわない）

述べるべきだった事柄は、だいたい以上の通りなのではないかと思います。

反省

なにより、nminoru さんがきちんと文献を確認しなおして書かれているのに 対し、私は手元に文献がない状態のまま誤ったことを書いてしまっていた箇所が いくつもあります。これはとても不誠実な態度だったと反省しています。 すみません。

観測されるのは順序であって、各 load/store がそれぞれ global visible になった 瞬間に「あ、いまだ」と観測されるわけではありません。 結果的にプログラムがどう動いたか（だれの、いつの時点の store 値を load が受 け取ったか）を通じて、順序が観測されるのです。

これは正しいのですが、TSO memory model を out-of-order 実行システムで実現した場合の話になって しまっています。 つまり、余計な、関係の無い話だったと言えます。 →修正：普通にただしいことを書いているよな。

V8 が手元になかったので（手抜きですみません）、V9 と言葉使いが変わらないもの として。

SPARC の用語定義においては、Memory order と memory model (こちらは global visibility に関する) global visiblility order とは別の概念です。

Memory order の方は、ほぼ dependency order / self-consistency と同じ意味で 定義されています (V9 manual で D.2)

これは、本気でまるごと嘘っぱちを書いてしまいました。 すみませんでしたとしか申し上げようがありません。

> SPARC V9 Spec も memory ordering は memory transaction がメモリに届く順序 だと規定しています。

そんなことないでしょう。SPARC V9 では、D章にトランザクションは明にでてこない はず。（8章が description, D 章が形式的定義となっています）

これも嘘を書いてしまいました。 SPARC の仕様には memory transaction という用語がずばりもちいられています。 ただし、これが実システムにおける何に相当するのかは明らかではありません。 Model は Model だから、インプリは指定しないということなのでしょう（以下）。

The SPARC-V9 architecture is a model that specifies the behavior observed by software on SPARC-V9 systems. Therefore, access to memory can be implemented in any manner, as long as the behavior observed by software conforms to that of the models ... (Chapter. 8 Memory Models, 8.1 Introduction, SPARC-V9)

現実問題として、メモリトランザクションというと、普通はプロセッサチップから メモリバスへ発行されるトランザクションを彷彿することが多いと思われますが、 これと memory model は無関係です。 このことが念頭にあったので、上の「そんなことないでしょう」発言をしてしまいま した。

あきらかな嘘っぱちを書いてしまったのは、以上２点なのではないかと思いますが、 他にも議論にとって有効でないことを書き散らすなど、 反省すべき点がたくさんありました。

反省材料として、私にとっては価値があったのですが、 nminoru さんにはご迷惑だったと思います。お詫びします。