Skip to content

Commit

Permalink
also document the !Unpin exception
Browse files Browse the repository at this point in the history
  • Loading branch information
RalfJung committed Jun 23, 2022
1 parent 919180b commit ae47b93
Showing 1 changed file with 6 additions and 4 deletions.
10 changes: 6 additions & 4 deletions wip/stacked-borrows.md
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ Changes from to the latest post (2.1) to the paper:

Changes since publication of the paper:

* HACK: Mutable references to `!Unpin` types do not make uniqueness assumptions.
* Items with `SharedReadWrite` permission are not protected even with `FnEntry` retagging.

[Miri]: https://github.com/solson/miri/
Expand Down Expand Up @@ -288,8 +289,9 @@ fn reborrow(
We will grant `new_tag` permission for all the locations covered by this place, by calling `grant` for each location.
The parent tag (`derived_from`) is given by the place.
The interesting question is which permission to use for the new item:
- For non-two-phase `Unique`, the permission is `Unique`.
- For mutable raw pointers and two-phase `Unique`, the permission is `SharedReadWrite`.
- For non-two-phase `Unique` to an `Unpin` type, the permission is `Unique`.
(The `Unpin` exception is a special hack to avoid soundness issues due to self-referential generators.)
- For mutable raw pointers and the remaining `Unique`, the permission is `SharedReadWrite`.
- For `Shared` and immutable raw pointers, the permission is different for locations inside of and outside of `UnsafeCell`.
Inside `UnsafeCell`, it is `SharedReadWrite`; outside it is `SharedReadOnly`.
- The `UnsafeCell` detection is entirely static: it recurses through structs,
Expand All @@ -306,10 +308,10 @@ Otherwise the new item will not have a protector.
So, basically, for every location, we call `grant` like this:
```rust
let (perm, protect) = match ref_kind {
RefKind::Unique { two_phase: false } =>
RefKind::Unique { two_phase: false } if unpin =>
(Permission::Unique, protect),
RefKind::Raw { mutable: true } |
RefKind::Unique { two_phase: true } =>
RefKind::Unique { .. } =>
(Permission::SharedReadWrite, protect),
RefKind::Raw { mutable: false } |
RefKind::Shared =>
Expand Down

0 comments on commit ae47b93

Please sign in to comment.