make Stacked Borrows retags act like data races

src/stacked_borrows/mod.rs

@@ -874,8 +874,8 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                 // We need a frozen-sensitive reborrow.
                 // We have to use shared references to alloc/memory_extra here since
                 // `visit_freeze_sensitive` needs to access the global state.
-                let extra = this.get_alloc_extra(alloc_id)?;
-                let mut stacked_borrows = extra
+                let alloc_extra = this.get_alloc_extra(alloc_id)?;
+                let mut stacked_borrows = alloc_extra
                     .stacked_borrows
                     .as_ref()
                     .expect("we should have Stacked Borrows data")
@@ -910,7 +910,16 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
                     );
                     stacked_borrows.for_each(range, dcx, |stack, dcx, exposed_tags| {
                         stack.grant(orig_tag, item, access, &global, dcx, exposed_tags)
-                    })
+                    })?;
+                    drop(global);
+                    if let Some(access) = access {
+                        assert!(access == AccessKind::Read);
+                        // Make sure the data race model also knows about this.
+                        if let Some(data_race) = alloc_extra.data_race.as_ref() {
+                            data_race.read(alloc_id, range, &this.machine)?;
+                        }
+                    }
+                    Ok(())
                 })?;
                 return Ok(Some(alloc_id));
             }
@@ -938,6 +947,14 @@ trait EvalContextPrivExt<'mir: 'ecx, 'tcx: 'mir, 'ecx>: crate::MiriInterpCxExt<'
         stacked_borrows.for_each(range, dcx, |stack, dcx, exposed_tags| {
             stack.grant(orig_tag, item, access, &global, dcx, exposed_tags)
         })?;
+        drop(global);
+        if let Some(access) = access {
+            assert!(access == AccessKind::Write);
+            // Make sure the data race model also knows about this.
+            if let Some(data_race) = alloc_extra.data_race.as_mut() {
+                data_race.write(alloc_id, range, machine)?;
+            }
+        }
 
         Ok(Some(alloc_id))
     }

tests/fail/stacked_borrows/retag_data_race_read.rs

@@ -0,0 +1,31 @@
+//! Make sure that a retag acts like a write for the data race model.
+//@compile-flags: -Zmiri-preemption-rate=0
+#[derive(Copy, Clone)]
+struct SendPtr(*mut u8);
+
+unsafe impl Send for SendPtr {}
+
+fn thread_1(p: SendPtr) {
+    let p = p.0;
+    unsafe {
+        let _r = &*p;
+    }
+}
+
+fn thread_2(p: SendPtr) {
+    let p = p.0;
+    unsafe {
+        *p = 5; //~ ERROR: Data race detected between Write on thread `<unnamed>` and Read on thread `<unnamed>`
+    }
+}
+
+fn main() {
+    let mut x = 0;
+    let p = std::ptr::addr_of_mut!(x);
+    let p = SendPtr(p);
+
+    let t1 = std::thread::spawn(move || thread_1(p));
+    let t2 = std::thread::spawn(move || thread_2(p));
+    let _ = t1.join();
+    let _ = t2.join();
+}

tests/fail/stacked_borrows/retag_data_race_read.stderr

@@ -0,0 +1,20 @@
+error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Read on thread `<unnamed>` at ALLOC
+  --> $DIR/retag_data_race_read.rs:LL:CC
+   |
+LL |         *p = 5;
+   |         ^^^^^^ Data race detected between Write on thread `<unnamed>` and Read on thread `<unnamed>` at ALLOC
+   |
+   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
+   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
+   = note: BACKTRACE:
+   = note: inside `thread_2` at $DIR/retag_data_race_read.rs:LL:CC
+note: inside closure at $DIR/retag_data_race_read.rs:LL:CC
+  --> $DIR/retag_data_race_read.rs:LL:CC
+   |
+LL |     let t2 = std::thread::spawn(move || thread_2(p));
+   |                                         ^^^^^^^^^^^
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+

tests/fail/stacked_borrows/retag_data_race_write.rs

@@ -0,0 +1,31 @@
+//! Make sure that a retag acts like a write for the data race model.
+//@compile-flags: -Zmiri-preemption-rate=0
+#[derive(Copy, Clone)]
+struct SendPtr(*mut u8);
+
+unsafe impl Send for SendPtr {}
+
+fn thread_1(p: SendPtr) {
+    let p = p.0;
+    unsafe {
+        let _r = &mut *p;
+    }
+}
+
+fn thread_2(p: SendPtr) {
+    let p = p.0;
+    unsafe {
+        *p = 5; //~ ERROR: Data race detected between Write on thread `<unnamed>` and Write on thread `<unnamed>`
+    }
+}
+
+fn main() {
+    let mut x = 0;
+    let p = std::ptr::addr_of_mut!(x);
+    let p = SendPtr(p);
+
+    let t1 = std::thread::spawn(move || thread_1(p));
+    let t2 = std::thread::spawn(move || thread_2(p));
+    let _ = t1.join();
+    let _ = t2.join();
+}

tests/fail/stacked_borrows/retag_data_race_write.stderr

@@ -0,0 +1,20 @@
+error: Undefined Behavior: Data race detected between Write on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC
+  --> $DIR/retag_data_race_write.rs:LL:CC
+   |
+LL |         *p = 5;
+   |         ^^^^^^ Data race detected between Write on thread `<unnamed>` and Write on thread `<unnamed>` at ALLOC
+   |
+   = help: this indicates a bug in the program: it performed an invalid operation, and caused Undefined Behavior
+   = help: see https://doc.rust-lang.org/nightly/reference/behavior-considered-undefined.html for further information
+   = note: BACKTRACE:
+   = note: inside `thread_2` at $DIR/retag_data_race_write.rs:LL:CC
+note: inside closure at $DIR/retag_data_race_write.rs:LL:CC
+  --> $DIR/retag_data_race_write.rs:LL:CC
+   |
+LL |     let t2 = std::thread::spawn(move || thread_2(p));
+   |                                         ^^^^^^^^^^^
+
+note: some details are omitted, run with `MIRIFLAGS=-Zmiri-backtrace=full` for a verbose backtrace
+
+error: aborting due to previous error
+