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

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

P0 P0 P0 P1
a: W x=1 a: R x=1 a: R x=2 c: W x=2
rf
co poloc poloc rf poloc co
b: W x=2 b: W x=1 b: W x=1
coWW coRW1 coRW2

P0 P1 P0 P1
a: W x=1 c: W x=2 a: R x=1 c: W x=1
co rf
fr poloc rf poloc fr
rf
b: R x=2 b: R x=0
coWR coRR
图 8 SCPL 禁止的 5 种访存模式的 Litmus 示意图

4 基于确定有限状态自动机的 SCPL 定理证明

4.1 基于确定有限状态自动机的定理证明方法
为了证明 RVWMO 下的任意访存序列满足 SCPL, 本文引入确定有限状态自动机 (deterministic finite automata,
DFA) [20] 进行归纳证明. 该自动机可接收任意访存序列, 从而将问题分解为多个子问题逐一证明. 具体证明思路
如下.
(1) 将证明目标由任意访存事件的序列满足 SCPL 转为任意序列模式满足 SCPL.
(2) 引入确定有限状态自动机 M, 任意序列模式可被 M 接受.
(3) 证明自动机 M 中所有状态对应的序列模式均满足 SCPL.
(4) 证明某个序列模式满足 SCPL, 可由其在自动机 M 中对应的序列模式满足 SCPL 间接证明.
第 4.1.1–4.1.4 节将分别解释以上 4 个步骤.

4.1.1 序列模式
定义 20 (序列模式). 将访存事件序列中每个事件对应的类型构成的序列定义为该序列的模式. 对于任意长度
为 n (n>0) 的访存事件序列 s (s=e 0 ,e 1 ,e 2 ,…,e n–1 ), 其序列模式 K(s)=k 0 k 1 k 2 …k n–1 , 满足 k i =kind(e i ), 0≤i<n. 例如,
s=e 0 ,e 1 ,e 2 且 e 0 ∈R, e 1 ∈W, e 2 ∈R, 则 K(s)=RWR. 将定义 17 中 perloc 作用的访存事件序列扩展至序列模式. 对于任意
长度为 n (n>0) 的序列模式 X=k 0 k 1 k 2 …k n–1 , perloc(X)≜∀e 0 ∈k 0 , e 1 ∈k 1 , …, e n–1 ∈k n–1 , perloc(e 0 ,e 1 ,e 2 ,…,e n–1 ). 类似地, 将
定义 19 中 SCPL 的判定对象由访存序列扩展至序列模式. 对于任意长度为 n (n>0) 的序列模式 X=k 0 k 1 k 2 …k n–1 , SCPL(X)≜
∀e 0 ∈k 0 , e 1 ∈k 1 , …, e n–1 ∈k n–1 , perloc(e 0 ,e 1 ,e 2 ,…,e n–1 )→¬perloc(e n–1 ,e 0 ).
通过引入序列模式, 将证明目标由任意的访存事件序列满足 SCPL 转为其对应的序列模式满足 SCPL. 显然,
对于任意访存序列 s, SCPL(K(s))→SCPL(s).

4.1.2 确定有限状态自动机
定义 21 (DFA). 任意序列模式的构造被抽象为图 9 所示的确定有限状态自动机 M [20] , 由五元组 (Q,Σ,δ,q 0 ,F)
表示, 其中,
● Q 为有限状态集合, 共有 12 个, 记为 q 0 , q 1 , …, q 11 . 每个状态对应一种序列模式, 例如, q 2 代表序列模式 RR.
● Σ 为输入集合, 包含两种事件类型 R 和 W.
● δ 是状态转移函数, 类型为 Q×Σ →Q, 以当前状态和 Σ 中的某个符号或符号序列作为输入, 输出 Q 中的某个
*
状态.例如, δ(q 0 ,R)=q 1 , δ(q 1 ,ε)=q 1 , δ(q 0 ,RRW)=q 3 , δ(q 2 ,RRR)=q 2 . 由于 M 是确定有限状态自动机, ∀X∈Σ , ∀x∈Σ,
*
∀q∈Q, δ(q,Xx)=δ(δ(q,X),x).