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

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,