add twinsem paper

[web.git] / personal / _posts / 2018-08-07-stacked-borrows.md

diff --git a/personal/_posts/2018-08-07-stacked-borrows.md b/personal/_posts/2018-08-07-stacked-borrows.md
index 678775465c3a19b620edf0325f5c0f0a1bab6e18..94f2bb6689b7b1bd51b63c089755900ac76d09fc 100644 (file)
--- a/personal/_posts/2018-08-07-stacked-borrows.md
+++ b/personal/_posts/2018-08-07-stacked-borrows.md
@@ -1,6 +1,7 @@
 ---
 title: "Stacked Borrows: An Aliasing Model For Rust"
 categories: internship rust
 ---
 title: "Stacked Borrows: An Aliasing Model For Rust"
 categories: internship rust

+forum: https://internals.rust-lang.org/t/stacked-borrows-an-aliasing-model-for-rust/8153

 ---
 
 In this post, I am proposing "Stacked Borrows": A set of rules defining which kinds of aliasing are allowed in Rust.
 ---
 
 In this post, I am proposing "Stacked Borrows": A set of rules defining which kinds of aliasing are allowed in Rust.


@@ -12,7 +13,7 @@ The model I am proposing here is by far not the first attempt at giving a defini
 <!-- MORE -->
 
 But before I delve into my latest proposal, I want to briefly discuss a key difference between my previous model and this one:
 <!-- MORE -->
 
 But before I delve into my latest proposal, I want to briefly discuss a key difference between my previous model and this one:

-"Types as Contracts" was a fully "validity"-based model, while "Stacked Borrows" is (to some extend) "access"-based.
+"Types as Contracts" was a fully "validity"-based model, while "Stacked Borrows" is (to some extent) "access"-based.

 
 ## 1 Validity-based vs. Access-based
 
 
 ## 1 Validity-based vs. Access-based
 


@@ -30,7 +31,7 @@ Validity-based models have several advantages: Eager checking means we can typic
 
 However, in Rust, we cannot talk about references and whether the are valid at their given type without talking about lifetimes.
 With "Types as Contracts", the exact place where a lifetime ended turned out to be really important.
 
 However, in Rust, we cannot talk about references and whether the are valid at their given type without talking about lifetimes.
 With "Types as Contracts", the exact place where a lifetime ended turned out to be really important.

-Not only did this make the specification complex and hard to understand; the implementation in [Miri]({% post_url 2017-06-06-MIR-semantics %}) also had to actively work against the compiler's general intention to forget about lifetimes as early as possible.
+Not only did this make the specification complex and hard to understand; the implementation in Miri also had to actively work against the compiler's general intention to forget about lifetimes as early as possible.

 With non-lexical lifetimes, the "end" of a lifetime is not even so clearly defined any more.
 
 ## 2 Stacking Borrows
 With non-lexical lifetimes, the "end" of a lifetime is not even so clearly defined any more.
 
 ## 2 Stacking Borrows


@@ -146,7 +147,7 @@ Shared references with interior mutability do not really have any restrictions i
 For every location in memory, we keep track of a stack of borrows (`Uniq(_)` or `Raw`), and potentially "top off" this stack by freezing the location.
 A frozen location is never written to, and no `Uniq` is pushed.
 
 For every location in memory, we keep track of a stack of borrows (`Uniq(_)` or `Raw`), and potentially "top off" this stack by freezing the location.
 A frozen location is never written to, and no `Uniq` is pushed.
 

-Whenever a mutable reference is created, a matching `Uniq` is pushed onto the stack for every location "covered by" the reference -- i.e., the locations that would be accessed when the reference is used (starting at where it points to, and going on for `mem::size_of::<T>` many bytes).
+Whenever a mutable reference is created, a matching `Uniq` is pushed onto the stack for every location "covered by" the reference -- i.e., the locations that would be accessed when the reference is used (starting at where it points to, and going on for `size_of_val` many bytes).

 Whenever a shared reference is created, if there is no interior mutability, we freeze the locations if they are not already frozen.
 If there is interior mutability, we just push a `Raw`.
 Whenever a raw pointer is created from a mutable reference, we push a `Raw`.
 Whenever a shared reference is created, if there is no interior mutability, we freeze the locations if they are not already frozen.
 If there is interior mutability, we just push a `Raw`.
 Whenever a raw pointer is created from a mutable reference, we push a `Raw`.


