Page 11 - 《软件学报》2025年第9期

3922 软件学报 2025 年第 36 卷第 9 期

[2]
对 RVWMO 的形式化建模方法主要分为操作模型 (operational model) 和公理模型 (axiomatic model) . 其中,
操作模型是通过对微架构 (乱序发射、写缓冲、流水线、存储层次、Cache 一致性协议等) 的抽象实现, 模拟出访
存行为从而得到合法的机器状态, 代表性工作是使用 Sail 语言 [17] 的 RMEM [18] . 公理模型直接以数学公理的形式约
束访存行为之间的顺序关系 (例如允许 Store-Load 乱序), 从而计算出合法的机器状态, 代表性工作有基于 Alloy [19]
[7]
和 Herd 的建模. 基于操作模型和公理模型, 可自动化地推理出并行程序的合法运行结果. 相比操作模型, 公理模
型并不对微架构建模, 方法更抽象, 描述更简单. 但操作模型更贴近微架构实现, 可根据微架构设计直接建模, 有利
于追踪微架构设计中的缺陷. 本文是基于公理模型在规范层面对 RVWMO 开展研究, 并不涉及微架构的实现.

1.2 Litmus 测试
本文将使用 Litmus 测试 [12] 对内存模型进行示例解释. Litmus 测试是一小段并行程序, 通常是某种访存序模式
的抽象, 用于测试或演示内存模型的某个性质. Litmus 测试通常包含各个线程执行的静态代码以及程序的初始状
态和最终状态. 图 3 中的例子本质上就是 Litmus 测试.
图 5(a) 和图 5(b) 分别给出了图 3 对应的 Litmus 标准语法描述和事件关系图示. 其中, 图 5(b) 是根据程序的
运行结果绘制的. 每个节点代表一个访存事件, 例如, c: W x=1 表示事件 c 向地址 x 写入 1, a: R x=2 表示事件 a 从
地址 x 读取 2. 每条边代表事件之间的关系 (详细定义见第 2.1 节), 例如 co 表示写事件的顺序, 由于 x 对应的最终
值为 2, 所以事件 d 发生在事件 c 之后; rf 为读取关系, 由于事件 a 读取的值为 2, 因此 a 的值读取自事件 d. 基于公
理模型的形式化验证工具 (如 Herd) 会基于模型公理对访存事件及其关系进行合法性检查, 进而判定程序的执行
结果是否满足对应的内存模型. 对于该例非法性的证明见命题 4.

RISC-V P0 P1
{
0:x5=0; 0:x7=0; 0:x6=x; /*初始状态*/
1:x5=1; 0:x7=2; 1:x6=x; a: R x=2 c: W x=1
} rf
P0 | P1 /*并行代码*/
lw x5,0(x6) | sw x5,0(x6) po co
lw x7,0(x6) | sw x7,0(x6) rf
exists /*最终状态*/
b: R x=1 d: W x=2
(x=2 /\ 0:x5=2 /\ 0:x7=1)
(a) 标准语法描述 (b) 事件关系图示
图 5 Litmus 测试标准语法描述与事件关系图示

2 RVWMO 公理模型

2.1 RVWMO 基础定义
本节定义了内存一致性公理模型 [7,10] 的基本关系及 RVWMO 的相关公理. 公理模型是内存模型的一种形式化
描述方法, 通过将内存模型表示成公理, 可对某个访存序的合法性进行判定. RISC-V 架构规范 [13] 的附录 A 中给出
了 RVWMO 的几种公理模型, 本节将介绍其中涉及 SCPL 证明的部分.
公理模型研究的基本元素是访存事件. 受分支选择以及多线程的执行顺序影响, 不同的程序执行可能产生不
同的访存事件. 公理模型是通过检查访存事件构成的二元关系是否符合所有公理从而对访存序的合法性进行判定
的. 在本文中, 使用符号≡表示等价, 使用符号≜ 解释定义.
定义 1 (访存事件). 访存事件由程序的执行产生, 定义为五元组 (id,proc,poidx,addr,kind). 其中, id 为该事件在
全局访存序中的索引, 不同的事件 id 不同; proc 为对应的线程号; poidx 为程序序索引, 同一线程的事件 poidx 不同;
addr 为访存地址; kind 为事件类型, 仅考虑读 (R) 和写 (W). 将访存事件 a 的 id 域表示为 id(a), proc 域表示为
proc(a), 以此类推; 将读 (写) 事件 a 表示为 a∈R (a∈W), 即 kind(a)=R(kind(a)=W).
定义 2. int (internal) 是一个二元关系集合, 表示两个事件位于同一线程. 若事件 a 和 b 满足 int 关系, 记为