5179e570ea74e0eebe6dbd7f760a750b98af3c51
[web.git] / personal / _drafts / stacked-borrows-implementation.md
1 ---
2 title: "Stacked Borrows Implemented"
3 categories: internship rust
4 ---
5
6 Three months ago, I proposed [Stacked Borrows]({% post_url
7 2018-08-07-stacked-borrows %}) as a model for defining what kinds of aliasing
8 are allowed in Rust, and the idea of a [validity invariant]({% post_url
9 2018-08-22-two-kinds-of-invariants %}) that has to be maintained by all code at
10 all times.  Since then I have been busy implementing both of these, and
11 developed Stacked Borrows further in doing so.  This post describes the latest
12 version of Stacked Borrows, and reports my findings from the implementation
13 phase: What worked, what did not, and what remains to be done.  There will also
14 be an opportunity for you to help the effort!
15
16 <!-- MORE -->
17
18 What Stacked Borrows does is that it defines a semantics for Rust programs such
19 that some things about references always hold true for every valid execution
20 (meaning executions where no [undefined behavior]({% post_url
21 2017-07-14-undefined-behavior %}) occurred): `&mut` references are unique (we
22 can rely on no accesses by other functions happening to the memory they point
23 to), and `&` references are read-only (we can rely on no writes happening to the
24 memory they point to, unless there is an `UnsafeCell`).  Usually we have the
25 borrow checker guarding us against such nefarious violations of reference type
26 guarantees, but alas, when we are writing unsafe code, the borrow checker cannot
27 help us.  We have to define a set of rules that makes sense even for unsafe
28 code.
29
30 I will try to explain at least parts of this model again in this post.  The
31 explanation is not going to be the same as last time, not only because it
32 changed a bit, but also because I think I understand the model better myself
33 now.
34
35 Ready?  Let's get started.  I hope you brought some time, because this is a
36 rather lengthy post.  If you are not interested in a detailed description of
37 Stacked Borrows, you can skip most of this post and go right to
38 [section 4](#4-differences-to-the-original-proposal).  If you only want to know
39 how to help, jump to [section 6](#6-evaluation-and-how-you-can-help).
40
41 ## 1 Enforcing Uniqueness
42
43 Let us first ignore the part about `&` references being read-only and focus on
44 uniqueness of mutable references.  Namely, we want to define our model in a way
45 that calling the following function will trigger undefined behavior:
46
47 {% highlight rust %}
48 fn demo0() {
49   let x = &mut 1u8;
50   let y = &mut *x;
51   *y = 5;
52   // Write through a pointer aliasing `y`
53   *x = 3;
54   // Use `y` again, asserting it is still exclusive
55   let _val = *y;
56 }
57 {% endhighlight %}
58
59 We want this function to be disallowed because between two uses of `y`, there is
60 a use of another pointer for the same location, violating the fact that `y`
61 should be unique.
62
63 Notice that this function does not compile, the borrow checker won't allow it.
64 That's great!  It is undefined behavior, after all.  But the entire point of
65 this exercise is to explain *why* we have undefined behavior here *without*
66 referring to the borrow checker, because we want to have rules that also work
67 for unsafe code.
68
69 To be able to do this, we have to pretend our machine has two thing which real
70 CPUs do not have.  This is an example of adding "shadow state" or "instrumented
71 state" to the "virtual machine" that we [use to specify Rust]({% post_url
72 2017-06-06-MIR-semantics %}).  This is not an uncommon approach, often times
73 source languages make distinctions that do not appear in the actual hardware.  A
74 related example is
75 [valgrind's memcheck](http://valgrind.org/docs/manual/mc-manual.html) which
76 keeps track of which memory is initialized to be able to detect memory errors:
77 During a normal execution, uninitialized memory looks just like all other
78 memory, but to figure out whether the program is violating C's memory rules, we
79 have to keep track of some extra state.
80
81 For stacked borrows, the extra state looks as follows:
82
83 1. For every pointer, we keep track of an extra "tag" that records when and how
84    this pointer was created.
85 2. For every location in memory, we keep track of a stack of tags, indicating
86    which tag a pointer must have to be allowed to access this location.
87
88 These exist separately, i.e., when a pointer is stored in memory, then we both
89 have a tag stored as part of this pointer value, and every byte occupied by the
90 pointer has a stack regulating access to this location.  Remember,
91 [a byte is more than a `u8`]({% post_url 2018-07-24-pointers-and-bytes %}).
92 Also these two do not interact, i.e., when loading a pointer from memory, we
93 just load the tag that was stored as part of this pointer.  The stack of a
94 location, and the tag of a pointer stored at some location, do not have any
95 effect on each other.
96
97 In our example, there are two pointers (`x` and `y`) and one location of
98 interest (the one both of these pointers point to, initialized with `1u8`).
99 When we initially create `x`, it gets tagged `Uniq(0)` to indicate that it is a
100 unique reference, and the location's stack has `Uniq(0)` at its top to indicate
101 that this is the latest reference allowed to access said location.  When we
102 create `y`, it gets a new tag, `Uniq(1)`, so that we can distinguish it from
103 `x`.  We also push `Uniq(1)` onto the stack, indicating not only that `Uniq(1)`
104 is the latest reference allow to access, but also that it is "derived from"
105 `Uniq(0)`: The tags higher up in the stack are descendants of the ones further
106 down.
107
108 So we have: `x` tagged `Uniq(0)`, `y` tagged `Uniq(1)`, and the stack contains
109 `[Uniq(0), Uniq(1)]`. (Top of the stack is on the right.)
110
111 When we use `y` to access the location, we make sure its tag is at the top of
112 the stack: Check, no problem here.  When we use `x`, we do the same thing: Since
113 it is not at the top yet, we pop the stack until it is, which is easy.  Now the
114 stack is just `[Uniq(0)]`.  Now we use `y` again and... blast!  Its tag is not
115 on the stack.  We have undefined behavior.
116
117 In case you got lost, here is the source code with comments indicating the tags
118 and the stack of the one location that interests us:
119
120 {% highlight rust %}
121 fn demo0() {
122   let x = &mut 1u8; // tag: `Uniq(0)`
123   // stack: [Uniq(0)]
124
125   let y = &mut *x; // tag: `Uniq(1)`
126   // stack: [Uniq(0), Uniq(1)]
127
128   // Pop until `Uniq(1)`, the tag of `y`, is on top of the stack:
129   // Nothing changes.
130   *y = 5;
131   // stack: [Uniq(0), Uniq(1)]
132
133   // Pop until `Uniq(0)`, the tag of `x`, is on top of the stack:
134   // We pop `Uniq(1)`.
135   *x = 3;
136   // stack: [Uniq(0)]
137
138   // Pop until `Uniq(1)`, the tag of `y`, is on top of the stack:
139   // That is not possible, hence we have undefined behavior.
140   let _val = *y;
141 }
142 {% endhighlight %}
143
144 Well, actually having undefined behavior here is good news, since that's what we
145 wanted from the start!  And since there is an implementation of the model in
146 [miri](https://github.com/solson/miri/), you can try this yourself: The amazing
147 @shepmaster has integrated miri into the playground, so you can
148 [put the example there](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=d15868687f79072688a0d0dd1e053721)
149 (adjusting it slightly to circumvent the borrow checker), then select "Tools -
150 Miri" and it will complain (together with a rather unreadable backtrace, we sure
151 have to improve that one):
152
153 ```
154  --> src/main.rs:6:14
155   |
156 6 |   let _val = *y;
157   |              ^^ Encountered reference with non-reactivatable tag: Borrow-to-reactivate Uniq(1245) does not exist on the stack
158   |
159 ```
160
161 ## 2 Enabling Sharing
162
163 If we just had unique pointers, Rust would be a rather dull language.  Lucky
164 enough, there are also two ways to have shared access to a location: Through
165 shared references (safely), and through raw pointers (unsafely).  Moreover,
166 shared references *sometimes* (but not when they point to an `UnsafeCell`)
167 assert an additional guarantee: Their destination is read-only.
168
169 For example, we want the following code to be allowed -- not least because this
170 is actually safe code accepted by the borrow checker, so we better make sure
171 this is not undefined behavior:
172
173 {% highlight rust %}
174 fn demo1() {
175   let x = &mut 1u8;
176   // Create several shared references, and we can also still read from `x`
177   let y1 = &*x;
178   let _val = *x;
179   let y2 = &*x;
180   let _val = *y1;
181   let _val = *y2;
182 }
183 {% endhighlight %}
184
185 However, the following code is *not* okay:
186
187 {% highlight rust %}
188 fn demo2() {
189   let x = &mut 1u8;
190   let y = &*x;
191   // Create raw reference aliasing `y` and write through it
192   let z = x as *const u8 as *mut u8;
193   unsafe { *z = 3; }
194   // Use `y` again, asserting it still points to the same value
195   let _val = *y;
196 }
197 {% endhighlight %}
198
199 If you
200 [try this in miri](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=1bc8c2f432941d02246fea0808e2e4f4),
201 you will see it complain:
202
203 ```
204  --> src/main.rs:6:14
205   |
206 6 |   let _val = *y;
207   |              ^^ Location is not frozen long enough
208   |
209 ```
210
211 How is it doing that, and what is a "frozen" location?
212
213 To explain this, we have to extend the "shadow state" of our "virtual machine" a
214 bit.  First of all, we introduce a new kind of tag that a pointer can carry: A
215 *shared* tag.  The following Rust type describes the possible tags of a pointer:
216
217 {% highlight rust %}
218 pub type Timestamp = u64;
219 pub enum Borrow {
220     Uniq(Timestamp),
221     Shr(Option<Timestamp>),
222 }
223 {% endhighlight %}
224
225 You can think of the timestamp as a unique ID, but as we will see, for shared
226 references, it is also important to be able to determine which of these IDs was
227 created first.  The timestamp is optional in the shared tag because that tag is
228 also used by raw pointers, and for raw pointers, we are often not able to track
229 when and how they are created (for example, when raw pointers are converted to
230 integers and back).
231
232 We use a separate type for the items on our stack, because there we do not need
233 a timestamp for shared pointers:
234
235 {% highlight rust %}
236 pub enum BorStackItem {
237     Uniq(Timestamp),
238     Shr,
239 }
240 {% endhighlight %}
241
242 And finally, a "borrow stack" consists of a stack of `BorStackItem`, together
243 with an indication of whether the stack (and the location it governs) is
244 currently *frozen*, meaning it may only be read, not written:
245
246 {% highlight rust %}
247 pub struct Stack {
248     borrows: Vec<BorStackItem>, // used as a stack; never empty
249     frozen_since: Option<Timestamp>, // virtual frozen "item" on top of the stack
250 }
251 {% endhighlight %}
252
253 ### 2.1 Executing the Examples
254
255 Let us now look at what happens when we execute our two example programs.  To
256 this end, I will embed comments in the source code.  There is only one location
257 of interest here, so whenever I talk about a "stack", I am referring to the
258 stack of that location.
259
260 {% highlight rust %}
261 fn demo1() {
262   let x = &mut 1u8; // tag: `Uniq(0)`
263   // stack: [Uniq(0)]; not frozen
264   
265   let y1 = &*x; // tag: `Shr(Some(1))`
266   // stack: [Uniq(0), Shr]; frozen since 1
267
268   // Access through `x`.  We first check whether its tag `Uniq(0)` is in the
269   // stack (it is).  Next, we make sure that either our item *or* `Shr` is on
270   // top *or* the location is frozen.  The latter is the case, so we go on.
271   let _val = *x;
272   // stack: [Uniq(0), Shr]; frozen since 1
273
274   // This is not an access, but we still dereference `x`, so we do the same
275   // actions as on a read.  Just like in the previous line, nothing happens.
276   let y2 = &*x; // tag: `Shr(Some(2))`
277   // stack: [Uniq(0), Shr]; frozen since 1
278
279   // Access through `y1`.  Since the shared tag has a timestamp (1) and the type
280   // (`u8`) does not allow interior mutability (no `UnsafeCell`), we check that
281   // the location is frozen since (at least) that timestamp.  It is.
282   let _val = *y1;
283   // stack: [Uniq(0), Shr]; frozen since 1
284
285   // Same as with `y2`: The location is frozen at least since 2 (actually, it
286   // is frozen since 1), so we are good.
287   let _val = *y2;
288   // stack: [Uniq(0), Shr]; frozen since 1
289 }
290 {% endhighlight %}
291
292 This example demonstrates a few new aspects.  First of all, there are actually
293 two operations that perform tag-related checks in this model (so far):
294 Dereferencing a pointer (whether you have a `*`, also implicitly), and actual
295 memory accesses.  Operations like `&*x` are an example of operations that
296 dereference a pointer without accessing memory.  Secondly, *reading* through a
297 mutable reference is actually okay *even when that reference is not exclusive*.
298 It is only *writing* through a mutable reference that "re-asserts" its
299 exclusivity.  I will come back to these points later, but let us first go
300 through another example.
301
302 {% highlight rust %}
303 fn demo2() {
304   let x = &mut 1u8; // tag: `Uniq(0)`
305   // stack: [Uniq(0)]; not frozen
306   
307   let y = &*x; // tag: `Shr(Some(1))`
308   // stack: [Uniq(0), Shr]; frozen since 1
309
310   // The `x` here really is a `&*x`, but we have already seen above what
311   // happens: `Uniq(0)` must be in the stack, but we leave it unchanged.
312   let z = x as *const u8 as *mut u8; // tag irrelevant because raw
313   // stack: [Uniq(0), Shr]; frozen since 1
314
315   // A write access through a raw pointer: Unfreeze the location and make sure
316   // that `Shr` is at the top of the stack.
317   unsafe { *z = 3; }
318   // stack: [Uniq(0), Shr]; not frozen
319
320   // Access through `y`.  There is a timestamp in the `Shr` tag, and the type
321   // `u8` does not allow interior mutability, but the location is not frozen.
322   // This is undefined behavior.
323   let _val = *y;
324 }
325 {% endhighlight %}
326
327 ### 2.2 Dereferencing a Pointer
328
329 As we have seen, we consider the tag of a pointer already when dereferencing it,
330 before any memory access happens.  The operation on a dereference never mutates
331 the stack, but it performs some basic checks that might declare the program UB.
332 The reason for this is twofold: First of all, I think we should require some
333 basic validity for pointers that are dereferenced even when they do not access
334 memory. Secondly, there is the practical concern for the implementation in miri:
335 When we dereference a pointer, we are guaranteed to have type information
336 available (crucial for things that depend on the presence of an `UnsafeCell`),
337 whereas having type information on every memory access would be quite hard to
338 achieve in miri.
339
340 Notice that on a dereference, we have *both* a tag at the pointer *and* the type
341 of a pointer, and the two might not agree which we do not always want to rule
342 out (we might have raw or shared pointers with a unique tag, for example).
343
344 The following checks are done on every pointer dereference:
345
346 1. If this is a raw pointer, do nothing and reset the tag used for the access to
347    `Shr(None)`.  Raw accesses are checked as little as possible.
348 2. If this is a unique reference and the tag is `Shr(Some(_))`, that's an error.
349 3. If the tag is `Uniq`, make sure there is a matching `Uniq` item with the same
350    ID on the stack of every location this reference points to (the size is
351    determine with `size_of_val`).
352 4. If the tag is `Shr(None)`, make sure that either the location is frozen or
353    else there is a `Shr` item on the stack of every location.
354 5. If the tag is `Shr(Some(t))`, then the check depends on whether a location is
355    inside an `UnsafeCell` or not, according to the type of the reference.
356     - Locations outside `UnsafeCell` must have `frozen_since` set to `t` or an
357       older timestamp.
358     - `UnsafeCell` locations must either be frozen or else have a `Shr` item in
359       their stack (same check as if the tag had no timestamp).
360
361 ### 2.3 Accessing Memory
362
363 On an actual memory access, we know the tag of the pointer that was used to
364 access (unless it was a raw pointer, in which case the tag we see is
365 `Shr(None)`), and we know whether we are reading from or writing to the current
366 location.  We perform the following operations:
367
368 1. If the location is frozen and this is a read access, nothing happens. (even
369    if the tag is `Uniq`).
370 2. Unfreeze the location (set `frozen_since` to `None`).
371 3. Pop the stack until the top item matches the tag of the pointer.
372     - A `Uniq` item matches a `Uniq` tag with the same ID.
373     - A `Shr` item matches any `Shr` tag (with or without timestamp).
374     - When we are reading, a `Shr` item matches a `Uniq` tag.
375
376     If, popping the stack, we make it empty, then we have undefined behavior.
377
378 To understand these rules better, try going back through the three examples we
379 have seen so far and applying these rules for dereferencing pointers and
380 accessing memory to understand how they interact.
381
382 The only thing that is subtle and potentially surprising here is that we make a
383 `Uniq` tag match a `Shr` item and also accept `Uniq` reads on frozen locations.
384 This is required to make `demo1` work: Rust permits read accesses through
385 mutable references even when they are not currently actually unique.  Our model
386 hence has to do the same.
387
388 ## 3 Retagging and Creating Raw Pointers
389
390 We have talked quite a bit about what happens when we *use* a pointer.  It is
391 time we take a close look at *how pointers are created*.  However, before we go
392 there, I would like us to consider one more example:
393
394 {% highlight rust %}
395 fn demo3(x: &mut u8) -> u8 {
396     some_function();
397     *x
398 }
399 {% endhighlight %}
400
401 The question is: Can we move the load of `x` to before the function call?
402 Remember that the entire point of Stacked Borrows is to enforce a certain
403 discipline when using references, in particular, to enforce uniqueness of
404 mutable references.  So we should hope that the answer to that question is "yes"
405 (and that, in turns, is good because we might use it for optimizations).
406 Unfortunately, things are not so easy.
407
408 The uniqueness of mutable references entirely rests on the fact that the pointer
409 has a unique tag: If our tag is at the top of the stack (and the location is not
410 frozen), then any access with another tag will pop our item from the stack (or
411 cause undefined behavior).  This is ensured by the memory access checks (and the
412 exception for matching `Uniq` tags with `Shr` items on reads does not affect
413 this property).  Hence, if our tag is *still* on the stack after some other
414 accesses happened (and we know it is still on the stack every time we
415 dereference the pointer, as per the dereference checks described above), we know
416 that no access through a pointer with a different tag can have happened.
417
418 ### 3.1 Guaranteed Freshness
419
420 However, what if `some_function` has an exact copy of `x`?  We got `x` from our
421 caller (whom we do not trust), maybe they used that same tag for another
422 reference (copied it with `transmute_copy` or so) and gave that to
423 `some_function`?  There is a simple way we can circumvent this concern: Generate
424 a new tag for `x`.  If *we* generate the tag (and we know generation never emits
425 the same tag twice, which is easy), we can be sure this tag is not used for any
426 other reference.  So let us make this explicit by putting a `Retag` instruction
427 into the code where we generate new tags:
428
429 {% highlight rust %}
430 fn demo3(x: &mut u8) -> u8 {
431     Retag(x);
432     some_function();
433     *x
434 }
435 {% endhighlight %}
436
437 These `Retag` instructions are inserted by the compiler pretty much any time
438 references are copied: At the beginning of every function, all inputs of
439 reference type get retagged.  On every assignment, if the assigned value is of
440 reference type, it gets retagged.  Moreover, we do this even when the reference
441 value is inside the field of a `struct` or `enum`, to make sure we really cover
442 all references.  (This recursive descend is already implemented, but the
443 implementation has not landed yet.)  However, we do *not* descend recursively
444 through references: Retagging a `&mut &mut u8` will only retag the *outer*
445 reference.
446
447 Retagging is the *only* operation that generates fresh tags.  Taking a reference
448 simply forwards the tag of the pointer we are basing this reference on.
449
450 Here is our very first example with explicit retagging:
451
452 {% highlight rust %}
453 fn demo0() {
454   let x = &mut 1u8;
455   Retag(x); // tag of `x` gets changed to `Uniq(0)`
456   // stack: [Uniq(0)]; not frozen
457   
458   let y = &mut *x;
459   Retag(x); // tag of `y` gets changed to `Uniq(1)`
460   // stack: [Uniq(0), Uniq(1)]; not frozen
461
462   // Check that `Uniq(1)` is on the stack, then pop to bring it to the top.
463   *y = 5;
464   // stack: [Uniq(0), Uniq(1)]; not frozen
465
466   // Check that `Uniq(0)` is on the stack, then pop to bring it to the top.
467   *x = 3;
468   // stack: [Uniq(0)]; not frozen
469
470   // Check that `Uniq(1)` is on the stack -- it is not, hence UB.
471   let _val = *y;
472 }
473 {% endhighlight %}
474
475 For each reference, `Retag` does the following (with one special exception that
476 will be explained later):
477
478 1. Compute a fresh tag, `Uniq(_)` for a mutable reference and `Shr(Some(_))` for
479    a shared reference.
480 2. Perform the checks that would also happen when we dereference this reference.
481 3. Perform the actions that would also happen when an actual access happens
482    through this reference (for shared references a read access, for mutable
483    references a write access).
484 4. If the new tag is `Uniq`, push it onto the stack.  (The location cannot be
485    frozen: `Uniq` tags are only created for mutable references, and we just
486    performed the actions of a write access to memory, which unfreezes
487    locations.)
488 5. If the new tag is `Shr`:
489     - If the location is already frozen, we do nothing.
490     - Otherwise:
491       1. Push a `Shr` item to the stack.
492       2. If the location is outside of `UnsafeCell`, it gets frozen with the
493          timestamp of the new reference.
494
495 ### 3.2 When Pointers Escape
496
497 Creating a shared reference is not the only way to share a location: We can also
498 create raw pointers, and if we are careful enough, use them to access a location
499 from different aliasing pointers.  (Of course, "careful enough" is not very
500 precise, but the precise answer is the very model I am describing here.)
501
502 To account for this, we need one final ingredient in our model: A special
503 instruction that indicates that a reference was cast to a raw pointer, and may
504 thus be accessed from these raw pointers in a shared way.  Consider the
505 [following example](https://play.rust-lang.org/?version=stable&mode=debug&edition=2015&gist=253868e96b7eba85ef28e1eabd557f66):
506
507 {% highlight rust %}
508 fn demo4() {
509   let x = &mut 1u8;
510   Retag(x); // tag of `x` gets changed to `Uniq(0)`
511   // stack: [Uniq(0)]; not frozen
512
513   // Make sure what `x` points to is accessible through raw pointers.
514   EscapeToRaw(x);
515   // stack: [Uniq(0), Shr]; not frozen
516   
517   let y1 = x as *mut u8;
518   let y2 = y1;
519   unsafe {
520     // All of these first dereference a raw pointer (no checks, tag gets
521     // ignored) and then perform a read or write access with `Shr(None)` as
522     // the tag, which is already the top of the stack so nothing changes.
523     *y1 = 3;
524     *y2 = 5;
525     *y2 = *y1;
526   }
527
528   // Writing to `x` again pops `Shr` off the stack, as per the rules for
529   // write accesses.
530   *x = 7;
531   // stack: [Uniq(0)]; not frozen
532
533   // Any further access through the raw pointers is undefined behavior, even
534   // reads: The write to `x` re-asserted that `x` is the unique reference for
535   // this memory.
536   let _val = unsafe { *y1 };
537 }
538 {% endhighlight %}
539
540 The behavior of `EscapeToRaw` is best described as "reborrowing for a raw
541 pointer": The steps are the same as for `Retag` above, except that the new
542 pointer's tag is `Shr(None)` and we do not freeze (i.e., we behave as if the
543 entire pointee was inside an `UnsafeCell`).
544
545 Knowing about both `Retag` and `EscapeToRaw`, you can now go back to `demo2` and
546 should be able to fully explain why the stack changes the way it does not that
547 example.
548
549 ### 3.3 The Case of the Aliasing References
550
551 Everything I described so far was pretty much in working condition as of about a
552 week ago.  However, there was one thorny problem that I only discovered fairly
553 late, and as usual it is best demonstrated by an example -- entirely in safe
554 code:
555
556 {% highlight rust %}
557 fn demo_refcell() {
558   let rc = &mut RefCell::new(23u8);
559   Retag(rc); // tag gets changed to `Uniq(0)`
560   // We will consider the stack of the location where `23` is stored; the
561   // `RefCell` bookkeeping counters are not of interest.
562   // stack: [Uniq(0)]
563
564   // Taking a shared reference shares the location but does not freeze, due
565   // to the `UnsafeCell`.
566   let rc_shr = &*rc;
567   Retag(rc_shr); // tag gets changed to `Shr(Some(1))`
568   // stack: [Uniq(0), Shr]; not frozen
569
570   // Lots of stuff happens here but it does not matter for this example.
571   let mut bmut = rc_shr.borrow_mut();
572   
573   // Obtain a mutable reference into the `RefCell`.
574   let mut_ref = &mut *bmut;
575   Retag(mut_ref); // tag gets changed to `Uniq(2)`
576   // stack: [Uniq(0), Shr, Uniq(2)]; not frozen
577   
578   // And at the same time, a fresh shared reference to its outside!
579   // This counts as a read access through `rc`, so we have to pop until
580   // at least a `Shr` is at the top of the stack.
581   let shr_ref = &*rc; // tag gets changed to `Shr(Some(3))`
582   Retag(shr_ref);
583   // stack: [Uniq(0), Shr]; not frozen
584
585   // Now using `mut_ref` is UB because its tag is no longer on the stack.  But
586   // that is bad, because it is usable in safe code.
587   *mut_ref += 19;
588 }
589 {% endhighlight %}
590
591 Notice how `mut_ref` and `shr_ref` alias!  And yet, creating a shared reference
592 to the memory already covered by our unique `mut_ref` must not invalidate
593 `mut_ref`.  If we follow the instructions above, when we retag `shr_ref` after
594 it got created, we have no choice but pop the item matching `mut_ref` off the
595 stack.  Ouch.
596
597 This made me realize that creating a shared reference has to be very weak when
598 on locations inside `UnsafeCell`.  In fact, it is entirely equivalent to
599 `EscapeToRaw`: We just have to make sure some kind of shared access is possible,
600 but we have to accept that there might be active mutable references assuming
601 exclusive access to the same locations.  That on its own is not enough, though.
602
603 I also added a new check to the retagging procedure: Before taking any action
604 (i.e., before step 3, which could pop items off the stack), we check if the
605 reborrow is redundant: If the new reference we want to create is already
606 dereferencable (because it item is already on the stack and, if applicable, the
607 stack is already frozen), *and* if the item that justifies this is moreover
608 "derived from" the item that corresponds to the old reference, then we just do
609 nothing.  Here, "derived from" means "further up the stack".  Basically, the
610 reborrow has already happened and the new reference is ready for use, and
611 (because of that "derived from" check), we know that using the new reference
612 will *not* pop the item corresponding to the old reference off the stack.  In
613 that case, we avoid popping anything, to keep other references valid.
614
615 This rule applies in our example above when we create `shr_ref` from `mut_ref`.
616 There is already a `Shr` on the stack (so the new reference is dereferencable),
617 and the item matching the old reference (`Uniq(0)`) is below that `Shr` (so
618 after using the new reference, the old one remains dereferencable).  Hence we do
619 nothing, keeping the `Uniq(2)` on the stack, such that the access through
620 `mut_ref` at the end remains valid.
621
622 This may sound like a weird rule, and it is.  I would surely not have thought of
623 this if `RefCell` would not force our hands here.  However, as we shall see in
624 [section 5](#5-key-properties), it also does not to break any of the important
625 properties of the model (mutable references being unique and shared references
626 being read-only except for `UnsafeCell`).
627
628 ## 4 Differences to the Original Proposal
629
630 The key differences to the original proposal is that the check performed on a
631 dereference, and the check performed on an access, are not the same check.  This
632 means there are more "moving parts" in the model, but it also means we do not
633 need a weird special exception for `demo1` any more like the original proposal
634 did.  The main reason for this, however, is that on an access, we just do not
635 know if we are inside an `UnsafeCell` or not, so we cannot do all the checks we
636 would like to do.
637
638 Beyond that, I made the behavior of shared references and raw pointers more
639 uniform.  This helped to fix test failures around `iter_mut` on slices, which
640 first creates a raw reference and then a shared reference: In the original
641 model, creating the shared reference invalidates previously created raw
642 pointers.  As part of unifying the two, this happens no longer.
643 (Coincidentally, I did not make this change with the intention of fixing
644 `iter_mut`.  I did this change because I wanted to reduce the number of case
645 distinctions in the model.  Then I realized the relevant test suddenly passed
646 even with the full model enabled, investigated what happened, and realized I
647 accidentally had had a great idea. :D )
648
649 The tag is now "typed" (`Uniq` vs `Shr`) to be able to support `transmute`
650 between references and shared pointers.  Such `transmute` were an open question
651 in the original model and some people raised concerns about it in the ensuing
652 discussion.  I invite all of you to come up with strange things you think you
653 should be able to `transmute` and throw them at miri so that we can see if your
654 use-cases are covered. :)
655
656 Creating a shared reference now always pushes a `Shr` item onto the stack, even
657 when there is no `UnsafeCell`. This means that starting with a mutable reference
658 `x`, `&*x as *const _ as *mut _` is pretty much equivalent to `x as *mut`.  This
659 came up during the implementation because I realized that in `x as *const _` on
660 a mutable reference, `x` actually first gets coerced to shared reference, which
661 then gets cast to a raw pointer.  This happens in `NonNull::from`, so if you
662 later write to that `NonNull`, you end up writing to a raw pointer that was
663 created from a shared reference.  Originally I intended this to be strictly
664 illegal.  This is writing to a shared reference after all, how dare you!
665 However, it turns out it's actually no big deal *if the shared reference does
666 not get used again later*.  This is an access-based model after all, if a
667 reference never gets used again we do not care much about enforcing any
668 guarantees for it.  (This is another example of a coincidental fix, where I had
669 a surprisingly passing test case and then investigated what happened.)
670
671 And finally, there is this special exception about creating raw references, to
672 fix `demo_refcell`.
673
674 Finally, the notion of "function barriers" from the original Stacked Borrows has
675 not been implemented yet.  This is the next item on my todo list.
676
677 ## 5 Key Properties
678
679 Let us look at the two key properties that I set out as design goals, and see
680 how the model guarantees that they hold true in all valid (UB-free) executions.
681
682 ### 5.1 Mutable References are Unique
683
684 The property I would like to establish here is that: After creating (retagging,
685 really) a `&mut`, if we then run some unknown code *that does not get passed the
686 reference* nor do we derive another reference from ours, and then we use the
687 reference again (reading or writing), we can be sure that this unknown code did
688 not access the memory behind our mutable reference at all (or we have UB).  For
689 example:
690
691 {% highlight rust %}
692 fn demo_mut_unique(our: &mut i32) -> i32 {
693   Retag(our); // So we can be sure the tag is unique
694
695   *our = 5;
696
697   unknown_code();
698
699   // We know this will return 5, and moreover if `unknown_code` does not panic
700   // we know we could do the write after calling `unknown_code` (because it
701   // cannot even read from `our`).
702   *our
703 }
704 {% endhighlight %}
705
706 The proof sketch goes as follows: After retagging the reference, we know it is
707 at the top of the stack and the location is not frozen.  (The "redundant
708 reborrow" rule does not apply because a fresh `Uniq` tag can never be
709 redundant.)  For any access performed by the unknown code, we know that access
710 cannot use the tag of our reference because the tags are unique and not
711 forgeable.  Hence if the unknown code accesses our locations, that would pop our
712 tag from the stack.  When we use our reference again, we know it is on the
713 stack, and hence has not been popped off.  Thus there cannot have been an access
714 from the unknown code.
715
716 Actually this theorem applies *any time* we have a reference whose tag we can be
717 sure has not been leaked to anyone else, and which points to locations which
718 have this tag at the top of the (unfrozen) stack.  This is not just the case
719 immediately after retagging.  We know our reference is at the top of the stack
720 after writing to it, so in the following example we know that `unknown_code_2`
721 cannot access `our`:
722
723 {% highlight rust %}
724 fn demo_mut_advanced_unique(our: &mut u8) -> u8 {
725   Retag(our); // So we can be sure the tag is unique
726
727   unknown_code_1(&*our);
728
729   // This "re-asserts" uniqueness of the reference: After writing, we know
730   // our tag is at the top of the stack.
731   *our = 5;
732
733   unknown_code_2();
734
735   // We know this will return 5
736   *our
737 }
738 {% endhighlight %}
739
740 ### 5.2 Shared References (without `UnsafeCell)` are Read-only
741
742 The key property of shared references is that: After creating (retagging,
743 really) a shared reference, if we then run some unknown code (it can even have
744 our reference if it wants), and then we use the reference again, we know that
745 the value pointed to by the reference has not been changed.  For example:
746
747 {% highlight rust %}
748 fn demo_shr_frozen(our: &u8) -> u8 {
749   Retag(our); // So we can be sure the tag actually carries a timestamp
750
751   // See what's in there.
752   let val = *our;
753   
754   unknown_code(our);
755
756   // We know this will return `val`
757   *our
758 }
759 {% endhighlight %}
760
761 The proof sketch goes as follows: After retagging the reference, we know the
762 location is frozen (this is the case even if the "redundant reborrow" rule
763 applies).  If the unknown code does any write, we know this will unfreeze the
764 location.  The location might get re-frozen, but only at the then-current
765 timestamp.  When we do our read after coming back from the unknown code, this
766 checks that the location is frozen *at least* since the timestamp given in its
767 tag, so if the location is unfrozen or got re-frozen by the unknown code, the
768 check would fail.  Thus the unknown code cannot have written to the location.
769
770 One interesting observation here for both of these proofs is that all we rely on
771 when the unknown code is executed are the actions performed on every memory
772 access.  The additional checks that happen when a pointer is dereferenced only
773 matter in *our* code, not in the foreign code.  This indicates that we could see
774 the checks on pointer dereference as another "shadow state operation" next to
775 `Retag` and `EscapeToRaw`, and then these three operations plus the actions on
776 memory accesses are all that there is to Stacked Borrows.  This is difficult to
777 implement in miri because dereferences can happen any time a path is evaluated,
778 but it is nevertheless interesting and might be useful in a "lower-level MIR"
779 that does not permit dereferences in paths.
780
781 ## 6 Evaluation, and How You Can Help
782
783 I have implemented both the validity invariant and the model as described above
784 in miri. This [uncovered](https://github.com/rust-lang/rust/issues/54908) two
785 [issues](https://github.com/rust-lang/rust/issues/54957) in the standard
786 library, but both were related to validity invariants, not Stacked Borrows.
787 With these exceptions, the model passes the entire test suite.  There were some
788 more test failures in earlier versions (as mentioned in section 4), but the
789 final model accepts all the code covered by miri's test suite.  Moreover I wrote
790 a bunch of compile-fail tests to make sure the model catches various violations
791 of the key properties it should ensure.
792
793 However, miri's test suite is tiny, and I have but one brain to come up with
794 counterexamples!  In fact I am quite a bit worried because I literally came up
795 with `demo_refcell` less than two weeks ago, so what else might I have missed?
796 This where you come in.  Please test this model!  Come up with something funny
797 you think should work (I am thinking about funny `transmute` in particular,
798 using type punning through unions or raw pointers if you prefer that), or maybe
799 you have some crate that has some unsafe code and a test suite (you do have a
800 test suite, right?) that might run under miri.
801
802 The easiest way to try the model is the
803 [playground](https://play.rust-lang.org/): Type the code, select "Tools - Miri",
804 and you'll see what it does.
805
806 For things that are too long for the playground, you have to install miri on
807 your own computer.  miri depends on rustc nightly and has to be updated
808 regularly to keep working, so it is not currently on crates.io.  Installation
809 instructions for miri are provided
810 [in the README](https://github.com/solson/miri/#running-miri).  Please let me
811 know if you are having trouble with anything.  You can report issues, comment on
812 this post or find me in chat (as of recently, I am partial to Zulip where we
813 have an
814 [unsafe code guidelines stream](https://rust-lang.zulipchat.com/#narrow/stream/136281-wg-unsafe-code-guidelines)).
815
816 With miri installed, you can `cargo miri` a project with a binary to run it in
817 miri.  Dependencies should be fully supported, so you can use any crate you
818 like.  It is not unlikely, however, that you will run into issues because miri
819 does not support some operation.  In that case please search the
820 [issue tracker](https://github.com/solson/miri/issues) and report the issue if
821 it is new.  We cannot support everything, but we might be able to do something
822 for your case.
823
824 Unfortunately, `cargo miri test` is currently broken; if you want to help with
825 that [here are some details](https://github.com/solson/miri/issues/479).
826 Moreover, wouldn't it be nice if we could run the entire libcore, liballoc and
827 libstd test suite in miri?  There are tons of interesting cases of Rust's core
828 data structures being exercise there, and the comparatively tiny miri test suite
829 has already helped to find two soundness bugs, so there are probably more.  Once
830 `cargo miri test` works again, it would be great to find a way to run it on the
831 standard library test suites, and set up something so that this happens
832 automatically on a regular basis (so that we notice regressions).
833
834 As you can see, there is more than enough work for everyone.  Don't be shy!  I
835 have a mere three weeks left on this internship, after which I will have to
836 significantly reduce my Rust activities in favor of finishing my PhD.  I won't
837 disappear entirely though, don't worry -- I will still be able to mentor you if
838 you want to help with any of the above tasks. :)