@@ -847,6 +847,7 @@ impl VClockAlloc {
847
847
kind : MemoryKind ,
848
848
current_span : Span ,
849
849
) -> VClockAlloc {
850
+ // Determine the thread that did the allocation, and when it did it.
850
851
let ( alloc_timestamp, alloc_index) = match kind {
851
852
// User allocated and stack memory should track allocation.
852
853
MemoryKind :: Machine (
@@ -858,21 +859,22 @@ impl VClockAlloc {
858
859
| MiriMemoryKind :: Mmap ,
859
860
)
860
861
| MemoryKind :: Stack => {
861
- let ( alloc_index, clocks) = global. current_thread_state ( thread_mgr) ;
862
+ let ( alloc_index, clocks) = global. active_thread_state ( thread_mgr) ;
862
863
let mut alloc_timestamp = clocks. clock [ alloc_index] ;
863
864
alloc_timestamp. span = current_span;
864
865
( alloc_timestamp, alloc_index)
865
866
}
866
867
// Other global memory should trace races but be allocated at the 0 timestamp
867
- // (conceptually they are allocated before everything).
868
+ // (conceptually they are allocated on the main thread before everything).
868
869
MemoryKind :: Machine (
869
870
MiriMemoryKind :: Global
870
871
| MiriMemoryKind :: Machine
871
872
| MiriMemoryKind :: Runtime
872
873
| MiriMemoryKind :: ExternStatic
873
874
| MiriMemoryKind :: Tls ,
874
875
)
875
- | MemoryKind :: CallerLocation => ( VTimestamp :: ZERO , VectorIdx :: MAX_INDEX ) ,
876
+ | MemoryKind :: CallerLocation =>
877
+ ( VTimestamp :: ZERO , global. thread_index ( ThreadId :: MAIN_THREAD ) ) ,
876
878
} ;
877
879
VClockAlloc {
878
880
alloc_ranges : RefCell :: new ( RangeMap :: new (
@@ -930,7 +932,7 @@ impl VClockAlloc {
930
932
ptr_dbg : Pointer < AllocId > ,
931
933
ty : Option < Ty < ' _ > > ,
932
934
) -> InterpResult < ' tcx > {
933
- let ( current_index , current_clocks ) = global. current_thread_state ( thread_mgr) ;
935
+ let ( active_index , active_clocks ) = global. active_thread_state ( thread_mgr) ;
934
936
let mut other_size = None ; // if `Some`, this was a size-mismatch race
935
937
let write_clock;
936
938
let ( other_access, other_thread, other_clock) =
@@ -939,30 +941,30 @@ impl VClockAlloc {
939
941
// we are reporting races between two non-atomic reads.
940
942
if !access. is_atomic ( ) &&
941
943
let Some ( atomic) = mem_clocks. atomic ( ) &&
942
- let Some ( idx) = Self :: find_gt_index ( & atomic. write_vector , & current_clocks . clock )
944
+ let Some ( idx) = Self :: find_gt_index ( & atomic. write_vector , & active_clocks . clock )
943
945
{
944
946
( AccessType :: AtomicStore , idx, & atomic. write_vector )
945
947
} else if !access. is_atomic ( ) &&
946
948
let Some ( atomic) = mem_clocks. atomic ( ) &&
947
- let Some ( idx) = Self :: find_gt_index ( & atomic. read_vector , & current_clocks . clock )
949
+ let Some ( idx) = Self :: find_gt_index ( & atomic. read_vector , & active_clocks . clock )
948
950
{
949
951
( AccessType :: AtomicLoad , idx, & atomic. read_vector )
950
952
// Then check races with non-atomic writes/reads.
951
- } else if mem_clocks. write . 1 > current_clocks . clock [ mem_clocks. write . 0 ] {
953
+ } else if mem_clocks. write . 1 > active_clocks . clock [ mem_clocks. write . 0 ] {
952
954
write_clock = mem_clocks. write ( ) ;
953
955
( AccessType :: NaWrite ( mem_clocks. write_type ) , mem_clocks. write . 0 , & write_clock)
954
- } else if let Some ( idx) = Self :: find_gt_index ( & mem_clocks. read , & current_clocks . clock ) {
956
+ } else if let Some ( idx) = Self :: find_gt_index ( & mem_clocks. read , & active_clocks . clock ) {
955
957
( AccessType :: NaRead ( mem_clocks. read [ idx] . read_type ( ) ) , idx, & mem_clocks. read )
956
958
// Finally, mixed-size races.
957
959
} else if access. is_atomic ( ) && let Some ( atomic) = mem_clocks. atomic ( ) && atomic. size != access_size {
958
960
// This is only a race if we are not synchronized with all atomic accesses, so find
959
961
// the one we are not synchronized with.
960
962
other_size = Some ( atomic. size ) ;
961
- if let Some ( idx) = Self :: find_gt_index ( & atomic. write_vector , & current_clocks . clock )
963
+ if let Some ( idx) = Self :: find_gt_index ( & atomic. write_vector , & active_clocks . clock )
962
964
{
963
965
( AccessType :: AtomicStore , idx, & atomic. write_vector )
964
966
} else if let Some ( idx) =
965
- Self :: find_gt_index ( & atomic. read_vector , & current_clocks . clock )
967
+ Self :: find_gt_index ( & atomic. read_vector , & active_clocks . clock )
966
968
{
967
969
( AccessType :: AtomicLoad , idx, & atomic. read_vector )
968
970
} else {
@@ -975,7 +977,7 @@ impl VClockAlloc {
975
977
} ;
976
978
977
979
// Load elaborated thread information about the racing thread actions.
978
- let current_thread_info = global. print_thread_metadata ( thread_mgr, current_index ) ;
980
+ let active_thread_info = global. print_thread_metadata ( thread_mgr, active_index ) ;
979
981
let other_thread_info = global. print_thread_metadata ( thread_mgr, other_thread) ;
980
982
let involves_non_atomic = !access. is_atomic ( ) || !other_access. is_atomic ( ) ;
981
983
@@ -1003,8 +1005,8 @@ impl VClockAlloc {
1003
1005
} ,
1004
1006
op2: RacingOp {
1005
1007
action: access. description( ty, other_size. map( |_| access_size) ) ,
1006
- thread_info: current_thread_info ,
1007
- span: current_clocks . clock. as_slice( ) [ current_index . index( ) ] . span_data( ) ,
1008
+ thread_info: active_thread_info ,
1009
+ span: active_clocks . clock. as_slice( ) [ active_index . index( ) ] . span_data( ) ,
1008
1010
} ,
1009
1011
} ) ) ?
1010
1012
}
@@ -1026,7 +1028,7 @@ impl VClockAlloc {
1026
1028
let current_span = machine. current_span ( ) ;
1027
1029
let global = machine. data_race . as_ref ( ) . unwrap ( ) ;
1028
1030
if global. race_detecting ( ) {
1029
- let ( index, mut thread_clocks) = global. current_thread_state_mut ( & machine. threads ) ;
1031
+ let ( index, mut thread_clocks) = global. active_thread_state_mut ( & machine. threads ) ;
1030
1032
let mut alloc_ranges = self . alloc_ranges . borrow_mut ( ) ;
1031
1033
for ( mem_clocks_range, mem_clocks) in
1032
1034
alloc_ranges. iter_mut ( access_range. start , access_range. size )
@@ -1069,7 +1071,7 @@ impl VClockAlloc {
1069
1071
let current_span = machine. current_span ( ) ;
1070
1072
let global = machine. data_race . as_mut ( ) . unwrap ( ) ;
1071
1073
if global. race_detecting ( ) {
1072
- let ( index, mut thread_clocks) = global. current_thread_state_mut ( & machine. threads ) ;
1074
+ let ( index, mut thread_clocks) = global. active_thread_state_mut ( & machine. threads ) ;
1073
1075
for ( mem_clocks_range, mem_clocks) in
1074
1076
self . alloc_ranges . get_mut ( ) . iter_mut ( access_range. start , access_range. size )
1075
1077
{
@@ -1454,7 +1456,7 @@ impl GlobalState {
1454
1456
// Setup the main-thread since it is not explicitly created:
1455
1457
// uses vector index and thread-id 0.
1456
1458
let index = global_state. vector_clocks . get_mut ( ) . push ( ThreadClockSet :: default ( ) ) ;
1457
- global_state. vector_info . get_mut ( ) . push ( ThreadId :: new ( 0 ) ) ;
1459
+ global_state. vector_info . get_mut ( ) . push ( ThreadId :: MAIN_THREAD ) ;
1458
1460
global_state
1459
1461
. thread_info
1460
1462
. get_mut ( )
@@ -1518,7 +1520,7 @@ impl GlobalState {
1518
1520
thread : ThreadId ,
1519
1521
current_span : Span ,
1520
1522
) {
1521
- let current_index = self . current_index ( thread_mgr) ;
1523
+ let current_index = self . active_thread_index ( thread_mgr) ;
1522
1524
1523
1525
// Enable multi-threaded execution, there are now at least two threads
1524
1526
// so data-races are now possible.
@@ -1642,7 +1644,7 @@ impl GlobalState {
1642
1644
/// `thread_joined`.
1643
1645
#[ inline]
1644
1646
pub fn thread_terminated ( & mut self , thread_mgr : & ThreadManager < ' _ , ' _ > , current_span : Span ) {
1645
- let current_index = self . current_index ( thread_mgr) ;
1647
+ let current_index = self . active_thread_index ( thread_mgr) ;
1646
1648
1647
1649
// Increment the clock to a unique termination timestamp.
1648
1650
let vector_clocks = self . vector_clocks . get_mut ( ) ;
@@ -1680,9 +1682,9 @@ impl GlobalState {
1680
1682
op : impl FnOnce ( VectorIdx , RefMut < ' _ , ThreadClockSet > ) -> InterpResult < ' tcx , bool > ,
1681
1683
) -> InterpResult < ' tcx > {
1682
1684
if self . multi_threaded . get ( ) {
1683
- let ( index, clocks) = self . current_thread_state_mut ( thread_mgr) ;
1685
+ let ( index, clocks) = self . active_thread_state_mut ( thread_mgr) ;
1684
1686
if op ( index, clocks) ? {
1685
- let ( _, mut clocks) = self . current_thread_state_mut ( thread_mgr) ;
1687
+ let ( _, mut clocks) = self . active_thread_state_mut ( thread_mgr) ;
1686
1688
clocks. increment_clock ( index, current_span) ;
1687
1689
}
1688
1690
}
@@ -1725,13 +1727,15 @@ impl GlobalState {
1725
1727
Ref :: map ( clocks, |c| & c. clock )
1726
1728
}
1727
1729
1730
+ fn thread_index ( & self , thread : ThreadId ) -> VectorIdx {
1731
+ self . thread_info . borrow ( ) [ thread] . vector_index . expect ( "thread has no assigned vector" )
1732
+ }
1733
+
1728
1734
/// Load the vector index used by the given thread as well as the set of vector clocks
1729
1735
/// used by the thread.
1730
1736
#[ inline]
1731
1737
fn thread_state_mut ( & self , thread : ThreadId ) -> ( VectorIdx , RefMut < ' _ , ThreadClockSet > ) {
1732
- let index = self . thread_info . borrow ( ) [ thread]
1733
- . vector_index
1734
- . expect ( "Loading thread state for thread with no assigned vector" ) ;
1738
+ let index = self . thread_index ( thread) ;
1735
1739
let ref_vector = self . vector_clocks . borrow_mut ( ) ;
1736
1740
let clocks = RefMut :: map ( ref_vector, |vec| & mut vec[ index] ) ;
1737
1741
( index, clocks)
@@ -1741,9 +1745,7 @@ impl GlobalState {
1741
1745
/// used by the thread.
1742
1746
#[ inline]
1743
1747
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" ) ;
1748
+ let index = self . thread_index ( thread) ;
1747
1749
let ref_vector = self . vector_clocks . borrow ( ) ;
1748
1750
let clocks = Ref :: map ( ref_vector, |vec| & vec[ index] ) ;
1749
1751
( index, clocks)
@@ -1752,7 +1754,7 @@ impl GlobalState {
1752
1754
/// Load the current vector clock in use and the current set of thread clocks
1753
1755
/// in use for the vector.
1754
1756
#[ inline]
1755
- pub ( super ) fn current_thread_state (
1757
+ pub ( super ) fn active_thread_state (
1756
1758
& self ,
1757
1759
thread_mgr : & ThreadManager < ' _ , ' _ > ,
1758
1760
) -> ( VectorIdx , Ref < ' _ , ThreadClockSet > ) {
@@ -1762,7 +1764,7 @@ impl GlobalState {
1762
1764
/// Load the current vector clock in use and the current set of thread clocks
1763
1765
/// in use for the vector mutably for modification.
1764
1766
#[ inline]
1765
- pub ( super ) fn current_thread_state_mut (
1767
+ pub ( super ) fn active_thread_state_mut (
1766
1768
& self ,
1767
1769
thread_mgr : & ThreadManager < ' _ , ' _ > ,
1768
1770
) -> ( VectorIdx , RefMut < ' _ , ThreadClockSet > ) {
@@ -1772,22 +1774,20 @@ impl GlobalState {
1772
1774
/// Return the current thread, should be the same
1773
1775
/// as the data-race active thread.
1774
1776
#[ inline]
1775
- fn current_index ( & self , thread_mgr : & ThreadManager < ' _ , ' _ > ) -> VectorIdx {
1777
+ fn active_thread_index ( & self , thread_mgr : & ThreadManager < ' _ , ' _ > ) -> VectorIdx {
1776
1778
let active_thread_id = thread_mgr. get_active_thread_id ( ) ;
1777
- self . thread_info . borrow ( ) [ active_thread_id]
1778
- . vector_index
1779
- . expect ( "active thread has no assigned vector" )
1779
+ self . thread_index ( active_thread_id)
1780
1780
}
1781
1781
1782
1782
// SC ATOMIC STORE rule in the paper.
1783
1783
pub ( super ) fn sc_write ( & self , thread_mgr : & ThreadManager < ' _ , ' _ > ) {
1784
- let ( index, clocks) = self . current_thread_state ( thread_mgr) ;
1784
+ let ( index, clocks) = self . active_thread_state ( thread_mgr) ;
1785
1785
self . last_sc_write . borrow_mut ( ) . set_at_index ( & clocks. clock , index) ;
1786
1786
}
1787
1787
1788
1788
// SC ATOMIC READ rule in the paper.
1789
1789
pub ( super ) fn sc_read ( & self , thread_mgr : & ThreadManager < ' _ , ' _ > ) {
1790
- let ( .., mut clocks) = self . current_thread_state_mut ( thread_mgr) ;
1790
+ let ( .., mut clocks) = self . active_thread_state_mut ( thread_mgr) ;
1791
1791
clocks. read_seqcst . join ( & self . last_sc_fence . borrow ( ) ) ;
1792
1792
}
1793
1793
}
0 commit comments