Page 76 - 《软件学报》2025年第8期

何韬 等: GhostFunc: 一种针对 Rust 操作系统内核的验证方法 3499

一个表达式 (或操作), 第 2 个元素表示一个状态 (如内存状态). 在操作语义中, 这种表示方式用来描述程序在某个
.
状态下执行某个表达式的过程, 例如 ⟨expr,σ⟩ 表示在内存状态 σ 下执行操作 expr σ 表示内存状态, 通常是内存地
址到值的映射. p 为内存地址即指针. σ[p 7→ v] 表示更新内存状态, 将新分配的内存地址 p 映射到值. → 表示状态
转变. p ∈ dom(σ) 表示地址 p 存在于内存状态 σ 的域中. unit 表示释放操作的返回值, 通常为单位类型 (无意义值),
p h ⊢ v 1 = v 2 表示在内存状态
σ−{p} 表示从内存状态 σ 中移除地址 . h 下, v 1 等于 . 在判断操作语义中 1 表示 true,
v 2
0 表示 false.
E-Z 表示常量 z 在任何状态 σ 下都保持不变, 即不引起状态的改变, E-VAR 表示为变量 x 添加内存映射.
′ ′ ′ ′
E-ADD1 表示当 e 2 在状态 σ 下化简为 e 且状态变为 σ 时, 表达式 e 1 + e 2 化简为 e + e 2 , 状态也变为 σ . E-ADD2
1
2
跟 E-ADD1 类似, E-ADD3 表示当两个值 v 1 和 v 2 相加时, 结果为 , 且状态 σ 保持不变. E-ALLOC, E-FREE, E-
v 3
LOAD, E-STORE 这 4 个操作是有关内存方面的操作. E-ALLOC 表示当在内存状态 σ 下分配一个值 时, 如果 p
v
是一个新地址, 则结果状态为新地址 p 和更新后的内存状态 σ[p 7→ v]. E-FREE 表示当在内存状态 σ 下释放地址 p
时, 如果 p 存在于 σ 中, 则结果状态为单位类型和更新后的内存状态 (移除了 p). E-LOAD 表示当在内存状态 σ 下
从地址 p 读取值时, 如果 p 存在于 σ 中, 则结果状态为读取的值 σ(p) 和未改变的内存状态 σ. E-STORE 表示当在
v
内存状态 σ 下将值 写入地址 p 时, 如果 p 存在于 σ 中, 则结果状态为单位类型和更新后的内存状态 σ[p 7→ v].
下面介绍求值评估操作语义之外的拓展操作语义部分.
定义 3. 拓展操作语义.

′ ′
⟨e,σ⟩ → ⟨e ,σ ⟩
[O-IF]
′
′
⟨if e then s 1 else s 2 ,σ⟩ → ⟨if e then s 1 else s 2 ,σ ⟩
′
′
⟨e,σ⟩ → ⟨true,σ ⟩ ⟨e,σ⟩ → ⟨false,σ ⟩
[O-IF-TRUE] [O-IF-FALSE]
′
′
⟨if true then s 1 else s 2 ,σ⟩ → ⟨s 1 ,σ ⟩ ⟨if false then s 1 else s 2 ,σ⟩ → ⟨s 2 ,σ ⟩
′ ′
⟨e,σ⟩ → ⟨e ,σ ⟩
[O-WHILE]
′
⟨while e do s,σ⟩ → ⟨if e then (s; while e do s) else skip,σ ⟩
[O-CALL] [O-RET]
⟨call f(¯x) ret k,σ⟩ → ⟨let cont k(¯x) := F 1 in F 2 ,σ⟩ ⟨ret v,σ⟩ → ⟨v,σ⟩
[O-FORK] [O-LOCK]
⟨fork {e},σ⟩ → ⟨e,σ⟩ | ⟨e,σ⟩ ⟨lock(p),σ⟩ → ⟨unit,σ[p 7→ locked]⟩
h(ℓ) = (reading 0,v )
′
[O-CAS-SUCCESS]
⟨CAS (ℓ,v 1 ,v 2 ),h⟩ → ⟨1,h[ℓ ← (reading 0,v 2 )]⟩
′ ′
h(ℓ) = (reading 0,v )∗v , v 1
[O-CAS-FAIL]
⟨CAS (ℓ,v 1 ,v 2 ),h⟩ → ⟨0,h⟩
′
′
O-IF 当条件表达式 e 在状态 σ 下简化为 e 时, 条件语句 if e then s 1 else s 2 简化为 if e then s 1 else s 2 , 状态也变
′
为 e . O-IF-TRUE 表示在当条件表达式 e 在状态 σ 下化简为 true 时, 条件语句 if true then s 1 else s 2 化简为 s 1 同时
′
状态变为 e . O-IF-FALSE 和 O-WHILE 与 O-IF-TRUE 的条件判断类似.
call f(¯x) ret k 表示调用函数 f 并返回给 k. [O-CALL] 表示当调用函数 f 时, 将函数体 F 1 和 F 2 放入上下文中,
σ 下继续执行. [O-RET] 表示当执行返回操作时, 返回值 并且内存状态保持不变. [O-FORK] 表示
v
并在内存状态
当创建一个新的并发线程时, 结果状态包含两个线程各自执行表达式 e 的状态, 而内存状态 σ 被共享.
CAS 操作在并发环境下是原子的, 所以要确保 CAS 操作不能被打断. 我们定义 CAS (ℓ,v 1 ,v 2 ) 表示比较并交换
ℓ
′
操作, 将地址 ℓ 上的值从 v 1 更新为 , ′ h 中, 地址 的当前值为 v 并且没有读写
v 2 h(ℓ) = (reading 0,v ) 表示在内存状态
ℓ
锁. h[ℓ ← (reading 0,v 2 )] 表示更新内存状态, 将地址 的值设置为 . [O-CAS] 表示当执行比较并交换操作时, 如果
v 2
v 2 并返回 1 表示成功; 如果地址 上的值不为 , 则返回 0 表示失败, 内存状态
ℓ
地址 ℓ 上的值为 , 则将其更新为 v 1
v 1
保持不变.

4 任务管理与调度验证实例
本节将以任务管理模块验证为例, 以第 3 节和第 4 节为基础形式化任务管理模块中的 unsafe 代码部分, 并同