rvwmo

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:

  1. Store that write that byte and that precede i in the global memory order
  2. 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。