From 8cab0d561716e4b1991683c608a0beda7ad6bd81 Mon Sep 17 00:00:00 2001 From: Ralf Jung Date: Sat, 20 Apr 2024 09:24:22 +0200 Subject: [PATCH] restrict VClock API surface --- src/tools/miri/src/concurrency/data_race.rs | 6 +- .../miri/src/concurrency/vector_clock.rs | 64 ++++++++++++------- 2 files changed, 44 insertions(+), 26 deletions(-) diff --git a/src/tools/miri/src/concurrency/data_race.rs b/src/tools/miri/src/concurrency/data_race.rs index 6c34716b592..2281609a049 100644 --- a/src/tools/miri/src/concurrency/data_race.rs +++ b/src/tools/miri/src/concurrency/data_race.rs @@ -547,9 +547,9 @@ fn read_race_detect( ) -> 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 @@ fn write_race_detect( ) -> 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 index 0178b01e0b8..2cd3d031b1e 100644 --- a/src/tools/miri/src/concurrency/vector_clock.rs +++ b/src/tools/miri/src/concurrency/vector_clock.rs @@ -4,7 +4,7 @@ use std::{ cmp::Ordering, fmt::Debug, - ops::{Index, IndexMut, Shr}, + ops::{Index, Shr}, }; use super::data_race::NaReadType; @@ -92,7 +92,7 @@ pub fn read_type(&self) -> NaReadType { } #[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 @@ fn cmp(&self, other: &Self) -> Ordering { 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 @@ pub fn new_with_index(index: VectorIdx, timestamp: VTimestamp) -> 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 @@ fn get_mut_with_min_len(&mut self, min_len: usize) -> &mut [VTimestamp] { /// 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 @@ pub fn join(&mut self, other: &Self) { } } - /// 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 @@ fn index(&self, index: VectorIdx) -> &VTimestamp { } } -impl IndexMut 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 @@ fn assert_order(l: &[u32], r: &[u32], o: Option) { "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); + } }