From 70f20df6d28746ef5b042d950826243fb5d8dffa Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Mon, 18 Nov 2019 20:43:40 +0100 Subject: [PATCH] Stacked Borrows blog post --- .../2019-11-18-stacked-borrows-paper.md | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 ralf/_posts/2019-11-18-stacked-borrows-paper.md diff --git a/ralf/_posts/2019-11-18-stacked-borrows-paper.md b/ralf/_posts/2019-11-18-stacked-borrows-paper.md new file mode 100644 index 0000000..467b085 --- /dev/null +++ b/ralf/_posts/2019-11-18-stacked-borrows-paper.md @@ -0,0 +1,23 @@ +--- +title: "Stacked Borrows: An Aliasing Model for Rust (the paper)" +categories: research rust +--- + +I have [blogged]({% post_url 2019-05-21-stacked-borrows-2.1 %}) a [few]({% post_url 2019-04-30-stacked-borrows-2 %}) times before about [Stacked Borrows](https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md), my proposed aliasing model for Rust. +But I am a researcher, and what researchers (are expected to) do is write papers---so that's what we did for Stacked Borrows as well. +After a lot of work, I can now finally present to you our paper [Stacked Borrows: An Aliasing Model for Rust](https://plv.mpi-sws.org/rustbelt/stacked-borrows/) (thanks to open access, the paper is available under the CC-BY 4.0 license). + + + +If you have already read my blog posts, the paper does not say much you have not seen already. +However, the paper is the most coherent and most complete introduction to Stacked Borrows so far. +So if you were always confused by some aspect of Stacked Borrows, or if you have not read the previous blog posts, the paper is a great way to learn about Stacked Borrows. + +If there is nothing new, you may wonder what to us so long, then, and why we needed 4 people for that? +The answer is that my coauthor Hai, with some help from Jeehoon and me, took on the Herculean task of [formalizing Stacked Borrows in Coq](https://gitlab.mpi-sws.org/FP/stacked-borrows) and then formally verifying that some key optimizations are actually sound under that model. +Those proofs turned out to be more complex to carry out than we expected, but now I am sure that what I claimed about Stacked Borrows in previous posts is actually correct. +(In fact we were not able to complete the proof in time for the conference submission deadline, but lucky enough the reviewers were convinced enough by the informal description and the evaluation with Miri that they still accepted the paper.) + +Let me also use this opportunity to thank Mozilla and the Rust community for their help with this project. +This work would not have been possible without Mozilla hiring me for two internships, without all the great feedback that you all gave me in response to my blog posts, and without all the support that I got in implementing Stacked Borrows, testing the standard library and a growing number of external crates in Miri, and fixing Stacked Borrows errors as they came up. +Thank you all so much for working with me on this, this has been (and will hopefully continue to be) great fun. :-) -- 2.30.2