projects
/
web.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (from parent 1:
b107841
)
say immutable instead of read-only
author
Ralf Jung
<post@ralfj.de>
Thu, 15 Nov 2018 12:50:28 +0000
(13:50 +0100)
committer
Ralf Jung
<post@ralfj.de>
Thu, 15 Nov 2018 12:50:28 +0000
(13:50 +0100)
ralf/_drafts/stacked-borrows-implementation.md
patch
|
blob
|
history
diff --git
a/ralf/_drafts/stacked-borrows-implementation.md
b/ralf/_drafts/stacked-borrows-implementation.md
index ac3624da458cb6f07dcbdef4773b8d483fd8f327..1bc1ef12d0012fd0a09d20eaf6209b2d547947c8 100644
(file)
--- a/
ralf/_drafts/stacked-borrows-implementation.md
+++ b/
ralf/_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
(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
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
## 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:
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`)
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
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
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.
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 %}
}
{% 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
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