From 78216bc120c8145c96be5c2702e36fc06c894d5c Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Tue, 18 Jul 2017 10:59:37 -0700 Subject: [PATCH] example typos and generally improve ref example --- personal/_posts/2017-07-17-types-as-contracts.md | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/personal/_posts/2017-07-17-types-as-contracts.md b/personal/_posts/2017-07-17-types-as-contracts.md index e01e750..4d791f2 100644 --- a/personal/_posts/2017-07-17-types-as-contracts.md +++ b/personal/_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)) { - Validate(Acquire, [x, y]); + Validate(Acquire, [x, y, z]); 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]); @@ -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`. -(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`. -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. -- 2.30.2