Trait miri::concurrency::data_race::EvalContextPrivExt

source · [−]
trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
    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 atomic_access_check(
        &self,
        place: &MPlaceTy<'tcx, Provenance>
    ) -> InterpResult<'tcx> { ... }
    fn validate_atomic_load(
        &self,
        place: &MPlaceTy<'tcx, Provenance>,
        atomic: AtomicReadOrd
    ) -> InterpResult<'tcx> { ... }
    fn validate_atomic_store(
        &mut self,
        place: &MPlaceTy<'tcx, Provenance>,
        atomic: AtomicWriteOrd
    ) -> InterpResult<'tcx> { ... }
    fn validate_atomic_rmw(
        &mut self,
        place: &MPlaceTy<'tcx, Provenance>,
        atomic: AtomicRwOrd
    ) -> InterpResult<'tcx> { ... }
    fn validate_atomic_op<A: Debug + Copy>(
        &self,
        place: &MPlaceTy<'tcx, Provenance>,
        atomic: A,
        description: &str,
        op: impl FnMut(&mut MemoryCellClocks, &mut ThreadClockSet, VectorIdx, A) -> Result<(), DataRace>
    ) -> 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.

Checks that an atomic access is legal at the given place.

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.

Generic atomic operation implementation

Implementors