@@ -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 (
@@ -864,15 +865,16 @@ impl VClockAlloc {
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 (
@@ -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 ( )
@@ -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)
@@ -1774,9 +1776,7 @@ impl GlobalState {
1774
1776
#[ inline]
1775
1777
fn current_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.
0 commit comments