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

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

(5) 由 (1)、(3) 以及 po 和 gmo 的非对称性, 与 (4) 推出矛盾.
引理 8. ∀a,b∈E, rfe(a,b)→gmo(a,b).
证明: 已知 rfe(a,b) 证明 gmo(a,b).
(1) 由 rfe(a,b) 的定义以及公理 4 可得: po(a,b)∨gmo(a,b).
(2) 由 rfe(a,b) 可得: ext(a,b), 又由 po 的定义可得: ¬po(a,b).
(3) 由 (1) 和 (2) 可证 gmo(a,b).
引理 9. ∀a, b∈E, fr(a,b)→gmo(a,b).
证明: 由定义 14 中的推论可知 fr(a,b)≜fri(a,b)∨fre(a,b), 将条件分两种情况证明.
(1) 若 fri(a,b) 成立, 由引理 6 可得: poloc(a,b), 又由 ppo1 的定义以及公理 2 可证 gmo(a,b).
(2) 若 fre(a,b) 成立:
(2.1) 由 fre 的定义以及 loc 的对称性可得: a≠b∧loc(b,a).
(2.2) 反证法. 假设¬gmo(a,b) 成立. 由 (2.1) 和 gmo 定义, 将¬gmo(a,b) 替换为 gmo(b,a).
(2.3) 由 fre 的定义可得: ∃x∈E, rf(x,a)∧co(x,b).
(2.4) 由 (2.3) 以及 co 的定义可得: gmo(x,b).
(2.5) 由 (2.3) 以及公理 4 可得: ∄y∈W, loc(y,a)∧gmo(x,y)∧(po(y,a)∨gmo(y,a).
(2.6) 由 (2.1)、(2.2) 和 (2.4) 可得: loc(b,a)∧gmo(x,b)∧gmo(b,a), 与 (2.5) 推出矛盾.
引理 10. ∀a,b,c∈E, fr(a,b)∧rf(b,c)→¬poloc(c,a).
证明: 已知 fr(a,b), rf(b,c) 证明¬poloc(c,a).
(1) 反证法. 假设 poloc(c,a) 成立.
由定义 14 中的推论可知: fr(a,b)≜fri(a,b)∨fre(a,b), rf(b,c)≜rfi(b,c)∨rfe(b,c), 将条件分 4 种情况证明.
(2) 若 fri(a,b)∧rfi(b,c) 成立:
(2.1) 由 fri(a,b) 和引理 6 可得: poloc(a,b).
(2.2) 由 rfi(b,c) 和引理 7 可得: poloc(b,c).
(2.3) 由 (2.1)、(2.2) 以及 poloc 的传递性可得: poloc(a,c).
(2.4) 由 poloc 的非对称性推出矛盾.
(3) 若 fri(a,b)∧rfe(b,c) 成立:
(3.1) 由定义 14 可得: int(a,b)∧ext(b,c).
(3.2) 由 (3.1) 以及 int 和 ext 定义可得: ext(a,c).
(3.3) 由 (3.2) 以及 po 的定义与 (1) 推出矛盾.
(4) 若 fre(a,b)∧rfi(b,c) 成立, 证明方法与 (3) 类似.
(5) 若 fre(a,b)∧rfe(b,c) 成立:
(5.1) 由引理 8 和引理 9 可得: gmo(a,b)∧gmo(b,c).
下面求证 ppo2(c,a). 由 ppo2 的定义, 我们需要证明 5 个条件. 其中, poloc(c,a), c∈R 和 a∈R 是已知的, 需要证
明∄x∈W, poloc(c,x)∧poloc(x,a) 以及∄x∈W, rf(x,c)∧rf(x,a).
(5.2) 证明∄x∈W, poloc(c,x)∧poloc(x,a). 反证法. 假设∃x∈W, poloc(c,x)∧poloc(x,a).
(5.2.1) 由 poloc(c,x), ppo1 的定义以及公理 2 可得: gmo(c,x).
(5.2.2) 由 fre(a,b) 以及 fr 的定义可得: ∃y∈E, rf(y,a)∧co(y,b).
(5.2.3) 由 (5.2.2) 以及 co 的定义可得: gmo(y,b).
(5.2.4) 由 (5.2.2) 以及公理 4 可得: ∄z∈W, loc(z,a)∧gmo(y,z)∧(po(z,a)∨gmo(z,a)).
(5.2.5) 由 poloc(x,a) 以及 poloc 的定义可得: po(x,a)∧loc(x,a).
(5.2.6) 由 (5.2.4) 和 (5.2.5) 可得: ¬gmo(y,x). 又由 gmo 的定义可得: gmo(x,y).
(5.2.7) 由 (5.2.1)、(5.2.3)、(5.2.6) 以及 gmo 的传递性可得: gmo(c,b).