From 1b73d6706f511579edd9fb15bcf52110b5b3a7fc Mon Sep 17 00:00:00 2001
From: Andy Wang <cbeuw.andy@gmail.com>
Date: Wed, 2 Feb 2022 23:16:02 +0000
Subject: [PATCH] Comments addressing deviations from paper's operational
 semantics

---
 src/weak_memory.rs | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/src/weak_memory.rs b/src/weak_memory.rs
index ab07baf9e4..8ff21584e7 100644
--- a/src/weak_memory.rs
+++ b/src/weak_memory.rs
@@ -110,6 +110,16 @@ impl Default for StoreBuffer {
     }
 }
 
+// Operational semantics in the paper has several problems:
+// 1. Store elements keep a copy of the atomic object's vector clock (AtomicCellClocks::sync_vector in miri),
+// but this is not used anywhere so it's omitted
+// 2. §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)
+// 3. W_SC ; R_SC case requires the SC load to ignore all but last store maked SC (stores not marked SC are not
+// affected). But this rule is applied to all loads in ReadsFromSet (last two lines of code), not just SC load.
+// This is implemented correctly in tsan11
+// (https://github.com/ChrisLidbury/tsan11/blob/ecbd6b81e9b9454e01cba78eb9d88684168132c7/lib/tsan/rtl/tsan_relaxed.cc#L295)
 impl<'mir, 'tcx: 'mir> StoreBuffer {
     /// Selects a valid store element in the buffer.
     /// The buffer does not contain the value used to initialise the atomic object
@@ -134,7 +144,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
                 if !keep_searching {
                     return false;
                 }
-                // CoWR: if a store in modification order happens-before the current load,
+                // CoWR: if a store happens-before the current load,
                 // then we can't read-from anything earlier in modification order.
                 if store_elem.timestamp <= clocks.clock[store_elem.store_index] {
                     log::info!("Stopped due to coherent write-read");
@@ -196,9 +206,7 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
         candidates.choose(rng)
     }
 
-    /// ATOMIC STORE IMPL in the paper
-    /// The paper also wants the variable's clock (AtomicMemoryCellClocks::sync_vector in our code)
-    /// to be in the store element, but it's not used anywhere so we don't actually need it
+    /// ATOMIC STORE IMPL in the paper (except we don't need the location's vector clock)
     fn store_impl(
         &mut self,
         val: ScalarMaybeUninit<Tag>,
@@ -223,12 +231,8 @@ impl<'mir, 'tcx: 'mir> StoreBuffer {
         }
         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
+            // 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.
-            //
-            // 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;