一句话：通过同步幽灵状态，将 RustBelt 的 Rust 语义健全性证明扩展到宽松内存，并发现 Arc 库中的数据竞争。
Rust 依靠所有权类型系统保证系统编程安全，RustBelt 此前用 Iris/Coq 分离逻辑为 Rust 的 λ 演算模型及若干使用 unsafe 的库建立了机器验证的语义健全性证明，但假设顺序一致内存。本文把 RustBelt 扩展到并发 Rust 库实际使用的宽松内存操作，核心挑战是在宽松内存下推理资源回收。为此提出同步幽灵状态（synchronized ghost state）这一逻辑构造，用于协调资源所有权与宽松内存行为。该扩展在验证过程中暴露了 Arc 库中的一个数据竞争。
The Rust programming language supports safe systems programming by means of a strong ownership-tracking type system. In their prior work on RustBelt, Jung et al. began the task of setting Rust’s safety claims on a more rigorous formal foundation. Specifically, they used Iris, a Coq-based separation logic framework, to build a machine-checked proof of semantic soundness for a λ-calculus model of Rust, as well as for a number of widely-used Rust libraries that internally employ unsafe language features. However, they also made the significant simplifying assumption that the language is sequentially consistent. In this paper, we adapt RustBelt to account for the relaxed-memory operations that concurrent Rust libraries actually use, in the process uncovering a data race in the Arc library. We focus on the most interesting technical problem: how to reason about resource reclamation under relaxed memory , using a logical construction we call synchronized ghost state .
@article{paperbot511,
title = {RustBelt meets relaxed memory},
author = {Hoang-Hai Dang and Jacques-Henri Jourdan and Jan-Oliver Kaiser and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371102}
}