Skip to content

Commit a0485c5

Browse files
committed
Auto merge of #1686 - thomcc:cmpxchg_weak, r=oli-obk
Add random failures to compare_exchange_weak In practice this is pretty useful for detecting bugs. This fails more frequently than realistic (~~50%~~ (now 80%, controlled by a flag) of the time). I couldn't find any existing code that tries to model this (tsan, cdschecker, etc all seem to have TODOs there). Relacy models it with a 25% or 50% failure chance depending on some settings. CC `@JCTyblaidd` who wrote the code this modifies initially, and seems interested in this subject.
2 parents e23e0b2 + d310620 commit a0485c5

File tree

6 files changed

+77
-20
lines changed

6 files changed

+77
-20
lines changed

src/bin/miri.rs

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -282,6 +282,14 @@ fn main() {
282282
};
283283
miri_config.tracked_alloc_id = Some(miri::AllocId(id));
284284
}
285+
arg if arg.starts_with("-Zmiri-compare-exchange-weak-failure-rate=") => {
286+
let rate = match arg.strip_prefix("-Zmiri-compare-exchange-weak-failure-rate=").unwrap().parse::<f64>() {
287+
Ok(rate) if rate >= 0.0 && rate <= 1.0 => rate,
288+
Ok(_) => panic!("-Zmiri-compare-exchange-weak-failure-rate must be between `0.0` and `1.0`"),
289+
Err(err) => panic!("-Zmiri-compare-exchange-weak-failure-rate requires a `f64` between `0.0` and `1.0`: {}", err),
290+
};
291+
miri_config.cmpxchg_weak_failure_rate = rate;
292+
}
285293
_ => {
286294
// Forward to rustc.
287295
rustc_args.push(arg);

src/data_race.rs

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -75,7 +75,7 @@ use rustc_target::abi::Size;
7575

7676
use crate::{
7777
ImmTy, Immediate, InterpResult, MPlaceTy, MemPlaceMeta, MiriEvalContext, MiriEvalContextExt,
78-
OpTy, Pointer, RangeMap, ScalarMaybeUninit, Tag, ThreadId, VClock, VTimestamp,
78+
OpTy, Pointer, RangeMap, Scalar, ScalarMaybeUninit, Tag, ThreadId, VClock, VTimestamp,
7979
VectorIdx, MemoryKind, MiriMemoryKind
8080
};
8181

@@ -544,31 +544,43 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
544544

545545
/// Perform an atomic compare and exchange at a given memory location.
546546
/// On success an atomic RMW operation is performed and on failure
547-
/// only an atomic read occurs.
547+
/// only an atomic read occurs. If `can_fail_spuriously` is true,
548+
/// then we treat it as a "compare_exchange_weak" operation, and
549+
/// some portion of the time fail even when the values are actually
550+
/// identical.
548551
fn atomic_compare_exchange_scalar(
549552
&mut self,
550553
place: MPlaceTy<'tcx, Tag>,
551554
expect_old: ImmTy<'tcx, Tag>,
552555
new: ScalarMaybeUninit<Tag>,
553556
success: AtomicRwOp,
554557
fail: AtomicReadOp,
558+
can_fail_spuriously: bool,
555559
) -> InterpResult<'tcx, Immediate<Tag>> {
560+
use rand::Rng as _;
556561
let this = self.eval_context_mut();
557562

558563
// Failure ordering cannot be stronger than success ordering, therefore first attempt
559564
// to read with the failure ordering and if successful then try again with the success
560565
// read ordering and write in the success case.
561566
// Read as immediate for the sake of `binary_op()`
562567
let old = this.allow_data_races_mut(|this| this.read_immediate(place.into()))?;
563-
564568
// `binary_op` will bail if either of them is not a scalar.
565569
let eq = this.overflowing_binary_op(mir::BinOp::Eq, old, expect_old)?.0;
566-
let res = Immediate::ScalarPair(old.to_scalar_or_uninit(), eq.into());
570+
// If the operation would succeed, but is "weak", fail some portion
571+
// of the time, based on `rate`.
572+
let rate = this.memory.extra.cmpxchg_weak_failure_rate;
573+
let cmpxchg_success = eq.to_bool()?
574+
&& (!can_fail_spuriously || this.memory.extra.rng.borrow_mut().gen::<f64>() < rate);
575+
let res = Immediate::ScalarPair(
576+
old.to_scalar_or_uninit(),
577+
Scalar::from_bool(cmpxchg_success).into(),
578+
);
567579

568580
// Update ptr depending on comparison.
569581
// if successful, perform a full rw-atomic validation
570582
// otherwise treat this as an atomic load with the fail ordering.
571-
if eq.to_bool()? {
583+
if cmpxchg_success {
572584
this.allow_data_races_mut(|this| this.write_scalar(new, place.into()))?;
573585
this.validate_atomic_rmw(place, success)?;
574586
} else {

src/eval.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -50,6 +50,9 @@ pub struct MiriConfig {
5050
pub track_raw: bool,
5151
/// Determine if data race detection should be enabled
5252
pub data_race_detector: bool,
53+
/// Rate of spurious failures for compare_exchange_weak atomic operations,
54+
/// between 0.0 and 1.0, defaulting to 0.8 (80% chance of failure).
55+
pub cmpxchg_weak_failure_rate: f64,
5356
}
5457

5558
impl Default for MiriConfig {
@@ -68,6 +71,7 @@ impl Default for MiriConfig {
6871
tracked_alloc_id: None,
6972
track_raw: false,
7073
data_race_detector: true,
74+
cmpxchg_weak_failure_rate: 0.8,
7175
}
7276
}
7377
}

src/machine.rs

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -135,6 +135,9 @@ pub struct MemoryExtra {
135135

136136
/// Controls whether alignment of memory accesses is being checked.
137137
pub(crate) check_alignment: AlignmentCheck,
138+
139+
/// Failure rate of compare_exchange_weak, between 0.0 and 1.0
140+
pub(crate) cmpxchg_weak_failure_rate: f64,
138141
}
139142

140143
impl MemoryExtra {
@@ -162,6 +165,7 @@ impl MemoryExtra {
162165
rng: RefCell::new(rng),
163166
tracked_alloc_id: config.tracked_alloc_id,
164167
check_alignment: config.check_alignment,
168+
cmpxchg_weak_failure_rate: config.cmpxchg_weak_failure_rate,
165169
}
166170
}
167171

src/shims/intrinsics.rs

Lines changed: 11 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -518,9 +518,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
518518
Ok(())
519519
}
520520

521-
fn atomic_compare_exchange(
521+
fn atomic_compare_exchange_impl(
522522
&mut self, args: &[OpTy<'tcx, Tag>], dest: PlaceTy<'tcx, Tag>,
523-
success: AtomicRwOp, fail: AtomicReadOp
523+
success: AtomicRwOp, fail: AtomicReadOp, can_fail_spuriously: bool
524524
) -> InterpResult<'tcx> {
525525
let this = self.eval_context_mut();
526526

@@ -538,22 +538,26 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
538538

539539

540540
let old = this.atomic_compare_exchange_scalar(
541-
place, expect_old, new, success, fail
541+
place, expect_old, new, success, fail, can_fail_spuriously
542542
)?;
543543

544544
// Return old value.
545545
this.write_immediate(old, dest)?;
546546
Ok(())
547547
}
548548

549-
fn atomic_compare_exchange_weak(
549+
fn atomic_compare_exchange(
550550
&mut self, args: &[OpTy<'tcx, Tag>], dest: PlaceTy<'tcx, Tag>,
551551
success: AtomicRwOp, fail: AtomicReadOp
552552
) -> InterpResult<'tcx> {
553+
self.atomic_compare_exchange_impl(args, dest, success, fail, false)
554+
}
553555

554-
// FIXME: the weak part of this is currently not modelled,
555-
// it is assumed to always succeed unconditionally.
556-
self.atomic_compare_exchange(args, dest, success, fail)
556+
fn atomic_compare_exchange_weak(
557+
&mut self, args: &[OpTy<'tcx, Tag>], dest: PlaceTy<'tcx, Tag>,
558+
success: AtomicRwOp, fail: AtomicReadOp
559+
) -> InterpResult<'tcx> {
560+
self.atomic_compare_exchange_impl(args, dest, success, fail, true)
557561
}
558562

559563
fn float_to_int_unchecked<F>(

tests/run-pass/atomic.rs

Lines changed: 33 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ fn main() {
55
atomic_isize();
66
atomic_u64();
77
atomic_fences();
8+
weak_sometimes_fails();
89
}
910

1011
fn atomic_bool() {
@@ -24,7 +25,20 @@ fn atomic_bool() {
2425
assert_eq!(*ATOMIC.get_mut(), false);
2526
}
2627
}
27-
28+
// There isn't a trait to use to make this generic, so just use a macro
29+
macro_rules! compare_exchange_weak_loop {
30+
($atom:expr, $from:expr, $to:expr, $succ_order:expr, $fail_order:expr) => {
31+
loop {
32+
match $atom.compare_exchange_weak($from, $to, $succ_order, $fail_order) {
33+
Ok(n) => {
34+
assert_eq!(n, $from);
35+
break;
36+
}
37+
Err(n) => assert_eq!(n, $from),
38+
}
39+
}
40+
};
41+
}
2842
fn atomic_isize() {
2943
static ATOMIC: AtomicIsize = AtomicIsize::new(0);
3044

@@ -40,11 +54,11 @@ fn atomic_isize() {
4054
ATOMIC.compare_exchange(0, 1, SeqCst, SeqCst).ok();
4155

4256
ATOMIC.store(0, SeqCst);
43-
44-
assert_eq!(ATOMIC.compare_exchange_weak(0, 1, Relaxed, Relaxed), Ok(0));
57+
compare_exchange_weak_loop!(ATOMIC, 0, 1, Relaxed, Relaxed);
4558
assert_eq!(ATOMIC.compare_exchange_weak(0, 2, Acquire, Relaxed), Err(1));
4659
assert_eq!(ATOMIC.compare_exchange_weak(0, 1, Release, Relaxed), Err(1));
47-
assert_eq!(ATOMIC.compare_exchange_weak(1, 0, AcqRel, Relaxed), Ok(1));
60+
compare_exchange_weak_loop!(ATOMIC, 1, 0, AcqRel, Relaxed);
61+
assert_eq!(ATOMIC.load(Relaxed), 0);
4862
ATOMIC.compare_exchange_weak(0, 1, AcqRel, Relaxed).ok();
4963
ATOMIC.compare_exchange_weak(0, 1, SeqCst, Relaxed).ok();
5064
ATOMIC.compare_exchange_weak(0, 1, Acquire, Acquire).ok();
@@ -58,10 +72,7 @@ fn atomic_u64() {
5872

5973
ATOMIC.store(1, SeqCst);
6074
assert_eq!(ATOMIC.compare_exchange(0, 0x100, AcqRel, Acquire), Err(1));
61-
assert_eq!(
62-
ATOMIC.compare_exchange_weak(1, 0x100, AcqRel, Acquire),
63-
Ok(1)
64-
);
75+
compare_exchange_weak_loop!(ATOMIC, 1, 0x100, AcqRel, Acquire);
6576
assert_eq!(ATOMIC.load(Relaxed), 0x100);
6677
}
6778

@@ -75,3 +86,17 @@ fn atomic_fences() {
7586
compiler_fence(Acquire);
7687
compiler_fence(AcqRel);
7788
}
89+
90+
fn weak_sometimes_fails() {
91+
let atomic = AtomicBool::new(false);
92+
let tries = 100;
93+
for _ in 0..tries {
94+
let cur = atomic.load(Relaxed);
95+
// Try (weakly) to flip the flag.
96+
if atomic.compare_exchange_weak(cur, !cur, Relaxed, Relaxed).is_err() {
97+
// We failed, so return and skip the panic.
98+
return;
99+
}
100+
}
101+
panic!("compare_exchange_weak succeeded {} tries in a row", tries);
102+
}

0 commit comments

Comments
 (0)