@@ -262,6 +262,104 @@ enum AccessType {
262
262
AtomicRmw ,
263
263
}
264
264
265
+ /// Per-byte vector clock metadata for data-race detection.
266
+ #[ derive( Clone , PartialEq , Eq , Debug ) ]
267
+ struct MemoryCellClocks {
268
+ /// The vector-clock timestamp and the thread that did the last non-atomic write. We don't need
269
+ /// a full `VClock` here, it's always a single thread and nothing synchronizes, so the effective
270
+ /// clock is all-0 except for the thread that did the write.
271
+ write : ( VectorIdx , VTimestamp ) ,
272
+
273
+ /// The type of operation that the write index represents,
274
+ /// either newly allocated memory, a non-atomic write or
275
+ /// a deallocation of memory.
276
+ write_type : NaWriteType ,
277
+
278
+ /// The vector-clock of all non-atomic reads that happened since the last non-atomic write
279
+ /// (i.e., we join together the "singleton" clocks corresponding to each read). It is reset to
280
+ /// zero on each write operation.
281
+ read : VClock ,
282
+
283
+ /// Atomic access, acquire, release sequence tracking clocks.
284
+ /// For non-atomic memory this value is set to None.
285
+ /// For atomic memory, each byte carries this information.
286
+ atomic_ops : Option < Box < AtomicMemoryCellClocks > > ,
287
+ }
288
+
289
+ /// Extra metadata associated with a thread.
290
+ #[ derive( Debug , Clone , Default ) ]
291
+ struct ThreadExtraState {
292
+ /// The current vector index in use by the
293
+ /// thread currently, this is set to None
294
+ /// after the vector index has been re-used
295
+ /// and hence the value will never need to be
296
+ /// read during data-race reporting.
297
+ vector_index : Option < VectorIdx > ,
298
+
299
+ /// Thread termination vector clock, this
300
+ /// is set on thread termination and is used
301
+ /// for joining on threads since the vector_index
302
+ /// may be re-used when the join operation occurs.
303
+ termination_vector_clock : Option < VClock > ,
304
+ }
305
+
306
+ /// Global data-race detection state, contains the currently
307
+ /// executing thread as well as the vector-clocks associated
308
+ /// with each of the threads.
309
+ // FIXME: it is probably better to have one large RefCell, than to have so many small ones.
310
+ #[ derive( Debug , Clone ) ]
311
+ pub struct GlobalState {
312
+ /// Set to true once the first additional
313
+ /// thread has launched, due to the dependency
314
+ /// between before and after a thread launch.
315
+ /// Any data-races must be recorded after this
316
+ /// so concurrent execution can ignore recording
317
+ /// any data-races.
318
+ multi_threaded : Cell < bool > ,
319
+
320
+ /// A flag to mark we are currently performing
321
+ /// a data race free action (such as atomic access)
322
+ /// to suppress the race detector
323
+ ongoing_action_data_race_free : Cell < bool > ,
324
+
325
+ /// Mapping of a vector index to a known set of thread
326
+ /// clocks, this is not directly mapping from a thread id
327
+ /// since it may refer to multiple threads.
328
+ vector_clocks : RefCell < IndexVec < VectorIdx , ThreadClockSet > > ,
329
+
330
+ /// Mapping of a given vector index to the current thread
331
+ /// that the execution is representing, this may change
332
+ /// if a vector index is re-assigned to a new thread.
333
+ vector_info : RefCell < IndexVec < VectorIdx , ThreadId > > ,
334
+
335
+ /// The mapping of a given thread to associated thread metadata.
336
+ thread_info : RefCell < IndexVec < ThreadId , ThreadExtraState > > ,
337
+
338
+ /// Potential vector indices that could be re-used on thread creation
339
+ /// values are inserted here on after the thread has terminated and
340
+ /// been joined with, and hence may potentially become free
341
+ /// for use as the index for a new thread.
342
+ /// Elements in this set may still require the vector index to
343
+ /// report data-races, and can only be re-used after all
344
+ /// active vector-clocks catch up with the threads timestamp.
345
+ reuse_candidates : RefCell < FxHashSet < VectorIdx > > ,
346
+
347
+ /// The timestamp of last SC fence performed by each thread
348
+ last_sc_fence : RefCell < VClock > ,
349
+
350
+ /// The timestamp of last SC write performed by each thread
351
+ last_sc_write : RefCell < VClock > ,
352
+
353
+ /// Track when an outdated (weak memory) load happens.
354
+ pub track_outdated_loads : bool ,
355
+ }
356
+
357
+ impl VisitProvenance for GlobalState {
358
+ fn visit_provenance ( & self , _visit : & mut VisitWith < ' _ > ) {
359
+ // We don't have any tags.
360
+ }
361
+ }
362
+
265
363
impl AccessType {
266
364
fn description ( self , ty : Option < Ty < ' _ > > , size : Option < Size > ) -> String {
267
365
let mut msg = String :: new ( ) ;
@@ -315,30 +413,6 @@ impl AccessType {
315
413
}
316
414
}
317
415
318
- /// Per-byte vector clock metadata for data-race detection.
319
- #[ derive( Clone , PartialEq , Eq , Debug ) ]
320
- struct MemoryCellClocks {
321
- /// The vector-clock timestamp and the thread that did the last non-atomic write. We don't need
322
- /// a full `VClock` here, it's always a single thread and nothing synchronizes, so the effective
323
- /// clock is all-0 except for the thread that did the write.
324
- write : ( VectorIdx , VTimestamp ) ,
325
-
326
- /// The type of operation that the write index represents,
327
- /// either newly allocated memory, a non-atomic write or
328
- /// a deallocation of memory.
329
- write_type : NaWriteType ,
330
-
331
- /// The vector-clock of all non-atomic reads that happened since the last non-atomic write
332
- /// (i.e., we join together the "singleton" clocks corresponding to each read). It is reset to
333
- /// zero on each write operation.
334
- read : VClock ,
335
-
336
- /// Atomic access, acquire, release sequence tracking clocks.
337
- /// For non-atomic memory this value is set to None.
338
- /// For atomic memory, each byte carries this information.
339
- atomic_ops : Option < Box < AtomicMemoryCellClocks > > ,
340
- }
341
-
342
416
impl AtomicMemoryCellClocks {
343
417
fn new ( size : Size ) -> Self {
344
418
AtomicMemoryCellClocks {
@@ -1469,80 +1543,6 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
1469
1543
}
1470
1544
}
1471
1545
1472
- /// Extra metadata associated with a thread.
1473
- #[ derive( Debug , Clone , Default ) ]
1474
- struct ThreadExtraState {
1475
- /// The current vector index in use by the
1476
- /// thread currently, this is set to None
1477
- /// after the vector index has been re-used
1478
- /// and hence the value will never need to be
1479
- /// read during data-race reporting.
1480
- vector_index : Option < VectorIdx > ,
1481
-
1482
- /// Thread termination vector clock, this
1483
- /// is set on thread termination and is used
1484
- /// for joining on threads since the vector_index
1485
- /// may be re-used when the join operation occurs.
1486
- termination_vector_clock : Option < VClock > ,
1487
- }
1488
-
1489
- /// Global data-race detection state, contains the currently
1490
- /// executing thread as well as the vector-clocks associated
1491
- /// with each of the threads.
1492
- // FIXME: it is probably better to have one large RefCell, than to have so many small ones.
1493
- #[ derive( Debug , Clone ) ]
1494
- pub struct GlobalState {
1495
- /// Set to true once the first additional
1496
- /// thread has launched, due to the dependency
1497
- /// between before and after a thread launch.
1498
- /// Any data-races must be recorded after this
1499
- /// so concurrent execution can ignore recording
1500
- /// any data-races.
1501
- multi_threaded : Cell < bool > ,
1502
-
1503
- /// A flag to mark we are currently performing
1504
- /// a data race free action (such as atomic access)
1505
- /// to suppress the race detector
1506
- ongoing_action_data_race_free : Cell < bool > ,
1507
-
1508
- /// Mapping of a vector index to a known set of thread
1509
- /// clocks, this is not directly mapping from a thread id
1510
- /// since it may refer to multiple threads.
1511
- vector_clocks : RefCell < IndexVec < VectorIdx , ThreadClockSet > > ,
1512
-
1513
- /// Mapping of a given vector index to the current thread
1514
- /// that the execution is representing, this may change
1515
- /// if a vector index is re-assigned to a new thread.
1516
- vector_info : RefCell < IndexVec < VectorIdx , ThreadId > > ,
1517
-
1518
- /// The mapping of a given thread to associated thread metadata.
1519
- thread_info : RefCell < IndexVec < ThreadId , ThreadExtraState > > ,
1520
-
1521
- /// Potential vector indices that could be re-used on thread creation
1522
- /// values are inserted here on after the thread has terminated and
1523
- /// been joined with, and hence may potentially become free
1524
- /// for use as the index for a new thread.
1525
- /// Elements in this set may still require the vector index to
1526
- /// report data-races, and can only be re-used after all
1527
- /// active vector-clocks catch up with the threads timestamp.
1528
- reuse_candidates : RefCell < FxHashSet < VectorIdx > > ,
1529
-
1530
- /// The timestamp of last SC fence performed by each thread
1531
- last_sc_fence : RefCell < VClock > ,
1532
-
1533
- /// The timestamp of last SC write performed by each thread
1534
- last_sc_write : RefCell < VClock > ,
1535
-
1536
- /// Track when an outdated (weak memory) load happens.
1537
- pub track_outdated_loads : bool ,
1538
- }
1539
-
1540
- impl VisitProvenance for GlobalState {
1541
- fn visit_provenance ( & self , _visit : & mut VisitWith < ' _ > ) {
1542
- // We don't have any tags.
1543
- }
1544
- }
1545
-
1546
1546
impl GlobalState {
1547
1547
/// Create a new global state, setup with just thread-id=0
1548
1548
/// advanced to timestamp = 1.
0 commit comments