@@ -159,61 +159,25 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
159
159
& self , place : MPlaceTy < ' tcx , Tag > , atomic : AtomicReadOp
160
160
) -> InterpResult < ' tcx > {
161
161
let this = self . eval_context_ref ( ) ;
162
- let data_race = & * this. memory . extra . data_race ;
163
- if data_race. multi_threaded . get ( ) {
164
-
165
- // Load an log the atomic operation
166
- // the memory access has to be `get_raw` since otherwise this despite only
167
- // mutating MemoryExtra will still trigger errors on read-only memory
168
- let place_ptr = place. ptr . assert_ptr ( ) ;
169
- let size = place. layout . size ;
170
- let alloc_meta = & this. memory . get_raw ( place_ptr. alloc_id ) ?. extra . data_race ;
171
- log:: trace!(
172
- "Atomic op({}) with ordering {:?} on memory({:?}, offset={}, size={})" ,
173
- "Atomic load" , & atomic, place_ptr. alloc_id, place_ptr. offset. bytes( ) , size. bytes( )
174
- ) ;
175
-
176
- // Perform the atomic operation
177
- let data_race = & alloc_meta. global ;
178
- data_race. maybe_perform_sync_operation ( move |index, mut clocks| {
179
- for ( _, range) in alloc_meta. alloc_ranges . borrow_mut ( ) . iter_mut ( place_ptr. offset , size) {
180
- let res = if atomic == AtomicReadOp :: Relaxed {
181
- range. load_relaxed ( & mut * clocks, index)
182
- } else {
183
- range. acquire ( & mut * clocks, index)
184
- } ;
185
- if let Err ( DataRace ) = res {
186
- mem:: drop ( clocks) ;
187
- return VClockAlloc :: report_data_race (
188
- & alloc_meta. global , range, "Atomic load" , true ,
189
- place_ptr, size
190
- ) ;
191
- }
192
- }
193
- Ok ( ( ) )
194
- } ) ?;
195
-
196
- // Log changes to atomic memory
197
- if log:: log_enabled!( log:: Level :: Trace ) {
198
- for ( _, range) in alloc_meta. alloc_ranges . borrow ( ) . iter ( place_ptr. offset , size) {
199
- log:: trace!(
200
- "Updated atomic memory({:?}, offset={}, size={}) to {:#?}" ,
201
- place. ptr. assert_ptr( ) . alloc_id, place_ptr. offset. bytes( ) , size. bytes( ) ,
202
- range. atomic_ops
203
- ) ;
162
+ this. validate_atomic_op (
163
+ place, atomic, "Atomic Load" ,
164
+ move |memory, clocks, index, atomic| {
165
+ if atomic == AtomicReadOp :: Relaxed {
166
+ memory. load_relaxed ( & mut * clocks, index)
167
+ } else {
168
+ memory. acquire ( & mut * clocks, index)
204
169
}
205
170
}
206
- }
207
- Ok ( ( ) )
171
+ )
208
172
}
209
173
210
174
/// Update the data-race detector for an atomic write occuring at the
211
175
/// associated memory-place and on the current thread
212
176
fn validate_atomic_store (
213
177
& mut self , place : MPlaceTy < ' tcx , Tag > , atomic : AtomicWriteOp
214
178
) -> InterpResult < ' tcx > {
215
- let this = self . eval_context_mut ( ) ;
216
- this. validate_atomic_op_mut (
179
+ let this = self . eval_context_ref ( ) ;
180
+ this. validate_atomic_op (
217
181
place, atomic, "Atomic Store" ,
218
182
move |memory, clocks, index, atomic| {
219
183
if atomic == AtomicWriteOp :: Relaxed {
@@ -233,8 +197,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
233
197
use AtomicRWOp :: * ;
234
198
let acquire = matches ! ( atomic, Acquire | AcqRel | SeqCst ) ;
235
199
let release = matches ! ( atomic, Release | AcqRel | SeqCst ) ;
236
- let this = self . eval_context_mut ( ) ;
237
- this. validate_atomic_op_mut (
200
+ let this = self . eval_context_ref ( ) ;
201
+ this. validate_atomic_op (
238
202
place, atomic, "Atomic RMW" ,
239
203
move |memory, clocks, index, _| {
240
204
if acquire {
@@ -276,25 +240,27 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
276
240
impl < ' mir , ' tcx : ' mir > EvalContextPrivExt < ' mir , ' tcx > for MiriEvalContext < ' mir , ' tcx > { }
277
241
trait EvalContextPrivExt < ' mir , ' tcx : ' mir > : MiriEvalContextExt < ' mir , ' tcx > {
278
242
279
- /// Generic atomic operation implementation, this however
280
- /// cannot be used for the atomic read operation since
281
- /// that requires non mutable memory access to not trigger
282
- /// the writing to read-only memory errors during `get_raw_mut`
283
- fn validate_atomic_op_mut < A : Debug + Copy > (
284
- & mut self , place : MPlaceTy < ' tcx , Tag > ,
243
+ /// Generic atomic operation implementation,
244
+ /// this accesses memory via get_raw instead of
245
+ /// get_raw_mut, due to issues calling get_raw_mut
246
+ /// for atomic loads from read-only memory
247
+ /// FIXME: is this valid, or should get_raw_mut be used for
248
+ /// atomic-stores/atomic-rmw?
249
+ fn validate_atomic_op < A : Debug + Copy > (
250
+ & self , place : MPlaceTy < ' tcx , Tag > ,
285
251
atomic : A , description : & str ,
286
252
mut op : impl FnMut (
287
253
& mut MemoryCellClocks , & mut ThreadClockSet , VectorIdx , A
288
254
) -> Result < ( ) , DataRace >
289
255
) -> InterpResult < ' tcx > {
290
- let this = self . eval_context_mut ( ) ;
256
+ let this = self . eval_context_ref ( ) ;
291
257
let data_race = & * this. memory . extra . data_race ;
292
258
if data_race. multi_threaded . get ( ) {
293
259
294
260
// Load an log the atomic operation
295
261
let place_ptr = place. ptr . assert_ptr ( ) ;
296
262
let size = place. layout . size ;
297
- let alloc_meta = & mut this. memory . get_raw_mut ( place_ptr. alloc_id ) ?. extra . data_race ;
263
+ let alloc_meta = & this. memory . get_raw ( place_ptr. alloc_id ) ?. extra . data_race ;
298
264
log:: trace!(
299
265
"Atomic op({}) with ordering {:?} on memory({:?}, offset={}, size={})" ,
300
266
description, & atomic, place_ptr. alloc_id, place_ptr. offset. bytes( ) , size. bytes( )
@@ -800,6 +766,29 @@ impl ThreadClockSet {
800
766
}
801
767
}
802
768
769
+ /// Extra metadata associated with a thread
770
+ #[ derive( Debug , Clone , Default ) ]
771
+ struct ThreadExtraState {
772
+
773
+ /// The current vector index in use by the
774
+ /// thread currently, this is set to None
775
+ /// after the vector index has been re-used
776
+ vector_index : Option < VectorIdx > ,
777
+
778
+ /// The name of the thread, updated for better
779
+ /// diagnostics when reporting detected data
780
+ /// races
781
+ thread_name : Option < Box < str > > ,
782
+
783
+ /// Thread termination vector clock, this
784
+ /// is set on thread termination and is used
785
+ /// for joining on threads that have already
786
+ /// terminated. This should be used first
787
+ /// on joining as there is the possibility
788
+ /// that `vector_index` is None in some cases
789
+ termination_vector_clock : Option < VClock > ,
790
+ }
791
+
803
792
/// Global data-race detection state, contains the currently
804
793
/// executing thread as well as the vector-clocks associated
805
794
/// with each of the threads.
@@ -822,18 +811,18 @@ pub struct GlobalState {
822
811
/// Mapping of a given vector index to the current thread
823
812
/// that the execution is representing, this may change
824
813
/// if a vector index is re-assigned to a new thread
825
- vector_info : RefCell < IndexVec < VectorIdx , ThreadId > > , //FIXME: make option
814
+ vector_info : RefCell < IndexVec < VectorIdx , ThreadId > > ,
826
815
827
- /// The mapping of a given thread to a known vector clock
828
- thread_info : RefCell < IndexVec < ThreadId , ( Option < VectorIdx > , Option < Box < str > > ) > > ,
816
+ /// The mapping of a given thread to assocaited thread metadata
817
+ thread_info : RefCell < IndexVec < ThreadId , ThreadExtraState > > ,
829
818
830
819
/// The current vector index being executed
831
820
current_index : Cell < VectorIdx > ,
832
821
833
822
/// Potential vector indices that could be re-used on thread creation
834
- /// values are inserted here on thread join events, and can be
835
- /// re-used once the vector clocks of all current threads
836
- /// are equal to the vector clock of the joined thread
823
+ /// values are inserted here on thread termination, vector index values
824
+ /// are then re-used once all the termination event happens-before all
825
+ /// existing thread-clocks
837
826
reuse_candidates : RefCell < FxHashSet < VectorIdx > > ,
838
827
}
839
828
impl GlobalState {
@@ -856,8 +845,12 @@ impl GlobalState {
856
845
let index = global_state. vector_clocks . borrow_mut ( ) . push ( ThreadClockSet :: default ( ) ) ;
857
846
global_state. vector_info . borrow_mut ( ) . push ( ThreadId :: new ( 0 ) ) ;
858
847
global_state. thread_info . borrow_mut ( ) . push (
859
- ( Some ( index) , Some ( "main" . to_string ( ) . into_boxed_str ( ) )
860
- ) ) ;
848
+ ThreadExtraState {
849
+ vector_index : Some ( index) ,
850
+ thread_name : Some ( "main" . to_string ( ) . into_boxed_str ( ) ) ,
851
+ termination_vector_clock : None
852
+ }
853
+ ) ;
861
854
862
855
global_state
863
856
}
@@ -873,10 +866,9 @@ impl GlobalState {
873
866
clock. clock [ candidate] == target_timestamp
874
867
} ) {
875
868
// All vector clocks for each vector index are equal to
876
- // the target timestamp, therefore since the thread has
877
- // terminated and cannot update the vector clock.
878
- // No more data-races involving this vector index are possible
879
- // so it can be re-used
869
+ // the target timestamp, and the thread is known to have
870
+ // terminated, therefore this vector clock index cannot
871
+ // report any more data-races
880
872
assert ! ( reuse. remove( & candidate) ) ;
881
873
return Some ( candidate)
882
874
}
@@ -916,7 +908,7 @@ impl GlobalState {
916
908
917
909
// Mark the thread the vector index was associated with as no longer
918
910
// representing a thread index
919
- thread_info[ old_thread] . 0 = None ;
911
+ thread_info[ old_thread] . vector_index = None ;
920
912
921
913
reuse_index
922
914
} else {
@@ -927,7 +919,7 @@ impl GlobalState {
927
919
} ;
928
920
929
921
// Mark the chosen vector index as in use by the thread
930
- thread_info[ thread] . 0 = Some ( created_index) ;
922
+ thread_info[ thread] . vector_index = Some ( created_index) ;
931
923
932
924
// Create a thread clock set if applicable
933
925
let mut vector_clocks = self . vector_clocks . borrow_mut ( ) ;
@@ -952,15 +944,13 @@ impl GlobalState {
952
944
953
945
/// Hook on a thread join to update the implicit happens-before relation
954
946
/// between the joined thead and the current thread.
955
- /// Called after the join has occured, and hence implicitly also states
956
- /// that the thread must have terminated as well
957
947
#[ inline]
958
948
pub fn thread_joined ( & self , current_thread : ThreadId , join_thread : ThreadId ) {
959
949
let ( current_index, join_index) = {
960
950
let thread_info = self . thread_info . borrow ( ) ;
961
- let current_index = thread_info[ current_thread] . 0
951
+ let current_index = thread_info[ current_thread] . vector_index
962
952
. expect ( "Joining into thread with no assigned vector" ) ;
963
- let join_index = thread_info[ join_thread] . 0
953
+ let join_index = thread_info[ join_thread] . vector_index
964
954
. expect ( "Joining thread with no assigned vector" ) ;
965
955
( current_index, join_index)
966
956
} ;
@@ -976,16 +966,31 @@ impl GlobalState {
976
966
current. join_with ( join) ;
977
967
978
968
// Post increment clocks after atomic operation
969
+ // the join clock is not incremented, since there will
970
+ // be no future events, also if it was incremented
971
+ // the thread re-use condition would never pass
979
972
current. increment_clock ( current_index) ;
980
- join. increment_clock ( join_index) ;
973
+ }
974
+
975
+ /// On thread termination, the vector-clock may re-used
976
+ /// in the future once all remaining thread-clocks catch
977
+ /// up with the time index of the terminated thread
978
+ #[ inline]
979
+ pub fn thread_terminated ( & self , terminated_thread : ThreadId ) {
980
+ let mut thread_info = self . thread_info . borrow_mut ( ) ;
981
+ let termination_meta = & mut thread_info[ terminated_thread] ;
982
+
983
+ // Find the terminated index & setup the termination vector-clock
984
+ // in case thread join is called in the future after the thread
985
+ // has been re-used
986
+ let terminated_index = termination_meta. vector_index
987
+ . expect ( "Joining into thread with no assigned vector" ) ;
988
+ let vector_clocks = self . vector_clocks . borrow ( ) ;
989
+ termination_meta. termination_vector_clock = Some ( vector_clocks[ terminated_index] . clock . clone ( ) ) ;
981
990
982
- // The joined thread vector clock is a potential candidate
983
- // for re-use given sufficient time, mark as available once
984
- // threads have been created. This is because this function
985
- // is called once join_thread has terminated and such cannot
986
- // update any-more
991
+ // Add this thread as a candidate for re-use
987
992
let mut reuse = self . reuse_candidates . borrow_mut ( ) ;
988
- reuse. insert ( join_index ) ;
993
+ reuse. insert ( terminated_index ) ;
989
994
}
990
995
991
996
/// Hook for updating the local tracker of the currently
@@ -994,7 +999,7 @@ impl GlobalState {
994
999
#[ inline]
995
1000
pub fn thread_set_active ( & self , thread : ThreadId ) {
996
1001
let thread_info = self . thread_info . borrow ( ) ;
997
- let vector_idx = thread_info[ thread] . 0
1002
+ let vector_idx = thread_info[ thread] . vector_index
998
1003
. expect ( "Setting thread active with no assigned vector" ) ;
999
1004
self . current_index . set ( vector_idx) ;
1000
1005
}
@@ -1007,7 +1012,7 @@ impl GlobalState {
1007
1012
pub fn thread_set_name ( & self , thread : ThreadId , name : String ) {
1008
1013
let name = name. into_boxed_str ( ) ;
1009
1014
let mut thread_info = self . thread_info . borrow_mut ( ) ;
1010
- thread_info[ thread] . 1 = Some ( name) ;
1015
+ thread_info[ thread] . thread_name = Some ( name) ;
1011
1016
}
1012
1017
1013
1018
@@ -1036,7 +1041,7 @@ impl GlobalState {
1036
1041
/// returns the id and the name for better diagnostics
1037
1042
fn print_thread_metadata ( & self , vector : VectorIdx ) -> String {
1038
1043
let thread = self . vector_info . borrow ( ) [ vector] ;
1039
- let thread_name = & self . thread_info . borrow ( ) [ thread] . 1 ;
1044
+ let thread_name = & self . thread_info . borrow ( ) [ thread] . thread_name ;
1040
1045
if let Some ( name) = thread_name {
1041
1046
let name: & str = name;
1042
1047
format ! ( "Thread(id = {:?}, name = {:?})" , thread. to_u32( ) , & * name)
@@ -1079,7 +1084,7 @@ impl GlobalState {
1079
1084
/// used by the thread
1080
1085
#[ inline]
1081
1086
fn load_thread_state_mut ( & self , thread : ThreadId ) -> ( VectorIdx , RefMut < ' _ , ThreadClockSet > ) {
1082
- let index = self . thread_info . borrow ( ) [ thread] . 0
1087
+ let index = self . thread_info . borrow ( ) [ thread] . vector_index
1083
1088
. expect ( "Loading thread state for thread with no assigned vector" ) ;
1084
1089
let ref_vector = self . vector_clocks . borrow_mut ( ) ;
1085
1090
let clocks = RefMut :: map ( ref_vector, |vec| & mut vec[ index] ) ;
0 commit comments