riscv内存模型分析

基本逻辑

各个CPU构架的弱内存模型都会定义一些规则，这些规则约束各种内存序，在这些规则之外
各种内存访问都是可以乱序的，所谓barrier指令只是其中的一些规则，这些规则用指令的
方式显示约束了内存序，所以，只从barrier指令去看内存序，始终是只能看到其中的一部分，
整体认识上还是模模糊糊。如果编程中会遇到可能的内存序问题，这些规则怎么说也的通读
一遍，不然基本上就是一个“能跑就行”的程序。

riscv协议在Chapter 14定义了这些规则(ARMv8/v9协议在2.3章定义了相关规则)，在附录里
专门做了这些规则的解释(RVWMO Explanatory Material, Version 0.1)，在附录里还有内存
序相关的形式化验证模型(Formal Memory Model Specifications, Version 0.1)。

注意内存序(consistency)和cache一致性(coherence)是两个不同的概念，前者是说的是硬件
故意放松一些指令执行上的循序，依此来提高硬件性能，指令的这种乱序行为是程序员可以
直接感知的，本文讨论的就是内存序的相关问题，而后者指的是，多核系统上，因为多核
共享内存或者cache而引发的数据存储一致性上的问题，硬件需要用一定的cache一致性协议
(比如MESI协议)在硬件层面解决这个问题。

riscv内存序规则

riscv在Chapter 14定义了它的弱内存序，定义的逻辑是这样的，”Memory Model Primitives”
这一节是一些术语的定义，”Syntactic Dependencies”这一节定义的是两个指令关系的名称，
这一节并没有定义内存序的规则，后面定义规则时依赖这一节里定义的指令关系，”Preserved Program Order”
这一节定义的是riscv弱内存序的规则，这一节是这一章的主体，一共定义了13条规则(rule)，
随后在”Memory Model Axioms”这一节里定义了三条公理(Axioms)，这些约束大部分是符合
我们的直观的认识，但是也有一些和直观的认知是不同的。学习这些规则时，我们要认识到
这些规则之外的情况，这些情况都是可以乱序的，barrier指令正是对有可能出现的乱序情况
的约束。下面逐条看下这些规则:

• Overlapping-Address Orderings

  1. b is a store, and a and b access overlapping memory addresses  

  2. a and b are loads, x is a byte read by both a and b, there is no store to x
     between a and b in program order, and a and b return values for x written by
     different memory operations  

  3. a is generated by an AMO or SC instruction, b is a load, and b returns a value
     written by a

访存地址有重合的情况，第一条规则是说后面的store不能跑到前面的指令之前执行。

第二条规则就比较绕了，直接翻译是，a和b是load操作，x是a和b要读的数据，a和b之间没有
store修改x(在内存)的值，a和b load的值之前被不同的内存写操作修改。这一条规则进一步的
解释是，两个load读同一个地址上值，新的load不能读到旧load读到的值，但是，还要进一步
考虑两种情况，第一种是a和b之间有store修改x的值，这种情况下a和b不保序，第二种情况
是，a和b读到的值是被不同写内存操作修改的值，这种情况a和b也不保序。

第三条规则是说，后面的load不能超过之前由AMO/SC触发的写操作，直观的理解也是这样。

注意，根据如上的定义，当a是一个普通的store，b是一个load，他们访问相同地址，load
是可以跑到store之前的，不过load到的值是store缓存在store buff里的值，这个就是Intel
TSO内存序上唯一放松的内存序。

再次总结下，load/store的四种可能情况是：1. load-load, 2, load-store, 3, store-store,
4. store-load。规则1说的是2/3两种情况不能乱序，规则2说的是1的情况，规则3只说了
AMO/SC-load的情况，不能乱序，所以普通store-load的情况是可以乱序的，这种情况就是
我们上面提到了TSO内存序上唯一的一个放松约束。

• Explicit Synchronization 

  4. There is a FENCE instruction that orders a before b

  5. a has an acquire annotation

  6. b has a release annotation

  7. a and b both have RCsc annotations 

  8. a is paired with b

用显示的barrier指令指定内存序的情况，这些去看barrier的定义就好，需要注意的点有：

acquire语意是说acquire后面的读写指令不能排到acquire之前(没有约束acquire之前读写
指令的顺序)，逻辑示意如下。release的语意正好相反。

         +-------------+
         | load/store  |---------+
         +-------------+         |
                                 |
----- instruction with acquire --+--
  ^                              |
  |      +-------------+         |
  +------| load/store  |         v
         +-------------+

