src/tools/miri/tests/fail/stacked_borrows/retag_data_race_read.rs

   1 //! Make sure that a retag acts like a write for the data race model.
   2 //@compile-flags: -Zmiri-preemption-rate=0
   3 #[derive(Copy, Clone)]
   4 struct SendPtr(*mut u8);
   5
   6 unsafe impl Send for SendPtr {}
   7
   8 fn thread_1(p: SendPtr) {
   9     let p = p.0;
  10     unsafe {
  11         let _r = &*p;
  12     }
  13 }
  14
  15 fn thread_2(p: SendPtr) {
  16     let p = p.0;
  17     unsafe {
  18         *p = 5; //~ ERROR: Data race detected between Write on thread `<unnamed>` and Read on thread `<unnamed>`
  19     }
  20 }
  21
  22 fn main() {
  23     let mut x = 0;
  24     let p = std::ptr::addr_of_mut!(x);
  25     let p = SendPtr(p);
  26
  27     let t1 = std::thread::spawn(move || thread_1(p));
  28     let t2 = std::thread::spawn(move || thread_2(p));
  29     let _ = t1.join();
  30     let _ = t2.join();
  31 }