@@ -168,7 +169,7 @@ In particular, notice that `x` and `y` in the first example have the same addres
 If we compared them as raw pointers, they would turn out equal.
 And yet, it makes a huge difference if we use `x` or `y`!
 
 If we compared them as raw pointers, they would turn out equal.
 And yet, it makes a huge difference if we use `x` or `y`!
 

-If you read my previous post on [why pointers are complicated](2018-07-24-pointers-and-bytes), this should not come as too much of a surprise.
+If you read my previous post on [why pointers are complicated]({% post_url 2018-07-24-pointers-and-bytes %}), this should not come as too much of a surprise.

 There is more to a pointer, or a reference (I am using these terms mostly interchangeably), than the address in memory that it points to.
 
 For the purpose of this model, we assume that a value of reference type consists of two parts: An address in memory, and a tag used to store the time when the reference was created.
 There is more to a pointer, or a reference (I am using these terms mostly interchangeably), than the address in memory that it points to.
 
 For the purpose of this model, we assume that a value of reference type consists of two parts: An address in memory, and a tag used to store the time when the reference was created.


@@ -228,7 +229,7 @@ With this additional step, it is now easy to argue that `demo4` above is UB when
 After using `x`, we know it is active.
 Next we use and activate `y`, which has to pop `Uniq(x)` as they have distinct tags.
 Finally, we use `x` again even though it is no longer in the stack, triggering UB.
 After using `x`, we know it is active.
 Next we use and activate `y`, which has to pop `Uniq(x)` as they have distinct tags.
 Finally, we use `x` again even though it is no longer in the stack, triggering UB.

-(A `Uniq` is only veer pushed when it is created, so it is never in the stack more than once.)
+(A `Uniq` is only ever pushed when it is created, so it is never in the stack more than once.)

 
 ### 4.2 Barriers
 
 
 ### 4.2 Barriers
 


@@ -238,7 +239,7 @@ It is also needed to explain why we can put the [`noalias` parameter attribute](
 
 Consider the following code:
 {% highlight rust %}
 
 Consider the following code:
 {% highlight rust %}

-fn demo5(x: &mut i32, y: usize) -> i32 {
+fn demo5(x: &mut i32, y: usize) {

   *x = 42;
   foo(y);
 }
   *x = 42;
   foo(y);
 }


@@ -404,7 +405,7 @@ This is where the code gets more "pseudo" and less Rust. ;)
 For each of these operation, we iterate over all affected locations; let us call the loop variable `loc` of type `MemoryByte`.
 We also have a variable `tag` with the tag of the pointer we are operating on (loading, or storing, or casting to a raw pointer, ...).
 
 For each of these operation, we iterate over all affected locations; let us call the loop variable `loc` of type `MemoryByte`.
 We also have a variable `tag` with the tag of the pointer we are operating on (loading, or storing, or casting to a raw pointer, ...).
 

-Moreover, we have a boolean variable `in_unsafe_cell` indicating whether, according to the type of the pointer, the location we are currently working on is covered by an [`UnsafeCell`](https://doc.rust-lang.org/beta/std/cell/struct.UnsafeCell.html).
+Moreover, we have a boolean variable `in_unsafe_cell` indicating whether, according to the type of the pointer, the location we are currently working on is covered by an [`UnsafeCell`](https://doc.rust-lang.org/stable/std/cell/struct.UnsafeCell.html).

 (This realizes the conditions checking whether we have interior mutability or not.)
 For example, in `&Cell<i32>`, all 4 locations are inside an `UnsafeCell`.
 However, in `&(i32, Cell<i32>)`, only the last 4 of the 8 covered locations are inside an `UnsafeCell`.
 (This realizes the conditions checking whether we have interior mutability or not.)
 For example, in `&Cell<i32>`, all 4 locations are inside an `UnsafeCell`.
 However, in `&(i32, Cell<i32>)`, only the last 4 of the 8 covered locations are inside an `UnsafeCell`.


@@ -464,4 +465,4 @@ I hope to explore this question further in the following weeks by implementing a
 It is just easier to answer these questions when you do not have to *manually* reevaluate all examples after every tiny change.
 However, I can always use more examples, so if you think you found some interesting or surprising corner case, please let me know!
 
 It is just easier to answer these questions when you do not have to *manually* reevaluate all examples after every tiny change.
 However, I can always use more examples, so if you think you found some interesting or surprising corner case, please let me know!
 

-<!-- As always, if you have any questions or comments, feel free to [ask in the forums](). -->
+As always, if you have any questions or comments, feel free to [ask in the forums](https://internals.rust-lang.org/t/stacked-borrows-an-aliasing-model-for-rust/8153).