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

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

此处的有关引用计数的一系列操作, 来自于我们之前在 GhostArc 中定义的一系列对外的接口, 所以即使此处
的建模抽象层级达不到控制引用计数的程度, 我们依然可以通过 GhostArc 进行这种细粒度更高的操作.
下面介绍此验证如何与 GhostArc 组合验证, 我们需要定义相关的接口, 在定义接口时, 我们着重维护 GhostArc
的引用计数以及所有权的属性等不变式. 不变式的形式化定义如下:

′ ′
∀γ,∀s,∃s , pre_clear_current_thread(s) → post_clear_current_thread(s, s )∧
own(γ,Excl (s ))∧inv(γ,valid_ref_count(s )∧valid_ownership(s )∧valid_locked(s )).
′
′
′
′
′
Arc<T> 在 safe 代码接口在 Coq 中的形式化如下.
Definition update_ref_count(s s' : State T) : iProp Σ :=
∃ rc, rc 7→ s.ref_count ∗
⌜s'.ref_count = s.ref_count + 1⌝ ∗
rc 7→ s'.ref_count.
Definition remove_ref_count(s s' : State T) : iProp Σ :=
∃ rc, rc 7→ s.ref_count ∗
⌜s'.ref_count = s.ref_count – 1⌝ ∗
rc 7→ s'.ref_count.

接口的定义在满足前后置条件后继而保证整个大系统的一致性, 即可组合完成.

4.3.3 模块内 API 验证
对于任务管理与调度模块, 对外暴露的 API 包括创建线程 (create thread API), 调度线程 (thread scheduler API),
运行当前线程 (run current thread API), 清除当前线程 (clear current thread API).
下面以运行当前线程为例介绍模块内 API 验证过程.
run_current_thread 函数的主要作用是从全局变量中获取当前线程并执行它, 直到线程状态不再是 Ready. 我
们需要验证以下关键点:
● 函数在当前线程为 Some(thread) 且状态为 Ready 时, 正确地执行该线程.
● 在执行线程时, 线程状态的变化符合预期.
● 函数在处理用户态陷入内核态的异常时, 不会导致不一致的状态或数据破坏.
基于此, 我们定义本 API 的不变式如下.
不变式 1: 线程的状态一致性.
Definition thread_state_invariant(t : Thread) : iProp Σ :=
⌜t.state = Ready⌝ ∨
⌜t.state = Running⌝ ∨
⌜t.state = Suspended⌝ ∨
⌜t.state = Exit⌝.
不变式 2: 系统中断状态一致性.

Definition irq_state_invariant(s : State T) (t : Thread) : iProp Σ :=
⌜t.state = Running → s.irq_state = Disabled⌝ ∧
⌜t.state = Suspended → s.irq_state = Enabled⌝ ∧
⌜t.state = Exit → s.irq_state = Enabled⌝.

不变式 3: 用户态陷入内核态的异常处理一致性.