Fix C++20 SC access unsoundness

Author: cbeuw

src/concurrency/weak_memory.rs

@@ -6,7 +6,7 @@
 //! but it is incapable of producing all possible weak behaviours allowed by the model. There are
 //! certain weak behaviours observable on real hardware but not while using this.
 //!
-//! Note that this implementation does not take into account of C++20's memory model revision to SC accesses
+//! Note that this implementation does not fully take into account of C++20's memory model revision to SC accesses
 //! and fences introduced by P0668 (<https://www.open-std.org/jtc1/sc22/wg21/docs/papers/2018/p0668r5.html>).
 //! This implementation is not fully correct under the revised C++20 model and may generate behaviours C++20
 //! disallows (<https://github.com/rust-lang/miri/issues/2301>).
@@ -134,9 +134,17 @@ struct StoreElement {
     // partially initialized data.
     val: ScalarMaybeUninit<Provenance>,
 
+    /// Metadata about loads from this store element,
+    /// behind a RefCell to keep load op take &self
+    load_info: RefCell<LoadInfo>,
+}
+
+#[derive(Debug, Clone, PartialEq, Eq, Default)]
+struct LoadInfo {
     /// Timestamp of first loads from this store element by each thread
-    /// Behind a RefCell to keep load op take &self
-    loads: RefCell<FxHashMap<VectorIdx, VTimestamp>>,
+    timestamps: FxHashMap<VectorIdx, VTimestamp>,
+    /// Whether this store element has been read by an SC load
+    sc_loaded: bool,
 }
 
 impl StoreBufferAlloc {
@@ -236,18 +244,23 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
             timestamp: 0,
             val: init,
             is_seqcst: false,
-            loads: RefCell::new(FxHashMap::default()),
+            load_info: RefCell::new(LoadInfo::default()),
         };
         ret.buffer.push_back(store_elem);
         ret
     }
 
     /// Reads from the last store in modification order
-    fn read_from_last_store(&self, global: &DataRaceState, thread_mgr: &ThreadManager<'_, '_>) {
+    fn read_from_last_store(
+        &self,
+        global: &DataRaceState,
+        thread_mgr: &ThreadManager<'_, '_>,
+        is_seqcst: bool,
+    ) {
         let store_elem = self.buffer.back();
         if let Some(store_elem) = store_elem {
             let (index, clocks) = global.current_thread_state(thread_mgr);
-            store_elem.load_impl(index, &clocks);
+            store_elem.load_impl(index, &clocks, is_seqcst);
         }
     }
 
@@ -277,7 +290,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
         validate()?;
 
         let (index, clocks) = global.current_thread_state(thread_mgr);
-        let loaded = store_elem.load_impl(index, &clocks);
+        let loaded = store_elem.load_impl(index, &clocks, is_seqcst);
         Ok((loaded, recency))
     }
 
@@ -322,9 +335,9 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
                     // then we can't read-from anything earlier in modification order.
                     // C++20 §6.9.2.2 [intro.races] paragraph 18
                     false
-                } else if store_elem.loads.borrow().iter().any(|(&load_index, &load_timestamp)| {
-                    load_timestamp <= clocks.clock[load_index]
-                }) {
+                } else if store_elem.load_info.borrow().timestamps.iter().any(
+                    |(&load_index, &load_timestamp)| load_timestamp <= clocks.clock[load_index],
+                ) {
                     // CoRR: if there was a load from this store which happened-before the current load,
                     // then we cannot read-from anything earlier in modification order.
                     // C++20 §6.9.2.2 [intro.races] paragraph 16
@@ -341,12 +354,22 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
                     // cannot read-before the last SC store executed before the fence.
                     // C++17 §32.4 [atomics.order] paragraph 4
                     false
-                } else if is_seqcst && store_elem.timestamp <= clocks.read_seqcst[store_elem.store_index] {
+                } else if is_seqcst
+                    && store_elem.timestamp <= clocks.read_seqcst[store_elem.store_index]
+                {
                     // The current SC load cannot read-before the last store sequenced-before
                     // the last SC fence.
                     // C++17 §32.4 [atomics.order] paragraph 5
                     false
-                } else {true};
+                } else if is_seqcst && store_elem.load_info.borrow().sc_loaded {
+                    // The current SC load cannot read-before a store that an earlier SC load has observed.
+                    // See https://github.com/rust-lang/miri/issues/2301#issuecomment-1222720427
+                    // Consequences of C++20 §31.4 [atomics.order] paragraph 3.1, 3.3 (coherence-ordered before)
+                    // and 4.1 (coherence-ordered before between SC makes global total order S)
+                    false
+                } else {
+                    true
+                };
 
                 true
             })
@@ -387,7 +410,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
             // access
             val,
             is_seqcst,
-            loads: RefCell::new(FxHashMap::default()),
+            load_info: RefCell::new(LoadInfo::default()),
         };
         self.buffer.push_back(store_elem);
         if self.buffer.len() > STORE_BUFFER_LIMIT {
@@ -419,8 +442,11 @@ impl StoreElement {
         &self,
         index: VectorIdx,
         clocks: &ThreadClockSet,
+        is_seqcst: bool,
     ) -> ScalarMaybeUninit<Provenance> {
-        let _ = self.loads.borrow_mut().try_insert(index, clocks.clock[index]);
+        let mut load_info = self.load_info.borrow_mut();
+        load_info.sc_loaded |= is_seqcst;
+        let _ = load_info.timestamps.try_insert(index, clocks.clock[index]);
         self.val
     }
 }
@@ -480,7 +506,7 @@ pub(super) trait EvalContextExt<'mir, 'tcx: 'mir>:
             }
             let range = alloc_range(base_offset, place.layout.size);
             let buffer = alloc_buffers.get_or_create_store_buffer_mut(range, init)?;
-            buffer.read_from_last_store(global, threads);
+            buffer.read_from_last_store(global, threads, atomic == AtomicRwOrd::SeqCst);
             buffer.buffered_write(new_val, global, threads, atomic == AtomicRwOrd::SeqCst)?;
         }
         Ok(())
@@ -587,7 +613,11 @@ pub(super) trait EvalContextExt<'mir, 'tcx: 'mir>:
             if let Some(alloc_buffers) = this.get_alloc_extra(alloc_id)?.weak_memory.as_ref() {
                 let buffer = alloc_buffers
                     .get_or_create_store_buffer(alloc_range(base_offset, size), init)?;
-                buffer.read_from_last_store(global, &this.machine.threads);
+                buffer.read_from_last_store(
+                    global,
+                    &this.machine.threads,
+                    atomic == AtomicReadOrd::SeqCst,
+                );
             }
         }
         Ok(())