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

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

rf(a,b)≡rfi(a,b)∨rfe(a,b), co(a,b)≡coi(a,b)∨coe(a,b), fr(a,b)≡fri(a,b)∨fre(a,b).
+
定义 15. 二元关系 r 的传递闭包记为 r , 满足:
+
+
+
+
∀a,b∈E, (a,b)∈r→(a,b)∈r ∧∀a,b,c∈E, (a,b)∈r ∧(b,c)∈r →(a,c)∈r .
+
定义 16. 二元关系 r 无环记为 acyclic(r), 满足: acyclic(r)≜∄x∈E, (x,x)∈r .
定义 17. 二元关系 perloc 满足: perloc≜poloc∪rf∪fr∪co. 若在长度为 n 的访存事件序列 s=e 0 ,e 1 ,e 2 ,…,e n– 中,
1
相邻事件满足 perloc 关系, 则记为 perloc(s). 例如, 当 s=a,b,c 时, perloc(s)≜perloc(a,b)∧perloc(b,c). 为方便叙述, 我
们在不引起歧义的上下文中, 也将 perloc(s) 直接写为 perloc(a,b,c).
定义 18 (执行实例). 一段 (并行) 程序的执行实例定义为四元组 (E,po,rf,co). 其中, E 为访存事件集合 (见定
义 1), po 为程序序关系集合 (见定义 6), rf 为读取关系集合 (见定义 7), co 为写事件的顺序关系集合 (见定义 8). 注
意, 执行实例对应的四元组是由程序执行确定的, 无须推导和证明 (另见第 1.2 节).

2.2 RVWMO 公理
本节定义了 4 条用于证明 SCPL 的公理, 均总结自 RISC-V 架构手册第 14.1 节 [13] .
公理 1 (read from). 每一个读事件的值必然来自某个写事件:
∀a∈R, ∃b∈W, rf(b,a).
若在全局访存序中, 某个读事件先于任何同地址的写事件, 表明该读事件的值来自内存初始值. 在模型检验
时, 此时会额外创建一个对应该内存初始值的写事件 [7,10] , 该公理依然适用.
公理 2 (单拷贝原子性). 一个读事件的值仅来自一个写事件:
∀a,b∈E, rf(a,b)→∄x∈E, x≠a∧rf(x,b).
显然, 我们可以得到∀a,b,c∈E, rf(a,c)∧rf(b,c)→a=b.
公理 3 (保留程序序). 两个事件的全局访存序与 ppo 关系顺序一致: ∀a,b∈E, ppo(a,b)→gmo(a,b).
公理 4 (加载值). 将第 1.1 节描述的加载值公理定义如下:
∀a,b∈E, rf(a,b)→(po(a,b)∨gmo(a,b))∧(∄x∈W, loc(x,b)∧gmo(a,x)∧(po(x,b)∨gmo(x,b)).

3 同地址顺序一致性定理

同地址顺序一致性 [7,10] 描述的是: 对于某个内存模型下的任意执行实例产生的访存事件集合, 其中存在的 rf,
fr 和 co 关系与 poloc 的顺序是一致的, 即不能成环, 表示为 acyclic(poloc∪rf∪fr∪co) 或 acyclic(perloc) (见定
义 17). SCPL 的另一个等价表述为: 对于任意的以 x 开始, 以 y 结束的访存事件序列, 若相邻的事件之间均存在
perloc 关系, 则 perloc(y,x) 必然不成立, 即不能成环 (见图 7). 本文中, 将 SCPL 作为主定理进行证明.

perloc

perloc perloc perloc
x y
图 7 基于访存事件序列的 SCPL 定理描述示意

定义 19 (SCPL). 假设 s 为某个长度为 n (n>0) 的访存事件序列, 即 s=e 0 ,e 1 ,e 2 ,…,e n–1 , 若序列满足 SCPL, 记为
SCPL(s) 且 SCPL(s)≜perloc(s)→¬perloc(e n–1 ,e 0 ).
主定理 (RVWMO 满足 SCPL). 假设 E 为在 RVWMO 下任意执行实例构成的访存事件集合, 由 E 包含的访
存事件构成的任意序列 s, 满足 SCPL(s). 第 4 节给出了定理的证明思路和步骤.
图 8 给出了违背 SCPL 的 5 种访存模式的 Litmus 示意图 [6,7] . 5 种模式中所有访存操作的目标地址均为 x. 例
如, coWW 模式描述的是同一线程存在先后两个写操作 a 和 b, x 的最终值来自前者 a 而不是 b. coRW1 模式描述
的是同一线程中的读操作 a 的值来自其之后的写操作 b. 这些例子都是反直觉的. 直观来看, 5 种模式中存在的
perloc 关系均成环, 利用 SCPL 定理可以轻易证明它们的非法性. 关于 SCPL 定理的应用另见第 5 节.