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

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

(1.3.5.3.2) 由 (1.3.5.3.1) 以及引理 11 可得: co(x,b). 由 co 定义进而得到: gmo(x,b).
(1.3.5.3.3) 由 (1.3.5.1)、(1.3.5.3.2) 以及 gmo 的传递性可得: gmo(c,b).
(1.3.5.3.4) 因 (1.3.2) 以及 gmo 的非对称性与 (1.3.5.3.3) 推出矛盾.
(1.3.5.4) 若 rfe(x,a) 成立:
(1.3.5.4.1) 由 rfe(x,a) 以及引理 8 可得: gmo(x,a).
(1.3.5.4.2) 根据 (1.3.5.4.1)、(1.3.1)、(1.3.2) 以及 gmo 的传递性可得: gmo(x,c).
(1.3.5.4.3) 根据 (1.3.5.4.2) 以及 gmo 的非对称性与 (1.3.5.1) 推出矛盾.
(1.3.6) 由 (1.3.3)、(1.3.5) 以及 co 定义可得: rf(x,a)∧co(x,c). 又由 fr 定义可得: fr(a,c). perloc(a,c) 得证.
(2) 若 fr(a,b) 成立:
(2.1) 由 fr 定义可得: ∃ x∈E, rf(x,a)∧co(x,b).
(2.2) 由假设中 co(b,c)、(2.1) 中 co(x,b) 以及 co 的传递性可得: co(x,c).
(2.3) 由 (2.1) 中 rf(x,a)、(2.2) 以及 fr 定义可得: fr(a,c). perloc(a,c) 得证.
定理 12 (RrW 转换). ∀a,b∈R, ∀c∈W, perloc(a,b,c)→perloc(a,c).
证明: 根据表 3, 将目标替换为: 已知 poloc(a,b), poloc(b,c)∨fr(b,c), 求证 perloc(a,c). 分两种情况证明.
(1) 若 poloc(b,c) 成立, 由 poloc 的传递性可证.
(2) 若 fr(b,c) 成立:
(2.1) 由 fr 的定义可知: ∃ x∈E, rf(x,b)∧co(x,c).
(2.2) 由公理 1 可知: ∃y∈W, rf(y,a).
(2.3) 由 rf(y,a)、rf(x,b)、poloc(a,b) 以及引理 13 可得: x=y∨co(y,x). 分两种情况证明.
(2.4) 若 x=y 成立, 由 rf(x,a)、co(x,c) 以及 fr 的定义可得: fr(a,c). 由 perloc 的定义, perloc(a,c) 得证.
(2.5) 若 co(y,x) 成立, 将 a、x、c 分别代入定理 11 的 a、b、c, 可得: perloc(a,c).
定理 13 (WrW 转换). ∀a,c∈W, ∀b∈R, perloc(a,b,c)→perloc(a,c).
证明: 已知 a∈W, b∈R, c∈W, perloc(a,b), perloc(b,c), 求证 perloc(a,c).
(1) 证明 a≠c. 由反证法可证: 若 a=c 成立, 可得: perloc(a,b), perloc(b,a), 由推论 2 可推出矛盾.
(2) 由 (1) 以及 co 定义可得: co(a,c)∨co(c,a).
为了证明 perloc(a,c), 只需证明¬co(c,a). 反证法. 假设 co(c,a) 成立, 由推论 4 推出矛盾.
定理 14 (WwW 转换). ∀a,b,c∈W, perloc(a,b,c)→perloc(a,c).
证明: 根据表 3 及引理 11, 将目标替换为: 已知 co(a,b)∧co(b,c), 求证 co(a,c). 由 co 的传递性可证.
推论 6 (RwrW 转换). ∀a,c∈R, ∀b,d∈W, perloc(a,b,c,d)→perloc(a,d).
证明: 已知 a∈R, b∈W, c∈R, d∈W, perloc(a,b), perloc(b,c), perloc(c,d), 求证 perloc(a,d).
(1) 将 b、c、d 分别代入定理 13 的 a、b、c, 可得: perloc(b,d).
(2) 将 a、b、d 分别代入定理 11 的 a、b、c, 可得: perloc(a,d).
推论 7 (RWRrR 转换). ∀a,c,d,e∈R, ∀b∈W, perloc(a,b,c,d,e)→perloc(a,b,c,e).
证明: 已知 a∈R, b∈W, c∈R, d∈R, e∈R, perloc(a,b,c,d,e), 求证 perloc(a,b,c,e). 只需证明 perloc(c,e). 可由将 c、d、
e 分别代入定理 10 的 a、b、c 证明.
推论 8 (WrrW 转换). ∀a,d∈W, ∀b,c∈R, perloc(a,b,c,d)→perloc(a,d).
证明: 已知 a∈W, b∈R, c∈R, d∈W, perloc(a,b,c,d), 求证 perloc(a,d).
(1) 将 b、c、d 分别代入定理 12 的 a、b、c, 可得: perloc(b,d).
(2) 将 a、b、d 分别代入定理 13 的 a、b、c, 可得: perloc(a,d).
推论 9 (RwrrW 转换). ∀a,c,d∈R, ∀b,e∈W, perloc(a,b,c,d,e)→perloc(a,e).
证明: 已知 a∈R, b∈W, c∈R, d∈R, e∈W, perloc(a,b,c,d,e), 求证 perloc(a,e).
(1) 将 b、c、d、e 分别代入推论 8 的 a、b、c、d, 可得: perloc(b,e).