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