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

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

Definition user_trap_invariant(t : Thread) (ctx : Context) : iProp Σ :=
⌜valid_context(ctx)⌝ ∧
⌜handle_user_trap(t, ctx) = Some(new_ctx)⌝ ∧
⌜t.state = Running⌝.
具体来说, 这些不变式可以帮助我们验证:
● 线程状态的变化是合法的: 线程在 Ready 状态时执行, 并且仅在合法的状态序列中转换.
● 中断状态的设置是正确的: 中断的启用和禁用与线程的状态保持一致, 不会导致在执行过程中发生意外中断.
● 异常处理流程的完整性: 在处理用户态陷入内核态的过程中, 能够正确处理异常, 并且在异常处理结束后,
系统和线程状态保持一致.
下一步为细化前置条件和后置条件并进行形式化建模, 建模过程中, 需要将涉及的 unsafe 代码块抽象出
GhostFunc 接口. 例如在此 API 中涉及的中断状态判断中大部分为 unsafe 代码, 此处涉及约 150 行 Coq 代码, 由于
篇幅原因, 展示其 GhostFunc 定义的一部分.

Definition ghost_handle_irq(s : State T) : iProp Σ :=
∃ (irq_state_before irq_state_after : IrqState)
(thread_before thread_after : Thread)
(context_before context_after : Context)
(ticks_before ticks_after : nat),
(* 保存当前的中断状态 *)
(⌜irq_state_before = s.irq_state⌝ ∗
arch_save_irq_state(irq_state_before) ∗
(* 中断状态保存 *)
Definition arch_save_irq_state(irq_state : IrqState) : iProp Σ :=
(* 假设我们有一个低级别的内存模型来表示中断状态的保存 *)
⌜irq_state = Disabled⌝ ∨ ⌜irq_state = Enabled⌝ ∗
own(irq_state 7→ saved_state).
(* 中断状态恢复 *)
Definition arch_restore_irq_state(irq_state : IrqState) : iProp Σ :=
(* 恢复之前保存的中断状态 *)
saved_state 7→ irq_state ∗
⌜irq_state = Disabled⌝ ∨ ⌜irq_state = Enabled⌝.
在验证过程中即可结合 ghost_handle_irq 的定义对 API 运行当前线程 run_current_thread 进行验证.

4.4 GhostFunc 验证方法分析
本节是本文的重点章节, 详细介绍了 GhostFunc 的形式化叙述, 并以例子介绍了部分 unsafe 代码的建模以及
在 GhostFunc 中的接口定义, 同时介绍了 safe 代码部分以及任务管理与调度模块框架的形式化验证过程.
我们的形式化模型通过一系列精确的定义, 捕捉了操作系统内核中关键操作的行为. 例如, 模型中定义的
run_current_thread 函数通过对线程状态和中断状态的不变式维护, 准确反映了实际代码中的操作逻辑. 具体来说,
模型中的 ghost_handle_irq 函数抽象了代码中涉及的 unsafe 中断处理操作, 并通过保持中断状态和线程状态的一
致性, 确保了代码在执行中的安全性.
这种模型与代码之间的紧密对应关系, 表明我们的形式化模型在捕捉系统行为方面是准确且有效的. 尽管没
有完成全部的精化验证, 我们可以通过模型与代码的结构和逻辑的相似性来推断它们之间的一致性.