芯耀
2425
1、前言
在RISC-V中，只有當存在一個全局內(nèi)存順序(global memory order)符合preserved program order，并且滿足load value axiom、atomicity axiom和progress axiom時，RISC-V程序的執(zhí)行才遵循RVWMO內(nèi)存一致性模型。今天主要講下load value公理、atomicity公理和progress公理。
2、load?value公理
loadA讀到的每個字節(jié)來自于store寫入該字節(jié)的值，loadA可以讀到store的值來自于以下兩種場景：
在全局內(nèi)存順序中，在loadA之前的store寫該字節(jié)
在program order中，在loadA之前的store寫該字節(jié) (可以forward)
全局內(nèi)存順序排在loadA之前的store，loadA肯定可以觀察到。另外第二點意思是現(xiàn)在幾乎所有的CPU實現(xiàn)中都存在store buffer，store操作的數(shù)據(jù)可能會暫時存放在這里面，而且還沒有全局可見，后續(xù)younger的load其實就可以提前forward里面的寫數(shù)據(jù)來執(zhí)行。因此，對于其它hart來說，在全局內(nèi)存順序上將觀察到load在store之前執(zhí)行。
我們可以看下面經(jīng)典的一個例子，假如這段程序是在具有store buffer的hart上運行的，那么最終結(jié)果可能是：a0=1，a1=0，a2=1，a3=0。
程序一種執(zhí)行順序如下：
執(zhí)行并進入第一個hart的store buffer；
執(zhí)行并轉(zhuǎn)發(fā)store buffer中(a)的返回值1；
執(zhí)行，因為所有先前的load（即(b)）已完成；
執(zhí)行并從內(nèi)存中讀取值0；
執(zhí)行并進入第二個hart的store buffer；
執(zhí)行并轉(zhuǎn)發(fā)store buffer中(e)的返回值1；
執(zhí)行，因為所有先前的load（即(f)）已經(jīng)完成；
執(zhí)行并從內(nèi)存中讀取值0；
從第一個hart的store buffer中寫到內(nèi)存；
(e)從第二個hart的store buffer中寫到內(nèi)存；
然而，即使(b)在全局內(nèi)存順序上先于(a)和，(f)先于(e)，在本例中唯一合理的可能性是(b)返回由(a)寫入的值，(f)和(e)也是如此，這種情況的結(jié)合促使了load value公理定義中的第二種選擇。即使(b)在全局內(nèi)存順序上在(a)之前，(a)仍然對(b)可見，因為(b)執(zhí)行時(a)位于store buffer中。因此，即使(b)在全局內(nèi)存順序上先于(a), (b)也應(yīng)該返回由(a)寫的值，因為(a)在程序順序上先于(b)。(e)和(f)也是如此。
3、atomicity公理
如果r和w是分別由hart h中對齊的LR和SC指令生成的成對load和store操作，s是對字節(jié)x的store，r返回由s寫的值，那么在全局內(nèi)存順序中，s必須位于w之前，并且在全局內(nèi)存順序中，除了h之外不能有其它hart的同地址store出現(xiàn)在s之后和w之前。
上面這段話看的是不是有點暈，我們可以看下圖，簡單說，就是如果r從s讀到數(shù)據(jù)了，那么s和w之間不可能穿插其它hart的store數(shù)據(jù)了，但允許本hart穿插其它同地址store數(shù)據(jù)，由此來確保一個hart使用LR和SC的原子性。
Atomicity公理禁止來自其它hart的同地址store穿插在LR和SC之間，但它不禁止其它同地址load穿插在其中。
Atomicity公理理論上支持不同寬度和不匹配地址的LR/SC對，因為實現(xiàn)允許SC操作在這種情況下成功。不過在實踐中，這樣的模式是罕見的，并且不鼓勵使用它們。
RISC-V包含兩種類型的原子操作：AMO和LR/SC對，它們的行為有所不同。LR/SC的行為就好像舊的值返回給hart，hart對它進行修改，并寫回主存，這中間不被其它hart的store打斷，否則就是失敗的。AMO的行為就好像是在內(nèi)存中直接進行的，因此AMO本質(zhì)上就是原子性的。
4、progress公理
在全局內(nèi)存順序中，任何內(nèi)存操作都不能在其他內(nèi)存操作的無限序列之前進行。
這個公理保證程序終究可以往前執(zhí)行，確保來自一個hart的store最終在有限的時間內(nèi)對系統(tǒng)中的其它hart可見，并且來自其它hart的load最終能夠讀取這些值。如果沒有這個規(guī)則，例如spinlock在一個值上無限自旋是合法的，即使有來自其它一個hart的store等到解鎖該自旋鎖。
