From a3b7839bbdde0c5856720dc885250752aefd4207 Mon Sep 17 00:00:00 2001
From: JCTyBlaidd <JCTyblaidd@users.noreply.github.com>
Date: Sun, 15 Nov 2020 20:12:58 +0000
Subject: [PATCH] Add comment regarding seq-cst ordering & add test for
 disabling the data-race detector.

---
 src/data_race.rs                              | 11 ++++++++
 .../concurrency/disable_data_race_detector.rs | 28 +++++++++++++++++++
 .../disable_data_race_detector.stderr         |  2 ++
 3 files changed, 41 insertions(+)
 create mode 100644 tests/run-pass/concurrency/disable_data_race_detector.rs
 create mode 100644 tests/run-pass/concurrency/disable_data_race_detector.stderr

diff --git a/src/data_race.rs b/src/data_race.rs
index 822ceab8fa0..bad757bc70e 100644
--- a/src/data_race.rs
+++ b/src/data_race.rs
@@ -27,6 +27,16 @@
 //! from acquire/release operations. If weak memory orderings are explored then this
 //! may need to change or be updated accordingly.
 //!
+//! Per the C++ spec for the memory model a sequentially consistent operation:
+//!   "A load operation with this memory order performs an acquire operation,
+//!    a store performs a release operation, and read-modify-write performs
+//!    both an acquire operation and a release operation, plus a single total
+//!    order exists in which all threads observe all modifications in the same
+//!    order (see Sequentially-consistent ordering below) "
+//! So in the absence of weak memory effects a seq-cst load & a seq-cst store is identical
+//! to a acquire load and a release store given the global sequentially consistent order
+//! of the schedule.
+//!
 //! FIXME:
 //! currently we have our own local copy of the currently active thread index and names, this is due
 //! in part to the inability to access the current location of threads.active_thread inside the AllocExtra
@@ -196,6 +206,7 @@ struct MemoryCellClocks {
 
     /// The vector-clock of the timestamp of the last read operation
     /// performed by a thread since the last write operation occured.
+    /// It is reset to zero on each write operation.
     read: VClock,
 
     /// Atomic acquire & release sequence tracking clocks.
diff --git a/tests/run-pass/concurrency/disable_data_race_detector.rs b/tests/run-pass/concurrency/disable_data_race_detector.rs
new file mode 100644
index 00000000000..e47a2079c20
--- /dev/null
+++ b/tests/run-pass/concurrency/disable_data_race_detector.rs
@@ -0,0 +1,28 @@
+// ignore-windows: Concurrency on Windows is not supported yet.
+// compile-flags: -Zmiri-disable-data-race-detector
+
+use std::thread::spawn;
+
+#[derive(Copy, Clone)]
+struct EvilSend<T>(pub T);
+
+unsafe impl<T> Send for EvilSend<T> {}
+unsafe impl<T> Sync for EvilSend<T> {}
+
+pub fn main() {
+    let mut a = 0u32;
+    let b = &mut a as *mut u32;
+    let c = EvilSend(b);
+    unsafe {
+        let j1 = spawn(move || {
+            *c.0 = 32;
+        });
+
+        let j2 = spawn(move || {
+            *c.0 = 64; //~ ERROR Data race
+        });
+
+        j1.join().unwrap();
+        j2.join().unwrap();
+    }
+}
diff --git a/tests/run-pass/concurrency/disable_data_race_detector.stderr b/tests/run-pass/concurrency/disable_data_race_detector.stderr
new file mode 100644
index 00000000000..7ba8087a9b4
--- /dev/null
+++ b/tests/run-pass/concurrency/disable_data_race_detector.stderr
@@ -0,0 +1,2 @@
+warning: thread support is experimental, no weak memory effects are currently emulated.
+