Rust 异步运行时的模块化响应性验证
Modular Responsiveness Verification of Rust Async Runtimes
浏览论文内容
中文总结 AI 辅助
针对Rust异步运行时，提出轻量级模块化证明技术，通过静态分析验证任务最终进展的活性属性，并应用于多个运行时关键组件。
中文摘要 AI 辅助
异步（async）编程是管理并发的一种流行范式。提供异步支持的语言通常有一个运行时来管理异步执行。这些运行时是关键基础设施，然而对它们的验证却很少受到关注。原因之一是用户最关心的异步运行时属性是活性属性：提交给运行时的任务最终会取得进展。对于既并发又高度优化的库来说，验证活性具有挑战性。我们提出了一种轻量级且模块化的证明技术，用于验证 Rust 异步运行时的最终进展保证。我们在基于 Rust 和 Rust 异步模型的简单语言背景下描述了这一技术。然后，我们将这一证明技术实现为一组针对 Rust 的静态分析，并使用这些分析来验证多个 Rust 异步运行时实现的关键组件的最终进展。
英文摘要
Asynchronous (async) programming is a popular paradigm for managing concurrency. Languages that provide async support typically have a runtime to manage asynchronous executions. These runtimes are critical infrastructure, yet verifying them has received little attention. One reason is that a property that users care most about from an async runtime is a liveness property: tasks submitted to the runtime eventually make progress. Verifying liveness is challenging for libraries that are both concurrent and highly optimized. We present a lightweight and modular proof technique for verifying eventual progression guarantees for Rust async runtimes. We describe this technique in the context of a simple language based on Rust and Rust's async model. We then realize this proof technique as a set of static analyses for Rust and use these to verify eventual progression of several key components of multiple Rust async runtime implementations.
发表机构
- University of British Columbia（不列颠哥伦比亚大学）
机构由 AI 辅助整理，请以论文原文为准。
