Skip to Main content Skip to Navigation
Conference papers

RustBelt Meets Relaxed Memory

Abstract : 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.
Complete list of metadata

Cited literature [28 references]  Display  Hide  Download
Contributor : Jacques-Henri Jourdan <>
Submitted on : Wednesday, November 13, 2019 - 10:36:50 AM
Last modification on : Saturday, March 27, 2021 - 3:32:37 AM
Long-term archiving on: : Friday, February 14, 2020 - 2:30:27 PM


Files produced by the author(s)




Hoang-Hai Dang, Jacques-Henri Jourdan, Jan-Oliver Kaiser, Derek Dreyer. RustBelt Meets Relaxed Memory. POPL, Jan 2020, New Orleans, United States. ⟨10.1145/3371101⟩. ⟨hal-02351793⟩



Record views


Files downloads