RISC-VにおけるRVWMOのメモリモデルについて、仕様書を読み直すことにした。
もうちょっと詳しく、RISC-V仕様書のAppendxx A. RVWMOの節を読み解いていくことにした。
A.3 RVWMOルールの説明
RISC-Vアーキテクチャの重要な部分であるRVWMOメモリ一貫性モデルの規則と公理についての説明と例を示す。
A.3.1 保存プログラム順序とグローバルメモリ順序
保存プログラム順序: プログラム順序のサブセットであり、グローバルメモリ順序の中で維持されなければならない。 つまり、単一のHART（ハードウェアスレッド）によって実行された特定のイベントは、他のHARTや観測者に同じ順序で表示される必要がある。
グローバルメモリ順序: すべてのHARTにわたってメモリ操作（ロードとストア）が実行される観測可能な実際の順序。 これは、コヒーレンスプロトコルとメモリシステムによって決定され、ストアバッファなどの再順序付け効果により順序が変わることがある。
A.3.2 ロード値公理
この公理は、各ロード操作がグローバルメモリ順序またはプログラム順序で、そのロードに先行する最も新しいストアによって同じメモリ位置に書き込まれた値を返さなければならないと定めている。
A.3.3 原子性公理
このルールは、LR（Load Reserved）およびSC（Store Conditional）命令によって生成されるペアのロードおよびストア操作に適用される。 他のHARTからのストアがグローバルメモリ順序のこのロード-ストアのペアの間に挿入されない場合、ロードはストアによって書かれた値を返す。
A.3.4 進行公理
進行公理は、他のメモリ操作の無限のシーケンスによってメモリ操作が無期限に遅延されることがないことを保証する(つまりデッドロックしない)。 これは、すべてのHARTが最終的に他のHARTのストアの効果を観察できるようにすることを保証する。
A.3.5 重複アドレス順序付け（規則1〜3）
命令間でアドレスが重なっている場合の順序付けに関するRVWMOメモリモデルの規則が説明は、以下の3つの規則に要約される：
規則1
bがストアであり、aとbが重複するメモリアドレスにアクセスする場合、aはbに先行する必要がある。- これは直観的。ストアによるメモリ書き込みは取り消しが非常に困難なため、それに先行する
aは先に実行される必要がある。 - 一方で、古いストアに対する新しいロードは順序付けを守る必要はない。これは、マイクロアーキテクチャの観点からは、ストアバッファから後続のロードが可能であること、また新しいロードによる投機的な実行は取り消しが容易であるということから来ている。
規則2
- aとbがロードであり、xは両方のロードによって読まれるバイトで、プログラム順序においてaとbの間にxに対するストアがない場合、aとbは異なるメモリ操作によって書かれたxの値を返す必要がある。
これは通常"CoRR (Coherence for Read-Read pairs)"と呼ばれれおり、より新しいロードは、同じHART内でアクセスされる古いロードの値よりも古い値を返してはならない、というものである。
図A.5のリトマステストを考えてみる。これは"fri-rfi"パタンの一般的なケースを示している。 "fri-rfi"というのは(d),(e),(f)の流れを示している。
- (d)は(e)に対して、"from-reads"の制約を受ける(つまり、(d)は(e)の書き込んだ値よりも古いデータを読み出す)。
- (f)は(e)の書き込んだデータを読み出す。
マイクロアーキテクチャの観点からは、a0=0, a1=2, a2=0という動作は合法である。この時、以下のような動作が想定されるだろう：
- (d) がストールし、ロードが遅れる。
- (e) が実行され、データがストアバッファに書き込まれる。
- (f) が実行され、(e)のストアバッファの結果をロードする。
- (g), (h), (i) が実行される。
- (a) が実行されメモリに値が書き込まれる。(b)と(c)が実行されメモリに値が書き込まれる。
- (d) のストールが解消され実行開始される。
- (e) のストアがメモリに書き込まれる。
これは、つまりグローバルメモリ順序が(f), (i), (a), (c), (d), (e)の順序で実行されたことを意味する。 (f)が(d)の前に実行されたことにより、(f)の読み込んだ値は(d)が読み込んだ値のものよりも新しいものになっている。 したがって、この挙動は合法であり、CoRRの要件に対して違反することはない。
図A.6のリトマステストを考える。この時、a0=1, a1=v, a2=v, a3=0という挙動がありうる。ここでvは他のHARTによって書き込まれた任意の値である。
グローバルなメモリ順序は、(h), (k), (a), (c), (d), (g) というのが考えられるが、a1とa2の結果はs4とs2が同じアドレスを指しており、(g)の後の(h)はリプレイにより(g)と同じ値を返すと仮定すると、順序は守られる。
もしa1とa2が異なる値を返した場合、(h)は(g)よりも先に実行され、(h)は(g)よりも古い値を返してしまう可能性がある。これはPPOのルール2 (a and b are loads, x is a byte read by both a and b, there is no store to x between a and b in program order, and a and b return values for x written by different memory operations)に違反し、CoRRも違反となる。
規則3
aがAMO（アトミックメモリ操作）またはSC（ストア条件付き）命令によって生成され、bがロードであり、bがaによって書かれた値を返す場合、aはbに先行する必要がある （PPOルール3 : a is generated by an AMO or SC instruction, b is a load, and b returns a value written by a）。
