Add random failures to compare_exchange_weak
This commit is contained in:
parent
de0800e83b
commit
c678bd722e
@ -75,7 +75,7 @@ use rustc_target::abi::Size;
|
||||
|
||||
use crate::{
|
||||
ImmTy, Immediate, InterpResult, MPlaceTy, MemPlaceMeta, MiriEvalContext, MiriEvalContextExt,
|
||||
OpTy, Pointer, RangeMap, ScalarMaybeUninit, Tag, ThreadId, VClock, VTimestamp,
|
||||
OpTy, Pointer, RangeMap, Scalar, ScalarMaybeUninit, Tag, ThreadId, VClock, VTimestamp,
|
||||
VectorIdx, MemoryKind, MiriMemoryKind
|
||||
};
|
||||
|
||||
@ -544,7 +544,10 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
|
||||
|
||||
/// 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.
|
||||
/// 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.
|
||||
fn atomic_compare_exchange_scalar(
|
||||
&mut self,
|
||||
place: MPlaceTy<'tcx, Tag>,
|
||||
@ -552,7 +555,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
|
||||
new: ScalarMaybeUninit<Tag>,
|
||||
success: AtomicRwOp,
|
||||
fail: AtomicReadOp,
|
||||
can_fail_spuriously: bool,
|
||||
) -> InterpResult<'tcx, Immediate<Tag>> {
|
||||
use rand::Rng as _;
|
||||
let this = self.eval_context_mut();
|
||||
|
||||
// Failure ordering cannot be stronger than success ordering, therefore first attempt
|
||||
@ -560,15 +565,21 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
|
||||
// read ordering and write in the success case.
|
||||
// Read as immediate for the sake of `binary_op()`
|
||||
let old = this.allow_data_races_mut(|this| this.read_immediate(place.into()))?;
|
||||
|
||||
// `binary_op` will bail if either of them is not a scalar.
|
||||
let eq = this.overflowing_binary_op(mir::BinOp::Eq, old, expect_old)?.0;
|
||||
let res = Immediate::ScalarPair(old.to_scalar_or_uninit(), eq.into());
|
||||
// If the operation would succeed, but is "weak", fail 50% of the time.
|
||||
// FIXME: this is quite arbitrary.
|
||||
let cmpxchg_success = eq.to_bool()?
|
||||
&& (!can_fail_spuriously || this.memory.extra.rng.borrow_mut().gen_range(0, 2) == 0);
|
||||
let res = Immediate::ScalarPair(
|
||||
old.to_scalar_or_uninit(),
|
||||
Scalar::from_bool(cmpxchg_success).into(),
|
||||
);
|
||||
|
||||
// Update ptr depending on comparison.
|
||||
// if successful, perform a full rw-atomic validation
|
||||
// otherwise treat this as an atomic load with the fail ordering.
|
||||
if eq.to_bool()? {
|
||||
if cmpxchg_success {
|
||||
this.allow_data_races_mut(|this| this.write_scalar(new, place.into()))?;
|
||||
this.validate_atomic_rmw(place, success)?;
|
||||
} else {
|
||||
|
@ -518,9 +518,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn atomic_compare_exchange(
|
||||
fn atomic_compare_exchange_impl(
|
||||
&mut self, args: &[OpTy<'tcx, Tag>], dest: PlaceTy<'tcx, Tag>,
|
||||
success: AtomicRwOp, fail: AtomicReadOp
|
||||
success: AtomicRwOp, fail: AtomicReadOp, can_fail_spuriously: bool
|
||||
) -> InterpResult<'tcx> {
|
||||
let this = self.eval_context_mut();
|
||||
|
||||
@ -538,7 +538,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
|
||||
|
||||
|
||||
let old = this.atomic_compare_exchange_scalar(
|
||||
place, expect_old, new, success, fail
|
||||
place, expect_old, new, success, fail, can_fail_spuriously
|
||||
)?;
|
||||
|
||||
// Return old value.
|
||||
@ -546,14 +546,18 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
|
||||
Ok(())
|
||||
}
|
||||
|
||||
fn atomic_compare_exchange(
|
||||
&mut self, args: &[OpTy<'tcx, Tag>], dest: PlaceTy<'tcx, Tag>,
|
||||
success: AtomicRwOp, fail: AtomicReadOp
|
||||
) -> InterpResult<'tcx> {
|
||||
self.atomic_compare_exchange_impl(args, dest, success, fail, false)
|
||||
}
|
||||
|
||||
fn atomic_compare_exchange_weak(
|
||||
&mut self, args: &[OpTy<'tcx, Tag>], dest: PlaceTy<'tcx, Tag>,
|
||||
success: AtomicRwOp, fail: AtomicReadOp
|
||||
) -> InterpResult<'tcx> {
|
||||
|
||||
// FIXME: the weak part of this is currently not modelled,
|
||||
// it is assumed to always succeed unconditionally.
|
||||
self.atomic_compare_exchange(args, dest, success, fail)
|
||||
self.atomic_compare_exchange_impl(args, dest, success, fail, true)
|
||||
}
|
||||
|
||||
fn float_to_int_unchecked<F>(
|
||||
|
@ -24,7 +24,20 @@ fn atomic_bool() {
|
||||
assert_eq!(*ATOMIC.get_mut(), false);
|
||||
}
|
||||
}
|
||||
|
||||
// There isn't a trait to use to make this generic, so just use a macro
|
||||
macro_rules! compare_exchange_weak_loop {
|
||||
($atom:expr, $from:expr, $to:expr, $succ_order:expr, $fail_order:expr) => {
|
||||
loop {
|
||||
match $atom.compare_exchange_weak($from, $to, $succ_order, $fail_order) {
|
||||
Ok(n) => {
|
||||
assert_eq!(n, $from);
|
||||
break;
|
||||
}
|
||||
Err(n) => assert_eq!(n, $from),
|
||||
}
|
||||
}
|
||||
};
|
||||
}
|
||||
fn atomic_isize() {
|
||||
static ATOMIC: AtomicIsize = AtomicIsize::new(0);
|
||||
|
||||
@ -40,11 +53,11 @@ fn atomic_isize() {
|
||||
ATOMIC.compare_exchange(0, 1, SeqCst, SeqCst).ok();
|
||||
|
||||
ATOMIC.store(0, SeqCst);
|
||||
|
||||
assert_eq!(ATOMIC.compare_exchange_weak(0, 1, Relaxed, Relaxed), Ok(0));
|
||||
compare_exchange_weak_loop!(ATOMIC, 0, 1, Relaxed, Relaxed);
|
||||
assert_eq!(ATOMIC.compare_exchange_weak(0, 2, Acquire, Relaxed), Err(1));
|
||||
assert_eq!(ATOMIC.compare_exchange_weak(0, 1, Release, Relaxed), Err(1));
|
||||
assert_eq!(ATOMIC.compare_exchange_weak(1, 0, AcqRel, Relaxed), Ok(1));
|
||||
compare_exchange_weak_loop!(ATOMIC, 1, 0, AcqRel, Relaxed);
|
||||
assert_eq!(ATOMIC.load(Relaxed), 0);
|
||||
ATOMIC.compare_exchange_weak(0, 1, AcqRel, Relaxed).ok();
|
||||
ATOMIC.compare_exchange_weak(0, 1, SeqCst, Relaxed).ok();
|
||||
ATOMIC.compare_exchange_weak(0, 1, Acquire, Acquire).ok();
|
||||
@ -58,10 +71,7 @@ fn atomic_u64() {
|
||||
|
||||
ATOMIC.store(1, SeqCst);
|
||||
assert_eq!(ATOMIC.compare_exchange(0, 0x100, AcqRel, Acquire), Err(1));
|
||||
assert_eq!(
|
||||
ATOMIC.compare_exchange_weak(1, 0x100, AcqRel, Acquire),
|
||||
Ok(1)
|
||||
);
|
||||
compare_exchange_weak_loop!(ATOMIC, 1, 0x100, AcqRel, Acquire);
|
||||
assert_eq!(ATOMIC.load(Relaxed), 0x100);
|
||||
}
|
||||
|
||||
|
Loading…
x
Reference in New Issue
Block a user