Skip to content

Commit 919180b

Browse files
committed
adjust Stacked Borrows spec to allow deallocation of &UnsafeCell
See rust-lang/miri#2248 for the Miri change.
1 parent 99c8493 commit 919180b

File tree

1 file changed

+20
-13
lines changed

1 file changed

+20
-13
lines changed

wip/stacked-borrows.md

+20-13
Original file line numberDiff line numberDiff line change
@@ -15,11 +15,15 @@ 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+
* Items with `SharedReadWrite` permission are not protected even with `FnEntry` retagging.
26+
2327
[Miri]: https://github.com/solson/miri/
2428
[all-hands]: https://paper.dropbox.com/doc/Topic-Stacked-borrows--AXAkoFfUGViWL_PaSryqKK~hAg-2q57v4UM7cIkxCq9PQc22
2529

@@ -283,11 +287,10 @@ fn reborrow(
283287

284288
We will grant `new_tag` permission for all the locations covered by this place, by calling `grant` for each location.
285289
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).
287290
The interesting question is which permission to use for the new item:
288291
- For non-two-phase `Unique`, the permission is `Unique`.
289292
- 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`.
293+
- For `Shared` and immutable raw pointers, the permission is different for locations inside of and outside of `UnsafeCell`.
291294
Inside `UnsafeCell`, it is `SharedReadWrite`; outside it is `SharedReadOnly`.
292295
- The `UnsafeCell` detection is entirely static: it recurses through structs,
293296
tuples and the like, but when hitting an `enum` or `union` or so, it treats
@@ -296,23 +299,27 @@ The interesting question is which permission to use for the new item:
296299
memory accesses that are subject to Stacked Borrows rules.
297300
- For immutable raw pointers, the rules are the same as for `Shared`.
298301

302+
If the reborrow is protected and we are not inside an `UnsafeCell` behind a `Shared` or an immutable raw pointer,
303+
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).
304+
Otherwise the new item will not have a protector.
305+
299306
So, basically, for every location, we call `grant` like this:
300307
```rust
301-
let protector = if protect {
302-
Some(current_call_id())
303-
} else {
304-
None
305-
};
306-
let perm = match ref_kind {
308+
let (perm, protect) = match ref_kind {
307309
RefKind::Unique { two_phase: false } =>
308-
Permission::Unique,
310+
(Permission::Unique, protect),
309311
RefKind::Raw { mutable: true } |
310312
RefKind::Unique { two_phase: true } =>
311-
Permission::SharedReadWrite,
313+
(Permission::SharedReadWrite, protect),
312314
RefKind::Raw { mutable: false } |
313315
RefKind::Shared =>
314-
if inside_unsafe_cell { Permission::SharedReadWrite }
315-
else { Permission::SharedReadOnly }
316+
if inside_unsafe_cell { (Permission::SharedReadWrite, /* do not protect */ false) }
317+
else { (Permission::SharedReadOnly, protect) }
318+
};
319+
let protector = if protect {
320+
Some(current_call_id())
321+
} else {
322+
None
316323
};
317324

318325
location.stack.grant(

0 commit comments

Comments
 (0)