792
1、前言
在RISC-V中，只有当存在一个全局内存顺序(global memory order)符合preserved program order，并且满足load value axiom、atomicity axiom和progress axiom时，RISC-V程序的执行才遵循RVWMO内存一致性模型。今天主要讲下load value公理、atomicity公理和progress公理。
2、load value公理
loadA读到的每个字节来自于store写入该字节的值，loadA可以读到store的值来自于以下两种场景：
在全局内存顺序中，在loadA之前的store写该字节
在program order中，在loadA之前的store写该字节 (可以forward)
全局内存顺序排在loadA之前的store，loadA肯定可以观察到。另外第二点意思是现在几乎所有的CPU实现中都存在store buffer，store操作的数据可能会暂时存放在这里面，而且还没有全局可见，后续younger的load其实就可以提前forward里面的写数据来执行。因此，对于其它hart来说，在全局内存顺序上将观察到load在store之前执行。
我们可以看下面经典的一个例子，假如这段程序是在具有store buffer的hart上运行的，那么最终结果可能是：a0=1，a1=0，a2=1，a3=0。
程序一种执行顺序如下：
执行并进入第一个hart的store buffer；
执行并转发store buffer中(a)的返回值1；
执行，因为所有先前的load（即(b)）已完成；
执行并从内存中读取值0；
执行并进入第二个hart的store buffer；
执行并转发store buffer中(e)的返回值1；
执行，因为所有先前的load（即(f)）已经完成；
执行并从内存中读取值0；
从第一个hart的store buffer中写到内存；
(e)从第二个hart的store buffer中写到内存；
然而，即使(b)在全局内存顺序上先于(a)和，(f)先于(e)，在本例中唯一合理的可能性是(b)返回由(a)写入的值，(f)和(e)也是如此，这种情况的结合促使了load value公理定义中的第二种选择。即使(b)在全局内存顺序上在(a)之前，(a)仍然对(b)可见，因为(b)执行时(a)位于store buffer中。因此，即使(b)在全局内存顺序上先于(a), (b)也应该返回由(a)写的值，因为(a)在程序顺序上先于(b)。(e)和(f)也是如此。
3、atomicity公理
如果r和w是分别由hart h中对齐的LR和SC指令生成的成对load和store操作，s是对字节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公理
在全局内存顺序中，任何内存操作都不能在其他内存操作的无限序列之前进行。
这个公理保证程序终究可以往前执行，确保来自一个hart的store最终在有限的时间内对系统中的其它hart可见，并且来自其它hart的load最终能够读取这些值。如果没有这个规则，例如spinlock在一个值上无限自旋是合法的，即使有来自其它一个hart的store等到解锁该自旋锁。
