X-Git-Url: https://git.ralfj.de/web.git/blobdiff_plain/287752b8fdeb0d834069982020895bbcd5a5bca7..69b83467e9dbf4b7a6076dfadda1ac25ebee0c4d:/ralf/_drafts/stacked-borrows-implementation.md

diff --git a/ralf/_drafts/stacked-borrows-implementation.md b/ralf/_drafts/stacked-borrows-implementation.md
index 029b0be..e5dae22 100644
--- a/ralf/_drafts/stacked-borrows-implementation.md
+++ b/ralf/_drafts/stacked-borrows-implementation.md
@@ -33,8 +33,10 @@ changed a bit, but also because I think I understand the model better myself
 now.
 
 Ready?  Let's get started.  I hope you brought some time, because this is a
-rather lengthy post.  If you are not interested in the details, you can skip
-right to section 4.  If you only want to know how to help, go to section 6.
+rather lengthy post.  If you are not interested in a detailed description of
+Stacked Borrows, you can skip most of this post and go right to
+[section 4](#4-differences-to-the-original-proposal).  If you only want to know
+how to help, jump to [section 6](#6-evaluation-and-how-you-can-help).
 
 ## 1 Enforcing Uniqueness
 
@@ -112,8 +114,35 @@ it is not at the top yet, we pop the stack until it is, which is easy.  Now the
 stack is just `[Uniq(0)]`.  Now we use `y` again and... blast!  Its tag is not
 on the stack.  We have undefined behavior.
 
-Well, actually that is good news, since that's what we wanted from the start!
-And since there is an implementation of the model in
+In case you got lost, here is the source code with comments indicating the tags
+and the stack of the one location that interests us:
+
+{% highlight rust %}
+fn demo0() {
+  let x = &mut 1u8; // tag: `Uniq(0)`
+  // stack: [Uniq(0)]
+
+  let y = &mut *x; // tag: `Uniq(1)`
+  // stack: [Uniq(0), Uniq(1)]
+
+  // Pop until `Uniq(1)`, the tag of `y`, is on top of the stack:
+  // Nothing changes.
+  *y = 5;
+  // stack: [Uniq(0), Uniq(1)]
+
+  // Pop until `Uniq(0)`, the tag of `x`, is on top of the stack:
+  // We pop `Uniq(1)`.
+  *x = 3;
+  // stack: [Uniq(0)]
+
+  // Pop until `Uniq(1)`, the tag of `y`, is on top of the stack:
+  // That is not possible, hence we have undefined behavior.
+  let _val = *y;
+}
+{% endhighlight %}
+
+Well, actually having undefined behavior here is good news, since that's what we
+wanted from the start!  And since there is an implementation of the model in
 [miri](https://github.com/solson/miri/), you can try this yourself: The amazing
 @shepmaster has integrated miri into the playground, so you can
 [put the example there](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=d15868687f79072688a0d0dd1e053721)
@@ -225,8 +254,8 @@ pub struct Stack {
 
 Let us now look at what happens when we execute our two example programs.  To
 this end, I will embed comments in the source code.  There is only one location
-of interest here, so whenever I talk about a "stack", it's the stack of that
-location.
+of interest here, so whenever I talk about a "stack", I am referring to the
+stack of that location.
 
 {% highlight rust %}
 fn demo1() {
@@ -410,8 +439,10 @@ references are copied: At the beginning of every function, all inputs of
 reference type get retagged.  On every assignment, if the assigned value is of
 reference type, it gets retagged.  Moreover, we do this even when the reference
 value is inside the field of a `struct` or `enum`, to make sure we really cover
-all references.  However, we do *not* descend recursively through references:
-Retagging a `&mut &mut u8` will only retag the *outer* reference.
+all references.  (This recursive descend is already implemented, but the
+implementation has not landed yet.)  However, we do *not* descend recursively
+through references: Retagging a `&mut &mut u8` will only retag the *outer*
+reference.
 
 Retagging is the *only* operation that generates fresh tags.  Taking a reference
 simply forwards the tag of the pointer we are basing this reference on.
@@ -755,7 +786,7 @@ implement in miri because dereferences can happen any time a path is evaluated,
 but it is nevertheless interesting and might be useful in a "lower-level MIR"
 that does not permit dereferences in paths.
 
-## Evaluation, and How You Can Help
+## 6 Evaluation, and How You Can Help
 
 I have implemented both the validity invariant and the model as described above
 in miri. This [uncovered](https://github.com/rust-lang/rust/issues/54908) two