add link to department website

[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 37cdf504668b6fbb2ce48d9819c586125a2a34de..7397780b0edb87210813671bc800b0ebc3d54be6 100644 (file)
--- a/personal/_posts/2018-08-07-stacked-borrows.md
+++ b/personal/_posts/2018-08-07-stacked-borrows.md
@@ -15,6 +15,12 @@ The model I am proposing here is by far not the first attempt at giving a defini
 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 extent) "access"-based.
 
 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 extent) "access"-based.
 

+**Update:**
+Since publishing this post, I have written [another]({% post_url 2018-11-16-stacked-borrows-implementation %}) blog post about a slightly adjusted version of Stacked Borrows (the first version that actually got implemented).
+That other post is self-contained, so if you are just interested in the current state of Stacked Borrows, I suggest you go there.
+Only go on reading here if you want some additional historic context.
+**/Update**
+

 ## 1 Validity-based vs. Access-based
 
 An "access"-based model is one where certain properties -- in this case, mutable references being unique and shared references pointing to read-only memory -- are only enforced when the reference is actually used to *access* memory.
 ## 1 Validity-based vs. Access-based
 
 An "access"-based model is one where certain properties -- in this case, mutable references being unique and shared references pointing to read-only memory -- are only enforced when the reference is actually used to *access* memory.


@@ -57,7 +63,7 @@ fn demo0(x: &mut i32) -> i32 {
   let y = &mut *x; // Now `Uniq(y)` is pushed onto the stack, as new active reference.
   // The stack now contains: Uniq(y), Uniq(x), ...
   *y = 5; // Okay because `y` is active.
   let y = &mut *x; // Now `Uniq(y)` is pushed onto the stack, as new active reference.
   // The stack now contains: Uniq(y), Uniq(x), ...
   *y = 5; // Okay because `y` is active.

-  *x = 3; // This "activates" `x` by popping the stack.
+  *x = 3; // This "reactivates" `x` by popping the stack.

   // The stack now contains: Uniq(x), ...
   *y // This is UB! `Uniq(y)` is not on the stack of borrows, so `y` must not be used.
 }
   // The stack now contains: Uniq(x), ...
   *y // This is UB! `Uniq(y)` is not on the stack of borrows, so `y` must not be used.
 }


@@ -82,7 +88,7 @@ fn demo1(x: &mut i32) -> i32 {
   let y = unsafe { &mut *raw }; // Now `y` is pushed onto the stack, as new active reference.
   // The stack now contains: Uniq(y), Raw, Uniq(x), ...
   *y = 5; // Okay because `y` is active.
   let y = unsafe { &mut *raw }; // Now `y` is pushed onto the stack, as new active reference.
   // The stack now contains: Uniq(y), Raw, Uniq(x), ...
   *y = 5; // Okay because `y` is active.

-  *x = 3; // This "activates" `x` by popping the stack twice.
+  *x = 3; // This "reactivates" `x` by popping the stack twice.

   *y // This is UB! `Uniq(y)` is not on the stack of borrows, so `y` must not be used.
 }
 {% endhighlight %}
   *y // This is UB! `Uniq(y)` is not on the stack of borrows, so `y` must not be used.
 }
 {% endhighlight %}


@@ -107,7 +113,7 @@ fn demo2(x: &mut i32) -> i32 {
   let y = unsafe { &mut *raw }; // Now `y` is pushed onto the stack, as new active reference.
   // The stack now contains: Uniq(y), Raw, Uniq(x), ...
   *y = 5; // Okay because `y` is active.
   let y = unsafe { &mut *raw }; // Now `y` is pushed onto the stack, as new active reference.
   // The stack now contains: Uniq(y), Raw, Uniq(x), ...
   *y = 5; // Okay because `y` is active.

-  unsafe { *raw = 5 }; // Using a raw pointer, so `Raw` gets activated by popping the stack!
+  unsafe { *raw = 5 }; // Using a raw pointer, so `Raw` gets reactivated by popping the stack!

   // The stack now contains: Raw, Uniq(x), ...
   *y // This is UB! `Uniq(y)` is not on the stack of borrows, so `y` must not be used.
 }
   // The stack now contains: Raw, Uniq(x), ...
   *y // This is UB! `Uniq(y)` is not on the stack of borrows, so `y` must not be used.
 }


