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