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

3502 软件学报 2025 年第 36 卷第 8 期

κ 在锁由某个线程持有的情况下结束, 那么这个线程就会
′
内容的借用, 在形式上我们将这两种情况统一起来, 如果
因此拥有这个锁原本含有的内容. 这就是为什么我们在介绍 Arc 的时候 κ 的下标为 full, 也就是完整的借用.
′
下面介绍 Mutex 的基本定义.
定义 7. Mutex 的基本属性定义.

Definition [[Mutex(τ)]].size := [[τ]].size+1.
Definition [[Mutex(τ)]].own(t, ¯v) := [[bool×τ]].own(t, ¯v)
Definition [[Mutex(τ)]].own(tid,vl) :=
∃rc l, vl = [#l] ∗
l 7→ 1(rc, [[τ]].own tid) ∗
rc 7→ {1}#1 ∗
□(rc 7→ {1}#1 ⇒ [[τ]].inv tid l).
Definition Mutex(τ).shr(κ, tid, l) := ∃rc, rc 7→ κ#1 ∗ [[τ]].shr κ tid l.
定义和前面 Arc 的定义一致, 但由于在内核中我们不会对 Mutex 类型保护的数据进行共享, 也不会涉及内部
可变性的运用, 所以在此处我们不同于 λ Rust 中的定义 shr 的属性控制其生命周期与堆叠借用等, 而是将其与一个
bool 值相对应, 锁的状态改变不涉及非原子操作.
下面介绍 Mutex 方法 new, lock, get_mut 方法定义.
定义 8. Mutex 包含的方法形式化定义.

[[Mutex(τ).new(w)]] := fn() → Mutex(τ)
[[[Mutex(τ).lock(l)]] := fn(k) → ∃v,l 7→ true∗[[τ]].own(t,v)
[[[Mutex(τ).get_mut(l)]] := fn() → ∃v,l 7→ true∗[[τ]].own(_).
由于 Mutex 的形式化定义相较于 Arc 的结构简单一些, 所以此处没有采用 Arc 的前后置条件的展示方法, 这
里操作的返回值即是后置条件. new 方法用于创建新 Mutex 实例, 并初始化内部的数据, 返回新的实例. lock 方法
用于尝试获取 Mutex 的锁, 并返回保护数据的引用, 这里表示尝试获取锁 l, 如果获取成功, 则返回一个线程 t 以及
被保护的数据 v 的所有权. get_mut 用于在不需要获取锁的情况下, 获取 Mutex 内部数据的可变引用, 涉及 Rust 中
的可变引用机制, 在内核中用处主要用于内核模块加载过程的初始数据结构的加载等, 因为在这个阶段, 尚未有其
他线程运行, 因此可以安全地使用 get_mut 方法对数据结构进行初始化.
我们分析 Mutex 在内核中所需保持的不变性. Mutex 在内核中主要用于确保并发访问的安全性, 保证在任何
时刻只有一个线程可以访问被保护的数据. 因此, 第 1 个不变性就是被保护的数据的访问权限需要保持一致. 其
次, Mutex 需要确保其锁的状态在任何时刻都准确反映当前的持有状态. 基于此, 我们可以定义出 Mutex 的不变式
Mutex_inv.
定义 9. Mutex 不变式定义.

Mutex_inv τ (l,t,v) := l 7→ true∗(t 7→ own(t,v))∨l 7→ false,
其中, l 表示 Mutex 的锁状态, t 表示线程, v 表示被保护的数据. 当锁被持有时, 锁的状态 l 为 true, 且存在一个线程
t 持有 Mutex, 并拥有被保护数据 v 的所有权; 当锁未被持有时, 锁的状态 l 为 false.

4.2 GhostFunc 形式化规范
在第 3 节, 我们完成了对于某内核中 unsafe 代码的形式化工作, 定义了一系列语义语法, 在本节我们将对 unsafe
代码与 safe 代码之间的接口定义形式化规范. 我们提出一种命名为 GhostFunc 的接口定义方法, 也就是为 unsafe
代码定义辅助的接口“函数”, 在 GhostFunc 中完成一次抽象规约, 规约后的接口可以与 safe 代码进行组合验证.

4.2.1 GhostFunc 定义
GhostFunc 取名来自于 GhostState, 用于辅助两个抽象层级不同的模块进行组合验证. 以 Arc 的 GhostFunc 定
义介绍在图 2 中介绍辅助验证流程, unsafe code module 和 safe code module 通过 GhostFunc 进行组合, 从而完成整
个系统的验证.