Add simple data-race detector

src/data_race.rs

@@ -39,21 +39,14 @@
 //!
 //! 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
+//! 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.
+//! As per the paper a threads timestamp is only incremented after a release operation is performed
+//! so some atomic operations that only perform acquires do not increment the timestamp, due to shared
+//! code some atomic operations may increment the timestamp when not necessary but this has no effect
+//! on the data-race detection code.
 //!
 //! FIXME:
 //! currently we have our own local copy of the currently active thread index and names, this is due
@@ -516,7 +509,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
         Ok(old)
     }
 
-    /// Perform an atomic compare and exchange at a given memory location
+    /// Perform an atomic compare and exchange at a given memory location.
     /// On success an atomic RMW operation is performed and on failure
     /// only an atomic read occurs.
     fn atomic_compare_exchange_scalar(
@@ -640,7 +633,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
                     // Either Release | AcqRel | SeqCst
                     clocks.apply_release_fence();
                 }
-                Ok(())
+
+                // Increment timestamp if hase release semantics
+                Ok(atomic != AtomicFenceOp::Acquire)
             })
         } else {
             Ok(())
@@ -651,9 +646,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
 /// Vector clock metadata for a logical memory allocation.
 #[derive(Debug, Clone)]
 pub struct VClockAlloc {
-    /// Range of Vector clocks, this gives each byte a potentially
-    /// unqiue set of vector clocks, but merges identical information
-    /// together for improved efficiency.
+    /// Assigning each byte a MemoryCellClocks.
     alloc_ranges: RefCell<RangeMap<MemoryCellClocks>>,
 
     // Pointer to global state.
@@ -935,10 +928,12 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
                                 true,
                                 place_ptr,
                                 size,
-                            );
+                            ).map(|_| true);
                         }
                     }
-                    Ok(())
+
+                    // This conservatively assumes all operations have release semantics
+                    Ok(true)
                 })?;
 
                 // Log changes to atomic memory.
@@ -1159,6 +1154,7 @@ impl GlobalState {
         created.join_with(current);
 
         // Advance both threads after the synchronized operation.
+        // Both operations are considered to have release semantics.
         current.increment_clock(current_index);
         created.increment_clock(created_index);
     }
@@ -1185,11 +1181,9 @@ impl GlobalState {
 
         // The join thread happens-before the current thread
         // so update the current vector clock.
+        // Is not a release operation so the clock is not incremented.
         current.clock.join(join_clock);
 
-        // Increment clocks after atomic operation.
-        current.increment_clock(current_index);
-
         // Check the number of active threads, if the value is 1
         // then test for potentially disabling multi-threaded execution.
         let active_threads = self.active_thread_count.get();
@@ -1287,13 +1281,14 @@ impl GlobalState {
     /// operation may create.
     fn maybe_perform_sync_operation<'tcx>(
         &self,
-        op: impl FnOnce(VectorIdx, RefMut<'_, ThreadClockSet>) -> InterpResult<'tcx>,
+        op: impl FnOnce(VectorIdx, RefMut<'_, ThreadClockSet>) -> InterpResult<'tcx, bool>,
     ) -> InterpResult<'tcx> {
         if self.multi_threaded.get() {
             let (index, clocks) = self.current_thread_state_mut();
-            op(index, clocks)?;
-            let (_, mut clocks) = self.current_thread_state_mut();
-            clocks.increment_clock(index);
+            if op(index, clocks)? {
+                let (_, mut clocks) = self.current_thread_state_mut();
+                clocks.increment_clock(index);
+            }
         }
         Ok(())
     }
@@ -1313,10 +1308,11 @@ impl GlobalState {
 
     /// Acquire a lock, express that the previous call of
     /// `validate_lock_release` must happen before this.
+    /// As this is an acquire operation, the thread timestamp is not
+    /// incremented.
     pub fn validate_lock_acquire(&self, lock: &VClock, thread: ThreadId) {
-        let (index, mut clocks) = self.load_thread_state_mut(thread);
+        let (_, mut clocks) = self.load_thread_state_mut(thread);
         clocks.clock.join(&lock);
-        clocks.increment_clock(index);
     }
 
     /// Release a lock handle, express that this happens-before
@@ -1335,8 +1331,8 @@ 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
+    /// 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);

src/shims/posix/sync.rs

@@ -62,8 +62,6 @@ fn mutex_get_kind<'mir, 'tcx: 'mir>(
     mutex_op: OpTy<'tcx, Tag>,
 ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> {
     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::Relaxed
@@ -76,8 +74,6 @@ fn mutex_set_kind<'mir, 'tcx: 'mir>(
     kind: impl Into<ScalarMaybeUninit<Tag>>,
 ) -> 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::Relaxed
@@ -88,8 +84,6 @@ fn mutex_get_id<'mir, 'tcx: 'mir>(
     ecx: &MiriEvalContext<'mir, 'tcx>,
     mutex_op: OpTy<'tcx, Tag>,
 ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> {
-    //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::Relaxed
@@ -101,8 +95,6 @@ fn mutex_set_id<'mir, 'tcx: 'mir>(
     mutex_op: OpTy<'tcx, Tag>,
     id: impl Into<ScalarMaybeUninit<Tag>>,
 ) -> 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::Relaxed
@@ -135,8 +127,6 @@ 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<Tag>> {
     ecx.read_scalar_at_offset_atomic(
         rwlock_op, 4, ecx.machine.layouts.u32,
@@ -149,8 +139,6 @@ fn rwlock_set_id<'mir, 'tcx: 'mir>(
     rwlock_op: OpTy<'tcx, Tag>,
     id: impl Into<ScalarMaybeUninit<Tag>>,
 ) -> 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::Relaxed
@@ -207,8 +195,6 @@ fn cond_get_id<'mir, 'tcx: 'mir>(
     ecx: &MiriEvalContext<'mir, 'tcx>,
     cond_op: OpTy<'tcx, Tag>,
 ) -> InterpResult<'tcx, ScalarMaybeUninit<Tag>> {
-    //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::Relaxed
@@ -220,8 +206,6 @@ fn cond_set_id<'mir, 'tcx: 'mir>(
     cond_op: OpTy<'tcx, Tag>,
     id: impl Into<ScalarMaybeUninit<Tag>>,
 ) -> 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::Relaxed