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

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

(a,b)∈int 或 int(a,b), 满足: int(a,b)≜proc(a)=proc(b).
定义 3. ext (external) 是一个二元关系集合, 表示两个事件位于不同线程. 若事件 a 和 b 满足 ext 关系, 记为
(a,b)∈ext 或 ext(a,b), 满足: ext(a,b)≜proc(a)≠proc(b).
由 int 和 ext 的定义可得: ∀a,b∈E, int(a,b)∨ext(a,b).
定义 4. loc (same location) 是一个二元关系集合, 表示两个事件的访存地址相同. 若事件 a 和 b 满足 loc 关系,
可知 addr(a)=addr(b), 记为 (a,b)∈loc 或 loc(a,b). 显然, loc 具有传递性和对称性.
定义 5. gmo 是一个二元关系集合, 表示两个事件在全局访存序中的顺序关系. 若事件 a 和 b 满足 gmo 关系,
记为 (a,b)∈gmo 或 gmo(a,b), 满足: gmo(a,b)≜id(a)<id(b). 显然, gmo 是非对称的. 所有访存事件在 gmo 中构成全序,
即: ∀a,b∈E, a≠b→gmo(a,b)∨gmo(b,a).
定义 6. po 是一个二元关系集合, 表示同线程内两个事件在程序执行中的先后顺序. 若事件 a 和 b 满足 po 关
系, 记为 (a,b)∈po 或 po(a,b), 满足: po(a,b)≜int(a,b)∧poidx(a)<poidx(b). 显然, po 是传递的、非对称的. 同线程的访
存事件在 po 上构成全序, 即: ∀a,b∈E, a≠b∧int(a,b)→po(a,b)∨po(b,a).
定义 7. rf (read from) 是一个二元关系集合, 表示读事件的值来自某个写事件. 若事件 a 和 b 满足 rf 关系, 可
知: loc(a,b)∧a∈W∧b∈R, 记为 (a,b)∈rf 或 rf(a,b). 注意, 满足 loc(a,b)∧a∈W∧b∈R 的事件 a 和 b 并不一定满足 rf
关系.
定义 8. co (coherence order) 是一个二元关系集合, 表示对同地址的两个写事件的顺序关系. 若事件 a 和 b 满
足 co 关系, 记为 (a,b)∈co 或 co(a,b), 满足: co(a,b)≜loc(a,b)∧a∈W∧b∈W∧gmo(a,b). 显然, co 是传递的、非对称的.
由 gmo 的定义可知, 所有同地址的写事件在 co 上构成全序, 即: ∀a,b∈W, a≠b∧loc(a,b)→co(a,b)∨co(b,a).
定义 9. fr (from read) 是一个二元关系集合, 属于 rf 和 co 的派生关系. 若事件 a 和 b 满足 fr 关系, 记为
(a,b)∈fr 或 fr(a,b), 满足: fr(a,b)≜a∈R∧b∈W∧(∃x∈E, rf(x,a)∧co(x,b)). 图 6 给出了 fr 关系的示意图.

a: R x=1
rf fr
co
x: W x=1 b: W x=2
图 6 派生关系 fr 的示意图

定义 10. poloc (program order with the same location) 是一个二元关系集合, 属于 po 和 loc 的派生关系. 若事件
a 和 b 满足 poloc 关系, 记为 (a,b)∈poloc 或 poloc(a,b), 满足: poloc(a,b)≜po(a,b)∧loc(a,b). 显然, poloc 关系是传递
的和非对称的.
定义 11. ppo1 是一个二元关系集合, 表示符合保留程序序规则 1 的事件关系. 若事件 a 和 b 满足 ppo1 关系,
记为 (a,b)∈ppo1 或 ppo1(a,b), 满足: ppo1(a,b)≜poloc(a,b)∧b∈W.
定义 12. ppo2 是一个二元关系集合, 表示符合保留程序序规则 2 的事件关系. 若事件 a 和 b 满足 ppo2 关系,
记为 (a,b)∈ppo2 或 ppo2(a,b), 满足:
ppo2(a,b)≜poloc(a,b)∧a∈R∧b∈R∧(∄x∈W, poloc(a,x)∧poloc(x,b))∧(∄x∈W, rf(x,a)∧rf(x,b)).
定义 13. ppo 是一个二元关系集合, 表示保留程序序, 是程序序中不允许乱序的部分. RVWMO 定义了 13 条
保留程序序规则, 本文使用前两条, 记为 ppo1 和 ppo2. 其余 11 条规则与本文的定理证明无关. 若事件 a 和 b 满足
ppo 关系, 记为 (a,b)∈ppo 或 ppo(a,b), 满足: ppo(a,b)≜ppo1(a,b)∨ppo2(a,b).
定义 14. 部分关系根据是否位于同一线程划分为两个子关系:
rfi(a,b)≜rf(a,b)∧int(a,b), rfe(a,b)≜rf(a,b)∧ext(a,b);
coi(a,b)≜co(a,b)∧int(a,b), coe(a,b)≜co(a,b)∧ext(a,b);
fri(a,b)≜fr(a,b)∧int(a,b), fre(a,b)≜fr(a,b)∧ext(a,b).
进一步可得: