Skip to content

Commit 9872d9e

Browse files
authored
Merge pull request rust-lang#343 from RalfJung/sb
adjust Stacked Borrows spec to allow deallocation of &UnsafeCell
2 parents 8cd1cc5 + ae47b93 commit 9872d9e

File tree

1 file changed

+25
-16
lines changed

1 file changed

+25
-16
lines changed

wip/stacked-borrows.md

+25-16
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,16 @@ Stacked Borrows is also the subject of the following blog-posts:
1515
* [Stacked Borrows 2.0](https://www.ralfj.de/blog/2019/04/30/stacked-borrows-2.html) is a re-design of Stacked Borrows 1 that maintains the original core ideas, but changes the mechanism to support more precise tracking of shared references.
1616
* [Stacked Borrows 2.1](https://www.ralfj.de/blog/2019/05/21/stacked-borrows-2.1.html) slightly tweaks the rules for read and write accesses and describes a high-level way of thinking about the new shape of the "stack" in Stacked Borrows 2.
1717

18-
Changes compared to the latest post (2.1):
18+
Changes from to the latest post (2.1) to the paper:
1919

2020
* Retags are "shallow" instead of recursively looking for references inside compound types.
2121
* Reborrowing of a shared reference, when searching for `UnsafeCell`, no longer reads enum discriminants. It treats enums like unions now.
2222

23+
Changes since publication of the paper:
24+
25+
* HACK: Mutable references to `!Unpin` types do not make uniqueness assumptions.
26+
* Items with `SharedReadWrite` permission are not protected even with `FnEntry` retagging.
27+
2328
[Miri]: https://github.com/solson/miri/
2429
[all-hands]: https://paper.dropbox.com/doc/Topic-Stacked-borrows--AXAkoFfUGViWL_PaSryqKK~hAg-2q57v4UM7cIkxCq9PQc22
2530

@@ -283,11 +288,11 @@ fn reborrow(
283288

284289
We will grant `new_tag` permission for all the locations covered by this place, by calling `grant` for each location.
285290
The parent tag (`derived_from`) is given by the place.
286-
If the reborrow is protected, the new item will have its protector set to the `CallId` of the current function call (i.e., of the topmost frame in the call stack).
287291
The interesting question is which permission to use for the new item:
288-
- For non-two-phase `Unique`, the permission is `Unique`.
289-
- For mutable raw pointers and two-phase `Unique`, the permission is `SharedReadWrite`.
290-
- For `Shared`, the permission is different for locations inside of and outside of `UnsafeCell`.
292+
- For non-two-phase `Unique` to an `Unpin` type, the permission is `Unique`.
293+
(The `Unpin` exception is a special hack to avoid soundness issues due to self-referential generators.)
294+
- For mutable raw pointers and the remaining `Unique`, the permission is `SharedReadWrite`.
295+
- For `Shared` and immutable raw pointers, the permission is different for locations inside of and outside of `UnsafeCell`.
291296
Inside `UnsafeCell`, it is `SharedReadWrite`; outside it is `SharedReadOnly`.
292297
- The `UnsafeCell` detection is entirely static: it recurses through structs,
293298
tuples and the like, but when hitting an `enum` or `union` or so, it treats
@@ -296,24 +301,28 @@ The interesting question is which permission to use for the new item:
296301
memory accesses that are subject to Stacked Borrows rules.
297302
- For immutable raw pointers, the rules are the same as for `Shared`.
298303

304+
If the reborrow is protected and we are not inside an `UnsafeCell` behind a `Shared` or an immutable raw pointer,
305+
the new item will have its protector set to the `CallId` of the current function call (i.e., of the topmost frame in the call stack).
306+
Otherwise the new item will not have a protector.
307+
299308
So, basically, for every location, we call `grant` like this:
300309
```rust
310+
let (perm, protect) = match ref_kind {
311+
RefKind::Unique { two_phase: false } if unpin =>
312+
(Permission::Unique, protect),
313+
RefKind::Raw { mutable: true } |
314+
RefKind::Unique { .. } =>
315+
(Permission::SharedReadWrite, protect),
316+
RefKind::Raw { mutable: false } |
317+
RefKind::Shared =>
318+
if inside_unsafe_cell { (Permission::SharedReadWrite, /* do not protect */ false) }
319+
else { (Permission::SharedReadOnly, protect) }
320+
};
301321
let protector = if protect {
302322
Some(current_call_id())
303323
} else {
304324
None
305325
};
306-
let perm = match ref_kind {
307-
RefKind::Unique { two_phase: false } =>
308-
Permission::Unique,
309-
RefKind::Raw { mutable: true } |
310-
RefKind::Unique { two_phase: true } =>
311-
Permission::SharedReadWrite,
312-
RefKind::Raw { mutable: false } |
313-
RefKind::Shared =>
314-
if inside_unsafe_cell { Permission::SharedReadWrite }
315-
else { Permission::SharedReadOnly }
316-
};
317326

318327
location.stack.grant(
319328
place.tag,

0 commit comments

Comments
 (0)