@@ -134,8 +140,8 @@ fn demo3(x: &mut i32) -> i32 {
   // The stack now contains: Raw, Uniq(x), ...
   let y = unsafe { & *raw }; // Now memory gets frozen (recording the timestamp)
   let _val = *y; // Okay because memory was frozen since `y` was created
   // The stack now contains: Raw, Uniq(x), ...
   let y = unsafe { & *raw }; // Now memory gets frozen (recording the timestamp)
   let _val = *y; // Okay because memory was frozen since `y` was created

-  *x = 3; // This "activates" `x` by unfreezing and popping the stack.
-  let z = unsafe { & *raw }; // Now memory gets frozen *again*
+  *x = 3; // This "reactivates" `x` by unfreezing and popping the stack.
+  let z = &*x; // Now memory gets frozen *again*

   *y // This is UB! Memory has been frozen strictly after `y` got created.
 }
 {% endhighlight %}
   *y // This is UB! Memory has been frozen strictly after `y` got created.
 }
 {% endhighlight %}


@@ -157,8 +163,10 @@ A mutable reference `x` is "active" for a location if that location is not froze
 A shared reference without interior mutability is active if the location is frozen at least since the location was created.
 A shared reference with interior mutability is active is `Raw` is on top of the stack.
 
 A shared reference without interior mutability is active if the location is frozen at least since the location was created.
 A shared reference with interior mutability is active is `Raw` is on top of the stack.
 

-Whenever a reference is used to do something (anything), we make sure that it is active for all locations that it covers; this can involve unfreezing and popping the stack.
-If it is not possible to activate the reference this way, we have UB.
+Whenever a reference is used to do something (anything), we make sure that it is active again for all locations that it covers; this can involve unfreezing and popping the stack.
+If it is not possible to reactivate the reference this way, we have UB.
+
+**Update:** I previously talked about "activating" the reference instead of "reactivating it"; I decided to change terminology to make it clearer that this is an old reference being used again, so it must be on the stack already (but might not be at the top). **/Update**

 
 ## 3 Tracking Borrows
 
 
 ## 3 Tracking Borrows
 


@@ -196,7 +204,7 @@ However, I now came to the conclusion that tagging pointers is a price worth pay
 
 I hope you now have a clear idea of the basic structure of the model I am proposing: The stack of borrows, the freeze flag, and references tagged with the time at which they got created.
 The full model is not quite as simple, but it is not much more complicated either.
 
 I hope you now have a clear idea of the basic structure of the model I am proposing: The stack of borrows, the freeze flag, and references tagged with the time at which they got created.
 The full model is not quite as simple, but it is not much more complicated either.

-We need two add just two more concepts: Retagging and barriers.
+We need to add just two more concepts: Retagging and barriers.

 
 ### 4.1 Retagging
 
 
 ### 4.1 Retagging
 


@@ -227,7 +235,7 @@ In particular, two different references can never be both "active" for the same
 
 With this additional step, it is now easy to argue that `demo4` above is UB when `x` and `y` alias, no matter their initial tag:
 After using `x`, we know it is active.
 
 With this additional step, it is now easy to argue that `demo4` above is UB when `x` and `y` alias, no matter their initial tag:
 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.
