Skip to content

Commit

Permalink
Allow configuring the failure rate with -Zmiri-compare-exchange-weak-…
Browse files Browse the repository at this point in the history
…failure-rate
  • Loading branch information
thomcc committed Jan 26, 2021
1 parent a59a4ce commit f0b5176
Show file tree
Hide file tree
Showing 4 changed files with 20 additions and 3 deletions.
8 changes: 8 additions & 0 deletions src/bin/miri.rs
Original file line number Diff line number Diff line change
Expand Up @@ -282,6 +282,14 @@ fn main() {
};
miri_config.tracked_alloc_id = Some(miri::AllocId(id));
}
arg if arg.starts_with("-Zmiri-compare-exchange-weak-failure-rate=") => {
let rate = match arg.strip_prefix("-Zmiri-compare-exchange-weak-failure-rate=").unwrap().parse::<f64>() {
Ok(rate) if rate >= 0.0 && rate <= 1.0 => rate,
Ok(_) => panic!("-Zmiri-compare-exchange-weak-failure-rate must be between `0.0` and `1.0`"),
Err(err) => panic!("-Zmiri-compare-exchange-weak-failure-rate requires a `f64` between `0.0` and `1.0`: {}", err),
};
miri_config.cmpxchg_weak_failure_rate = rate;
}
_ => {
// Forward to rustc.
rustc_args.push(arg);
Expand Down
7 changes: 4 additions & 3 deletions src/data_race.rs
Original file line number Diff line number Diff line change
Expand Up @@ -567,10 +567,11 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
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;
// If the operation would succeed, but is "weak", fail 80% of the time.
// FIXME: this is quite arbitrary.
// If the operation would succeed, but is "weak", fail some portion
// of the time, based on `rate`.
let rate = this.memory.extra.cmpxchg_weak_failure_rate;
let cmpxchg_success = eq.to_bool()?
&& (!can_fail_spuriously || this.memory.extra.rng.borrow_mut().gen_range(0, 10) < 8);
&& (!can_fail_spuriously || this.memory.extra.rng.borrow_mut().gen::<f64>() < rate);
let res = Immediate::ScalarPair(
old.to_scalar_or_uninit(),
Scalar::from_bool(cmpxchg_success).into(),
Expand Down
4 changes: 4 additions & 0 deletions src/eval.rs
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,9 @@ pub struct MiriConfig {
pub track_raw: bool,
/// Determine if data race detection should be enabled
pub data_race_detector: bool,
/// Rate of spurious failures for compare_exchange_weak atomic operations,
/// between 0.0 and 1.0, defaulting to 0.8 (80% chance of failure).
pub cmpxchg_weak_failure_rate: f64,
}

impl Default for MiriConfig {
Expand All @@ -68,6 +71,7 @@ impl Default for MiriConfig {
tracked_alloc_id: None,
track_raw: false,
data_race_detector: true,
cmpxchg_weak_failure_rate: 0.8,
}
}
}
Expand Down
4 changes: 4 additions & 0 deletions src/machine.rs
Original file line number Diff line number Diff line change
Expand Up @@ -135,6 +135,9 @@ pub struct MemoryExtra {

/// Controls whether alignment of memory accesses is being checked.
pub(crate) check_alignment: AlignmentCheck,

/// Failure rate of compare_exchange_weak, between 0.0 and 1.0
pub(crate) cmpxchg_weak_failure_rate: f64,
}

impl MemoryExtra {
Expand Down Expand Up @@ -162,6 +165,7 @@ impl MemoryExtra {
rng: RefCell::new(rng),
tracked_alloc_id: config.tracked_alloc_id,
check_alignment: config.check_alignment,
cmpxchg_weak_failure_rate: config.cmpxchg_weak_failure_rate,
}
}

Expand Down

0 comments on commit f0b5176

Please sign in to comment.