Trait miri::concurrency::data_race::EvalContextExt
source · pub trait EvalContextExt<'tcx>: MiriInterpCxExt<'tcx> {
// Provided methods
fn read_scalar_atomic(
&self,
place: &MPlaceTy<'tcx>,
atomic: AtomicReadOrd,
) -> InterpResult<'tcx, Scalar> { ... }
fn write_scalar_atomic(
&mut self,
val: Scalar,
dest: &MPlaceTy<'tcx>,
atomic: AtomicWriteOrd,
) -> InterpResult<'tcx> { ... }
fn atomic_rmw_op_immediate(
&mut self,
place: &MPlaceTy<'tcx>,
rhs: &ImmTy<'tcx>,
op: BinOp,
not: bool,
atomic: AtomicRwOrd,
) -> InterpResult<'tcx, ImmTy<'tcx>> { ... }
fn atomic_exchange_scalar(
&mut self,
place: &MPlaceTy<'tcx>,
new: Scalar,
atomic: AtomicRwOrd,
) -> InterpResult<'tcx, Scalar> { ... }
fn atomic_min_max_scalar(
&mut self,
place: &MPlaceTy<'tcx>,
rhs: ImmTy<'tcx>,
min: bool,
atomic: AtomicRwOrd,
) -> InterpResult<'tcx, ImmTy<'tcx>> { ... }
fn atomic_compare_exchange_scalar(
&mut self,
place: &MPlaceTy<'tcx>,
expect_old: &ImmTy<'tcx>,
new: Scalar,
success: AtomicRwOrd,
fail: AtomicReadOrd,
can_fail_spuriously: bool,
) -> InterpResult<'tcx, Immediate<Provenance>> { ... }
fn atomic_fence(&mut self, atomic: AtomicFenceOrd) -> InterpResult<'tcx> { ... }
fn allow_data_races_all_threads_done(&mut self) { ... }
fn release_clock<'a>(&'a self) -> Option<Ref<'a, VClock>>
where 'tcx: 'a { ... }
fn acquire_clock(&self, clock: &VClock) { ... }
}
Provided Methods§
sourcefn read_scalar_atomic(
&self,
place: &MPlaceTy<'tcx>,
atomic: AtomicReadOrd,
) -> InterpResult<'tcx, Scalar>
fn read_scalar_atomic( &self, place: &MPlaceTy<'tcx>, atomic: AtomicReadOrd, ) -> InterpResult<'tcx, Scalar>
Perform an atomic read operation at the memory location.
sourcefn write_scalar_atomic(
&mut self,
val: Scalar,
dest: &MPlaceTy<'tcx>,
atomic: AtomicWriteOrd,
) -> InterpResult<'tcx>
fn write_scalar_atomic( &mut self, val: Scalar, dest: &MPlaceTy<'tcx>, atomic: AtomicWriteOrd, ) -> InterpResult<'tcx>
Perform an atomic write operation at the memory location.
sourcefn atomic_rmw_op_immediate(
&mut self,
place: &MPlaceTy<'tcx>,
rhs: &ImmTy<'tcx>,
op: BinOp,
not: bool,
atomic: AtomicRwOrd,
) -> InterpResult<'tcx, ImmTy<'tcx>>
fn atomic_rmw_op_immediate( &mut self, place: &MPlaceTy<'tcx>, rhs: &ImmTy<'tcx>, op: BinOp, not: bool, atomic: AtomicRwOrd, ) -> InterpResult<'tcx, ImmTy<'tcx>>
Perform an atomic RMW operation on a memory location.
sourcefn atomic_exchange_scalar(
&mut self,
place: &MPlaceTy<'tcx>,
new: Scalar,
atomic: AtomicRwOrd,
) -> InterpResult<'tcx, Scalar>
fn atomic_exchange_scalar( &mut self, place: &MPlaceTy<'tcx>, new: Scalar, atomic: AtomicRwOrd, ) -> InterpResult<'tcx, Scalar>
Perform an atomic exchange with a memory place and a new scalar value, the old value is returned.
sourcefn atomic_min_max_scalar(
&mut self,
place: &MPlaceTy<'tcx>,
rhs: ImmTy<'tcx>,
min: bool,
atomic: AtomicRwOrd,
) -> InterpResult<'tcx, ImmTy<'tcx>>
fn atomic_min_max_scalar( &mut self, place: &MPlaceTy<'tcx>, rhs: ImmTy<'tcx>, min: bool, atomic: AtomicRwOrd, ) -> InterpResult<'tcx, ImmTy<'tcx>>
Perform an conditional atomic exchange with a memory place and a new scalar value, the old value is returned.
sourcefn atomic_compare_exchange_scalar(
&mut self,
place: &MPlaceTy<'tcx>,
expect_old: &ImmTy<'tcx>,
new: Scalar,
success: AtomicRwOrd,
fail: AtomicReadOrd,
can_fail_spuriously: bool,
) -> InterpResult<'tcx, Immediate<Provenance>>
fn atomic_compare_exchange_scalar( &mut self, place: &MPlaceTy<'tcx>, expect_old: &ImmTy<'tcx>, new: Scalar, success: AtomicRwOrd, fail: AtomicReadOrd, can_fail_spuriously: bool, ) -> InterpResult<'tcx, Immediate<Provenance>>
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.
sourcefn atomic_fence(&mut self, atomic: AtomicFenceOrd) -> InterpResult<'tcx>
fn atomic_fence(&mut self, atomic: AtomicFenceOrd) -> InterpResult<'tcx>
Update the data-race detector for an atomic fence on the current thread.
sourcefn allow_data_races_all_threads_done(&mut self)
fn allow_data_races_all_threads_done(&mut self)
After all threads are done running, this allows data races to occur for subsequent ‘administrative’ machine accesses (that logically happen outside of the Abstract Machine).
sourcefn release_clock<'a>(&'a self) -> Option<Ref<'a, VClock>>where
'tcx: 'a,
fn release_clock<'a>(&'a self) -> Option<Ref<'a, VClock>>where
'tcx: 'a,
Returns the release
clock of the current thread.
Other threads can acquire this clock in the future to establish synchronization
with this program point.
sourcefn acquire_clock(&self, clock: &VClock)
fn acquire_clock(&self, clock: &VClock)
Acquire the given clock into the current thread, establishing synchronization with
the moment when that clock snapshot was taken via release_clock
.
Implementors§
impl<'tcx> EvalContextExt<'tcx> for MiriInterpCx<'tcx>
Evaluation context extensions.