example typos and generally improve ref example

diff --git a/ralf/_posts/2017-07-17-types-as-contracts.md b/ralf/_posts/2017-07-17-types-as-contracts.md
index e01e7509c059e3abc1267c36183148f08ad033f6..4d791f2c9ea4c6915ba567c87e1a06dfac5db58b 100644 (file)
--- a/ralf/_posts/2017-07-17-types-as-contracts.md
+++ b/ralf/_posts/2017-07-17-types-as-contracts.md
@@ -240,12 +240,12 @@ Overall, our code now looks like this (with all reborrowing being explicit):
 // Defined elsewhere: fn fun<'z>(x: &i32, z: &'z mut (i32, i32)) -> &'z mut i32  { ... }
 
 fn example(x: &i32, y: &mut i32, z: &mut (i32, i32)) {
 // Defined elsewhere: fn fun<'z>(x: &i32, z: &'z mut (i32, i32)) -> &'z mut i32  { ... }
 
 fn example(x: &i32, y: &mut i32, z: &mut (i32, i32)) {

-    Validate(Acquire, [x, y]);
+    Validate(Acquire, [x, y, z]);

     let x_val = *x;
     let y_val = *y;
 
     {   // 'inner begins here
     let x_val = *x;
     let y_val = *y;
 
     {   // 'inner begins here

-        Validate(Suspend('z), [z]);
+        Validate(Suspend('inner), [z]);

         let z_for_fun = &'inner mut z;
         Validate(Acquire, [z_for_fun]);
 
         let z_for_fun = &'inner mut z;
         Validate(Acquire, [z_for_fun]);
 


@@ -268,12 +268,15 @@ When `z` gets reborrowed to be passed to `fun` with lifetime `'inner`, we *suspe
 This models the fact that, no matter what we do with the newly created reference, we know that when `'inner` ends, we get our exclusive access back.
 After the suspension, we don't hold a lock any more for what is now `*z_for_fun`, so we immediately acquire a write lock again.
 However, following the type of `z_for_fun`, we will acquire this lock only for lifetime `'inner`.
 This models the fact that, no matter what we do with the newly created reference, we know that when `'inner` ends, we get our exclusive access back.
 After the suspension, we don't hold a lock any more for what is now `*z_for_fun`, so we immediately acquire a write lock again.
 However, following the type of `z_for_fun`, we will acquire this lock only for lifetime `'inner`.

-(Releasing and then acquiring the write lock may sound somewhat redundant.
-However, notice that, if we were to take a shared reference, we would now acquire a read lock rather than a write lock.)
+(Suspending and then acquiring the write lock may sound somewhat redundant.
+However, notice that, if we were to take a shared reference, we would now acquire a read lock rather than a write lock.
+Furthermore, even here, the overall effect is far from a no-op: The suspended lock will stay around even if the reacquired lock is released.  In fact, this is exactly what happens next.)

 
 Next, we call `fun`.
 
 Next, we call `fun`.

-At this point, we release our write lock on `*z_for_fun` again.
-However, notice that the suspended lock of `*z` stays around -- so while we gave up control of `z` (aka `z_for_fun`) for lifetime `'inner`, we still know that we will get control back when `'inner` ends!
+At this point, we release our write lock on `*z_for_fun` again, as usual when passing a mutable reference to a function.
+(The acquire-release of `z_for_fun` is indeed redundant here, but notice that the two validation statements arise from two separate MIR operations:  taking a reference and calling a function.
+These operations just happen to occur just after one another here.)
+However, the suspended lock of `*z` stays around -- so while we gave up control of `z` (aka `z_for_fun`) for lifetime `'inner`, we still know that we will get control back when `'inner` ends!

 `fun` is now free to do whatever it wants, as long as it does not violate our still-existing write lock of `*y` and the read lock of `*x`.
 
 When `fun` returns, we obtain a new mutable reference.
 `fun` is now free to do whatever it wants, as long as it does not violate our still-existing write lock of `*y` and the read lock of `*x`.
 
 When `fun` returns, we obtain a new mutable reference.