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

徐学政 等: RISC-V 内存一致性模型的同地址顺序一致性定理证明 3921

意同地址访存序列的构建抽象为确定有限状态自动机, 每个状态对应一种访存序列的模式, 通过对各个模式满足
SCPL 以及模式转换正确性的证明, 从而实现对任意访存序列满足 SCPL 的证明. 证明过程使用 Coq 进行了验证.
本研究是对 RVWMO 相关形式化方法的一个理论补充.

初始条件: x=0
线程 0 线程 1
a: r 1 =x; c: x=1;
b: r 2 =x; d: x=2;
最终结果: x=2; r 1 =2; r 2 =1
图 3 被 RVWMO 禁止的访存序模式 (x 为共享变量, r 1 和 r 2 为寄存器)

本文涉及的 Coq 脚本与实验数据已开源 (https://gitee.com/twohaha/scpl_proof).
本文第 1 节详细介绍 RVWMO 及 Litmus 测试. 第 2 节介绍 RVWMO 公理模型的相关形式化定义. 第 3 节介
绍 SCPL 及其形式化描述. 第 4 节介绍基于确定有限状态自动机的定理证明过程. 第 5 节应用 SCPL 进行案例分
析. 最后总结全文.

1 背景知识

1.1 RVWMO 概述
RVWMO 是一种宽松的内存一致性模型, 属于 RC 模型 [15] 的变种. RVWMO 规定并行程序执行生成的所有访
存原语遵循全局访存序, 顺序与保留程序序一致, 且符合加载值公理, 原子性公理和进度保证公理. 其中, 访存原语
指的是不可中断的读写操作, 是访存操作的基本单元, 在后文中统称为访存事件或操作. 全局访存序指的是所有硬
件线程的访存事件遵循一个共同的观测顺序, 这是由 RVWMO 满足多拷贝原子性 [17] 决定的. 相比之下, Power 内
存模型 [5] 不具备多拷贝原子性, 各个线程无法形成统一的全局访存序. 程序序 (program order, po) 指的是单个线程
执行的指令序列构成的顺序, 而保留程序序指的是程序序中必须维护保留的部分, 即不可乱序的部分. 例如, 具有
依赖关系的两条指令在执行时不可乱序. RVWMO 共定义了 13 条保留程序序规则. 这里给出前两条规则的非形
式化定义 (形式化定义见第 2.1 节). (1) 具有程序序的两个对同地址的访存操作, 后者是写操作. (2) 具有程序序的
两个对同地址的读操作, 二者的值来自不同的写操作, 且程序序在二者之间不存在对同地址的写操作.
RVWMO 定义了 3 条公理对模型进行补充. 加载值公理规定, 对于任意读操作 r, 其目标地址 x 的值来自在以
下所有操作中位于全局访存序末位的操作: (1) 全局访存序位于 r 之前的所有对 x 的写操作; (2) 程序序位于 r 之前
的所有对 x 的写操作. 图 4 给出了加载值公理的示意图, 其中所有操作的目标地址均相同, r 和 w 分别表示读操作
和写操作. 其中, r 的值可能来自全局访存序在其之前的写操作 (w 1 和 w 2 ) 以及程序序在其之前的写操作 (w 3 ), 将
以上 3 个写操作放在全局访存序中比较, r 的值最终来自排在末位的 w 3 . 值得注意的是, w 3 的全局访存序在 r 之
后, 这是因为 RVWMO 允许线程内的写和读乱序. X86/TSO 模型同样放松了该约束 [2,3] , 主要由微架构中的写缓冲
机制导致的. 原子性公理规定了成对出现的读保留 (load-reserved) 和条件写 (store-conditional) 的相关访存约束. 进
度保证公理规定了访存操作在有限时间内全局可见, 这要求我们在判定访存序合法性时考虑每一个访存操作. 本
文的证明主要利用了加载值公理.

w 3
r
w 1 w 2 w 3 w 4
全局访存序
w 5
程序序
图 4 加载值公理的示意图 (r 表示读操作, w 表示写操作)