Trait miri::concurrency::data_race::EvalContextExt

source · [−]
pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {

Show 14 methods    fn allow_data_races_ref<R>(
        &self,
        op: impl FnOnce(&MiriEvalContext<'mir, 'tcx>) -> R
    ) -> R { ... }
    fn allow_data_races_mut<R>(
        &mut self,
        op: impl FnOnce(&mut MiriEvalContext<'mir, 'tcx>) -> R
    ) -> R { ... }
    fn read_scalar_at_offset_atomic(
        &self,
        op: &OpTy<'tcx, Tag>,
        offset: u64,
        layout: TyAndLayout<'tcx>,
        atomic: AtomicReadOrd
    ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> { ... }
    fn write_scalar_at_offset_atomic(
        &mut self,
        op: &OpTy<'tcx, Tag>,
        offset: u64,
        value: impl Into<ScalarMaybeUninit<Tag>>,
        layout: TyAndLayout<'tcx>,
        atomic: AtomicWriteOrd
    ) -> InterpResult<'tcx> { ... }
    fn read_scalar_atomic(
        &self,
        place: &MPlaceTy<'tcx, Tag>,
        atomic: AtomicReadOrd
    ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> { ... }
    fn write_scalar_atomic(
        &mut self,
        val: ScalarMaybeUninit<Tag>,
        dest: &MPlaceTy<'tcx, Tag>,
        atomic: AtomicWriteOrd
    ) -> InterpResult<'tcx> { ... }
    fn atomic_op_immediate(
        &mut self,
        place: &MPlaceTy<'tcx, Tag>,
        rhs: &ImmTy<'tcx, Tag>,
        op: BinOp,
        neg: bool,
        atomic: AtomicRwOrd
    ) -> InterpResult<'tcx, ImmTy<'tcx, Tag>> { ... }
    fn atomic_exchange_scalar(
        &mut self,
        place: &MPlaceTy<'tcx, Tag>,
        new: ScalarMaybeUninit<Tag>,
        atomic: AtomicRwOrd
    ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> { ... }
    fn atomic_min_max_scalar(
        &mut self,
        place: &MPlaceTy<'tcx, Tag>,
        rhs: ImmTy<'tcx, Tag>,
        min: bool,
        atomic: AtomicRwOrd
    ) -> InterpResult<'tcx, ImmTy<'tcx, Tag>> { ... }
    fn atomic_compare_exchange_scalar(
        &mut self,
        place: &MPlaceTy<'tcx, Tag>,
        expect_old: &ImmTy<'tcx, Tag>,
        new: ScalarMaybeUninit<Tag>,
        success: AtomicRwOrd,
        fail: AtomicReadOrd,
        can_fail_spuriously: bool
    ) -> InterpResult<'tcx, Immediate<Tag>> { ... }
    fn validate_atomic_load(
        &self,
        place: &MPlaceTy<'tcx, Tag>,
        atomic: AtomicReadOrd
    ) -> InterpResult<'tcx> { ... }
    fn validate_atomic_store(
        &mut self,
        place: &MPlaceTy<'tcx, Tag>,
        atomic: AtomicWriteOrd
    ) -> InterpResult<'tcx> { ... }
    fn validate_atomic_rmw(
        &mut self,
        place: &MPlaceTy<'tcx, Tag>,
        atomic: AtomicRwOrd
    ) -> InterpResult<'tcx> { ... }
    fn validate_atomic_fence(
        &mut self,
        atomic: AtomicFenceOrd
    ) -> InterpResult<'tcx> { ... }

}

Provided Methods

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.
  • The memory being accessed should be treated as internal state, that cannot be accessed by the interpreted program.
  • Execution of the interpreted program execution has halted.

Same as allow_data_races_ref, this temporarily disables any data-race detection and so should only be used for atomic operations or internal state that the program cannot access.

Atomic variant of read_scalar_at_offset.

Atomic variant of write_scalar_at_offset.

Perform an atomic read operation at the memory location.

Perform an atomic write operation at the memory location.

Perform an atomic operation on a memory location.

Perform an atomic exchange with a memory place and a new scalar value, the old value is returned.

Perform an conditional atomic exchange with a memory place and a new scalar value, the old value is returned.

Perform an atomic compare and exchange at a given memory location. On success an atomic RMW operation is performed and on failure only an atomic read occurs. If can_fail_spuriously is true, then we treat it as a “compare_exchange_weak” operation, and some portion of the time fail even when the values are actually identical.

Update the data-race detector for an atomic read occurring at the associated memory-place and on the current thread.

Update the data-race detector for an atomic write occurring at the associated memory-place and on the current thread.

Update the data-race detector for an atomic read-modify-write occurring at the associated memory place and on the current thread.

Update the data-race detector for an atomic fence on the current thread.

Implementors

Evaluation context extensions.