Skip to content

Commit 11f6c9b

Browse files
committed
update to stacked borrows 2.1
1 parent 3b853a7 commit 11f6c9b

File tree

1 file changed

+61
-92
lines changed

1 file changed

+61
-92
lines changed

wip/stacked-borrows.md

Lines changed: 61 additions & 92 deletions
Original file line numberDiff line numberDiff line change
@@ -41,8 +41,11 @@ pub enum Permission {
4141
Unique,
4242
/// Grants shared mutable access.
4343
SharedReadWrite,
44-
/// Greants shared read-only access.
44+
/// Grants shared read-only access.
4545
SharedReadOnly,
46+
/// Grants no access, but separates two groups of SharedReadWrite so they are not
47+
/// all considered mutually compatible.
48+
Disabled,
4649
}
4750

4851
/// An item on the per-location stack, controlling which pointers may access this location and how.
@@ -55,10 +58,12 @@ pub struct Item {
5558
protector: Option<CallId>,
5659
}
5760
/// Per-location stack of borrow items.
58-
/// Making use of an item towards the bottom of the stack removes all the items above it that are
59-
/// "incompatible" (see below).
6061
pub struct Stack {
61-
borrows: Vec<Item>, // used *mostly* as a stack; never empty
62+
/// Used *mostly* as a stack; never empty.
63+
/// Invariants:
64+
/// * Above a `SharedReadOnly` there can only be more `SharedReadOnly`.
65+
/// * Except for `Untagged`, no tag occurs in the stack more than once.
66+
borrows: Vec<Item>,
6267
}
6368

