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