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