RISC-VにおけるRVWMOの仕様について読み直す (1)

RISC-VにおけるRVWMOのメモリモデルについて、仕様書を読み直すことにした。

もうちょっと詳しく、RISC-V仕様書のAppendxx A. RVWMOの節を読み解いていくことにした。

ここでの内容は、公理や保存プログラム順序の規則の意味と意図を明確にすることを目的としている。

A.1 なぜRVWMOなのか？

メモリ一貫性モデルは、弱いものから強いものまで存在している。

弱いメモリモデルは、より複雑なプログラミングモデルを犠牲にする代わりに、ハードウェア実装の柔軟性を高め、パフォーマンス、性能あたりの電力、電力消費、スケーラビリティ、ハードウェア検証のオーバーヘッドにおいて、強いモデルよりも良好な結果を提供すると言われている。
強いモデルはよりシンプルなプログラミングモデルを提供するが、パイプラインやメモリシステム内で実行できる（非推測的な）ハードウェア最適化により多くの制限を課すことになり、その結果、電力、面積オーバーヘッド、検証負担のコストが発生する。

RISC-Vは、リリース一貫性のバリアントであるRVWMOメモリモデルを選択しました。これはメモリモデルスペクトラムの2つ（弱いメモリモデルと強いメモリモデル）の間に位置している。 RVWMOメモリモデルは、アーキテクトがシンプルな実装、積極的な実装、大きなシステムの深い部分に組み込まれた実装、または複雑なメモリシステムの相互作用に対処する必要がある実装など、あらゆる可能性を構築することを可能にし、同時に高性能でプログラミング言語のメモリモデルをサポートするのに十分な強さを備えている。

他のアーキテクチャからのコード移植を容易にするために、一部のハードウェア実装では、デフォルトでより厳密なRVTSO順序セマンティクスを提供するZtso拡張を実装することを選択するかもしれない。 RVWMO用に書かれたコードは、RVTSOと自動的に互換性があるが、RVTSOを前提として書かれたコードがRVWMO実装で正しく動作することは保証されない。実際、ほとんどのRVWMO実装は、RVTSO専用のバイナリを実行することは推奨されない。したがって、各実装はRVTSOコードとの互換性を優先するか（例えば、x86からの移植を容易にするため）、またはRVWMOを実装する他のRISC-Vコアとの互換性を優先するかを選択する必要がある。

RVWMO用に書かれたコードの中には、RVTSOの下では冗長になるフェンスやメモリ順序付けアノテーションが存在している。 RVWMOのデフォルト実装がZtso実装に課すコストは、その実装でno-opになるフェンス（例：FENCE R,RWやFENCE RW,W）をフェッチする増分オーバーヘッドとなる。ただし、非Ztso実装との互換性が望ましい場合、これらのフェンスはコードに残す必要がある。

A.2 リトマステスト

この章での説明では、リトマステスト、つまりメモリモデルの特定の側面をテストまたは強調するために設計された小さなプログラムを使用している。図A.1は2つのHARTを持つリトマステストの例を示している。この図およびこの章に続くすべての図についての慣例として、s0–s2がすべてのHARTで同じ値に事前設定されており、s0がラベルxのアドレス、s1がy、s2がzを保持していると仮定する。ここで、x, y, zは8バイト境界に整列された互いに重複しないメモリアドレスを示している。各図は、左側にリトマステストコードを、右側に特定の有効または無効な実行の視覚化を示している(図A.1の場合は違反動作を示していることに注意)。

リトマステストは、具体的な特定の状況におけるメモリモデルの意味合いを理解するために使用される。例えば、図A.1のリトマステストでは、実行時に各HARTからの命令ストリームが動的にインターリーブされる方法に応じて、

最初のHARTのa0の最終値は2、4、または5のいずれかになるはずである。
しかし、この例では、Hart 0のa0の最終値は決して1または3にはならない。
直感的には、ロードが実行される時点で値1はもはや可視ではなく、値3はロードが実行される時点でまだ可視ではない。

以下では、このテストと多くの他のテストを分析する。

例えば、図A.1では、a0=1が発生するには、以下のいずれかが真である必要がある：

(b)がグローバルメモリ順序（および一貫性順序co）で(a)の前に現れる。
- しかし、これはRVWMO PPOルール1に違反する。
- この矛盾は、(b)から(a)へのcoエッジによって強調される
(a)がグローバルメモリ順序（および一貫性順序co）で(b)の前に現れる。
- しかし、この場合、ロード値公理が違反する。
- なぜなら、(a)はプログラム順序において(c)の前の最新のアドレスが一致するストアではない。
- (c)から(b)へのfrエッジがこの矛盾を強調している。

これらのシナリオのいずれもRVWMO公理を満たさないため、結果a0=1は禁止される。