Mark stores SC if it must precede the ongoing SC store in modification order

src/tools/miri/src/concurrency/weak_memory.rs

diff --git a/src/tools/miri/src/concurrency/weak_memory.rs b/src/tools/miri/src/concurrency/weak_memory.rs
index 3aded9a..b3124a3 100644
--- a/src/tools/miri/src/concurrency/weak_memory.rs
+++ b/src/tools/miri/src/concurrency/weak_memory.rs
@@ -19,6 +19,9 @@
 //!   that C++20 intended to copy (<https://plv.mpi-sws.org/scfix/paper.pdf>); a change was
 //!   introduced when translating the math to English. According to Viktor Vafeiadis, this
 //!   difference is harmless. So we stick to what the standard says, and allow fewer behaviors.)
+//! - If an SC store happens after a load (of any ordering), then the existing store (of any ordering)
+//!   seen by the load is marked as an SC store. (The paper's model only marks stores that happen-before
+//!   an SC store as SC.)
 //! - SC fences are treated like AcqRel RMWs to a global clock, to ensure they induce enough
 //!   synchronization with the surrounding accesses. This rules out legal behavior, but it is really
 //!   hard to be more precise here.
@@ -77,8 +80,9 @@
 //
 // 3. §4.5 of the paper wants an SC store to mark all existing stores in the buffer that happens before it
 // as SC. This is not done in the operational semantics but implemented correctly in tsan11
-// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L160-L167)
-// and here.
+// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L160-L167).
+// On top of this we've added a C++20 change: if the current SC store happens after a load, then the store seen by that load
+// is marked SC.
 //
 // 4. W_SC ; R_SC case requires the SC load to ignore all but last store marked SC (stores not marked SC are not
 // affected). But this rule is applied to all loads in ReadsFromSet from the paper (last two lines of code), not just SC load.
