RISC-VはメモリコンシステンシモデルとしてRVWMO (RISC-V Weakl Memory Ordering)を採用している。 RVWMOについての説明はRISC-Vの仕様書のAppendixについて説明されているが、ここを読んでいくことにする。
RVWMOを理解するにあたって、リトマステストというのを使用する。リトマステストについてはかつて論文を読んで勉強していたのだが、本章を読んで思い出してみよう。
GitHub - riscv/riscv-isa-manual: RISC-V Instruction Set Manual
A.2 リトマステスト
本章では、メモリモデルのある特定の側面をテストしたり、強調したりするために設計された小さなプログラムである、リトマステストを用いて説明します。図 A.1は、2 つの hart を使ったリトマステストの例です。ここでは、すべての hart で s0～s2 が同じ値に設定されており、s0 が x、s1 が y、s2 が z と表示されたアドレスを保持しているものとします。左側にリトマステストのコード、右側に有効または無効な実行結果を表示しています。
リトマステストは、特定の具体的な状況におけるメモリモデルの意味合いを理解するために使用されます。例えば、図 A.1のリトマステストでは、第 1 の hart の a0 の最終値は、実行時の各 hart からの命令ストリームの動的インターリーブによって、2、4、5 のいずれかになります。しかし、この例では、hart 0 の a0 の最終的な値が 1や 3 になることはありません。直感的には、ロードが実行される時点では 1 の値は見えなくなり、ロードが実行される時点では 3 の値はまだ見えていません。