6469
/// Extra per-call-frame state: the ID of this function call.
@@ -163,89 +168,34 @@ pub enum AccessKind {
163168

164169
/// This defines for a given permission, whether it permits the given kind of access.
165170
fn grants(self: Permission, access: AccessKind) -> bool {
166-
match (self, access) {
167-
// Unique and SharedReadWrite allow any kind of access.
168-
(Permission::Unique, _) |
169-
(Permission::SharedReadWrite, _) =>
170-
true,
171-
// SharedReadOnly only permits read access.
172-
(Permission::SharedReadOnly, AccessKind::Read) =>
173-
true,
174-
(Permission::SharedReadOnly, AccessKind::Write) =>
175-
false,
176-
}
171+
// Disabled grants nothing. Otherwise, all items grant read access, and except for SharedReadOnly they grant write access.
172+
self != Permission::Disabled && (access == AccessKind::Read || self != Permission::SharedReadOnly)
177173
}
178174
```
179175

180176
Based on this, we define the *granting* item in a stack (for a given tag and access) to be the topmost item that grants the given access to this tag:
181177

182178
```rust
183-
/// Find the item granting the given kind of access to the given tag, and where that item is in the stack.
184-
fn find_granting(self: &Stack, access: AccessKind, tag: Tag) -> Option<(usize, Permission)> {
179+
/// Find the item granting the given kind of access to the given tag, and return where that item is in the stack.
180+
fn find_granting(self: &Stack, access: AccessKind, tag: Tag) -> Option<usize> {
185181
self.borrows.iter()
186182
.enumerate() // we also need to know *where* in the stack
187183
.rev() // search top-to-bottom
188184
// Return permission of first item that grants access.
189185
.find_map(|(idx, item)|
190186
if item.perm.grants(access) && tag == item.tag {
191-
Some((idx, item.perm))
187+
Some(idx)
192188
} else {
193189
None
194190
}
195191
)
196192
}
197193
```
198194

199-
The following table defines whether an item (granting some access) is compatible with another item (living on top of the first in the stack):
200-
201-
|**Granting item** \ **Compatible with**| `Unique` | `SharedReadWrite` | `SharedReadOnly` |
202-
|---:|---|---|---|
203-
|`Unique` | no | only reads | only reads |
204-
|`SharedReadWrite` | no | yes | only reads |
205-
|`SharedReadOnly` | no | no | only reads |
206-
207-
The same is expressed by the following code:
208-
```rust
209-
/// This defines for a given permission, which other permissions it can tolerate "above" itself
210-
/// for which kinds of accesses.
211-
/// If true, then `other` is allowed to remain on top of `self` when `access` happens.
212-
fn compatible_with(self: Permission, access: AccessKind, other: Permission) -> bool {
213-
use self::Permission::*;
214-
215-
match (self, access, other) {
216-
// Some cases are impossible.
217-
(SharedReadOnly, _, SharedReadWrite) |
218-
(SharedReadOnly, _, Unique) =>
219-
bug!("There can never be a SharedReadWrite or a Unique on top of a SharedReadOnly"),
220-
// When `other` is `SharedReadOnly`, that is NEVER compatible with
221-
// write accesses.
222-
// This makes sure read-only pointers become invalid on write accesses (ensures F2a).
223-
(_, AccessKind::Write, SharedReadOnly) =>
224-
false,
225-
// When `other` is `Unique`, that is compatible with nothing.
226-
// This makes sure unique pointers become invalid on incompatible accesses (ensures U2).
227-
(_, _, Unique) =>
228-
false,
229-
// When we are unique and this is a write/dealloc, we tolerate nothing.
230-
// This makes sure we re-assert uniqueness ("being on top") on write accesses.
231-
// (This is particularily important such that when a new mutable ref gets created, it gets
232-
// pushed onto the right item -- this behaves like a write and we assert uniqueness of the
233-
// pointer from which this comes, *if* it was a unique pointer.)
234-
(Unique, AccessKind::Write, _) =>
235-
false,
236-
// `SharedReadWrite` items can tolerate any other akin items for any kind of access.
237-
(SharedReadWrite, _, SharedReadWrite) =>
238-
true,
239-
// Any item can tolerate read accesses for shared items.
240-
// This includes unique items! Reads from unique pointers do not invalidate
241-
// other pointers.
242-
(_, AccessKind::Read, SharedReadWrite) |
243-
(_, AccessKind::Read, SharedReadOnly) =>
244-
true,
245-
// That's it.
246-
}
247-
}
248-
```
195+
In general, the structure of the stack looks as follows:
196+
On the top, we might have a bunch of `SharedReadOnly` items. Below that, we have "blocks" consisting of either a single `Unique` item, or a bunch of consecutive `SharedReadWrite`.
197+
`Disabled` items serve to separate two blocks of `SharedReadWrite` that would otherwise be considered one block.
198+
Using any item within a block is equivalent to using any other item in that same block.
249199

250200
### Allocating memory
251201

@@ -264,51 +214,70 @@ We also initialize the stack of all the memory locations in this new memory allo
264214
On every memory access, we perform the following extra operation for every location that gets accessed (i.e., for a 4-byte access, this happens for each of the 4 bytes):
265215

266216
1. Find the granting item. If there is none, this is UB.
267-
2. For every item `item` above the granting item in the stack: if the granting item is not compatible with `item`, remove `item` from the stack.
268-
If furthermore `item` is protected (`item.protector.is_some()`) by an active call, this is UB.
217+
2. Check if this is a read access or a write access.
218+
- For write accesses, pop all *blocks* above the one containing the granting item. That is, remove all items above the granting one, except if the granting item is a `SharedReadWrite` in which case the consecutive `SharedReadWrite` above it are kept (but everything beyond is popped).
219+
- For read accesses, disable all `Unique` items above the granting one: change their permission to `Disabled`. This means they cannot be used any more. We do not remove them from the stack to avoid merging two blocks of `SharedReadWrite`.
269220

270221
### Reborrowing
271222

272223
Adding new permissions to the stack happens by reborrowing pointers.
273224

274225
**Granting a pointer permission to a location.**
275-
To grant new permissions to a location, we need a parent tag (the tag of the pointer from which the new pointer is derived), an `Item` for the newly created pointer that should be added to the stack (this indicates both which pointer is granted access and what the permission is), and a boolean indicating whether this is a "weak" or a "strong" grant operation.
276-
As a signature, this would be
226+
To grant new permissions to a location, we need a parent tag (the tag of the pointer from which the new pointer is derived), and an `Item` for the newly created pointer that should be added to the stack (this indicates both which pointer is granted access and what the permission is).
227+
As a Rust signature, this would be:
277228
```rust
278229
fn grant(
279230
self: &mut Stacks,
280231
derived_from: Tag,
281-
weak: bool,
282232
new: Item,
283233
)
284234
```
285235
We proceed as follows:
286236

287237
1. Find the granting item for the parent tag. If there is none, this is UB.
288-
2. Check if we are operating weakly or strongly.
289-
- If we are working weakly, just add the item directly above the granting item in the stack.
290-
- For strong grant operations, perform the actions of an access (this is a write access if `new.perm.grants(AccessKind::Write)`, i.e. if the new item grants write permission, and a read access otherwise).
238+
2. Check if we are adding a `SharedReadWrite`.
239+
- If yes, add the new item on top of the current block.
240+
- If no, perform the actions of an access (this is a write access if `new.perm.grants(AccessKind::Write)`, i.e. if the new item grants write permission, and a read access otherwise).
291241
Then push the new item to the top of the stack.
292242

293243
**Reborrowing a pointer.**
294244
To reborrow a pointer, we are given:
295-
- a (typed) place, i.e., a location in memory, a tag, a size (saying how many bytes this place covers) and the type of the data we expect there;
245+
- a (typed) place, i.e., a location in memory, a tag and the type of the data we expect there (from which we can compute the size);
296246
- which kind of reference/pointer this is (`Unique`, `Shared` or a raw pointer which might be mutable or not);
297247
- a `new_tag: Tag` for the reborrowed pointer;
298-
- whether this reborrow needs to be protected and/or is forced to be "weak".
248+
- whether this reborrow needs to be protected.
299249

300-
We will grant `new_tag` permission for all the locations covered by this place.
301-
The parent tag is given by the place.
250+
The type of the place and the kind of reference/pointer together give the full type of the reference/pointer (or as much of it was we need).
251+
As a Rust signature, this would be:
252+
```rust
253+
pub enum RefKind {
254+
/// `&mut` and `Box`.
255+
Unique { two_phase: bool },
256+
/// `&` with or without interior mutability.
257+
Shared,
258+
/// `*mut`/`*const` (raw pointers).
259+
Raw { mutable: bool },
260+
}
261+
262+
fn reborrow(
263+
self: &mut MiriInterpContext,
264+
place: MPlaceTy<Tag>,
265+
kind: RefKind,
266+
new_tag: Tag,
267+
protect: bool,
268+
)
269+
```
270+
271+
We will grant `new_tag` permission for all the locations covered by this place, by calling `grant` for each location.
272+
The parent tag (`derived_from`) is given by the place.
302273
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).
303274
The interesting question is which permission to use for the new item:
304-
- For `Unique`, the permission is `Unique`.
275+
- For non-two-phase `Unique`, the permission is `Unique`.
276+
- For mutable raw pointers and two-phase `Unique`, the permission is `SharedReadWrite`.
305277
- For `Shared`, the permission is different for locations inside of and outside of `UnsafeCell`.
306278
Inside `UnsafeCell`, it is `SharedReadWrite`; outside it is `SharedReadOnly`.
307-
- For mutable raw pointers, the permission is `SharedReadWrite`.
308279
- For immutable raw pointers, the rules are the same as for `Shared`.
309280

310-
The grant will be done weakly if the permission is `SharedReadWrite` or we forced to be "weak".
311-
312281
So, basically, for every location, we call `grant` like this:
313282
```rust
314283
let protector = if protect {
@@ -317,18 +286,19 @@ let protector = if protect {
317286
None
318287
};
319288
let perm = match ref_kind {
320-
RefKind::Unique => Permission::Unique,
321-
RefKind::Raw { mutable: true } => Permission::SharedReadWrite,
289+
RefKind::Unique =>
290+
Permission::Unique,
291+
RefKind::Raw { mutable: true } |
292+
RefKind::Unique { two_phase: true } =>
293+
Permission::SharedReadWrite,
322294
RefKind::Raw { mutable: false } |
323295
RefKind::Shared =>
324-
if inside_unsafe_cell { Permission::SharedReadWrite }
325-
else { Permission::SharedReadOnly }
296+
if inside_unsafe_cell { Permission::SharedReadWrite }
297+
else { Permission::SharedReadOnly }
326298
};
327-
let weak = (perm == Permission::SharedReadWrite) || force_weak;
328299

329300
location.stack.grant(
330301
place.tag,
331-
weak,
332302
Item { tag: new_tag, perm, protector }
333303
);
334304
```
@@ -341,8 +311,7 @@ For each reference (`&[mut] _`) and box (`Box<_>`) we encounter, and if `kind ==
341311
1. We compute a fresh tag: `Untagged` for raw pointers, `Tag(Tracking::new_ptr_id())` for everything else.
342312
2. We determine if we will want to protect the items we are going to generate:
343313
This is the case only if `kind == FnEntry` and the type of this pointer is a reference (not a box).
344-
3. We perform reborrowing of the memory this pointer points to with the new tag and indicating whether we want protection, treating boxes as `Unique`. We enforce weak mode if `kind == TwoPhase`.
345-
4. If `kind == TwoPhase`, we perform *another* reborrow from the *new* place (with the freshly generated tag), with the "new" tag set to the tag of the *old* place and treating it like a shared reference (without protection or forcing weak mode). Basically, we pretend that the old pointer is actually a shared reference derived from the new pointer. This allows reading from the old pointer without invalidating the new one.
314+
3. We perform reborrowing of the memory this pointer points to with the new tag and indicating whether we want protection, treating boxes as `RefKind::Unique`.
346315

347316
### Deallocating memory
348317

0 commit comments

Comments
 (0)