@@ -69,12 +69,8 @@ struct Mutex {
6969 lock_count : usize ,
7070 /// The queue of threads waiting for this mutex.
7171 queue : VecDeque < ThreadId > ,
72- /// Data race handle. This tracks the happens-before
73- /// relationship between each mutex access. It is
74- /// released to during unlock and acquired from during
75- /// locking, and therefore stores the clock of the last
76- /// thread to release this mutex.
77- data_race : VClock ,
72+ /// Mutex clock. This tracks the moment of the last unlock.
73+ clock : VClock ,
7874}
7975
8076declare_id ! ( RwLockId ) ;
@@ -91,16 +87,16 @@ struct RwLock {
9187 writer_queue : VecDeque < ThreadId > ,
9288 /// The queue of reader threads waiting for this lock.
9389 reader_queue : VecDeque < ThreadId > ,
94- /// Data race handle for writers. Tracks the happens-before
90+ /// Data race clock for writers. Tracks the happens-before
9591 /// ordering between each write access to a rwlock and is updated
9692 /// after a sequence of concurrent readers to track the happens-
9793 /// before ordering between the set of previous readers and
9894 /// the current writer.
9995 /// Contains the clock of the last thread to release a writer
10096 /// lock or the joined clock of the set of last threads to release
10197 /// shared reader locks.
102- data_race : VClock ,
103- /// Data race handle for readers. This is temporary storage
98+ clock_unlocked : VClock ,
99+ /// Data race clock for readers. This is temporary storage
104100 /// for the combined happens-before ordering for between all
105101 /// concurrent readers and the next writer, and the value
106102 /// is stored to the main data_race variable once all
@@ -110,7 +106,7 @@ struct RwLock {
110106 /// add happens-before orderings between shared reader
111107 /// locks.
112108 /// This is only relevant when there is an active reader.
113- data_race_reader : VClock ,
109+ clock_current_readers : VClock ,
114110}
115111
116112declare_id ! ( CondvarId ) ;
@@ -132,8 +128,8 @@ struct Condvar {
132128 /// between a cond-var signal and a cond-var
133129 /// wait during a non-spurious signal event.
134130 /// Contains the clock of the last thread to
135- /// perform a futex -signal.
136- data_race : VClock ,
131+ /// perform a condvar -signal.
132+ clock : VClock ,
137133}
138134
139135/// The futex state.
@@ -145,7 +141,7 @@ struct Futex {
145141 /// during a non-spurious wake event.
146142 /// Contains the clock of the last thread to
147143 /// perform a futex-wake.
148- data_race : VClock ,
144+ clock : VClock ,
149145}
150146
151147/// A thread waiting on a futex.
@@ -346,7 +342,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
346342 }
347343 mutex. lock_count = mutex. lock_count . checked_add ( 1 ) . unwrap ( ) ;
348344 if let Some ( data_race) = & this. machine . data_race {
349- data_race. validate_lock_acquire ( & mutex. data_race , thread) ;
345+ data_race. acquire_clock ( & mutex. clock , thread) ;
350346 }
351347 }
352348
@@ -373,11 +369,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
373369 // The mutex is completely unlocked. Try transferring ownership
374370 // to another thread.
375371 if let Some ( data_race) = & this. machine . data_race {
376- data_race. validate_lock_release (
377- & mut mutex. data_race ,
378- current_owner,
379- current_span,
380- ) ;
372+ mutex. clock . clone_from ( & data_race. release_clock ( current_owner, current_span) ) ;
381373 }
382374 this. mutex_dequeue_and_lock ( id) ;
383375 }
@@ -448,7 +440,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
448440 let count = rwlock. readers . entry ( reader) . or_insert ( 0 ) ;
449441 * count = count. checked_add ( 1 ) . expect ( "the reader counter overflowed" ) ;
450442 if let Some ( data_race) = & this. machine . data_race {
451- data_race. validate_lock_acquire ( & rwlock. data_race , reader) ;
443+ data_race. acquire_clock ( & rwlock. clock_unlocked , reader) ;
452444 }
453445 }
454446
@@ -474,20 +466,16 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
474466 }
475467 if let Some ( data_race) = & this. machine . data_race {
476468 // Add this to the shared-release clock of all concurrent readers.
477- data_race. validate_lock_release_shared (
478- & mut rwlock. data_race_reader ,
479- reader,
480- current_span,
481- ) ;
469+ rwlock. clock_current_readers . join ( & data_race. release_clock ( reader, current_span) ) ;
482470 }
483471
484472 // The thread was a reader. If the lock is not held any more, give it to a writer.
485473 if this. rwlock_is_locked ( id) . not ( ) {
486474 // All the readers are finished, so set the writer data-race handle to the value
487- // of the union of all reader data race handles, since the set of readers
488- // happen-before the writers
475+ // of the union of all reader data race handles, since the set of readers
476+ // happen-before the writers
489477 let rwlock = & mut this. machine . threads . sync . rwlocks [ id] ;
490- rwlock. data_race . clone_from ( & rwlock. data_race_reader ) ;
478+ rwlock. clock_unlocked . clone_from ( & rwlock. clock_current_readers ) ;
491479 this. rwlock_dequeue_and_lock_writer ( id) ;
492480 }
493481 true
@@ -511,7 +499,7 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
511499 let rwlock = & mut this. machine . threads . sync . rwlocks [ id] ;
512500 rwlock. writer = Some ( writer) ;
513501 if let Some ( data_race) = & this. machine . data_race {
514- data_race. validate_lock_acquire ( & rwlock. data_race , writer) ;
502+ data_race. acquire_clock ( & rwlock. clock_unlocked , writer) ;
515503 }
516504 }
517505
@@ -530,11 +518,9 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
530518 trace ! ( "rwlock_writer_unlock: {:?} unlocked by {:?}" , id, expected_writer) ;
531519 // Release memory to next lock holder.
532520 if let Some ( data_race) = & this. machine . data_race {
533- data_race. validate_lock_release (
534- & mut rwlock. data_race ,
535- current_writer,
536- current_span,
537- ) ;
521+ rwlock
522+ . clock_unlocked
523+ . clone_from ( & * data_race. release_clock ( current_writer, current_span) ) ;
538524 }
539525 // The thread was a writer.
540526 //
@@ -611,11 +597,11 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
611597
612598 // Each condvar signal happens-before the end of the condvar wake
613599 if let Some ( data_race) = data_race {
614- data_race . validate_lock_release ( & mut condvar . data_race , current_thread, current_span) ;
600+ condvar . clock . clone_from ( & * data_race. release_clock ( current_thread, current_span) ) ;
615601 }
616602 condvar. waiters . pop_front ( ) . map ( |waiter| {
617603 if let Some ( data_race) = data_race {
618- data_race. validate_lock_acquire ( & condvar. data_race , waiter. thread ) ;
604+ data_race. acquire_clock ( & condvar. clock , waiter. thread ) ;
619605 }
620606 ( waiter. thread , waiter. lock )
621607 } )
@@ -645,14 +631,14 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriInterpCxExt<'mir, 'tcx> {
645631
646632 // Each futex-wake happens-before the end of the futex wait
647633 if let Some ( data_race) = data_race {
648- data_race . validate_lock_release ( & mut futex . data_race , current_thread, current_span) ;
634+ futex . clock . clone_from ( & * data_race. release_clock ( current_thread, current_span) ) ;
649635 }
650636
651637 // Wake up the first thread in the queue that matches any of the bits in the bitset.
652638 futex. waiters . iter ( ) . position ( |w| w. bitset & bitset != 0 ) . map ( |i| {
653639 let waiter = futex. waiters . remove ( i) . unwrap ( ) ;
654640 if let Some ( data_race) = data_race {
655- data_race. validate_lock_acquire ( & futex. data_race , waiter. thread ) ;
641+ data_race. acquire_clock ( & futex. clock , waiter. thread ) ;
656642 }
657643 waiter. thread
658644 } )
0 commit comments