riscv上acquire/release的作为AMO或者lr/sc指令的属性一起使用，ARM64上则有STLR/LDAR
指令，这两条指令把acquire/release和普通load/store指令结合到了一起。

如下图所示，如果要确保地址无关的两个store不乱序，可以在其中加一个写fence，但是
这样会一把拦住fence前后的所有store，当把后一个store换成带release的store时(STLR)，
store和STLR保序的同时，STLR后面其它的地址无关的store/load也可以提前投机执行。

         +-------------+                            +-------------+          
         |    store    |---------+           ^      |    store    |---------+
         +-------------+         |           |      +-------------+         |
                                 v           |                              |
------------- fence -------------+--       --+---------- STLR --------------+--
  ^                                          |                              
  |      +-------------+                     |      +------------------+
  +------|    store    |                     +------| other store/load |         
         +-------------+                            +------------------+

第七条规则中的RCsc指的是Release Consistency with sequentially-consistent synchronization
operation，对应的概念还有RCpc，这两者是acquire/release的两种分类，描述的是，比如
上图中如果“other store/load“里如果有LDAR，那么这个LDAR是否可以和STLR乱序，如果
acquire/release的种类是RCsc，那么不能乱序，如果是RCpc，是可以乱序的。riscv的WMO
中的acquire/release的种类是RCsc。

第八条规则说的a和b是一个pair，是说lr/sc指令组成的pair。

• Syntactic Dependencies 

  9. b has a syntactic address dependency on a

  10. b has a syntactic data dependency on a

  11. b is a store, and b has a syntactic control dependency on a

这几条规则说的是指令之间语意上的依赖，和最开始访存地址重合的依赖比较类似。riscv
上对地址依赖和数据依赖的定义如下：对于两条内存操作指令，如果后一条指令的地址输入
寄存器依赖前一条指令，就存在一个地址依赖，如果后一条指令的数据依赖前一条指令，就
存在一个数据依赖，所以所谓地址依赖和数据依赖都描述的是两条访存指令之间的关系。

需要注意的是规则11，这条规则提到了“控制依赖”，控制依赖的定义是，指令a和指令b，
如果中间还有一条分支或者间接跳转指令(branch and indirect jump)m，如果a和m存在
Syntactic Dependencies，那么b和a之间就存在一个控制依赖，而规则11是说，在a和b之间
存在一个控制依赖时，如果b是个store指令，那么a和b是不能乱序的。

riscv spec里在“Syntactic Dependencies”这一节定义各种依赖关系的定义，但是只是说
当两条指令满足某种情况时，它们之间叫什么关系，并不是满足这种关系后就有序的约束，
riscv spec随后在“Preserved Program Order”这一节借助”Syntactic Dependencies”的定义，
描述内存序的约束，规则9和规则10，直接就说满足地址依赖和数据依赖的两条指令有内存
序上的约束，而规则11是说在满足控制依赖关系时，只对后面是store的情况有序上的约束。

规则11的代码示意如下，左边两个是不会乱序的情况，其中一个是汇编实现，一个是对应的
C语言实现，最右边的是需要加读barrier的场景。

1
2
3

load a0, a1(0)         a = read(p1);         a = read(p1); <--- 这个read后需要一个读barrier
beqi a0, #1, lable     if (a == 1)           if (a == 1)
store a2, a3(0)            write(p2, b);         c = read(p2);

这条规则是多么的反直觉，但是既然定义成了规则，它就是软硬件约定的编程接口！

• Pipeline Dependencies 

  12. b is a load, and there exists some store m between a and b in program order
      such that  m has an address or data dependency on a, and b returns a value
      written by m  

  13. b is a store, and there exists some instruction m between a and b in program
      order such that m has an address dependency on a

这两条规则是说，依赖之间是可以前后构成依赖链条的。

下面是三条Axioms的定义。

Load Value Axiom: 每个load指令得到值是global memory order上最近一次store的值，这个
store是global memory order或者是program order上在loadz之前。

Atomicity Axiom: 这个已经体现在lr/sc指令定义里。

Progress Axiom: 貌似是说乱序时提前执行总有一定的限制的。

riscv barrier指令

riscv上barrier有fence和fence.i，相关的指令可以参考这里。

ARM内存序以及barrier指令

Linux内核内存序介绍

Linux内核有详细介绍内存序的文档：Documentation/memory-barriers.txt。

参考

https://www.youtube.com/watch?v=QkbWgCSAEoo