restrict VClock API surface

RalfJung · RalfJung · commit 8cab0d561716 · 2024-04-20T10:09:31.000+02:00
diff --git a/src/tools/miri/src/concurrency/data_race.rs b/src/tools/miri/src/concurrency/data_race.rs
@@ -547,9 +547,9 @@ impl MemoryCellClocks {
     ) -> Result<(), DataRace> {
         trace!("Unsynchronized read with vectors: {:#?} :: {:#?}", self, thread_clocks);
         if !current_span.is_dummy() {
-            thread_clocks.clock[index].span = current_span;
+            thread_clocks.clock.index_mut(index).span = current_span;
         }
-        thread_clocks.clock[index].set_read_type(read_type);
+        thread_clocks.clock.index_mut(index).set_read_type(read_type);
         if self.write_was_before(&thread_clocks.clock) {
             let race_free = if let Some(atomic) = self.atomic() {
                 // We must be ordered-after all atomic accesses, reads and writes.
@@ -577,7 +577,7 @@ impl MemoryCellClocks {
     ) -> Result<(), DataRace> {
         trace!("Unsynchronized write with vectors: {:#?} :: {:#?}", self, thread_clocks);
         if !current_span.is_dummy() {
-            thread_clocks.clock[index].span = current_span;
+            thread_clocks.clock.index_mut(index).span = current_span;
         }
         if self.write_was_before(&thread_clocks.clock) && self.read <= thread_clocks.clock {
             let race_free = if let Some(atomic) = self.atomic() {
diff --git a/src/tools/miri/src/concurrency/vector_clock.rs b/src/tools/miri/src/concurrency/vector_clock.rs
@@ -4,7 +4,7 @@ use smallvec::SmallVec;
 use std::{
     cmp::Ordering,
     fmt::Debug,
-    ops::{Index, IndexMut, Shr},
+    ops::{Index, Shr},
 };
 
 use super::data_race::NaReadType;
@@ -92,7 +92,7 @@ impl VTimestamp {
     }
 
     #[inline]
-    pub fn set_read_type(&mut self, read_type: NaReadType) {
+    pub(super) fn set_read_type(&mut self, read_type: NaReadType) {
         self.time_and_read_type = Self::encode_time_and_read_type(self.time(), read_type);
     }
 
@@ -138,7 +138,7 @@ pub struct VClock(SmallVec<[VTimestamp; SMALL_VECTOR]>);
 impl VClock {
     /// Create a new vector-clock containing all zeros except
     /// for a value at the given index
-    pub fn new_with_index(index: VectorIdx, timestamp: VTimestamp) -> VClock {
+    pub(super) fn new_with_index(index: VectorIdx, timestamp: VTimestamp) -> VClock {
         let len = index.index() + 1;
         let mut vec = smallvec::smallvec![VTimestamp::ZERO; len];
         vec[index.index()] = timestamp;
@@ -147,10 +147,16 @@ impl VClock {
 
     /// Load the internal timestamp slice in the vector clock
     #[inline]
-    pub fn as_slice(&self) -> &[VTimestamp] {
+    pub(super) fn as_slice(&self) -> &[VTimestamp] {
+        debug_assert!(!self.0.last().is_some_and(|t| t.time() == 0));
         self.0.as_slice()
     }
 
+    #[inline]
+    pub(super) fn index_mut(&mut self, index: VectorIdx) -> &mut VTimestamp {
+        self.0.as_mut_slice().get_mut(index.to_u32() as usize).unwrap()
+    }
+
     /// Get a mutable slice to the internal vector with minimum `min_len`
     /// elements. To preserve invariants, the caller must modify
     /// the `min_len`-1 nth element to a non-zero value
@@ -166,7 +172,7 @@ impl VClock {
     /// Increment the vector clock at a known index
     /// this will panic if the vector index overflows
     #[inline]
-    pub fn increment_index(&mut self, idx: VectorIdx, current_span: Span) {
+    pub(super) fn increment_index(&mut self, idx: VectorIdx, current_span: Span) {
         let idx = idx.index();
         let mut_slice = self.get_mut_with_min_len(idx + 1);
         let idx_ref = &mut mut_slice[idx];
@@ -190,28 +196,36 @@ impl VClock {
         }
     }
 
-    /// Set the element at the current index of the vector
-    pub fn set_at_index(&mut self, other: &Self, idx: VectorIdx) {
+    /// Set the element at the current index of the vector. May only increase elements.
+    pub(super) fn set_at_index(&mut self, other: &Self, idx: VectorIdx) {
+        let new_timestamp = other[idx];
+        // Setting to 0 is different, since the last element cannot be 0.
+        if new_timestamp.time() == 0 {
+            if idx.index() >= self.0.len() {
+                // This index does not even exist yet in our clock. Just do nothing.
+                return;
+            }
+            // This changes an existing element. Since it can only increase, that
+            // can never make the last element 0.
+        }
+
         let mut_slice = self.get_mut_with_min_len(idx.index() + 1);
+        let mut_timestamp = &mut mut_slice[idx.index()];
 
-        let prev_span = mut_slice[idx.index()].span;
+        let prev_span = mut_timestamp.span;
 
-        mut_slice[idx.index()] = other[idx];
+        assert!(*mut_timestamp <= new_timestamp, "set_at_index: may only increase the timestamp");
+        *mut_timestamp = new_timestamp;
 
-        let span = &mut mut_slice[idx.index()].span;
+        let span = &mut mut_timestamp.span;
         *span = span.substitute_dummy(prev_span);
     }
 
     /// Set the vector to the all-zero vector
     #[inline]
-    pub fn set_zero_vector(&mut self) {
+    pub(super) fn set_zero_vector(&mut self) {
         self.0.clear();
     }
-
-    /// Return if this vector is the all-zero vector
-    pub fn is_zero_vector(&self) -> bool {
-        self.0.is_empty()
-    }
 }
 
 impl Clone for VClock {
@@ -407,13 +421,6 @@ impl Index<VectorIdx> for VClock {
     }
 }
 
-impl IndexMut<VectorIdx> for VClock {
-    #[inline]
-    fn index_mut(&mut self, index: VectorIdx) -> &mut VTimestamp {
-        self.0.as_mut_slice().get_mut(index.to_u32() as usize).unwrap()
-    }
-}
-
 /// Test vector clock ordering operations
 ///  data-race detection is tested in the external
 ///  test suite
@@ -553,4 +560,15 @@ mod tests {
             "Invalid alt (>=):\n l: {l:?}\n r: {r:?}"
         );
     }
+
+    #[test]
+    fn set_index_to_0() {
+        let mut clock1 = from_slice(&[0, 1, 2, 3]);
+        let clock2 = from_slice(&[0, 2, 3, 4, 0, 5]);
+        // Naively, this would extend clock1 with a new index and set it to 0, making
+        // the last index 0. Make sure that does not happen.
+        clock1.set_at_index(&clock2, VectorIdx(4));
+        // This must not have made the last element 0.
+        assert!(clock1.0.last().unwrap().time() != 0);
+    }
 }
