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

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

(2) 若 co(a,b)∧poloc(b,c)∧poloc(c,a) 成立:
(2.1) 由 poloc(b,c)∧poloc(c,a) 以及 poloc 的传递性可得: poloc(b,a).
(2.2) 由 co(a,b)、(2.1) 以及引理 12 可推得矛盾.
(3) 若 co(a,b)∧rf(b,c)∧poloc(c,a) 成立:
(3.1) 由 rf(b,c) 以及公理 4 可得: po(b,c)∨gmo(b,c).
(3.2) 由 poloc(c,a)、ppo1 的定义以及公理 2 可得: gmo(c,a).
(3.3) 由 co 的定义可得: gmo(a,b).
(3.4) 由 (3.2)、(3.3) 以及 gmo 的传递性可得: gmo(c,b). 又因 gmo 的非对称性可得: ¬gmo(b,c).
目前, 想要由 (3.1) 和 (3.4) 推出矛盾, 我们将求证目标变为¬po(b,c).
(3.5) 反证法. 假设 po(b,c) 成立. 又因 rf(b,c) 可知 loc(b,c), 可得: poloc(b,c).
(3.6) 由 (3.5)、poloc(c,a) 以及 poloc 的传递性可得: poloc(b,a).
(3.7) 由 co(a,b) 以及引理 12 的逆否命题可与 (3.6) 推出矛盾.
(4) 若 co(a,b)∧poloc(b,c)∧fr(c,a) 成立:
(4.1) 由 fr(c,a) 以及 fr 的定义可得: ∃x∈E, rf(x,c)∧co(x,a).
(4.2) 由 rf(x,c) 以及公理 4 可得: ∄y∈W, loc(y,c)∧gmo(x,y)∧(po(y,c)∨gmo(y,c).
将 b 代入 (4.2) 的 y, 将证明目标变为 loc(b,c)∧gmo(x,b)∧po(b,c), 其中, loc(b,c) 是显然的.
(4.3) 由 co(a,b)、(4.1) 中的 co(x,a)、co 的定义以及 gmo 的传递性可得: gmo(x,b).
(4.4) 由 poloc(b,c) 以及 poloc 的定义可得: po(b,c). 得证.
(5) 若 co(a,b)∧rf(b,c)∧fr(c,a) 成立:
(5.1) 由 fr(c,a) 以及 fr 的定义可得: ∃x∈E, rf(x,c)∧co(x,a).
(5.2) 由 (5.1)、rf(b,c) 以及公理 2 可得: x=b.
(5.3) 由 (5.1) 以及 (5.2) 可得: co(b,a). 由 co 的非对称性与 co(a,b) 推出矛盾.
推论 4 (WRW 模式). ∀a,c∈W, ∀b∈R, perloc(a,b,c)→¬perloc(c,a).
证明: 将 a、b、c 分别带入定理 9 中的 b、c、a 可证.
推论 5 (WWRR 模式). ∀a∈W, b∈W, c∈R, d∈R, perloc(a,b,c,d)→¬perloc(d,a).
证明: 已知 a∈W, b∈W, c∈R, d∈R, perloc(a,b,c,d), 求证¬perloc(d,a).
(1) 反证法. 假设 perloc(d,a) 成立.
(2) 将 d、a、b 分别代入定理 11 的 a、b、c, 可得: perloc(d,b).
(3) 将 d、b、c 分别代入定理 5 的 a、b、c, 可得: ¬perloc(c,d). 与条件中的 perloc(c,d) 矛盾.

4.3 序列模式转换正确性的证明
序列模式的转换共有 13 种情况需要证明 (见表 2). 其中 5 种情况处理的是长度为 3 的序列模式 (RRR、RWW、
RRW、WRW 和 WWW), 将被作为基础定理进行证明. 其余 8 种情况可由上述 5 个定理推导证明.
图 11 给出了序列模式转换的 5 个定理和 8 个推论的示意, 其中, 不同颜色的虚线箭头代表不同序列模式下产
生的 perloc 传递性, 黑色/灰色的 R 或 W 代表模式转换后保留/消除的部分. 图 11(b) 的推论可由一次或多次应用
图 11(a) 的定理进行证明.
定理 10 (RrR 转换). ∀a,b,c∈R, perloc(a,b,c)→perloc(a,c).
证明: 根据表 3, 将目标替换为: 已知 poloc(a,b), poloc(b,c), 求证 poloc(a,c). 由 poloc 的传递性可证.
引理 13. ∀a,b,c,d∈E, poloc(a,b)∧rf(c,a)∧rf(d,b)→c=d∨co(c,d).
证明: 已知 poloc(a,b), rf(c,a), rf(d,b), 求证 c=d∨co(c,d). 由排中律将 c=d∨c≠d 作为假设并分情况讨论. 若 c=d
成立, 证明是显然的. 这里只给出 c≠d 的证明过程. 由 c≠d 以及 co 的定义可知: co(c,d)∨co(d,c). 我们将证明目标转
换为¬co(d,c).