From 1b16aa2e24a61ab700ea19ea9bc45993d87f83b2 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Wed, 1 May 2019 12:12:30 +0200 Subject: [PATCH] add Stacked Borrows ToC to latest post and expand Stacked Borrows 1 post to hopefully more clearly tell people to not read the original one --- ...18-11-16-stacked-borrows-implementation.md | 21 ++++++++++++------- .../_posts/2019-04-30-stacked-borrows-2.md | 11 +++++++++- 2 files changed, 23 insertions(+), 9 deletions(-) diff --git a/personal/_posts/2018-11-16-stacked-borrows-implementation.md b/personal/_posts/2018-11-16-stacked-borrows-implementation.md index 35bf735..dbea705 100644 --- a/personal/_posts/2018-11-16-stacked-borrows-implementation.md +++ b/personal/_posts/2018-11-16-stacked-borrows-implementation.md @@ -4,16 +4,21 @@ categories: internship rust forum: https://internals.rust-lang.org/t/stacked-borrows-implemented/8847 --- -Three months ago, I proposed [Stacked Borrows]({% post_url -2018-08-07-stacked-borrows %}) as a model for defining what kinds of aliasing -are allowed in Rust, and the idea of a [validity invariant]({% post_url -2018-08-22-two-kinds-of-invariants %}) that has to be maintained by all code at -all times. Since then I have been busy implementing both of these, and +Three months ago, I proposed Stacked Borrows as a model for defining what kinds +of aliasing are allowed in Rust, and the idea of a [validity invariant]({% +post_url 2018-08-22-two-kinds-of-invariants %}) that has to be maintained by all +code at all times. Since then I have been busy implementing both of these, and developed Stacked Borrows further in doing so. This post describes the latest version of Stacked Borrows, and reports my findings from the implementation phase: What worked, what did not, and what remains to be done. There will also be an opportunity for you to help the effort! +This post is a self-contained introduction to Stacked Borrows. Other than +historical curiosity and some comparison with my earlier work on +[Types as Contracts]({% post_url 2017-07-17-types-as-contracts %}) there is no +reason to read the [original post]({% post_url 2018-08-07-stacked-borrows %}) at +this point. + What Stacked Borrows does is that it defines a semantics for Rust programs such @@ -29,9 +34,9 @@ help us. We have to define a set of rules that makes sense even for unsafe code. I will explain these rules again in this post. The explanation is not going to -be the same as last time, not only because it changed a bit, but also because I -think I understand the model better myself now so I can do a better job -explaining it. +be the same as [last time]({% post_url 2018-08-07-stacked-borrows %}), not only +because it changed a bit, but also because I think I understand the model better +myself now so I can do a better job explaining it. Ready? Let's get started. I hope you brought some time, because this is a rather lengthy post. If you are not interested in a detailed description of diff --git a/personal/_posts/2019-04-30-stacked-borrows-2.md b/personal/_posts/2019-04-30-stacked-borrows-2.md index 8436bff..c57098c 100644 --- a/personal/_posts/2019-04-30-stacked-borrows-2.md +++ b/personal/_posts/2019-04-30-stacked-borrows-2.md @@ -10,9 +10,18 @@ I assume some familiarity with the prior version and will not explain everything +## Stacked Borrows: Table of Contents + +Before we start, let me give a brief overview over the posts on Stacked Borrows that I have written so far. +I didn't plan this out in advance, so things are a bit more messy than I would like. + +* [Stacked Borrows: An Aliasing Model For Rust]({% post_url 2018-08-07-stacked-borrows %}) is the first post of the series and describes my initial ideas of what Stacked Borrows would look like before I started implementing them. It might be interesting for some of the context it gives, but is largely superseded by the next post. +* [Stacked Borrows Implemented]({% post_url 2018-11-16-stacked-borrows-implementation %}) describes Stacked Borrows 1 and my experience implementing it. It is self-contained; I was not happy with some of my explanations in the original post so I decided to give it another shot. This is the best post to start with, if you are catching up. +* [Barriers and Two-phase Borrows in Stacked Borrows]({% post_url 2018-12-26-stacked-borrows-barriers %}) describes how I extended Stacked Borrows 1 with partial support for two-phase borrows and explains the idea of "barriers". You do not have to have read that post to understand Stacked Borrows 2, except for the parts that specifically refer to barriers and two-phase borrows. + ## The problem -The problem I wanted to solve was that the first version of Stacked Borrows only performed very little tracking of shared references. +The problem I wanted to solve with Stacked Borrows 2 was that the first version of Stacked Borrows only performed very little tracking of shared references. My thinking was, if the location is read-only anyway, then it does not harm to grant anyone read access. However, [as @arielby noted](https://github.com/rust-lang/unsafe-code-guidelines/issues/87), this leads to loss of optimization potential in cases where a function receives a mutable reference (which is supposed to have no aliases) and then creates a shared reference from it: {% highlight rust %} -- 2.30.2