This commit is contained in:
Ralf Jung 2024-05-22 11:09:34 +02:00
parent a1bc030b70
commit abbe244a81
3 changed files with 10 additions and 8 deletions

View File

@ -17,6 +17,7 @@ enum PermissionPriv {
/// is relevant
/// - `conflicted` is set on foreign reads,
/// - `conflicted` must not be set on child writes (there is UB otherwise).
///
/// This is so that the behavior of `Reserved` adheres to the rules of `noalias`:
/// - foreign-read then child-write is UB due to `conflicted`,
/// - child-write then foreign-read is UB since child-write will activate and then
@ -339,15 +340,15 @@ pub mod diagnostics {
/// This function assumes that its arguments apply to the same location
/// and that they were obtained during a normal execution. It will panic otherwise.
/// - all transitions involved in `self` and `err` should be increasing
/// (Reserved < Active < Frozen < Disabled);
/// (Reserved < Active < Frozen < Disabled);
/// - between `self` and `err` the permission should also be increasing,
/// so all permissions inside `err` should be greater than `self.1`;
/// so all permissions inside `err` should be greater than `self.1`;
/// - `Active` and `Reserved(conflicted=false)` cannot cause an error
/// due to insufficient permissions, so `err` cannot be a `ChildAccessForbidden(_)`
/// of either of them;
/// due to insufficient permissions, so `err` cannot be a `ChildAccessForbidden(_)`
/// of either of them;
/// - `err` should not be `ProtectedDisabled(Disabled)`, because the protected
/// tag should not have been `Disabled` in the first place (if this occurs it means
/// we have unprotected tags that become protected)
/// tag should not have been `Disabled` in the first place (if this occurs it means
/// we have unprotected tags that become protected)
pub(in super::super) fn is_relevant(&self, err: TransitionError) -> bool {
// NOTE: `super::super` is the visibility of `TransitionError`
assert!(self.is_possible());

View File

@ -230,6 +230,7 @@ mod spurious_read {
/// - any access to the same location
/// - end of one of them being protected
/// - a retag that would change their relative position
///
/// The type `TestEvent` models these kinds of events.
///
/// In order to prevent `x` or `y` from losing their protector,

View File

@ -1106,9 +1106,9 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriInterpCxExt<'mir, 'tcx> {
/// Temporarily allow data-races to occur. This should only be used in
/// one of these cases:
/// - One of the appropriate `validate_atomic` functions will be called to
/// to treat a memory access as atomic.
/// treat a memory access as atomic.
/// - The memory being accessed should be treated as internal state, that
/// cannot be accessed by the interpreted program.
/// cannot be accessed by the interpreted program.
/// - Execution of the interpreted program execution has halted.
#[inline]
fn allow_data_races_ref<R>(&self, op: impl FnOnce(&MiriInterpCx<'mir, 'tcx>) -> R) -> R {