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