RISC-Vメモリ・コンシステンシ・モデル

備忘録。規格(The RISC-V Instruction Set Manual Volume I: Unprivileged ISA Document Version 20191213)を読む前準備として調べたことのメモ書き。

RISC-Vのメモリ・コンシステンシ・モデル

Weak Memory Ordering (WMO)：RISC-V標準のメモリ・コンシステンシ・モデル。別名RVWMO。
Total Store Ordering (TSO)：“Ztso” Standard ExtensionにてRVWMOからの差分で定義されている。x86やSPARCのメモリ・コンシステンシ・モデルはこれ。WMOより厳しい。

メモリ・コンシステンシ・モデル

複数のhart(RISC-Vにおけるハードウェアスレッドのこと)がありメモリを共有しているシステムでは、あるhartが複数の宛先の異なる書き込みを行った時に、それがどういう順序で他のhartに読めるようになるのかをよく意識しなければならない。
1つのhartが最低限保証しなければならないのは、プログラム順に矛盾しないように、同じ宛先へのWrite間、およびWriteとReadの順序が入れ替わらないようにすることだけである。メモリ・コンシステンシ・モデルは、メモリ・アクセスの順序についてこれ以上に何を保証するのかを決める。より緩い制約はプログラム順に縛られない実行入れ替えを可能にするので性能を高めるが、プログラム動作がどうなるのか直感的に理解しにくくなっていく。

Weak Memory Ordering

このモデルではメモリ・アクセスはプログラム順的にそれより前のメモリ・アクセスを追い越して実行される。順序制約が必要な時は同期命令(FENCE)を使って実現する。

例1：共有変数a, b, flagがありすべて初期値0とする。hartが2つあってそれぞれ以下のプログラムを実行するとする。ここでprint a;というのは単純にその変数をReadできたときにシミュレータ上で出力する疑似命令と理解してほしい。

// hart0
a=1;
b=2;
flag=1;

// hart1
while(flag==0);
print a;
print b;

直感的には、hart1の方はhart0がflag!=0にするのを待ってから、a, bの値を出力するプログラムに読めるから、出力は1,2であると期待されるが、これがWMOの時はそれは保証されない。hart0のa=1; b=2;flag=1;の結果のどれが先にhart1に読めるようになるのかは保証がないので、flagが最初に反映される可能性がある。
したがって(1,2)に加えて次の出力があり得る
(0,0) // a=1もb=2も反映される前の値を読んでしまう
(1,0) // a=1だけ反映された
(0,2) // b=2だけ反映された
(0,1) // a=1だけ反映されて、print a; print b;の読んだ順序も入れ替わった
(2,0) // b=2だけ反映されて、print a; print b;の読んだ順序も入れ替わった
(2,1) // 両方反映されたが、print a; print b;の読んだ順序が入れ替わった
hart0でflagの変更以前に行われたメモリ・アクセスをちゃんとhart1に反映したい場合はFENCEを使って次のようにする

// hart0
a=1;
b=2;
FENCE;
flag=1;

// hart1
while(flag==0);
FENCE;
print a;
print b;

FENCE命令の機能は、FENCE命令より後のメモリ・アクセスの発行は、FENCE命令より前のすべてのメモリ・アクセスが完了しないかぎり行われないというものである。これによって上記プログラムではflag=1のWriteはa=1, b=2のWriteの後に必ず行われるし、print a; print bのReadはflag==0のReadを追い越して行われない。

Total Store Ordering

Writeは先行するメモリアクセスの完了を待つ。
Readは先行するWriteの完了を待たずに完了可能とする。
複数Writeの順序は複数プロセッサで同じ順序で観測される。

ちなみに、あくまで現状の規格(The RISC-V Instruction Set Manual Volume I: Unprivileged ISA Document Version 20191213)が決めているのは通常のメモリへのロードストアについてのみで、デバイス領域へのオーダリングについては定義はない。デバイス領域へのオーダリングは個々のプロセッサのデータシートで定められている。