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

diff --git a/ralf/_drafts/stacked-borrows-implementation.md b/ralf/_drafts/stacked-borrows-implementation.md
index 029b0be..b4035fe 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() {
@@ -755,7 +784,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