add link to department website

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

diff --git a/personal/_posts/2018-11-16-stacked-borrows-implementation.md b/personal/_posts/2018-11-16-stacked-borrows-implementation.md
index 35bf7356f3779c8b2189b6684bd15df98cd21ce5..64f9e3172ad286a0642eb7238b4f5f2f232fad3c 100644 (file)
--- a/personal/_posts/2018-11-16-stacked-borrows-implementation.md
+++ b/personal/_posts/2018-11-16-stacked-borrows-implementation.md
@@ -4,16 +4,21 @@ categories: internship rust
 forum: https://internals.rust-lang.org/t/stacked-borrows-implemented/8847
 ---
 
 forum: https://internals.rust-lang.org/t/stacked-borrows-implemented/8847
 ---
 

-Three months ago, I proposed [Stacked Borrows]({% post_url
-2018-08-07-stacked-borrows %}) as a model for defining what kinds of aliasing
-are allowed in Rust, and the idea of a [validity invariant]({% post_url
-2018-08-22-two-kinds-of-invariants %}) that has to be maintained by all code at
-all times.  Since then I have been busy implementing both of these, and
+Three months ago, I proposed Stacked Borrows as a model for defining what kinds
+of aliasing are allowed in Rust, and the idea of a [validity invariant]({%
+post_url 2018-08-22-two-kinds-of-invariants %}) that has to be maintained by all
+code at all times.  Since then I have been busy implementing both of these, and

 developed Stacked Borrows further in doing so.  This post describes the latest
 version of Stacked Borrows, and reports my findings from the implementation
 phase: What worked, what did not, and what remains to be done.  There will also
 be an opportunity for you to help the effort!
 
 developed Stacked Borrows further in doing so.  This post describes the latest
 version of Stacked Borrows, and reports my findings from the implementation
 phase: What worked, what did not, and what remains to be done.  There will also
 be an opportunity for you to help the effort!
 

+This post is a self-contained introduction to Stacked Borrows.  Other than
+historical curiosity and some comparison with my earlier work on
+[Types as Contracts]({% post_url 2017-07-17-types-as-contracts %}) there is no
+reason to read the [original post]({% post_url 2018-08-07-stacked-borrows %}) at
+this point.
+

 <!-- MORE -->
 
 What Stacked Borrows does is that it defines a semantics for Rust programs such
 <!-- MORE -->
 
 What Stacked Borrows does is that it defines a semantics for Rust programs such


@@ -29,9 +34,9 @@ help us.  We have to define a set of rules that makes sense even for unsafe
 code.
 
 I will explain these rules again in this post.  The explanation is not going to
 code.
 
 I will explain these rules again in this post.  The explanation is not going to

-be the same as last time, not only because it changed a bit, but also because I
-think I understand the model better myself now so I can do a better job
-explaining it.
+be the same as [last time]({% post_url 2018-08-07-stacked-borrows %}), not only
+because it changed a bit, but also because I think I understand the model better
+myself now so I can do a better job explaining it.

 
 Ready?  Let's get started.  I hope you brought some time, because this is a
 rather lengthy post.  If you are not interested in a detailed description of
 
 Ready?  Let's get started.  I hope you brought some time, because this is a
 rather lengthy post.  If you are not interested in a detailed description of


@@ -492,7 +497,7 @@ refine these instructions later) on all locations covered by the 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
    references a write access).
 3. Perform the actions that would also happen when an actual access happens
    through this reference (for shared references a read access, for mutable
    references a write access).

-4. Check if the new tag is `Shr(Some(t))` and the location is inside an `UnsafeCell`.
+4. Check if the new tag is `Shr(Some(t))` and the location is *not* inside an `UnsafeCell`.

     - If both conditions apply, freeze the location with timestamp `t`.  If it
       is already frozen, do nothing.
     - Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`,
     - If both conditions apply, freeze the location with timestamp `t`.  If it
       is already frozen, do nothing.
     - Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`,


@@ -664,9 +669,8 @@ executed on all locations covered by the reference, according to `size_of_val`):
    Now the location cannot be frozen any more: If the fresh tag is `Uniq`, we
    just unfroze; if the fresh tag is `Shr` and the location was already frozen,
    then the redundancy check (step 3) would have kicked in.
    Now the location cannot be frozen any more: If the fresh tag is `Uniq`, we
    just unfroze; if the fresh tag is `Shr` and the location was already frozen,
    then the redundancy check (step 3) would have kicked in.

-5. Check if the new tag is `Shr(Some(t))` and the location is inside an `UnsafeCell`.
-    - If both conditions apply, freeze the location with timestamp `t`.  If it
-      is already frozen, do nothing.
+5. Check if the new tag is `Shr(Some(t))` and the location is *not* inside an `UnsafeCell`.
+    - If both conditions apply, freeze the location with timestamp `t`.

     - Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`,
       `Uniq(id)` if the tag is `Uniq(id)`.
 
     - Otherwise, push a new item onto the stack: `Shr` if the tag is a `Shr(_)`,
       `Uniq(id)` if the tag is `Uniq(id)`.