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

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

其中, C 为 Context 上下文的对应语法, k、u 分别处于内核与用户态, runtext 为切换内核状态的包装函数. C 表示调
用链, 包括调用链的来源, 去向以及路径和调用等. 值 Val 只包含最基本的数据类型和内核中基本的变量: 布尔值、
整数 z、内存中的位置 ℓ、函数 funrec、进程 id、设备名, 这里并没有表示内存块号, 而是选择将其用 ℓ 表示. 路径
Path 用来指向复合类型, n 为偏移量, 通过增加由 p 表达的指针 n 个内存单元来递增指针, context 用于管理上下文.
Instr 指令包含常见的算术操作, 内核常见的 syscall() 为系统调用总控函数, new 和 delete 为内存的分配和释放, *p
等表示从内存中加载操作以及赋值到内存等, newP 和 killP 表示进程的创建和删除. 函数体用于管理数据流和指令
流, 通过将指令串联来管理控制流, 支持递归的调用, newlft 和 endlft 为控制生命周期的辅助指令也称为“幽灵”指
令, 这是因为它们并不进行任何的操作并且也不存在于上下文中, 只存在于证明之中. call f(x) ret p 为递归调用的绑
定. x 是参数的绑定器列表, k 是返回延续的绑定器, 函数可以通过 call f(x) ret k 进行调用, 其中 x 是参数列表, k 是
函数返回时应调用的延续, 以此实现循环. 中断处理是专为内核验证定义的语法类型, 以处理内核中复杂的中断时
的处理时无需将中断分解, 以原子形式进行处理, 之所以这么做是由于某内核中中断涉及比较复杂的中断嵌套等情
况, 这样做可以简化验证, 更加聚焦于本方案的模块验证中, 但中断本身的验证仍需要进行, 在本文中不详细讨论.

3.2 操作语义

在 λ Rust 项目中定义了 λ Rust 核心语言来具体描述 Rust 的形式. 核心语言是一种具有指针运算和并发操作的 λ
演算, 我们在文中也采用类似的方式来定义但加入了操作系统中如上下文切换、系统调用等的操作, 选择 core 语
言的目的是将内核中一系列 unsafe 的操作更便捷的建模, 使推理更加简洁和清晰. core 语言模式如下.

z ∈ Z
o
Expr ∈ e ::= v |x |e 1 .e 2 |e 1 +e 2 |e 1 −e 2 |e 1 ⩽ e 2 |e 1 == e 2 |e(¯e) |∗ e
|e 1 : = o e 2 |CAS (e 0 ,e 1 ,e 2 ) |alloc(e) | free(e 1 ,e 2 ) |case e of ¯e |fork{e}
Val ∈ v ::= ∅ |ℓ |z |rec f(¯x) := e
Order ∈ o ::= sc |na |na ′
LockSt ∈ π ::= writing |reading n
Ctx ∋ K ::= K.e |v.K |K +e |v+ K |K −e |v− K |K ⩽ e |v ⩽ K |K == e |v == K
o
|K(¯e) |v( ¯ K ++[K]++¯e) |∗ K |K : = o e |v : = o K |CAS (K,e 1 ,e 2 ) |
CAS (v 0 ,K,e 2 ) |CAS (v 0 ,v 1 ,K) |alloc(K) |free(K,e 2 ) |free(e 1 ,K) |case K of ¯ e.
这里由于篇幅原因, 我们不对这里的细节做过多的介绍. 为了减少操作语义定义的工作量, 我们的操作语义的
定义也是基于 core 语言.
下面正式介绍我们基于 core 语言定义的操作语义, 但是注意我们在此处并没有用到在 λ Rust 中操作语义中所
有的语言构体, 而是选择了一部分, 并在部分语义中做了构造的适应于内核验证的操作语义拓展, 首先我们定义求
值评估操作语义.
定义 2. 求值评估操作语义.

[E-Z] [E-VAR]
⟨z,σ⟩ → ⟨z,σ⟩ ⟨x,σ⟩ → ⟨σ(x),σ⟩

′
′
⟨e 1 ,σ⟩ → ⟨e 1 ′,σ ⟩ ⟨e 2 ,σ⟩ → ⟨e 2 ′,σ ⟩
[E-ADD1] [E-ADD2]
′
′
⟨e 1 +e 2 ,σ⟩ → ⟨e 1 ′ +e 2 ,σ ⟩ ⟨v 1 +e 2 ,σ⟩ → ⟨v 1 +e 2 ′,σ ⟩

v 3 = v 1 +v 2
[E-ADD3]
⟨v 1 +v 2 ,σ⟩ → ⟨v 3 ,σ⟩

h ⊢ v 1 = v 2
[E-CAS ] [E-EQ]
′
⟨CAS (e 0 ,e 1 ,e 2 ),σ⟩ → ⟨v,σ ⟩ ⟨v 1 == v 2 ,h⟩ → ⟨1,h⟩

z 1 ⩽ z 2 z 1 > z 2
[E-LE] [E-GT]
⟨z 1 ⩽ z 2 ,σ⟩ → ⟨1,σ⟩ ⟨z 1 ⩽ z 2 ,σ⟩ → ⟨0,σ⟩

[E-ALLOC] [E-FREE]
⟨alloc(v),σ⟩ → ⟨p,σ[p 7→ v]⟩ ⟨free(p),σ⟩ → ⟨unit,σ−{p}⟩
[E-READ] [E-STORE]
⟨read(p),σ⟩ → ⟨σ(p),σ⟩ ⟨store(p,v),σ⟩ → ⟨unit,σ[p 7→ v]⟩
介绍操作语义之前, 我们先解释操作语义中符号的含义. ⟨⟩ 角括号用于表示一个有序对, 其中第 1 个元素表示