the journal paper is no longer a preprint

[web.git] / ralf / _posts / 2018-11-16-stacked-borrows-implementation.md

diff --git a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md b/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
index 211d21d32e9a08bb377e33f02c37da017fc00b7d..c1c02743bd85bb0b7b6634f122b8d75ae7e89b05 100644 (file)
--- a/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
+++ b/ralf/_posts/2018-11-16-stacked-borrows-implementation.md
@@ -1,6 +1,7 @@
 ---
 title: "Stacked Borrows Implemented"
 categories: internship rust
 ---
 title: "Stacked Borrows Implemented"
 categories: internship rust

+forum: https://internals.rust-lang.org/t/stacked-borrows-implemented/8847

 ---
 
 Three months ago, I proposed [Stacked Borrows]({% post_url
 ---
 
 Three months ago, I proposed [Stacked Borrows]({% post_url


@@ -313,7 +314,7 @@ fn demo2() {
 
   // The `x` here really is a `&*x`, but we have already seen above what
   // happens: `Uniq(0)` must be in the stack, but we leave it unchanged.
 
   // The `x` here really is a `&*x`, but we have already seen above what
   // happens: `Uniq(0)` must be in the stack, but we leave it unchanged.

-  let z = x as *const u8 as *mut u8; // tag irrelevant because raw
+  let z = x as *const u8 as *mut u8; // tag erased: `Shr(None)`

   // stack: [Uniq(0), Shr]; frozen since 1
 
   // A write access through a raw pointer: Unfreeze the location and make sure
   // stack: [Uniq(0), Shr]; frozen since 1
 
   // A write access through a raw pointer: Unfreeze the location and make sure


@@ -351,8 +352,7 @@ The following checks are done on every pointer dereference, for every location
 covered by the pointer (`size_of_val` tells us how many bytes the pointer
 covers):
 
 covered by the pointer (`size_of_val` tells us how many bytes the pointer
 covers):
 

-1. If this is a raw pointer, do nothing and reset the tag used for the access to
-   `Shr(None)`.  Raw accesses are checked as little as possible.
+1. If this is a raw pointer, do nothing.  Raw accesses are checked as little as possible.

 2. If this is a unique reference and the tag is `Shr(Some(_))`, that's an error.
 3. If the tag is `Uniq`, make sure there is a matching `Uniq` item with the same
    ID on the stack.
 2. If this is a unique reference and the tag is `Shr(Some(_))`, that's an error.
 3. If the tag is `Uniq`, make sure there is a matching `Uniq` item with the same
    ID on the stack.


@@ -369,10 +369,9 @@ covers):
 [section 2.3]: #23-accessing-memory
 
 On an actual memory access, we know the tag of the pointer that was used to
 [section 2.3]: #23-accessing-memory
 
 On an actual memory access, we know the tag of the pointer that was used to

-access (unless it was a raw pointer, in which case the tag we see is
-`Shr(None)`), and we know whether we are reading from or writing to the current
-location.  We perform the following operations on all locations affected by the
-access:
+access (we always use the actual tag and disregard the type of the pointer), and
+we know whether we are reading from or writing to the current location.  We
+perform the following operations on all locations affected by the access:

 
 1. If the location is frozen and this is a read access, nothing happens (even
    if the tag is `Uniq`).
 
 1. If the location is frozen and this is a read access, nothing happens (even
    if the tag is `Uniq`).


@@ -449,9 +448,10 @@ reference type get retagged.  On every assignment, if the assigned value is of
 reference type, it gets retagged.  Moreover, we do this even when the reference
 value is inside the field of a `struct` or `enum`, to make sure we really cover
 all references.  (This recursive descent is already implemented, but the
 reference type, it gets retagged.  Moreover, we do this even when the reference
 value is inside the field of a `struct` or `enum`, to make sure we really cover
 all references.  (This recursive descent is already implemented, but the

-implementation has not landed yet.)  However, we do *not* descend recursively
-through references: Retagging a `&mut &mut u8` will only retag the *outer*
-reference.
+implementation has not landed yet.)  Finally, `Box` is treated like a mutable
+reference, to encode that it asserts unique access.  However, we do *not*
+descend recursively through references: Retagging a `&mut &mut u8` will only
+retag the *outer* reference.

 
 Retagging is the *only* operation that generates fresh tags.  Taking a reference
 simply forwards the tag of the pointer we are basing this reference on.
 
 Retagging is the *only* operation that generates fresh tags.  Taking a reference
 simply forwards the tag of the pointer we are basing this reference on.


@@ -481,12 +481,12 @@ fn demo0() {
 }
 {% endhighlight %}
 
 }
 {% endhighlight %}
 

-For each reference, `Retag` does the following (we will slightly refine these
-instructions later) on all locations covered by the reference (again, according
-to `size_of_val`):
+For each reference and `Box`, `Retag` does the following (we will slightly
+refine these instructions later) on all locations covered by the reference
+(again, according to `size_of_val`):

 
 

-1. Compute a fresh tag, `Uniq(_)` for a mutable reference and `Shr(Some(_))` for
-   a shared reference.
+1. Compute a fresh tag: `Uniq(_)` for mutable references and `Box`, and
+   `Shr(Some(_))` for shared references.

 2. Perform the checks that would also happen when we dereference this reference.
 3. Perform the actions that would also happen when an actual access happens
    through this reference (for shared references a read access, for mutable
 2. Perform the checks that would also happen when we dereference this reference.
 3. Perform the actions that would also happen when an actual access happens
    through this reference (for shared references a read access, for mutable


@@ -527,7 +527,7 @@ fn demo4() {
   EscapeToRaw(x);
   // stack: [Uniq(0), Shr]; not frozen
   
   EscapeToRaw(x);
   // stack: [Uniq(0), Shr]; not frozen
   

-  let y1 = x as *mut u8;
+  let y1 = x as *mut u8; // tag erased: `Shr(None)`

   let y2 = y1;
   unsafe {
     // All of these first dereference a raw pointer (no checks, tag gets
   let y2 = y1;
   unsafe {
     // All of these first dereference a raw pointer (no checks, tag gets


@@ -555,6 +555,11 @@ pointer": The steps are the same as for `Retag` above, except that the new
 pointer's tag is `Shr(None)` and we do not freeze (i.e., we behave as if the
 entire pointee was inside an `UnsafeCell`).
 
 pointer's tag is `Shr(None)` and we do not freeze (i.e., we behave as if the
 entire pointee was inside an `UnsafeCell`).
 

+This is needed, because when casting a reference to a raw pointer (and actually,
+on any cast involving pointers), the tag gets erased, meaning it gets reset to
+`Shr(None)`.  Thanks to `EscapeToRaw`, there is a matching `Shr` on the stack,
+making sure the raw pointer can actually be used.
+

 Knowing about both `Retag` and `EscapeToRaw`, you can now go back to `demo2` and
 should be able to fully explain why the stack changes the way it does in that
 example.
 Knowing about both `Retag` and `EscapeToRaw`, you can now go back to `demo2` and
 should be able to fully explain why the stack changes the way it does in that
 example.


@@ -568,7 +573,7 @@ code:
 
 {% highlight rust %}
 fn demo_refcell() {
 
 {% highlight rust %}
 fn demo_refcell() {

-  let rc = &mut RefCell::new(23u8);
+  let rc: &mut RefCell<u8> = &mut RefCell::new(23u8);

   Retag(rc); // tag gets changed to `Uniq(0)`
   // We will consider the stack of the location where `23` is stored; the
   // `RefCell` bookkeeping counters are not of interest.
   Retag(rc); // tag gets changed to `Uniq(0)`
   // We will consider the stack of the location where `23` is stored; the
   // `RefCell` bookkeeping counters are not of interest.


@@ -576,22 +581,22 @@ fn demo_refcell() {
 
   // Taking a shared reference shares the location but does not freeze, due
   // to the `UnsafeCell`.
 
   // Taking a shared reference shares the location but does not freeze, due
   // to the `UnsafeCell`.

-  let rc_shr = &*rc;
+  let rc_shr: &RefCell<u8> = &*rc;

   Retag(rc_shr); // tag gets changed to `Shr(Some(1))`
   // stack: [Uniq(0), Shr]; not frozen
 
   // Lots of stuff happens here but it does not matter for this example.
   Retag(rc_shr); // tag gets changed to `Shr(Some(1))`
   // stack: [Uniq(0), Shr]; not frozen
 
   // Lots of stuff happens here but it does not matter for this example.

-  let mut bmut = rc_shr.borrow_mut();
+  let mut bmut: RefMut<u8> = rc_shr.borrow_mut();

   
   // Obtain a mutable reference into the `RefCell`.
   
   // Obtain a mutable reference into the `RefCell`.

-  let mut_ref = &mut *bmut;
+  let mut_ref: &mut u8 = &mut *bmut;

   Retag(mut_ref); // tag gets changed to `Uniq(2)`
   // stack: [Uniq(0), Shr, Uniq(2)]; not frozen
   
   // And at the same time, a fresh shared reference to its outside!
   // This counts as a read access through `rc`, so we have to pop until
   // at least a `Shr` is at the top of the stack.
   Retag(mut_ref); // tag gets changed to `Uniq(2)`
   // stack: [Uniq(0), Shr, Uniq(2)]; not frozen
   
   // And at the same time, a fresh shared reference to its outside!
   // This counts as a read access through `rc`, so we have to pop until
   // at least a `Shr` is at the top of the stack.

-  let shr_ref = &*rc; // tag gets changed to `Shr(Some(3))`
+  let shr_ref: &RefCell<u8> = &*rc; // tag gets changed to `Shr(Some(3))`

   Retag(shr_ref);
   // stack: [Uniq(0), Shr]; not frozen
 
   Retag(shr_ref);
   // stack: [Uniq(0), Shr]; not frozen
 


@@ -647,8 +652,8 @@ With this extension, the instructions for retagging and `EscapeToRaw` now look
 as follows (again executed on all locations covered by the reference, according
 to `size_of_val`):
 
 as follows (again executed on all locations covered by the reference, according
 to `size_of_val`):
 

-1. Compute a fresh tag: `Uniq(_)` for a mutable reference, `Shr(Some(_))` for a
-   shared reference, `Shr(None)` if this is `EscapeToRaw`.
+1. Compute a fresh tag: `Uniq(_)` for mutable references and `Box`,
+   `Shr(Some(_))` for shared references, `Shr(None)` if this is `EscapeToRaw`.

 2. Perform the checks that would also happen when we dereference this reference.
    Remember the position of the item matching the tag in the stack.
 3. Redundancy check: If the new tag passes the checks performed on a
 2. Perform the checks that would also happen when we dereference this reference.
    Remember the position of the item matching the tag in the stack.
 3. Redundancy check: If the new tag passes the checks performed on a


@@ -907,5 +912,17 @@ significantly reduce my Rust activities in favor of finishing my PhD.  I won't
 disappear entirely though, don't worry -- I will still be able to mentor you if
 you want to help with any of the above tasks. :)
 
 disappear entirely though, don't worry -- I will still be able to mentor you if
 you want to help with any of the above tasks. :)
 

-Thanks to @nikomatsakis for feedback on a draft of this post.
-<!-- If you want to help or report results of your experiments, if you have any questions or comments, please join the [discussion in the forums](). -->
+Thanks to @nikomatsakis for feedback on a draft of this post, to @shepmaster for
+making miri available on the playground, and to @oli-obk for reviewing all my
+PRs at unparalleled speed. <3
+
+If you want to
+help or report results of your experiments, if you have any questions or
+comments, please join the
+[discussion in the forums](https://internals.rust-lang.org/t/stacked-borrows-implemented/8847).
+
+## Changelog
+
+**2018-11-21:** Dereferencing a pointer now always preserves the tag, but
+casting to a raw pointer resets the tag to `Shr(None)`.  `Box` is treated like a
+mutable reference.