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

张卓若 等: 面向 Rust 语言的形式化验证方法研究综述 3611

Rust 进一步通过组合和默认实现来增强了 trait 的灵活性, Rust 高级 trait 绑定 (advanced trait bounds) 支持更复杂
的 trait 约束组合如多个 trait 的联合约束、特定生命周期的 trait 约束, 以及关联类型的 trait 约束. Rust 的 trait 与接
口相比其显著的优势在于其与类型系统的深度集成, 尤其是在所有权、借用和生命周期等 Rust 特有的安全机制
中. Rust 编译器会在编译时对 trait 的实现进行严格的类型检查, 确保所有权和借用规则不被违反, 这使得 Rust 的
trait 不仅是一种多态性实现的手段, 更是保证内存安全和并发安全的重要工具.

2.2.3 Rust 并发安全
Rust 在设计时充分考虑了并发编程的安全性和性能. 所有权系统是 Rust 并发编程的基础, 通过所有权、借用、
生命周期的设计 Rust 能够在编译时确保数据的一致性与安全性. Rust 的借用检查器在编译期确保只有一个可变
借用或多个不可变借用, 从而避免数据竞争. Rust 编译器通过自动实现 Send 和 Sync 这两个 traits 来帮助开发者确
保并发安全, Send 表示类型可以在线程间安全地传递, Sync 表示类型可以安全地在多个线程中同时访问. Rust 的
标准库中还提供了多种并发原语如线程 (std::thread)、消息传递 (std::sync::mpsc)、互斥锁 (std::sync::Mutex) 与读
写锁 (std::sync::RwLock).
Rust 最初的并发模型依赖于操作系统线程和标准库中基本的并发原语, 如 Mutex 和 mpsc 通道. 这种模型非
常强大, 但在高并发场景下, 尤其是需要大量线程或需要避免线程切换开销的场景下, 可能会遇到性能瓶颈. 为了
应对现代系统中广泛存在的 IO 绑定 (I/O-bound) 任务, Rust 引入了异步编程模型 (asynchronous programming),
Rust 的异步编程基于 Future trait, 它表示一个可能未完成的计算结果, 通过 poll 方法, Future 可以逐步推进, 直到
完成. 在 Rust 1.39 版本中, async/await 语法被稳定引入, 这使得异步代码的编写更加直观和易于理解. 在异步编程
中, Pin 和 Unpin 类型用于确保异步任务在内存中不会被移动, 从而防止数据竞争和内存安全问题. Rust 标准库本
身不提供异步运行时或执行器 (executor), 开发者通常使用第三方库 (如 tokio 或 async-std) 来执行异步任务, 这些
库提供了基于事件驱动的执行模型, 能够高效处理大量并发任务.
Rust 在并发编程中的安全性主要来自于其所有权系统和编译时的静态分析. 通过这些机制, Rust 在编译时防
止了许多潜在的并发错误, 如数据竞争和悬空指针, 提供了强大的静态安全性保证. 然而, 并发编程在涉及复杂的
生命周期、互斥锁的死锁或异步任务的协作等复杂的并发场景中仍然充满挑战, 需要开发者小心设计和实现以避
免逻辑错误. 形式化验证可以通过模型检查等技术在编译器的静态检查之外进一步确保并发程序的安全性和正确
性, 这对于构建高可靠性、高性能的并发系统尤为重要.

2.3 Rust 编译过程
Rustc 作为 Rust 编程语言的官方编译器, 承担着将 Rust 源代码转换为可执行程序或库文件的关键角色. 虽然
编译过程可能会因编译器的具体版本和所选优化等级而有所变化, 但其基本步骤可概括为如图 8 所示的编译过
程. Rust 源代码首先被解析成抽象语法树 (AST). 在这个阶段, 编译器首先进行词法分析, 将源代码文本分解成一
系列的词素 (tokens), 例如关键字、标识符、操作符等. 然后, 编译器进行语法分析, 根据 Rust 语言的语法规则, 将
这些 tokens 组合成 AST. AST 是源代码的树状结构表示, 反映了代码的语法结构. 该阶段中也会进行宏展开, 名称
解析等步骤. 接下来, AST 会被转换成 HIR (high-level intermediate representation), 这是一种对编译器更友好的
AST 表示法. 这个过程被称为降级 (lowering), 其中涉及大量的去糖 (desugar), 如 for 循环可能会被转换为迭代器
的调用, async 函数可能会被转换为状态机. 然后, 使用 HIR 进行类型推断 (自动检测表达式类型的过程)、trait 求
解 (将 impl 与 trait 的每个引用配对的过程) 和类型检查. 类型检查是将 HIR 中的类型 (代表用户编写的内容) 转换
为编译器使用的内部表示的过程. 之所以称为类型检查, 是因为这些信息用于验证程序中使用的类型的安全性、
正确性和一致性, 如检查变量的类型是否与预期一致, 以及确保类型转换不会引入错误. 在做类型检查后, 将 HIR
进一步降级为 MIR (mid-level intermediate representation). 该步骤会将函数中的语句及表达逻辑转换成控制流图
CFG, 精确捕捉程序的控制流和数据流, 以便对 Rust 的所有权和借用检查规则进行更深层次的优化. 在该过程中,
代码也会被单态化 (monomorphized), 即将泛型的类型参数替换为不同的具体类型, 复制相关泛型代码生成不同的
函数. 同时, 还在 MIR 层做一些优化以提高后面代码生成和编译速度. 在 MIR 上进行 Rust 的静态分析借用检查.