Sherlock's blog

有容乃大，无欲则刚

0%

使用herd7做ARM内存模型验证

发表于 更新于
本文介绍使用herd7做ARM内存模型验证的基本逻辑。

ARM内存模型

ARM spec的B2章节中介绍了ARM的内存模型，B2章节的核心内容是定义了一套指令之间需要
遵守的执行顺序上的规则，这些规则之外的指令顺序都是可以乱序的。

对于这些规则，ARM需要确保当这些规则运行在一起的时候，相互之间没有冲突。程序员要
确保在这组规则的下，写出的程序得到的各种结果是符合程序员预期的。

我们看一个两个core上指令序例的例子，这个例子其实就是一个简单的Litmus测试用例。

1
2
3
4
5
6
7
8
9
10
AArch64 MP 
{
0:X1=x; 0:X3=y;
1:X1=y; 1:X3=x;
}
 P0          | P1          ;
 MOV W0,#1   | LDR W0,[X1] ;
 STR W0,[X1] | LDR W2,[X3] ;
 MOV W2,#1   |             ;
 STR W2,[X3] |

P0/P1两个core, X1/X3表示两个寄存器，其中的内容是两个地址，x/y是对应地址上的值,
如果X1/X3是不同的地址，我们就先只看load/store的可能顺序，可能的顺序有：

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
------------------------------------------------------------
             | LDR W0,[X1]                   | LDR W0,[X1]
             |                               |
             | LDR W2,[X3]                   | LDR W2,[X3]
 STR W0,[X1] |                   STR W2,[X3] | 
             |                               |
 STR W2,[X3] |                   STR W0,[X1] | 
------------------------------------------------------------
             | LDR W0,[X1]                   | LDR W0,[X1]
 STR W0,[X1] |                   STR W2,[X3] | 
             | LDR W2,[X3]                   | LDR W2,[X3]
 STR W2,[X3] |                   STR W0,[X1] | 
------------------------------------------------------------
             | LDR W0,[X1]                   | LDR W0,[X1]
 STR W0,[X1] |                   STR W2,[X3] | 
             |                               |
 STR W2,[X3] |                   STR W0,[X1] | 
             | LDR W2,[X3]                   | LDR W2,[X3]
------------------------------------------------------------
 STR W0,[X1] |                   STR W2,[X3] | 
             | LDR W0,[X1]                   | LDR W0,[X1]
 STR W2,[X3] |                   STR W0,[X1] | 
             | LDR W2,[X3]                   | LDR W2,[X3]
------------------------------------------------------------
 STR W0,[X1] |                   STR W2,[X3] | 
             | LDR W0,[X1]                   | LDR W0,[X1]
             |                               |
             | LDR W2,[X3]                   | LDR W2,[X3]
 STR W2,[X3] |                   STR W0,[X1] | 
------------------------------------------------------------
 STR W0,[X1] |                   STR W2,[X3] | 
             |                               |
 STR W2,[X3] |                   STR W0,[X1] | 
             |                               |
             | LDR W0,[X1]                   | LDR W0,[X1]
             |                               |
             | LDR W2,[X3]                   | LDR W2,[X3]
------------------------------------------------------------
             | LDR W2,[X3]                   | LDR W2,[X3]
             |                               |
             | LDR W0,[X1]                   | LDR W0,[X1]
 STR W0,[X1] |                   STR W2,[X3] | 
             |                               |
 STR W2,[X3] |                   STR W0,[X1] | 
------------------------------------------------------------
             | LDR W2,[X3]                   | LDR W2,[X3]
 STR W0,[X1] |                   STR W2,[X3] | 
             | LDR W0,[X1]                   | LDR W0,[X1]
 STR W2,[X3] |                   STR W0,[X1] | 
------------------------------------------------------------
             | LDR W2,[X3]                   | LDR W2,[X3]
 STR W0,[X1] |                   STR W2,[X3] | 
             |                               |
 STR W2,[X3] |                   STR W0,[X1] | 
             | LDR W0,[X1]                   | LDR W0,[X1]
------------------------------------------------------------
 STR W0,[X1] |                   STR W2,[X3] | 
             | LDR W2,[X3]                   | LDR W2,[X3]
 STR W2,[X3] |                   STR W0,[X1] | 
             | LDR W0,[X1]                   | LDR W0,[X1]
------------------------------------------------------------
 STR W0,[X1] |                   STR W2,[X3] | 
             | LDR W2,[X3]                   | LDR W2,[X3]
             |                               |
             | LDR W0,[X1]                   | LDR W0,[X1]
 STR W2,[X3] |                   STR W0,[X1] | 
------------------------------------------------------------
 STR W0,[X1] |                   STR W2,[X3] | 
             |                               |
 STR W2,[X3] |                   STR W0,[X1] | 
             | LDR W2,[X3]                   | LDR W2,[X3]
             |                               |
             | LDR W0,[X1]                   | LDR W0,[X1]
------------------------------------------------------------

应该是4*3*2的一个全排列，那么也就需要验证如上所有的情况和其他规则不冲突，以上所有
的输出结果都是合法的结果。可以看到人脑已经无法完成这样的工作，需要借助特性的工具
来完成这样的验证。

herd7/cat/Litmus使用的基本逻辑

ARM使用herd7+cat+Litmus的方式来验证内存模型的正确性，ARM的官网上有一个herd7+cat+Litmus
验证内存模型的使用方式，具体可以参考这里。

其中我们用cat文件描述ARM的内存模型定义，可以看到cat文件里(aarch64-v08.cat)描述的
定义基本上和ARMspec B2.3章节是一一对应的。

用Litmus的方式定义要测试的指令序列，Litmus还可以写执行结果相关的断言，Litmus可以
遍历所有可能结果，以此检测断言的正确与否。

而herd7以cat文件和Litmus测试用例为参数运行模型，得到Litmus测试用例在cat定义模型下
的所有输出结果，并画出输出结果对应的图形。

ARM提供了一个网站，可以形象的展示如上的整个流程。把上一小节的Litmus测试用例输入
左边的窗口，右边的窗口可以选择不同的模型，点击Run按钮运行模型：
herd7验证ARM内存模型

在下面的输出窗口可以到看到P1上X0/X2的各种可能输出的值，已经产生这些输出值时，指令
的可能执行顺序：
如上模型的部分输出

可以看到P1 X0/X2的可能结果为00/01/10/11，图上用ca(coherence after)/rf(read from)
标记了产生对应结果的指令实际执行序列。

我们具体看下00/01的可能执行序列。先看00，当P0写X在P1读X之后，P0写Y在P1读Y之后，
P1的X0/X2的结果值就是0/0; 再看01，当P1读X在P0写X之后，P0写Y在P1读Y之后，P1的X0/X2
的结果值就是0/1。我们看这个图时，总是从箭头被指向的一方读起，比如W[y]=1 <–ca– R[y]=0
就是P0写Y coherence after P1读Y。

可以看到如上的这种表示方法以一种简洁的方式综合了导致某种结果的指令实际执行序列，
也简洁的表示出了某种场景下多核间可能的所有指令执行序列的情况。

整套herd+cat+Litmus的测试方法中，cat里描述的是完整的模型定义，但Litmus中只能有有限
的测试用例，所有Litmus用例都通过，并不能证明cat中定义的模型内部没有逻辑冲突。对于
Litmus中的单个用例，测试可以输出单个用例在模型中运行的所有可能结果。