1、前言

在RISC-V中，只有當存在一個全局內存順序(global memory order)符合preserved program order，并且滿足load value axiom、atomicity axiom和progress axiom時，RISC-V程序的執(zhí)行才遵循RVWMO內存一致性模型。今天主要講下load value公理、atomicity公理和progress公理。

2、load?value公理

loadA讀到的每個字節(jié)來自于store寫入該字節(jié)的值，loadA可以讀到store的值來自于以下兩種場景：

在全局內存順序中，在loadA之前的store寫該字節(jié)

在program order中，在loadA之前的store寫該字節(jié) (可以forward)

全局內存順序排在loadA之前的store，loadA肯定可以觀察到。另外第二點意思是現在幾乎所有的CPU實現中都存在store buffer，store操作的數據可能會暫時存放在這里面，而且還沒有全局可見，后續(xù)younger的load其實就可以提前forward里面的寫數據來執(zhí)行。因此，對于其它hart來說，在全局內存順序上將觀察到load在store之前執(zhí)行。

我們可以看下面經典的一個例子，假如這段程序是在具有store buffer的hart上運行的，那么最終結果可能是：a0=1，a1=0，a2=1，a3=0。

程序一種執(zhí)行順序如下：

執(zhí)行并進入第一個hart的store buffer；

執(zhí)行并轉發(fā)store buffer中(a)的返回值1；

執(zhí)行，因為所有先前的load（即(b)）已完成；

執(zhí)行并從內存中讀取值0；

執(zhí)行并進入第二個hart的store buffer；

執(zhí)行并轉發(fā)store buffer中(e)的返回值1；

執(zhí)行，因為所有先前的load（即(f)）已經完成；

執(zhí)行并從內存中讀取值0；

從第一個hart的store buffer中寫到內存；

(e)從第二個hart的store buffer中寫到內存；

然而，即使(b)在全局內存順序上先于(a)和，(f)先于(e)，在本例中唯一合理的可能性是(b)返回由(a)寫入的值，(f)和(e)也是如此，這種情況的結合促使了load value公理定義中的第二種選擇。即使(b)在全局內存順序上在(a)之前，(a)仍然對(b)可見，因為(b)執(zhí)行時(a)位于store buffer中。因此，即使(b)在全局內存順序上先于(a), (b)也應該返回由(a)寫的值，因為(a)在程序順序上先于(b)。(e)和(f)也是如此。

3、atomicity公理

如果r和w是分別由hart h中對齊的LR和SC指令生成的成對load和store操作，s是對字節(jié)x的store，r返回由s寫的值，那么在全局內存順序中，s必須位于w之前，并且在全局內存順序中，除了h之外不能有其它hart的同地址store出現在s之后和w之前。

上面這段話看的是不是有點暈，我們可以看下圖，簡單說，就是如果r從s讀到數據了，那么s和w之間不可能穿插其它hart的store數據了，但允許本hart穿插其它同地址store數據，由此來確保一個hart使用LR和SC的原子性。

Atomicity公理禁止來自其它hart的同地址store穿插在LR和SC之間，但它不禁止其它同地址load穿插在其中。

Atomicity公理理論上支持不同寬度和不匹配地址的LR/SC對，因為實現允許SC操作在這種情況下成功。不過在實踐中，這樣的模式是罕見的，并且不鼓勵使用它們。

RISC-V包含兩種類型的原子操作：AMO和LR/SC對，它們的行為有所不同。LR/SC的行為就好像舊的值返回給hart，hart對它進行修改，并寫回主存，這中間不被其它hart的store打斷，否則就是失敗的。AMO的行為就好像是在內存中直接進行的，因此AMO本質上就是原子性的。

4、progress公理

在全局內存順序中，任何內存操作都不能在其他內存操作的無限序列之前進行。

這個公理保證程序終究可以往前執(zhí)行，確保來自一個hart的store最終在有限的時間內對系統(tǒng)中的其它hart可見，并且來自其它hart的load最終能夠讀取這些值。如果沒有這個規(guī)則，例如spinlock在一個值上無限自旋是合法的，即使有來自其它一個hart的store等到解鎖該自旋鎖。