发表机构
Technical University of Darmstadt（达姆施塔特工业大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文提出一种基于局部抽象、全局具体框架的模块化 Rust 形式化语义，支持异步特性与 Tokio，并证明调度器公平性及程序逻辑可靠性。
AI 中文摘要
对 Rust 程序进行形式化推理需要严格的形式化语义，尤其是在演绎验证和并发编程的背景下。我们基于最近的局部抽象、全局具体语义框架，为（接近）源代码级别的 Rust 的一个重要子集提出了一种模块化、灵活的语义，该框架将表达式的局部求值与其组合成具体迹相分离。该语义被扩展以建模 Rust 的异步编程特性以及 Rust 最流行的异步运行时 Tokio。基于我们更抽象的形式化，我们确立了 Tokio 调度器的公平性。此外，我们通过为 Rust 程序逻辑提供可靠性证明，展示了我们的语义在 Rust 演绎验证中的适用性。
英文摘要
Formally reasoning about Rust programs requires a rigorous formal semantics, especially in the context of deductive verification and concurrent programming. We present a modular, flexible semantics for a significant subset of (close to) source code level Rust, based on the recent locally abstract, globally concrete semantics framework, separating local evaluation of expressions from their composition into concrete traces. The semantics is extended to model Rust's asynchronous programming features and Rust's most popular async runtime, Tokio. Based on our more abstract formalization, we establish the fairness of Tokio's scheduler. Further, we show the applicability of our semantics to deductive verification of Rust by providing soundness proofs for a Rust program logic.
CommentsSubmitted to ACM TOPLAS
