extend some comments regarding weak memory emulation

2 files changed, 17 insertions, 6 deletions

diff --git a/src/tools/miri/src/concurrency/data_race.rs b/src/tools/miri/src/concurrency/data_race.rs
index f86d1eb1dcb..e1fc22f6854 100644
--- a/src/tools/miri/src/concurrency/data_race.rs
+++ b/src/tools/miri/src/concurrency/data_race.rs
@@ -108,19 +108,25 @@ pub(super) struct ThreadClockSet {
     fence_acquire: VClock,
 
     /// The last timestamp of happens-before relations that
-    /// have been released by this thread by a fence.
+    /// have been released by this thread by a release fence.
     fence_release: VClock,
 
     /// Timestamps of the last SC fence performed by each
-    /// thread, updated when this thread performs an SC fence
+    /// thread, updated when this thread performs an SC fence.
+    /// This is never acquired into the thread's clock, it
+    /// just limits which old writes can be seen in weak memory emulation.
     pub(super) fence_seqcst: VClock,
 
     /// Timestamps of the last SC write performed by each
-    /// thread, updated when this thread performs an SC fence
+    /// thread, updated when this thread performs an SC fence.
+    /// This is never acquired into the thread's clock, it
+    /// just limits which old writes can be seen in weak memory emulation.
     pub(super) write_seqcst: VClock,
 
     /// Timestamps of the last SC fence performed by each
-    /// thread, updated when this thread performs an SC read
+    /// thread, updated when this thread performs an SC read.
+    /// This is never acquired into the thread's clock, it
+    /// just limits which old writes can be seen in weak memory emulation.
     pub(super) read_seqcst: VClock,
 }
 
diff --git a/src/tools/miri/src/concurrency/weak_memory.rs b/src/tools/miri/src/concurrency/weak_memory.rs
index c610f1999f7..7dac171b147 100644
--- a/src/tools/miri/src/concurrency/weak_memory.rs
+++ b/src/tools/miri/src/concurrency/weak_memory.rs
@@ -15,6 +15,10 @@
 //! Specifically, if an SC load reads from an atomic store of any ordering, then a later SC load cannot read from
 //! an earlier store in the location's modification order. This is to prevent creating a backwards S edge from the second
 //! load to the first, as a result of C++20's coherence-ordered before rules.
+//! (This seems to rule out behaviors that were actually permitted by the RC11 model 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.)
 //!
 //! Rust follows the C++20 memory model (except for the Consume ordering and some operations not performable through C++'s
 //! `std::atomic<T>` API). It is therefore possible for this implementation to generate behaviours never observable when the
@@ -138,6 +142,7 @@ struct StoreElement {
 
     /// The timestamp of the storing thread when it performed the store
     timestamp: VTimestamp,
+
     /// The value of this store. `None` means uninitialized.
     // FIXME: Currently, we cannot represent partial initialization.
     val: Option<Scalar>,
@@ -356,9 +361,9 @@ impl<'tcx> StoreBuffer {
                     false
                 } 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
+                    // 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)
+                    // and 4.1 (coherence-ordered before between SC makes global total order S).
                     false
                 } else {
                     true