add Stacked Borrows ToC to latest post and expand Stacked Borrows 1 post to hopefully...

diff --git a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md b/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
index 35bf7356f3779c8b2189b6684bd15df98cd21ce5..dbea705eefbe4d9e9518723e9433e9b58901a63d 100644 (file)
--- a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
+++ b/ralf/_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
 ---
 
 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!
 
 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.
+

 <!-- MORE -->
 
 What Stacked Borrows does is that it defines a semantics for Rust programs such
 <!-- MORE -->
 
 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
 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
 
 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/ralf/_posts/2019-04-30-stacked-borrows-2.md b/ralf/_posts/2019-04-30-stacked-borrows-2.md
index 8436bff12d820f64378f102163771c9e11172ea4..c57098c4aa7d977ac85fdc2b4be20d1542fce5b3 100644 (file)
--- a/ralf/_posts/2019-04-30-stacked-borrows-2.md
+++ b/ralf/_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
 
 <!-- MORE -->
 
 
 <!-- MORE -->
 

+## 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
 

-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 %}
 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 %}