Fix SC Store buffering and add test case

src/weak_memory.rs

@@ -216,6 +216,20 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
         if self.buffer.len() > STORE_BUFFER_LIMIT {
             self.buffer.pop_front();
         }
+        if is_seqcst {
+            // Every store that happens before this needs to be marked as SC
+            // so that in fetch_store, only the last SC store (i.e. this one) or stores that
+            // aren't ordered by hb with the last SC is picked.
+            //
+            // This is described in the paper (§4.5) and implemented in tsan11
+            // (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L160-L167)
+            // but absent in the operational semantics.
+            self.buffer.iter_mut().rev().for_each(|elem| {
+                if elem.timestamp <= thread_clock[elem.store_index] {
+                    elem.is_seqcst = true;
+                }
+            })
+        }
     }
 }
 

tests/run-pass/concurrency/weak_memory.rs

@@ -63,6 +63,28 @@ fn reads_value(loc: &AtomicUsize, val: usize) -> usize {
     val
 }
 
+// https://plv.mpi-sws.org/scfix/paper.pdf
+// Test case SB
+fn test_sc_store_buffering() {
+    let x = static_atomic(0);
+    let y = static_atomic(0);
+
+    let j1 = spawn(move || {
+        x.store(1, SeqCst);
+        y.load(SeqCst)
+    });
+
+    let j2 = spawn(move || {
+        y.store(1, SeqCst);
+        x.load(SeqCst)
+    });
+
+    let a = j1.join().unwrap();
+    let b = j2.join().unwrap();
+
+    assert_ne!((a, b), (0, 0));
+}
+
 // https://plv.mpi-sws.org/scfix/paper.pdf
 // 2.2 Second Problem: SC Fences are Too Weak
 fn test_rwc_syncs() {
@@ -247,6 +269,7 @@ pub fn main() {
     // prehaps each function should be its own test case so they
     // can be run in parallel
     for _ in 0..500 {
+        test_sc_store_buffering();
         test_mixed_access();
         test_load_buffering_acq_rel();
         test_message_passing();