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

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

内存一致性模型 [1,2] , 简称内存模型, 定义了并行程序在多核系统中的访存序约束, 是软硬件共同遵守的架构
[1]
[5]
[6]
规范, 经典的内存一致性模型包括 SC (sequential consistency) 、X86/TSO [3,4] 、Power 、ARM 等. 作为沟通多核
系统软硬件设计的规范, 学术界和工业界使用形式化方法 [5,7] 对内存模型进行描述, 以消除自然语言描述带来的歧
义. 公理模型 [7,8] 是最为经典的内存模型形式化描述方法之一, 其使用数学语言定义内存模型, 进而辅助软硬件的
形式化验证 [9] .
同地址顺序一致性 (sequential consistency per location, SCPL) [7,10] 是内存一致性公理模型的经典公理之一, 它
规定了多核系统中对于相同地址的所有访存操作遵循顺序一致性 [1] , X86/TSO、Power、ARM 等经典架构的内存
一致性模型均支持该公理 [7,8] . 此外, Linux Kernel 的内存模型 [11] 中也有类似的公理 (SC per variable). SCPL 直观地
描述了对于同地址访存操作的顺序约束, 简化了形式化方法在内存模型中的应用, 在芯片的内存一致性验证, 系统
软件和并行程序开发和验证等领域 [7,12] 发挥着重要作用.
RISC-V 是由加州大学伯克利分校提出的开源指令集规范 [13] , 具有精简、开放、模块化、高可定制的特点,
近年来受到了工业界和教育界的广泛关注, 已在物联网、云计算、人工智能、高性能计算等领域广泛应用 [14] .
RISC-V 内存模型 (RISC-V weak memory ordering, RVWMO) 是一种基于 Release Consistency (RC) [15] 的宽松内存
模型, 旨在为硬件设计提供灵活性的同时保证软件的易开发性. 在 RISC-V 架构规范 [13] 中, RVWMO 建立在访存原
语 (primitive memory operation) 基础上, 由全局访存序 (global memory order, gmo)、保留程序序 (preserved program
order, ppo) 以及模型公理构成 (见图 1). 其中, 模型公理包括加载值公理 (load value axiom)、原子性公理和进度保
证公理.

全局访存序 保留程序序 模型公理
( 多拷贝原子性) ( 13่Ќ਽ӱ྽྽ܿᄵ () 3条附加公理)
RVWMO
访存原语
( 不可中断的访存操作)

图 1 RVWMO 在 RISC-V 架构规范中的定义构成

RVWMO 并未将 SCPL 直接作为公理加入模型规范, 这对已有的内存模型验证工具和系统软件的开发带来了
挑战. 例如, RISC-V 架构规范 [13] 的附录 B.2 给出两种 RVWMO 的公理模型, 分别是基于 RVWMO 定义 (全局访存
序、13 条保留程序序规则和 3 条附加公理) 并不包含 SCPL 的公理模型以及另一种包含 SCPL 的公理模型. 规范
中指出, 后者是等价且更为高效的模型. 我们使用内存模型验证工具 Herd 分别加载两个模型, 对 RISC-V 的内存
[7]
模型测试套件 [16] 进行测试, 以验证架构规范中的结论. 实验表明, 后者对前者有超过 400% 的加速效果 (见图 2) 且
内存开销更小.

1 750 不包含 SCPL 的模型

1 500
累计时间 (s) 1 250 包含 SCPL 的模型
1 000
750
500
250
0
0 1 000 2 000 3 000 4 000 5 000 6 000 7 000
测试数目
图 2 Herd 基于两种 RVWMO 公理模型的验证效率对比

对于软件开发者, SCPL 是更为直观的公理, 将大大降低软件开发和验证的难度. 图 3 给出了 RVWMO 禁止发
生的访存序模式. 其中 x 为共享变量, r 1 和 r 2 为寄存器, 操作 a 和 b 为对 x 的读操作, c 和 d 为对 x 的写操作. 通过
运行结果可以看出, 读操作 a 和 b 的值分别来自写操作 d 和 c, 即两次读操作先读到新值, 再读到旧值, 这是反直
觉的. 该模式违背了 SCPL, 可直接判定其非法性. 如果不利用 SCPL 公理, 形式化验证工具和软件开发者需要利用
全局访存序、加载值公理以及保留程序序进行综合判断, 难度大大增加. 图 3 非法性的证明见命题 4.
本文面向 RVWMO, 基于指令集规范 [13] 中定义的公理和规则, 将 SCPL 作为定理进行了证明. 证明过程将任