Are there any documents ( blogs, papers etc ) that describe the memory model of Rust? Things like memory ordering, memory guarantees etc.
Thanks.
1 Like
I think "memory model" is a different thing from the "aliasing model" that Stacked Borrows provides, although they are deeply intertwined. The RalfJung blog posts that talk most about the memory model specifically are Pointers Are Complicated, or: What's in a Byte? and "What The Hardware Does" is not What Your Program Does: Uninitialized Memory.
Within official, normative Rust documentation, I believe the closest thing we have to a memory model specification is std::sync::atomic - Rust stating that:
Each method takes an
Orderingwhich represents the strength of the memory barrier for that operation. These orderings are the same as the C++20 atomic orderings. For more information see the nomicon.
In other words, we're explicitly borrowing C++'s memory model. However, C++'s memory model has some famously huge specification issues, so...
That about covers it for introductory material that I'm aware of. At a much more formal level, the RustBelt project recently published RustBelt Meets Relaxed Memory which extends previous soundness proofs of Rust subsets to account for non-sequentially consistent atomic orderings. This paper and many of the other papers it references talk a lot about the formal logic tools and proof checking systems used to achieve the final proof, but the actual memory model being used here is the "Repaired C11" model introduced in an earlier RustBelt paper Repairing Sequential Consistency in C/C++11 (which goes into great detail about those "famously huge specification issues" in the regular C11 model). So I would say that paper is the closest thing we have today of a formal specification of "the memory model" of Rust, but of course it's completely non-normative for now.
6 Likes
There is also the work in the unsafe code guidelines
1 Like
This topic was automatically closed 90 days after the last reply. New replies are no longer allowed.