diff --git a/src/data_race.rs b/src/data_race.rs index b9542f6e2d62..3f70631d1362 100644 --- a/src/data_race.rs +++ b/src/data_race.rs @@ -37,6 +37,24 @@ //! to a acquire load and a release store given the global sequentially consistent order //! of the schedule. //! +//! The timestamps used in the data-race detector assign each sequence of non-atomic operations +//! followed by a single atomic or concurrent operation a single timestamp. +//! Write, Read, Write, ThreadJoin will be represented by a single timestamp value on a thread +//! This is because extra increment operations between the operations in the sequence are not +//! required for accurate reporting of data-race values. +//! +//! If the timestamp was not incremented after the atomic operation, then data-races would not be detected: +//! Example - this should report a data-race but does not: +//! t1: (x,0), atomic[release A], t1=(x+1, 0 ), write(var B), +//! t2: (0,y) , atomic[acquire A], t2=(x+1, y+1), ,write(var B) +//! +//! The timestamp is not incremented before an atomic operation, since the result is indistinguishable +//! from the value not being incremented. +//! t: (x, 0), atomic[release _], (x + 1, 0) || (0, y), atomic[acquire _], (x, _) +//! vs t: (x, 0), atomic[release _], (x + 1, 0) || (0, y), atomic[acquire _], (x+1, _) +//! Both result in the sequence on thread x up to and including the atomic release as happening +//! before the acquire. +//! //! 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 @@ -499,7 +517,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> { } /// Perform an atomic compare and exchange at a given memory location - /// on success an atomic RMW operation is performed and on failure + /// On success an atomic RMW operation is performed and on failure /// only an atomic read occurs. fn atomic_compare_exchange_scalar( &mut self, @@ -1136,9 +1154,6 @@ impl GlobalState { // Now load the two clocks and configure the initial state. let (current, created) = vector_clocks.pick2_mut(current_index, created_index); - // Advance the current thread before the synchronized operation. - current.increment_clock(current_index); - // Join the created with current, since the current threads // previous actions happen-before the created thread. created.join_with(current); @@ -1167,14 +1182,12 @@ impl GlobalState { .as_ref() .expect("Joined with thread but thread has not terminated"); - // Pre increment clocks before atomic operation. - current.increment_clock(current_index); // The join thread happens-before the current thread // so update the current vector clock. current.clock.join(join_clock); - // Post increment clocks after atomic operation. + // Increment clocks after atomic operation. current.increment_clock(current_index); // Check the number of active threads, if the value is 1 @@ -1277,8 +1290,7 @@ impl GlobalState { op: impl FnOnce(VectorIdx, RefMut<'_, ThreadClockSet>) -> InterpResult<'tcx>, ) -> InterpResult<'tcx> { if self.multi_threaded.get() { - let (index, mut clocks) = self.current_thread_state_mut(); - clocks.increment_clock(index); + let (index, clocks) = self.current_thread_state_mut(); op(index, clocks)?; let (_, mut clocks) = self.current_thread_state_mut(); clocks.increment_clock(index); @@ -1303,16 +1315,18 @@ impl GlobalState { /// `validate_lock_release` must happen before this. pub fn validate_lock_acquire(&self, lock: &VClock, thread: ThreadId) { let (index, mut clocks) = self.load_thread_state_mut(thread); - clocks.increment_clock(index); clocks.clock.join(&lock); clocks.increment_clock(index); } /// Release a lock handle, express that this happens-before /// any subsequent calls to `validate_lock_acquire`. + /// For normal locks this should be equivalent to `validate_lock_release_shared` + /// since an acquire operation should have occured before, however + /// for futex & cond-var operations this is not the case and this + /// operation must be used. pub fn validate_lock_release(&self, lock: &mut VClock, thread: ThreadId) { let (index, mut clocks) = self.load_thread_state_mut(thread); - clocks.increment_clock(index); lock.clone_from(&clocks.clock); clocks.increment_clock(index); } @@ -1321,9 +1335,11 @@ impl GlobalState { /// any subsequent calls to `validate_lock_acquire` as well /// as any previous calls to this function after any /// `validate_lock_release` calls. + /// For normal locks this should be equivalent to `validate_lock_release` + /// this function only exists for joining over the set of concurrent readers + /// in a read-write lock and should not be used for anything else. pub fn validate_lock_release_shared(&self, lock: &mut VClock, thread: ThreadId) { let (index, mut clocks) = self.load_thread_state_mut(thread); - clocks.increment_clock(index); lock.join(&clocks.clock); clocks.increment_clock(index); } diff --git a/src/shims/posix/sync.rs b/src/shims/posix/sync.rs index 64308d06139f..efa441299194 100644 --- a/src/shims/posix/sync.rs +++ b/src/shims/posix/sync.rs @@ -62,9 +62,11 @@ fn mutex_get_kind<'mir, 'tcx: 'mir>( mutex_op: OpTy<'tcx, Tag>, ) -> InterpResult<'tcx, ScalarMaybeUninit> { let offset = if ecx.pointer_size().bytes() == 8 { 16 } else { 12 }; + //FIXME: this has been made atomic to fix data-race reporting inside the internal + // mutex implementation, it may not need to be atomic. ecx.read_scalar_at_offset_atomic( mutex_op, offset, ecx.machine.layouts.i32, - AtomicReadOp::Acquire + AtomicReadOp::Relaxed ) } @@ -74,9 +76,11 @@ fn mutex_set_kind<'mir, 'tcx: 'mir>( kind: impl Into>, ) -> InterpResult<'tcx, ()> { let offset = if ecx.pointer_size().bytes() == 8 { 16 } else { 12 }; + //FIXME: this has been made atomic to fix data-race reporting inside the internal + // mutex implementation, it may not need to be atomic. ecx.write_scalar_at_offset_atomic( - mutex_op, offset, kind, ecx.machine.layouts.i32, - AtomicWriteOp::Release + mutex_op, offset, kind, ecx.machine.layouts.i32, + AtomicWriteOp::Relaxed ) } @@ -84,8 +88,11 @@ fn mutex_get_id<'mir, 'tcx: 'mir>( ecx: &MiriEvalContext<'mir, 'tcx>, mutex_op: OpTy<'tcx, Tag>, ) -> InterpResult<'tcx, ScalarMaybeUninit> { + //FIXME: this has been made atomic to fix data-race reporting inside the internal + // mutex implementation, it may not need to be atomic. ecx.read_scalar_at_offset_atomic( - mutex_op, 4, ecx.machine.layouts.u32, AtomicReadOp::Acquire + mutex_op, 4, ecx.machine.layouts.u32, + AtomicReadOp::Relaxed ) } @@ -94,9 +101,11 @@ fn mutex_set_id<'mir, 'tcx: 'mir>( mutex_op: OpTy<'tcx, Tag>, id: impl Into>, ) -> InterpResult<'tcx, ()> { + //FIXME: this has been made atomic to fix data-race reporting inside the internal + // mutex implementation, it may not need to be atomic. ecx.write_scalar_at_offset_atomic( mutex_op, 4, id, ecx.machine.layouts.u32, - AtomicWriteOp::Release + AtomicWriteOp::Relaxed ) } @@ -126,10 +135,12 @@ fn mutex_get_or_create_id<'mir, 'tcx: 'mir>( fn rwlock_get_id<'mir, 'tcx: 'mir>( ecx: &MiriEvalContext<'mir, 'tcx>, rwlock_op: OpTy<'tcx, Tag>, + //FIXME: this has been made atomic to fix data-race reporting inside the internal + // rw-lock implementation, it may not need to be atomic. ) -> InterpResult<'tcx, ScalarMaybeUninit> { ecx.read_scalar_at_offset_atomic( rwlock_op, 4, ecx.machine.layouts.u32, - AtomicReadOp::Acquire + AtomicReadOp::Relaxed ) } @@ -138,9 +149,11 @@ fn rwlock_set_id<'mir, 'tcx: 'mir>( rwlock_op: OpTy<'tcx, Tag>, id: impl Into>, ) -> InterpResult<'tcx, ()> { + //FIXME: this has been made atomic to fix data-race reporting inside the internal + // rw-lock implementation, it may not need to be atomic. ecx.write_scalar_at_offset_atomic( rwlock_op, 4, id, ecx.machine.layouts.u32, - AtomicWriteOp::Release + AtomicWriteOp::Relaxed ) } @@ -194,9 +207,11 @@ fn cond_get_id<'mir, 'tcx: 'mir>( ecx: &MiriEvalContext<'mir, 'tcx>, cond_op: OpTy<'tcx, Tag>, ) -> InterpResult<'tcx, ScalarMaybeUninit> { + //FIXME: this has been made atomic to fix data-race reporting inside the internal + // cond-var implementation, it may not need to be atomic. ecx.read_scalar_at_offset_atomic( cond_op, 4, ecx.machine.layouts.u32, - AtomicReadOp::Acquire + AtomicReadOp::Relaxed ) } @@ -205,9 +220,11 @@ fn cond_set_id<'mir, 'tcx: 'mir>( cond_op: OpTy<'tcx, Tag>, id: impl Into>, ) -> InterpResult<'tcx, ()> { + //FIXME: this has been made atomic to fix data-race reporting inside the internal + // cond-var implementation, it may not need to be atomic. ecx.write_scalar_at_offset_atomic( cond_op, 4, id, ecx.machine.layouts.u32, - AtomicWriteOp::Release + AtomicWriteOp::Relaxed ) } diff --git a/src/shims/posix/thread.rs b/src/shims/posix/thread.rs index 847d083bfa9f..0ea20cdff6cb 100644 --- a/src/shims/posix/thread.rs +++ b/src/shims/posix/thread.rs @@ -15,7 +15,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx let this = self.eval_context_mut(); this.tcx.sess.warn( - "thread support is experimental, no weak memory effects are currently emulated.", + "thread support is experimental and incomplete: weak memory effects are not emulated." ); // Create the new thread diff --git a/tests/compile-fail/data_race/atomic_read_write_race.rs b/tests/compile-fail/data_race/atomic_read_na_write_race1.rs similarity index 100% rename from tests/compile-fail/data_race/atomic_read_write_race.rs rename to tests/compile-fail/data_race/atomic_read_na_write_race1.rs diff --git a/tests/compile-fail/data_race/atomic_read_write_race_alt.rs b/tests/compile-fail/data_race/atomic_read_na_write_race2.rs similarity index 100% rename from tests/compile-fail/data_race/atomic_read_write_race_alt.rs rename to tests/compile-fail/data_race/atomic_read_na_write_race2.rs diff --git a/tests/compile-fail/data_race/atomic_write_read_race.rs b/tests/compile-fail/data_race/atomic_write_na_read_race1.rs similarity index 100% rename from tests/compile-fail/data_race/atomic_write_read_race.rs rename to tests/compile-fail/data_race/atomic_write_na_read_race1.rs diff --git a/tests/compile-fail/data_race/atomic_write_read_race_alt.rs b/tests/compile-fail/data_race/atomic_write_na_read_race2.rs similarity index 100% rename from tests/compile-fail/data_race/atomic_write_read_race_alt.rs rename to tests/compile-fail/data_race/atomic_write_na_read_race2.rs diff --git a/tests/compile-fail/data_race/atomic_write_write_race.rs b/tests/compile-fail/data_race/atomic_write_na_write_race1.rs similarity index 100% rename from tests/compile-fail/data_race/atomic_write_write_race.rs rename to tests/compile-fail/data_race/atomic_write_na_write_race1.rs diff --git a/tests/compile-fail/data_race/atomic_write_write_race_alt.rs b/tests/compile-fail/data_race/atomic_write_na_write_race2.rs similarity index 100% rename from tests/compile-fail/data_race/atomic_write_write_race_alt.rs rename to tests/compile-fail/data_race/atomic_write_na_write_race2.rs diff --git a/tests/compile-fail/data_race/dangling_thread_async_race.rs b/tests/compile-fail/data_race/dangling_thread_async_race.rs index 6af5706835e3..d8b5d82f8304 100644 --- a/tests/compile-fail/data_race/dangling_thread_async_race.rs +++ b/tests/compile-fail/data_race/dangling_thread_async_race.rs @@ -29,9 +29,9 @@ fn main() { sleep(Duration::from_millis(100)); // Spawn and immediately join a thread - // to execute the join code-path - // and ensure that data-race detection - // remains enabled + // to execute the join code-path + // and ensure that data-race detection + // remains enabled nevertheless. spawn(|| ()).join().unwrap(); let join2 = unsafe { diff --git a/tests/compile-fail/data_race/dangling_thread_race.rs b/tests/compile-fail/data_race/dangling_thread_race.rs index c37f303bbab2..172b05bd4f0b 100644 --- a/tests/compile-fail/data_race/dangling_thread_race.rs +++ b/tests/compile-fail/data_race/dangling_thread_race.rs @@ -29,9 +29,9 @@ fn main() { sleep(Duration::from_millis(100)); // Spawn and immediately join a thread - // to execute the join code-path - // and ensure that data-race detection - // remains enabled + // to execute the join code-path + // and ensure that data-race detection + // remains enabled nevertheless. spawn(|| ()).join().unwrap(); diff --git a/tests/compile-fail/data_race/enable_after_join_to_main.rs b/tests/compile-fail/data_race/enable_after_join_to_main.rs index fba7ba4841cc..c29431777137 100644 --- a/tests/compile-fail/data_race/enable_after_join_to_main.rs +++ b/tests/compile-fail/data_race/enable_after_join_to_main.rs @@ -9,7 +9,7 @@ unsafe impl Send for EvilSend {} unsafe impl Sync for EvilSend {} pub fn main() { - // Enable and the join with multiple threads + // Enable and then join with multiple threads. let t1 = spawn(|| ()); let t2 = spawn(|| ()); let t3 = spawn(|| ()); @@ -19,7 +19,7 @@ pub fn main() { t3.join().unwrap(); t4.join().unwrap(); - // Perform write-write data race detection + // Perform write-write data race detection. let mut a = 0u32; let b = &mut a as *mut u32; let c = EvilSend(b); diff --git a/tests/compile-fail/data_race/relax_acquire_race.rs b/tests/compile-fail/data_race/relax_acquire_race.rs index 4b736e57208a..2ae0aacbcf77 100644 --- a/tests/compile-fail/data_race/relax_acquire_race.rs +++ b/tests/compile-fail/data_race/relax_acquire_race.rs @@ -16,6 +16,13 @@ pub fn main() { let b = &mut a as *mut u32; let c = EvilSend(b); + // Note: this is scheduler-dependent + // the operations need to occur in + // order: + // 1. store release : 1 + // 2. load acquire : 1 + // 3. store relaxed : 2 + // 4. load acquire : 2 unsafe { let j1 = spawn(move || { *c.0 = 1; diff --git a/tests/compile-fail/data_race/release_seq_race.rs b/tests/compile-fail/data_race/release_seq_race.rs index 0278e9864353..59263cb71204 100644 --- a/tests/compile-fail/data_race/release_seq_race.rs +++ b/tests/compile-fail/data_race/release_seq_race.rs @@ -18,6 +18,14 @@ pub fn main() { let b = &mut a as *mut u32; let c = EvilSend(b); + // Note: this is scheduler-dependent + // the operations need to occur in + // order, the sleep operations currently + // force the desired ordering: + // 1. store release : 1 + // 2. store relaxed : 2 + // 3. store relaxed : 3 + // 4. load acquire : 3 unsafe { let j1 = spawn(move || { *c.0 = 1; diff --git a/tests/compile-fail/data_race/rmw_race.rs b/tests/compile-fail/data_race/rmw_race.rs index c533f595f160..e523f8b374cc 100644 --- a/tests/compile-fail/data_race/rmw_race.rs +++ b/tests/compile-fail/data_race/rmw_race.rs @@ -16,6 +16,13 @@ pub fn main() { let b = &mut a as *mut u32; let c = EvilSend(b); + // Note: this is scheduler-dependent + // the operations need to occur in + // order: + // 1. store release : 1 + // 2. RMW relaxed : 1 -> 2 + // 3. store relaxed : 3 + // 4. load acquire : 3 unsafe { let j1 = spawn(move || { *c.0 = 1; diff --git a/tests/run-pass/concurrency/data_race.stderr b/tests/run-pass/concurrency/data_race.stderr index 7ba8087a9b4b..03676519d4f1 100644 --- a/tests/run-pass/concurrency/data_race.stderr +++ b/tests/run-pass/concurrency/data_race.stderr @@ -1,2 +1,2 @@ -warning: thread support is experimental, no weak memory effects are currently emulated. +warning: thread support is experimental and incomplete: weak memory effects are not emulated. diff --git a/tests/run-pass/concurrency/disable_data_race_detector.rs b/tests/run-pass/concurrency/disable_data_race_detector.rs index e47a2079c205..8b2d180f11d4 100644 --- a/tests/run-pass/concurrency/disable_data_race_detector.rs +++ b/tests/run-pass/concurrency/disable_data_race_detector.rs @@ -19,7 +19,7 @@ pub fn main() { }); let j2 = spawn(move || { - *c.0 = 64; //~ ERROR Data race + *c.0 = 64; //~ ERROR Data race (but not detected as the detector is disabled) }); j1.join().unwrap(); diff --git a/tests/run-pass/concurrency/disable_data_race_detector.stderr b/tests/run-pass/concurrency/disable_data_race_detector.stderr index 7ba8087a9b4b..03676519d4f1 100644 --- a/tests/run-pass/concurrency/disable_data_race_detector.stderr +++ b/tests/run-pass/concurrency/disable_data_race_detector.stderr @@ -1,2 +1,2 @@ -warning: thread support is experimental, no weak memory effects are currently emulated. +warning: thread support is experimental and incomplete: weak memory effects are not emulated. diff --git a/tests/run-pass/concurrency/linux-futex.stderr b/tests/run-pass/concurrency/linux-futex.stderr index 7ba8087a9b4b..03676519d4f1 100644 --- a/tests/run-pass/concurrency/linux-futex.stderr +++ b/tests/run-pass/concurrency/linux-futex.stderr @@ -1,2 +1,2 @@ -warning: thread support is experimental, no weak memory effects are currently emulated. +warning: thread support is experimental and incomplete: weak memory effects are not emulated. diff --git a/tests/run-pass/concurrency/simple.stderr b/tests/run-pass/concurrency/simple.stderr index 24444fdc17c1..f46b1442d749 100644 --- a/tests/run-pass/concurrency/simple.stderr +++ b/tests/run-pass/concurrency/simple.stderr @@ -1,4 +1,4 @@ -warning: thread support is experimental, no weak memory effects are currently emulated. +warning: thread support is experimental and incomplete: weak memory effects are not emulated. thread '' panicked at 'Hello!', $DIR/simple.rs:54:9 note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace diff --git a/tests/run-pass/concurrency/sync.stderr b/tests/run-pass/concurrency/sync.stderr index 7ba8087a9b4b..03676519d4f1 100644 --- a/tests/run-pass/concurrency/sync.stderr +++ b/tests/run-pass/concurrency/sync.stderr @@ -1,2 +1,2 @@ -warning: thread support is experimental, no weak memory effects are currently emulated. +warning: thread support is experimental and incomplete: weak memory effects are not emulated. diff --git a/tests/run-pass/concurrency/thread_locals.stderr b/tests/run-pass/concurrency/thread_locals.stderr index 7ba8087a9b4b..03676519d4f1 100644 --- a/tests/run-pass/concurrency/thread_locals.stderr +++ b/tests/run-pass/concurrency/thread_locals.stderr @@ -1,2 +1,2 @@ -warning: thread support is experimental, no weak memory effects are currently emulated. +warning: thread support is experimental and incomplete: weak memory effects are not emulated. diff --git a/tests/run-pass/concurrency/tls_lib_drop.stderr b/tests/run-pass/concurrency/tls_lib_drop.stderr index 7ba8087a9b4b..03676519d4f1 100644 --- a/tests/run-pass/concurrency/tls_lib_drop.stderr +++ b/tests/run-pass/concurrency/tls_lib_drop.stderr @@ -1,2 +1,2 @@ -warning: thread support is experimental, no weak memory effects are currently emulated. +warning: thread support is experimental and incomplete: weak memory effects are not emulated. diff --git a/tests/run-pass/libc.stderr b/tests/run-pass/libc.stderr index 7ba8087a9b4b..03676519d4f1 100644 --- a/tests/run-pass/libc.stderr +++ b/tests/run-pass/libc.stderr @@ -1,2 +1,2 @@ -warning: thread support is experimental, no weak memory effects are currently emulated. +warning: thread support is experimental and incomplete: weak memory effects are not emulated. diff --git a/tests/run-pass/panic/concurrent-panic.stderr b/tests/run-pass/panic/concurrent-panic.stderr index 885385a8dd93..1ee688c1d32c 100644 --- a/tests/run-pass/panic/concurrent-panic.stderr +++ b/tests/run-pass/panic/concurrent-panic.stderr @@ -1,4 +1,4 @@ -warning: thread support is experimental, no weak memory effects are currently emulated. +warning: thread support is experimental and incomplete: weak memory effects are not emulated. Thread 1 starting, will block on mutex Thread 1 reported it has started