@@ -547,9 +547,9 @@ impl MemoryCellClocks {
547547 ) -> Result < ( ) , DataRace > {
548548 trace ! ( "Unsynchronized read with vectors: {:#?} :: {:#?}" , self , thread_clocks) ;
549549 if !current_span. is_dummy ( ) {
550- thread_clocks. clock [ index] . span = current_span;
550+ thread_clocks. clock . index_mut ( index) . span = current_span;
551551 }
552- thread_clocks. clock [ index] . set_read_type ( read_type) ;
552+ thread_clocks. clock . index_mut ( index) . set_read_type ( read_type) ;
553553 if self . write_was_before ( & thread_clocks. clock ) {
554554 let race_free = if let Some ( atomic) = self . atomic ( ) {
555555 // We must be ordered-after all atomic accesses, reads and writes.
@@ -577,7 +577,7 @@ impl MemoryCellClocks {
577577 ) -> Result < ( ) , DataRace > {
578578 trace ! ( "Unsynchronized write with vectors: {:#?} :: {:#?}" , self , thread_clocks) ;
579579 if !current_span. is_dummy ( ) {
580- thread_clocks. clock [ index] . span = current_span;
580+ thread_clocks. clock . index_mut ( index) . span = current_span;
581581 }
582582 if self . write_was_before ( & thread_clocks. clock ) && self . read <= thread_clocks. clock {
583583 let race_free = if let Some ( atomic) = self . atomic ( ) {
@@ -1701,49 +1701,34 @@ impl GlobalState {
17011701 format ! ( "thread `{thread_name}`" )
17021702 }
17031703
1704- /// Acquire a lock, express that the previous call of
1705- /// `validate_lock_release` must happen before this .
1704+ /// Acquire the given clock into the given thread, establishing synchronization with
1705+ /// the moment when that clock snapshot was taken via `release_clock` .
17061706 /// As this is an acquire operation, the thread timestamp is not
17071707 /// incremented.
1708- pub fn validate_lock_acquire ( & self , lock : & VClock , thread : ThreadId ) {
1709- let ( _, mut clocks) = self . load_thread_state_mut ( thread) ;
1708+ pub fn acquire_clock ( & self , lock : & VClock , thread : ThreadId ) {
1709+ let ( _, mut clocks) = self . thread_state_mut ( thread) ;
17101710 clocks. clock . join ( lock) ;
17111711 }
17121712
1713- /// Release a lock handle, express that this happens-before
1714- /// any subsequent calls to `validate_lock_acquire`.
1715- /// For normal locks this should be equivalent to `validate_lock_release_shared`
1716- /// since an acquire operation should have occurred before, however
1717- /// for futex & condvar operations this is not the case and this
1718- /// operation must be used.
1719- pub fn validate_lock_release ( & self , lock : & mut VClock , thread : ThreadId , current_span : Span ) {
1720- let ( index, mut clocks) = self . load_thread_state_mut ( thread) ;
1721- lock. clone_from ( & clocks. clock ) ;
1722- clocks. increment_clock ( index, current_span) ;
1723- }
1724-
1725- /// Release a lock handle, express that this happens-before
1726- /// any subsequent calls to `validate_lock_acquire` as well
1727- /// as any previous calls to this function after any
1728- /// `validate_lock_release` calls.
1729- /// For normal locks this should be equivalent to `validate_lock_release`.
1730- /// This function only exists for joining over the set of concurrent readers
1731- /// in a read-write lock and should not be used for anything else.
1732- pub fn validate_lock_release_shared (
1733- & self ,
1734- lock : & mut VClock ,
1735- thread : ThreadId ,
1736- current_span : Span ,
1737- ) {
1738- let ( index, mut clocks) = self . load_thread_state_mut ( thread) ;
1739- lock. join ( & clocks. clock ) ;
1713+ /// Returns the `release` clock of the given thread.
1714+ /// Other threads can acquire this clock in the future to establish synchronization
1715+ /// with this program point.
1716+ pub fn release_clock ( & self , thread : ThreadId , current_span : Span ) -> Ref < ' _ , VClock > {
1717+ // We increment the clock each time this happens, to ensure no two releases
1718+ // can be confused with each other.
1719+ let ( index, mut clocks) = self . thread_state_mut ( thread) ;
17401720 clocks. increment_clock ( index, current_span) ;
1721+ drop ( clocks) ;
1722+ // To return a read-only view, we need to release the RefCell
1723+ // and borrow it again.
1724+ let ( _index, clocks) = self . thread_state ( thread) ;
1725+ Ref :: map ( clocks, |c| & c. clock )
17411726 }
17421727
17431728 /// Load the vector index used by the given thread as well as the set of vector clocks
17441729 /// used by the thread.
17451730 #[ inline]
1746- fn load_thread_state_mut ( & self , thread : ThreadId ) -> ( VectorIdx , RefMut < ' _ , ThreadClockSet > ) {
1731+ fn thread_state_mut ( & self , thread : ThreadId ) -> ( VectorIdx , RefMut < ' _ , ThreadClockSet > ) {
17471732 let index = self . thread_info . borrow ( ) [ thread]
17481733 . vector_index
17491734 . expect ( "Loading thread state for thread with no assigned vector" ) ;
@@ -1752,17 +1737,26 @@ impl GlobalState {
17521737 ( index, clocks)
17531738 }
17541739
1740+ /// Load the vector index used by the given thread as well as the set of vector clocks
1741+ /// used by the thread.
1742+ #[ inline]
1743+ fn thread_state ( & self , thread : ThreadId ) -> ( VectorIdx , Ref < ' _ , ThreadClockSet > ) {
1744+ let index = self . thread_info . borrow ( ) [ thread]
1745+ . vector_index
1746+ . expect ( "Loading thread state for thread with no assigned vector" ) ;
1747+ let ref_vector = self . vector_clocks . borrow ( ) ;
1748+ let clocks = Ref :: map ( ref_vector, |vec| & vec[ index] ) ;
1749+ ( index, clocks)
1750+ }
1751+
17551752 /// Load the current vector clock in use and the current set of thread clocks
17561753 /// in use for the vector.
17571754 #[ inline]
17581755 pub ( super ) fn current_thread_state (
17591756 & self ,
17601757 thread_mgr : & ThreadManager < ' _ , ' _ > ,
17611758 ) -> ( VectorIdx , Ref < ' _ , ThreadClockSet > ) {
1762- let index = self . current_index ( thread_mgr) ;
1763- let ref_vector = self . vector_clocks . borrow ( ) ;
1764- let clocks = Ref :: map ( ref_vector, |vec| & vec[ index] ) ;
1765- ( index, clocks)
1759+ self . thread_state ( thread_mgr. get_active_thread_id ( ) )
17661760 }
17671761
17681762 /// Load the current vector clock in use and the current set of thread clocks
@@ -1772,10 +1766,7 @@ impl GlobalState {
17721766 & self ,
17731767 thread_mgr : & ThreadManager < ' _ , ' _ > ,
17741768 ) -> ( VectorIdx , RefMut < ' _ , ThreadClockSet > ) {
1775- let index = self . current_index ( thread_mgr) ;
1776- let ref_vector = self . vector_clocks . borrow_mut ( ) ;
1777- let clocks = RefMut :: map ( ref_vector, |vec| & mut vec[ index] ) ;
1778- ( index, clocks)
1769+ self . thread_state_mut ( thread_mgr. get_active_thread_id ( ) )
17791770 }
17801771
17811772 /// Return the current thread, should be the same
0 commit comments