+Next we use and reactivate `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 ever pushed when it is created, so it is never in the stack more than once.)
 
 Finally, we use `x` again even though it is no longer in the stack, triggering UB.
 (A `Uniq` is only ever pushed when it is created, so it is never in the stack more than once.)
 


@@ -260,20 +268,20 @@ To this end, I propose to turn the dial a little more towards a validity-based m
 We want to ensure that turning the integer `y` into a reference does not pop `x` from the stack and continue executing the program (we want UB instead).
 This could happen if the stack contained, somewhere, a `Raw`.
 Remember that we do not tag raw pointers, so when a raw pointer was involved in creating `x`, that `Raw` item will still be on the stack, enabling any raw pointer to be used to access this location.
 We want to ensure that turning the integer `y` into a reference does not pop `x` from the stack and continue executing the program (we want UB instead).
 This could happen if the stack contained, somewhere, a `Raw`.
 Remember that we do not tag raw pointers, so when a raw pointer was involved in creating `x`, that `Raw` item will still be on the stack, enabling any raw pointer to be used to access this location.

-This is sometimes crucial, but in this case, `demo5` should be able to prevent those old historic borrows involved in creating `x` from being activated.
+This is sometimes crucial, but in this case, `demo5` should be able to prevent those old historic borrows involved in creating `x` from being reactivated.

 
 The idea is to put a "barrier" into the stack of all function arguments when `demo5` gets called, and to make it UB to pop that barrier from the stack before `demo5` returns.
 
 The idea is to put a "barrier" into the stack of all function arguments when `demo5` gets called, and to make it UB to pop that barrier from the stack before `demo5` returns.

-This way, all the borrows further down in the stack (below `Uniq(x)`) are temporarily disabled and cannot be activated while `demo5` runs.
-This means that even if `y` happens to be the memory address `x` points to, it is UB to cast `y` to a reference because the `Raw` item cannot be activated.
+This way, all the borrows further down in the stack (below `Uniq(x)`) are temporarily disabled and cannot be reactivated while `demo5` runs.
+This means that even if `y` happens to be the memory address `x` points to, it is UB to cast `y` to a reference because the `Raw` item cannot be reactivated.

 
 Another way to think about barriers is as follows:
 The model generally ignores lifetimes and does not know how long they last.
 
 Another way to think about barriers is as follows:
 The model generally ignores lifetimes and does not know how long they last.

-All we know is that when a reference is used, its lifetime must be ongoing, so we say that is when we activate the borrow.
+All we know is that when a reference is used, its lifetime must be ongoing, so we say that is when we reactivate the borrow.

 On top of this, barriers encode the fact that, when a reference is passed as an argument to a function, then its lifetime (whatever it is) extends beyond the current function call.
 In our example, this means that no borrow further up the stack (these are the borrows with even longer lifetimes) can be used while `demo5` is running.
 
 A nice side-effect of barriers in combination with renumbering is that even if `demo4` from the previous subsection would not use its arguments at all, it would *still* be UB to call it with two aliasing references:
 On top of this, barriers encode the fact that, when a reference is passed as an argument to a function, then its lifetime (whatever it is) extends beyond the current function call.
 In our example, this means that no borrow further up the stack (these are the borrows with even longer lifetimes) can be used while `demo5` is running.
 
 A nice side-effect of barriers in combination with renumbering is that even if `demo4` from the previous subsection would not use its arguments at all, it would *still* be UB to call it with two aliasing references:

-When renumbering `x`, we are pushing a barrier. Renumbering `y` would attempt to activate `Uniq(y)`, but that can only be behind the barrier, so it cannot be activated.
+When renumbering `x`, we are pushing a barrier. Renumbering `y` would attempt to reactivate `Uniq(y)`, but that can only be behind the barrier, so it cannot be reactivated.

 
 ## 5 The Model in Code
 
 
 ## 5 The Model in Code
 


@@ -344,8 +352,8 @@ impl MemoryByte {
     }
   }
 
     }
   }
 

-  /// Activate the given existing borrow for this location, fail if that is not possible.
-  fn activate(&mut self, bor: Borrow) {
+  /// Reactivate the given existing borrow for this location, fail if that is not possible.
+  fn reactivate(&mut self, bor: Borrow) {

     // Do NOT change anything if `bor` is already active -- in particular, if
     // it is a `Mut(Raw)` and we are frozen.
     if self.check(bor) { return; }
     // Do NOT change anything if `bor` is already active -- in particular, if
     // it is a `Mut(Raw)` and we are frozen.
     if self.check(bor) { return; }


@@ -359,7 +367,7 @@ impl MemoryByte {
     while let Some(itm) = self.borrows.last() {
       match itm {
         FnBarrier(_) => {
     while let Some(itm) = self.borrows.last() {
       match itm {
         FnBarrier(_) => {

-          bail!("Trying to activate a borrow that lives behind a barrier");
+          bail!("Trying to reactivate a borrow that lives behind a barrier");

         }
         Mut(loc_m) => {
           if loc_m == acc_m { return; }
         }
         Mut(loc_m) => {
           if loc_m == acc_m { return; }


@@ -367,7 +375,7 @@ impl MemoryByte {
         }
       }
     }
         }
       }
     }

-    bail!("Borrow-to-activate does not exist on the stack");
+    bail!("Borrow-to-reactivate does not exist on the stack");

   }
 
   /// Initiate the given (new) borrow for the location.
   }
 
   /// Initiate the given (new) borrow for the location.


@@ -420,17 +428,17 @@ We use `bor` to refer to the `Borrow` of the pointer we are working on.
 Now we can look at what happens for each operation.
 
 * Using a raw pointer directly is desugared to creating a shared reference (when reading) or a mutable reference (when writing), and using that. The appropriate steps below apply.
 Now we can look at what happens for each operation.
 
 * Using a raw pointer directly is desugared to creating a shared reference (when reading) or a mutable reference (when writing), and using that. The appropriate steps below apply.

-* Any time we use a (mutable or shared) reference to access memory, and any time we pass a reference to "the outside world" (passing it to a function, storing it in memory, returning it to our caller; also below structs or enums but not below unions or pointer indirectons), we activate.
-  - `loc.activate(borrow)`.
+* Any time we use a (mutable or shared) reference to access memory, and any time we pass a reference to "the outside world" (passing it to a function, storing it in memory, returning it to our caller; also below structs or enums but not below unions or pointer indirectons), we reactivate.
+  - `loc.reactivate(borrow)`.

 * Any time a *new* reference is created (any time we run an expression `&mut foo` or `&foo`), we (re)borrow.
   - Bump up the clock, and remember the old time as `new_tag`.
   - Compute `new_bor` from `new_tag` and the type of the reference being created.
   - `if loc.check(new_bor) {`
     * The new borrow is already active! This can happen because a mutable reference can be shared multiple times. We do not do anything else.
 * Any time a *new* reference is created (any time we run an expression `&mut foo` or `&foo`), we (re)borrow.
   - Bump up the clock, and remember the old time as `new_tag`.
   - Compute `new_bor` from `new_tag` and the type of the reference being created.
   - `if loc.check(new_bor) {`
     * The new borrow is already active! This can happen because a mutable reference can be shared multiple times. We do not do anything else.

-      As a special exception, we do *not* activate `bor` even though it is "used", because that would unfreeze the location!
+      As a special exception, we do *not* reactivate `bor` even though it is "used", because that would unfreeze the location!

 
     `} else {`
 
     `} else {`

-    * We might be creating a reference to a local variable. In that case, `loc.reset()`. Otherwise, `activate(bor)`.
+    * We might be creating a reference to a local variable. In that case, `loc.reset()`. Otherwise, `reactivate(bor)`.

     * `initiate(new_bor)`
 
     `}`
     * `initiate(new_bor)`
 
     `}`


@@ -438,16 +446,17 @@ Now we can look at what happens for each operation.
 * Any time a reference is passed to us from "the outside world" (as function argument, loaded from memory, or returned from a callee; also below structs or enums but not below unions or pointer indirectons), we retag.
   - Bump up the clock, and remember the old time as `new_tag`.
   - Compute `new_bor` from `new_tag` and the type of the reference being created.
 * Any time a reference is passed to us from "the outside world" (as function argument, loaded from memory, or returned from a callee; also below structs or enums but not below unions or pointer indirectons), we retag.
   - Bump up the clock, and remember the old time as `new_tag`.
   - Compute `new_bor` from `new_tag` and the type of the reference being created.

-  - `activate(bor)`.
+  - `reactivate(bor)`.

   - If this is a function argument coming in: `loc.borrows.push(FnBarrier(stack_height))`.
   - If this is a function argument coming in: `loc.borrows.push(FnBarrier(stack_height))`.

-  - `initiate(new_bor)`. Note that this is a NOP if `new_bor` is already active -- in particular, if the location is frozen and this is a shared reference with interior mutability, we do *not* push anything on top of the barrier. This is important, because we do not want to push that might unfreeze the location when being activated.
+  - `initiate(new_bor)`. Note that this is a NOP if `new_bor` is already active -- in particular, if the location is frozen and this is a shared reference with interior mutability, we do *not* push anything on top of the barrier. This is important, because any reactivation that unfreezes this location must lead to UB while the barrier is still present.

   - Change reference tag to `new_tag`.
 * Any time a raw pointer is created from a reference, we might have to do a raw reborrow.
   - Change reference tag to `new_tag`.
 * Any time a raw pointer is created from a reference, we might have to do a raw reborrow.

-  - `activate(bor)`.
+  - `reactivate(bor)`.

   - `initiate(Mut(Raw))`. This is a NOP when coming from a shared reference.
 * Any time a function returns, we have to clean up the barriers.
   - Iterate over all of memory and remove the matching `FnBarrier`. This is where the "stack" becomes a bit of a lie, because we also remove barriers from the middle of a stack.<br>
     This could be optimized by adding an indirection, so we just have to record somewhere that this function call has ended.
   - `initiate(Mut(Raw))`. This is a NOP when coming from a shared reference.
 * Any time a function returns, we have to clean up the barriers.
   - Iterate over all of memory and remove the matching `FnBarrier`. This is where the "stack" becomes a bit of a lie, because we also remove barriers from the middle of a stack.<br>
     This could be optimized by adding an indirection, so we just have to record somewhere that this function call has ended.

+* Any time memory is deallocated, this counts as mutation, so the usual rules for that apply. After that, the stacks of the deallocated bytes must not contain any barriers.

 
 
 If you want to test your own understanding of "Stacked Borrows", I invite you to go back to [Section 2.2 of "Types as Contracts"]({% post_url 2017-07-17-types-as-contracts %}#22-examples) and look at the three examples here.
 
 
 If you want to test your own understanding of "Stacked Borrows", I invite you to go back to [Section 2.2 of "Types as Contracts"]({% post_url 2017-07-17-types-as-contracts %}#22-examples) and look at the three examples here.