RISC-V筆記——內(nèi)存模型公理

1、前言

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

2、load?value公理

loadA讀到的每個(gè)字節(jié)來(lái)自于store寫(xiě)入該字節(jié)的值，loadA可以讀到store的值來(lái)自于以下兩種場(chǎng)景：

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

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

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

我們可以看下面經(jīng)典的一個(gè)例子，假如這段程序是在具有store buffer的hart上運(yùn)行的，那么最終結(jié)果可能是：a0=1，a1=0，a2=1，a3=0。

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

執(zhí)行并進(jìn)入第一個(gè)hart的store buffer；

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

執(zhí)行，因?yàn)樗邢惹暗膌oad（即(b)）已完成；

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

執(zhí)行并進(jìn)入第二個(gè)hart的store buffer；

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

執(zhí)行，因?yàn)樗邢惹暗膌oad（即(f)）已經(jīng)完成；

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

從第一個(gè)hart的store buffer中寫(xiě)到內(nèi)存；

(e)從第二個(gè)hart的store buffer中寫(xiě)到內(nèi)存；

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

3、atomicity公理

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

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

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

Atomicity公理理論上支持不同寬度和不匹配地址的LR/SC對(duì)，因?yàn)閷?shí)現(xiàn)允許SC操作在這種情況下成功。不過(guò)在實(shí)踐中，這樣的模式是罕見(jiàn)的，并且不鼓勵(lì)使用它們。

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

4、progress公理

在全局內(nèi)存順序中，任何內(nèi)存操作都不能在其他內(nèi)存操作的無(wú)限序列之前進(jìn)行。

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