From f417d9a042cbd9cb73976c8502d80e8148f56b35 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Thu, 15 Nov 2018 13:50:28 +0100 Subject: [PATCH 1/1] say immutable instead of read-only --- personal/_drafts/stacked-borrows-implementation.md | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/personal/_drafts/stacked-borrows-implementation.md b/personal/_drafts/stacked-borrows-implementation.md index ac3624d..1bc1ef1 100644 --- a/personal/_drafts/stacked-borrows-implementation.md +++ b/personal/_drafts/stacked-borrows-implementation.md @@ -20,7 +20,7 @@ that some things about references always hold true for every valid execution (meaning executions where no [undefined behavior]({% post_url 2017-07-14-undefined-behavior %}) occurred): `&mut` references are unique (we can rely on no accesses by other functions happening to the memory they point -to), and `&` references are read-only (we can rely on no writes happening to the +to), and `&` references are immutable (we can rely on no writes happening to the memory they point to, unless there is an `UnsafeCell`). Usually we have the borrow checker guarding us against such nefarious violations of reference type guarantees, but alas, when we are writing unsafe code, the borrow checker cannot @@ -39,7 +39,7 @@ you only want to know how to help, jump to [section 6]. ## 1 Enforcing Uniqueness -Let us first ignore the part about `&` references being read-only and focus on +Let us first ignore the part about `&` references being immutable and focus on uniqueness of mutable references. Namely, we want to define our model in a way that calling the following function will trigger undefined behavior: @@ -163,7 +163,7 @@ If we just had unique pointers, Rust would be a rather dull language. Luckily enough, there are also two ways to have shared access to a location: through shared references (safely), and through raw pointers (unsafely). Moreover, shared references *sometimes* (but not when they point to an `UnsafeCell`) -assert an additional guarantee: Their destination is read-only. +assert an additional guarantee: Their destination is immutable. For example, we want the following code to be allowed -- not least because this is actually safe code accepted by the borrow checker, so we better make sure @@ -634,7 +634,7 @@ the stack, such that the access through `mut_ref` at the end remains valid. This may sound like a weird rule, and it is. I would surely not have thought of this if `RefCell` would not force our hands here. However, as we shall see in [section 5], it also does not to break any of the important properties of the -model (mutable references being unique and shared references being read-only +model (mutable references being unique and shared references being immutable except for `UnsafeCell`). Moreover, when pushing an item to the stack (at the end of the retag action), we can be sure that the stack is not yet frozen: if it were frozen, the reborrow would be redundant. @@ -786,7 +786,7 @@ fn demo_mut_advanced_unique(our: &mut u8) -> u8 { } {% endhighlight %} -### 5.2 Shared References (without `UnsafeCell)` are Read-only +### 5.2 Shared References (without `UnsafeCell)` are Immutable The key property of shared references is that: After creating (retagging, really) a shared reference, if we then run some unknown code (it can even have -- 2.30.2