@@ -149,7 +153,8 @@ struct StoreElement {
     /// The vector clock that can be acquired by loading this store.
     sync_clock: VClock,
 
-    /// Whether this store is SC.
+    /// Whether this store is SC. If a store happens-before or precedes in `mo` another SC store,
+    /// then it is also marked as SC.
     is_seqcst: bool,
 
     /// The value of this store. `None` means uninitialized.
@@ -371,7 +376,7 @@ fn fetch_store<R: rand::Rng + ?Sized>(
                 } else if is_seqcst
                     && store_elem.store_timestamp <= clocks.read_seqcst[store_elem.store_thread]
                 {
-                    // The current SC load cannot read-before the last store sequenced-before
+                    // The current SC load cannot read-from any but the last store sequenced-before
                     // the last SC fence.
                     // C++17 §32.4 [atomics.order] paragraph 5
                     false
@@ -433,11 +438,23 @@ fn store_impl(
         }
         self.buffer.push_back(store_elem);
         if is_seqcst {
-            // Every store that happens before this needs to be marked as SC
-            // so that in a later SC load, only the last SC store (i.e. this one) or stores that
-            // aren't ordered by hb with the last SC is picked.
+            // Every store that happens-before or is coherence-ordered before the ongoing SC store
+            // needs to be marked as SC, so that in a later SC load, only the latest SC-marked store
+            // or unmarked stores can be picked.
             self.buffer.iter_mut().rev().for_each(|elem| {
                 if elem.store_timestamp <= thread_clock[elem.store_thread] {
+                    // This store happens-before the ongoing SC store.
+                    elem.is_seqcst = true;
+                } else if elem
+                    .load_info
+                    .borrow()
+                    .timestamps
+                    .iter()
+                    .any(|(&idx, &load_ts)| load_ts <= thread_clock[idx])
+                {
+                    // This store has a load which happens before the ongoing store.
+                    // This store must precede the onging store in modification order,
+                    // and is therefore coherence-ordered before the ongoing SC store.
                     elem.is_seqcst = true;
                 }
             })

src/tools/miri/tests/pass/0weak_memory/consistency_sc.rs

diff --git a/src/tools/miri/tests/pass/0weak_memory/consistency_sc.rs b/src/tools/miri/tests/pass/0weak_memory/consistency_sc.rs
index d92c0d1..74d3ea3 100644
--- a/src/tools/miri/tests/pass/0weak_memory/consistency_sc.rs
+++ b/src/tools/miri/tests/pass/0weak_memory/consistency_sc.rs
@@ -348,6 +348,85 @@ fn test_sc_relaxed() {
     assert!(!bad);
 }
 
+/// Test that coherence-ordered-before established by modification order prevents
+/// an SC load from reading before the last-in-mo store.
+/// Test by Joseph Perez (https://github.com/rust-lang/miri/issues/5104#issue-4644401606)
+fn test_cob_due_to_mo() {
+    let x = static_atomic(0);
+    let y = static_atomic(0);
+    x.store(0, Relaxed);
+    y.store(0, Relaxed);
+
+    let t1 = spawn(move || x.store(1, Release));
+    let t2 = spawn(move || {
+        let r0 = x.load(Relaxed);
+        x.store(2, SeqCst);
+        let r1 = y.load(SeqCst);
+        (r0, r1)
+    });
+    let t3 = spawn(move || {
+        y.store(1, SeqCst);
+        let r2 = x.load(SeqCst);
+        r2
+    });
+    let (r0, r1) = t2.join().unwrap();
+    let r2 = t3.join().unwrap();
+    t1.join().unwrap();
+    let bad = r0 == 1 && r1 == 0 && r2 == 1;
+    // This is bad because: T2's SC load of Y read 0, which means that
+    // T2's SC operations all precede T3's SC operations in the SC order.
+    // But in X's modification order, we must have T1's store before T2's store
+    // (since T2 observed a 1). As a result, T3's X.load reading from T1's store
+    // means it is coherence-ordered before and precedes in SC T2's X.store.
+    // This causes a cycle in SC.
+    assert!(!bad);
+}
+
+/// Variant of the test above, where the modification order is established by
+/// happens-before across three threads (t1, t2, and t3).
+fn test_cob_due_to_mo_hb() {
+    let x = static_atomic(0);
+    let y = static_atomic(0);
+    let gate = static_atomic(0);
+    x.store(0, Relaxed);
+    y.store(0, Relaxed);
+    gate.store(0, Relaxed);
+
+    let t1 = spawn(move || x.store(1, Release));
+    let t2 = spawn(move || {
+        let r0 = x.load(Acquire);
+        gate.store(1, Release);
+        r0
+    });
+
+    let t3 = spawn(move || {
+        while gate.load(Acquire) == 0 {}
+        x.store(2, SeqCst);
+        let r1 = y.load(SeqCst);
+        r1
+    });
+    let t4 = spawn(move || {
+        y.store(1, SeqCst);
+        let r2 = x.load(SeqCst);
+        r2
+    });
+
+    let r0 = t2.join().unwrap();
+    let r1 = t3.join().unwrap();
+    let r2 = t4.join().unwrap();
+    t1.join().unwrap();
+    let bad = r0 == 1 && r1 == 0 && r2 == 1;
+    // This is bad because: T3's SC load of Y read 0 means that
+    // T3's SC operations all precede T4's SC operations in the SC order.
+    // But in X's modification order, we must have T1's store before T3's store
+    // (since T1's store happens-before T3's store).
+    // As a result, T4's X.load reading from T1's store means it is
+    // coherence-ordered before and precedes in SC T3's X.store.
+    // This causes a cycle in SC.
+
+    assert!(!bad);
+}
+
 fn main() {
     for _ in 0..32 {
         test_sc_store_buffering();
@@ -359,5 +438,7 @@ fn main() {
         test_sc_fence_access_relacq();
         test_sc_multi_fence();
         test_sc_relaxed();
+        test_cob_due_to_mo();
+        test_cob_due_to_mo_hb();
     }
 }