Auto merge of #2424 - RalfJung:weak-memory-debug, r=RalfJung

add a flag to print a diagnostic when an outdated value is returned from an atomic load

Helps with #2313. It can still be annoying to figure out *which* outdated load is the important one in case there are many of them (and the issue contains some ideas for how to help with that situation), but having this flag is better than nothing.

Thanks to `@cbeuw` for the [original patch](cbeuw@64d738c) that I based this on.

README.md

@@ -377,6 +377,9 @@ to Miri failing to detect cases of undefined behavior in a program.
   happening and where in your code would be a good place to look for it.
   Specifying this argument multiple times does not overwrite the previous
   values, instead it appends its values to the list. Listing a tag multiple times has no effect.
+* `-Zmiri-track-weak-memory-loads` shows a backtrace when weak memory emulation returns an outdated
+  value from a load. This can help diagnose problems that disappear under
+  `-Zmiri-disable-weak-memory-emulation`.
 
 [function ABI]: https://doc.rust-lang.org/reference/items/functions.html#extern-function-qualifier
 

src/bin/miri.rs

@@ -358,6 +358,8 @@ fn main() {
             miri_config.isolated_op = miri::IsolatedOp::Allow;
         } else if arg == "-Zmiri-disable-weak-memory-emulation" {
             miri_config.weak_memory_emulation = false;
+        } else if arg == "-Zmiri-track-weak-memory-loads" {
+            miri_config.track_outdated_loads = true;
         } else if let Some(param) = arg.strip_prefix("-Zmiri-isolation-error=") {
             if matches!(isolation_enabled, Some(false)) {
                 panic!("-Zmiri-isolation-error cannot be used along with -Zmiri-disable-isolation");

src/concurrency/data_race.rs

@@ -1187,12 +1187,15 @@ pub struct GlobalState {
 
     /// The timestamp of last SC write performed by each thread
     last_sc_write: RefCell<VClock>,
+
+    /// Track when an outdated (weak memory) load happens.
+    pub track_outdated_loads: bool,
 }
 
 impl GlobalState {
     /// Create a new global state, setup with just thread-id=0
     /// advanced to timestamp = 1.
-    pub fn new() -> Self {
+    pub fn new(config: &MiriConfig) -> Self {
         let mut global_state = GlobalState {
             multi_threaded: Cell::new(false),
             ongoing_action_data_race_free: Cell::new(false),
@@ -1203,6 +1206,7 @@ impl GlobalState {
             terminated_threads: RefCell::new(FxHashMap::default()),
             last_sc_fence: RefCell::new(VClock::default()),
             last_sc_write: RefCell::new(VClock::default()),
+            track_outdated_loads: config.track_outdated_loads,
         };
 
         // Setup the main-thread since it is not explicitly created:

src/concurrency/weak_memory.rs

@@ -82,10 +82,7 @@ use rustc_const_eval::interpret::{
 };
 use rustc_data_structures::fx::FxHashMap;
 
-use crate::{
-    AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, Provenance, ThreadManager, VClock, VTimestamp,
-    VectorIdx,
-};
+use crate::*;
 
 use super::{
     data_race::{GlobalState as DataRaceState, ThreadClockSet},
@@ -113,6 +110,13 @@ pub(super) struct StoreBuffer {
     buffer: VecDeque<StoreElement>,
 }
 
+/// Whether a load returned the latest value or not.
+#[derive(PartialEq, Eq)]
+enum LoadRecency {
+    Latest,
+    Outdated,
+}
+
 #[derive(Debug, Clone, PartialEq, Eq)]
 struct StoreElement {
     /// The identifier of the vector index, corresponding to a thread
@@ -254,11 +258,11 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
         is_seqcst: bool,
         rng: &mut (impl rand::Rng + ?Sized),
         validate: impl FnOnce() -> InterpResult<'tcx>,
-    ) -> InterpResult<'tcx, ScalarMaybeUninit<Provenance>> {
+    ) -> InterpResult<'tcx, (ScalarMaybeUninit<Provenance>, LoadRecency)> {
         // Having a live borrow to store_buffer while calling validate_atomic_load is fine
         // because the race detector doesn't touch store_buffer
 
-        let store_elem = {
+        let (store_elem, recency) = {
             // The `clocks` we got here must be dropped before calling validate_atomic_load
             // as the race detector will update it
             let (.., clocks) = global.current_thread_state(thread_mgr);
@@ -274,7 +278,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
 
         let (index, clocks) = global.current_thread_state(thread_mgr);
         let loaded = store_elem.load_impl(index, &clocks);
-        Ok(loaded)
+        Ok((loaded, recency))
     }
 
     fn buffered_write(
@@ -296,7 +300,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
         is_seqcst: bool,
         clocks: &ThreadClockSet,
         rng: &mut R,
-    ) -> &StoreElement {
+    ) -> (&StoreElement, LoadRecency) {
         use rand::seq::IteratorRandom;
         let mut found_sc = false;
         // FIXME: we want an inclusive take_while (stops after a false predicate, but
@@ -359,9 +363,12 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
                 }
             });
 
-        candidates
-            .choose(rng)
-            .expect("store buffer cannot be empty, an element is populated on construction")
+        let chosen = candidates.choose(rng).expect("store buffer cannot be empty");
+        if std::ptr::eq(chosen, self.buffer.back().expect("store buffer cannot be empty")) {
+            (chosen, LoadRecency::Latest)
+        } else {
+            (chosen, LoadRecency::Outdated)
+        }
     }
 
     /// ATOMIC STORE IMPL in the paper (except we don't need the location's vector clock)
@@ -499,13 +506,16 @@ pub(super) trait EvalContextExt<'mir, 'tcx: 'mir>:
                     alloc_range(base_offset, place.layout.size),
                     latest_in_mo,
                 )?;
-                let loaded = buffer.buffered_read(
+                let (loaded, recency) = buffer.buffered_read(
                     global,
                     &this.machine.threads,
                     atomic == AtomicReadOrd::SeqCst,
                     &mut *rng,
                     validate,
                 )?;
+                if global.track_outdated_loads && recency == LoadRecency::Outdated {
+                    register_diagnostic(NonHaltingDiagnostic::WeakMemoryOutdatedLoad);
+                }
 
                 return Ok(loaded);
             }

src/diagnostics.rs

@@ -74,6 +74,7 @@ pub enum NonHaltingDiagnostic {
     Int2Ptr {
         details: bool,
     },
+    WeakMemoryOutdatedLoad,
 }
 
 /// Level of Miri specific diagnostics
@@ -474,6 +475,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
                         format!("progress report: current operation being executed is here"),
                     Int2Ptr { .. } =>
                         format!("integer-to-pointer cast"),
+                    WeakMemoryOutdatedLoad =>
+                        format!("weak memory emulation: outdated value returned from load"),
                 };
 
                 let (title, diag_level) = match e {
@@ -485,7 +488,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
                     | CreatedCallId(..)
                     | CreatedAlloc(..)
                     | FreedAlloc(..)
-                    | ProgressReport => ("tracking was triggered", DiagLevel::Note),
+                    | ProgressReport
+                    | WeakMemoryOutdatedLoad =>
+                        ("tracking was triggered", DiagLevel::Note),
                 };
 
                 let helps = match e {

src/eval.rs

@@ -102,6 +102,8 @@ pub struct MiriConfig {
     pub data_race_detector: bool,
     /// Determine if weak memory emulation should be enabled. Requires data race detection to be enabled
     pub weak_memory_emulation: bool,
+    /// Track when an outdated (weak memory) load happens.
+    pub track_outdated_loads: 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,
@@ -143,6 +145,7 @@ impl Default for MiriConfig {
             tracked_alloc_ids: HashSet::default(),
             data_race_detector: true,
             weak_memory_emulation: true,
+            track_outdated_loads: false,
             cmpxchg_weak_failure_rate: 0.8, // 80%
             measureme_out: None,
             panic_on_unsupported: false,

src/machine.rs

@@ -376,8 +376,11 @@ impl<'mir, 'tcx> Evaluator<'mir, 'tcx> {
         } else {
             None
         };
-        let data_race =
-            if config.data_race_detector { Some(data_race::GlobalState::new()) } else { None };
+        let data_race = if config.data_race_detector {
+            Some(data_race::GlobalState::new(config))
+        } else {
+            None
+        };
         Evaluator {
             stacked_borrows,
             data_race,