Show first example in annotated form early

[web.git] / personal / _drafts / stacked-borrows-implementation.md

diff --git a/personal/_drafts/stacked-borrows-implementation.md b/personal/_drafts/stacked-borrows-implementation.md
index 029b0be87070a3297f852d3876caec53e3dba96d..17c8d27c4be198149808f696d5618ea7750650cf 100644 (file)
--- a/personal/_drafts/stacked-borrows-implementation.md
+++ b/personal/_drafts/stacked-borrows-implementation.md
@@ -112,8 +112,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 +252,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() {