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

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

是利用了 perloc 关系的部分传递性. 因此, 证明序列模式转换的正确性实际是证明在某个序列模式下的 perloc 关
系的传递性. 关于 perloc 关系传递性的补充讨论见第 4.4 节.

perloc perloc

perloc perloc perloc perloc perloc
R R R R R R R R
perloc

图 10 基于访存事件序列等价转换的证明思路示意

表 2 给出了自动机 M 中需特别证明的模式转换, 即 perloc(X)→perloc(Y). 为了方便阅读, 我们在介绍定理和
推论时用大写字母表示序列模式转换前后保留的元素, 用小写字母表示转换后消除的元素. 例如, RwR 表示序列模
式 RWR 转换为 RR.

表 2 需要证明的序列模式转换

状态转移 转换前模式X 转换后模式Y 助记符 证明
RRR RR RrR 定理10
δ(q 2 ,R)=q 2
δ(q 3 ,W)=q 3 RWW RW RwW 定理11
RRW RW RrW 定理12
δ(q 2 ,W)=q 3
WRW WW WrW 定理13
δ(q 7 ,W)=q 9
WWW WW WwW 定理14
δ(q 9 ,W)=q 9
RWRW RW RwrW 推论6
δ(q 4 ,W)=q 3
δ(q 5 ,R)=q 5 RWRRR RWRR RWRrR 推论7
WRRW WW WrrW 推论8
δ(q 8 ,W)=q 9
RWRRW RW RwrrW 推论9
δ(q 5 ,W)=q 3
WRRR WRR WRrR 推论10
δ(q 8 ,R)=q 8
WWRW WW WwrW 推论11
δ(q 10 ,W)=q 9
δ(q 11 ,R)=q 10 WWRRR WWRR WWRrR 推论12
WWRRW WW WwrrW 推论13
δ(q 11 ,W)=q 9

虽然访存序列中相邻的两个事件满足 perloc 关系, 但根据事件类型不同可以得到更为具体的关系. 例如, 两个
满足 perloc 关系的读事件只可能存在 poloc 关系, 其他关系 (rf, fr 或 co) 根据定义至少需要一个写事件. 表 3 对此
类结论进行了总结. 证明是显然的.

表 3 根据事件类型可推断的具体 perloc 关系

a类型 b类型 若perloc(a,b), a和b可能满足的关系
R R poloc(a,b)
W W poloc(a,b)∨co(a,b)
R W poloc(a,b)∨fr(a,b)
W R poloc(a,b)∨rf(a,b)

4.2 基本序列模式满足 SCPL 的证明

定理 1 (ε 模式). 空访存事件序列满足 SCPL.
证明: 空序列对应的二元关系为空集, 证明是显然的.
定理 2 (R 模式). 仅包含一个读事件的访存事件序列满足 SCPL.
证明: 由于 perloc 包含的二元关系是非自反的, 证明是显然的.
引理 2. ∀a,b∈E, poloc(a,b)→¬poloc(b,a) .