Auto merge of #3031 - RalfJung:foreign-read, r=RalfJung
tree borrows: more comments in foreign_read transition
This commit is contained in:
commit
23b9d9558c
@ -68,17 +68,31 @@ fn child_read(state: PermissionPriv, _protected: bool) -> Option<PermissionPriv>
|
|||||||
fn foreign_read(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
|
fn foreign_read(state: PermissionPriv, protected: bool) -> Option<PermissionPriv> {
|
||||||
use Option::*;
|
use Option::*;
|
||||||
Some(match state {
|
Some(match state {
|
||||||
|
// Non-writeable states just ignore foreign reads.
|
||||||
|
non_writeable @ (Frozen | Disabled) => non_writeable,
|
||||||
|
// Writeable states are more tricky, and depend on whether things are protected.
|
||||||
// The inner data `ty_is_freeze` of `Reserved` is always irrelevant for Read
|
// The inner data `ty_is_freeze` of `Reserved` is always irrelevant for Read
|
||||||
// accesses, since the data is not being mutated. Hence the `{ .. }`
|
// accesses, since the data is not being mutated. Hence the `{ .. }`
|
||||||
res @ Reserved { .. } if !protected => res,
|
res @ Reserved { .. } =>
|
||||||
Reserved { .. } => Frozen, // protected reserved
|
if protected {
|
||||||
|
// Someone else read, make sure we won't write.
|
||||||
|
// We could make this `Disabled` but it doesn't look like we get anything out of that extra UB.
|
||||||
|
Frozen
|
||||||
|
} else {
|
||||||
|
// Before activation and without protectors, foreign reads are fine.
|
||||||
|
// That's the entire point of 2-phase borrows.
|
||||||
|
res
|
||||||
|
},
|
||||||
Active =>
|
Active =>
|
||||||
if protected {
|
if protected {
|
||||||
|
// We wrote, someone else reads -- that's bad.
|
||||||
|
// (If this is initialized, this move-to-protected will mean insta-UB.)
|
||||||
Disabled
|
Disabled
|
||||||
} else {
|
} else {
|
||||||
|
// We don't want to disable here to allow read-read reordering: it is crucial
|
||||||
|
// that the foreign read does not invalidate future reads through this tag.
|
||||||
Frozen
|
Frozen
|
||||||
},
|
},
|
||||||
non_writeable @ (Frozen | Disabled) => non_writeable,
|
|
||||||
})
|
})
|
||||||
}
|
}
|
||||||
|
|
||||||
|
Loading…
Reference in New Issue
Block a user