RISC-VにおけるRVWMOの仕様について読み直す (3. Preserved Program Order / Memory Model Axioms)

RISC-VにおけるRVWMOのメモリモデルについて、仕様書を読み直すことにした。 ChatGPTの力を借りながら、要点をまとめていく。

---

保存されたプログラム順序

プログラムの任意の実行におけるグローバルメモリのアクセス順序は、各HARTのプログラム順序の一部を尊重するが、全てを尊重するわけではない。

• 保存されたプログラム順序 : グローバルメモリ順序によって尊重されなければならないプログラム順序のサブセット。

逆に考えると、独立したメモリ操作や、互いに独立した命令間では、その順序を保持する必要はない。厳密に順序を守らなければならないのは以下のルールに従う：

• メモリ操作aがプログラム順序でメモリ操作bより先行し、aとbが共に通常のメイン・メモリにアクセスする（I/O領域ではない）場合、そして以下のいずれかが当てはまる場合、保存されたプログラム順序（そしてグローバル・メモリ順序でも）においてaはbより先行する：

• 重複アドレス順序：

• bがストア命令であり、aとbが重複するメモリアドレスにアクセスする。
• aとbがロード命令であり、xはaとbの両方によって読まれるバイトであり、aとbの間のプログラム順序でxに対するストアがなく、aとbはxに対して異なるメモリ操作によって書かれた値を返す。

• aはAMOまたはSC命令によって生成され、bはロードであり、bはaによって書かれた値を返す。

• 明示的同期：

• aの前にbを順序付けるFENCE命令が挿入されている
• aにはacquire注釈が付いている。
• bにはrelease注釈が付いている。
• aとbの両方にRCsc注釈が付いている。

• aはbとペアになっている。

• 構文依存性：

• bにはaに対する構文アドレス依存性がある。
• bにはaに対する構文データ依存性がある。

• bはストアであり、bにはaに対する構文制御依存性がある。

• パイプライン依存性：

• bはロードであり、aとbの間のプログラム順序で、mがaに対するアドレスまたはデータ依存性を持ち、bがmによって書かれた値を返すようなストアmが存在する。
• bはストアであり、aとbの間のプログラム順序で、mがaに対するアドレス依存性を持つような何らかの命令mが存在する。

メモリモデルの公理

RISC-Vプログラムの実行がRVWMOメモリ一貫性モデルに従うためには、保存プログラム順序に従い、ロード値公理、原子性公理、および進行公理を満たすグローバルメモリ順序が存在しなければならない。

ロード値公理

各ロードiの各バイトは、以下のストアの中でグローバルメモリ順序において最後のものによってそのバイトに書き込まれた値を返す必要がある： 1. そのバイトに書き込み、グローバルメモリ順序でiより先行するストア。 2. そのバイトに書き込み、プログラム順序でiより先行するストア。

（つまり、メモリからの読み込みがどのように最新のデータを反映するかを規定する）

原子性公理

もしrとwが、HART hにおいてAlignedなLRとSC命令によって生成されるペアのロードおよびストア操作であり、sがバイトxへのストアで、rがsによって書かれた値を返す場合、sはグローバルメモリ順序でwより先行しなければならず、sの後でかつwの前に、h以外のHARTからのバイトxへのストアはグローバルメモリ順序において存在してはならない。 （つまり、特定の命令ペアが適切に連携して動作することを保証する）

原子性公理は理論上、異なる幅のLR/SCペアや一致しないアドレスへのペアに対応していますが、実装はそのような場合にSC操作が成功することを許可するためである。 しかしながら、実際にはそのようなパターンは稀であり、その使用は推奨されていない。

進行公理

グローバルメモリ順序で、無限の他のメモリ操作のシーケンスによって先行されるメモリ操作は存在してはならない。 （つまり、メモリがデッドロックに陥らないことを保証するための公理）。