RVWMO(RISC-V Weak Memory Ordering) 是RISC-V定义的memory consistency model。
terms
global memory order, 所有harts产生的memory operations的所有顺序。通常，多线程程序有许多不同可能的执行，每个执行有它自己相对应的global memory order。global memory order是在hart的memory instructions 产生的load和store操作的基础上定义的。它受RVWMO的约束，所有满足这些约束的执行都是合法的执行。
program order，反应了在hart的动态指令流中load 和store逻辑上的顺序。也就是简单顺序处理器执行指令的顺序。
RCpc, release consistency with processor-consistent synchronization operations.
RCsc, release consistency with sequentially-consistent synchronization operations
acquire annotation, refers to acquire-RCpc annotation or acquire-RCsc annotation
release annotation, refers to release-RCpc annotation or release-RCsc annotation
RCpc, refers to an acquire-RCpc annotation or a release-RCpc annotation
RCsc, refers to an acquire-RCsc annotation or a release-RCsc annotation
preserved program order
如果memory operation a在程序上先于memory operation b，并且都是访问main memory，在以下情况发生时，a先于b是符合preserved program order的，当然也是符合global memory order的。
换句话说，preserverd program order就是当以下情况发生时，a必须要在b之前执行，也就是在以下情况时，不能乱序。只要不在下列情况里面，那就可以乱序。
Overlapping-Address Orderings
1. b is a store, and a and b access overlapping memeory address
b是store，a和b访问重叠的地址空间。这点很好理解，前提已经确定b是store，假设a也是store，而且a在b前面，那最终的值应该要是b存进去的值，显然a和b不能乱序；假设a是load，而且a在b前面，那a拿到的必须要是老的值，不然程序无法写了。所以，只要b是store，那它前面的任意指令，只要和b有重叠的地址访问，那必须保序。
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
a和b都是load，并且a和b有访问同一个byte地址x，a和b之间在程序顺序上没有store，并且a和b返回的x是被不同memory operation写过的。
这点不太好理解，前面三句都是前提条件，最后一句是重点，a和b返回的x是被不同memory operation写过的，而且第三句又说了它们之间没有对x的store，那就只可能是另一个hart对x有操作了。也就是说，站在memory的角度上看，假设a和b都是发自H0，另一个hart是H1。如果a和b之间没有H1的操作，那a和b返回的x的值一定他们之前的同一个store的，那就可以乱序。如果a和b之间有一个H1的对x的store操作，那么b拿到的值和a拿到的值是不一样的，对于程序来说，必须要求后面的load不能拿到比前面load更老的值，所以这种情况下，是不能乱序的，a就必须在b的前面，a必须拿到老的值，b必须拿到新的值。
3. a is generated by an AMO or SC instruction, b is a load, and b returns a value written by a
a是AMO或者SC指令，b是load，并且b返回的是a写入的值，那就不能乱序，这个比较好理解，如果这个能乱序，那程序就没法写了。
Explicit Synchronization
4. There is a FENCE instruction that orders a before b
a和b之间有FENCE指令，明显不能乱序了。
5. a has an acquire annotation
a有acquire注释，明显也不能乱序了，因为acquire就是把后面的操作都挡住。
6. b has a release annotation
b有release注释，明显也不能乱序了，因为release就是把前面的操作都挡住。
7. a and b both have RCsc annotation
a和b都有release consistency with sequentially-consistent synchronization operations。也是显示的要求不能乱序。
8. a is paired with b
a和b是成对的。成对的操作都是为了写同步代码的，所以也是显示规定不能乱序。
Syntactic Dependencies
9. b has a syntactic address dependency on a
b访问的地址依赖与a的结果，那明显不能乱序，只能等a算完之后，b才能拿到值。
Address dependency: the result of A is used to determine the address accessed by B.
10. b has a syntactic data dependency on a
b访问的数据依赖与a的结果，同样的道理也不能乱序。
Data dependency: the result of A is used to determine the value written by store B.
11. b is a store, and b has a syntactic control dependency on a
b是一笔store，并且b有控制依赖于a。
Control dependency: the result of A feeds a branch that determines whether B is executed at all
也就是：a的结果决定了一个branch是否执行，这个branch决定了b是否执行。所以a必须先于b执行。
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
b是load，在a和b之间有一个store m操作，m又依赖于a，意味着m一定要在a后面执行，然后b又要返回m写入的值，所以b要在m后面执行，那也就是a和b一定要保序了。相当于a和m要遵循9-10条规则，b和m要遵循10规则，推导而来a和b就要保序了。
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
b是store，a和b之间有一条指令m，m又依赖于a，所以m和a遵循9-10规则必然保序，b和m要遵循1规则，推导而来a和b就要保序了。
Memory Model Axioms
遵循RVWMO规则的程序，除了要遵循上述PPO之外，还要满足the load value axiom, the atomicity axiom and the progress axiom。
Load Value Axiom
Each byte of each load i returns the value written to that byte by the store that is the latest in global order among the following stores:
- Store that write that byte and that precede i in the global memory order
- Store that write that byte and that precede i in program order
这段很绕，我的理解是，load返回的要么是global memory order的数据，要么是program order的数据，不能是其他值了。或者说，load要么返回memory的数据，要么返回store buffer的数据。
Atomicity Axiom
If r and w are paired load and store operations generated by aligned LR and SC instructions in a hart h, s is a store to byte x, and r returns a value written by s, then s must precede w in the global memory order, and there can be no store from a hart other than h to byte x following s and preceding w in the global memory order.
这点还不理解。
s必须先于w在global memory order上反应，s之后w之前，不能有其他hart对a0进行写动作？？？
Progress Axiom
No memory operation may be preceded in the global memory order by an infinite sequence of other memory operations.
也就是说，一个hart发了store，在有限的时间内，另一个hart最终一定能够看到这条store。