@@ -582,88 +582,6 @@ impl<'tcx> ThreadManager<'tcx> {
582
582
interp_ok ( ( ) )
583
583
}
584
584
585
- /// Mark that the active thread tries to join the thread with `joined_thread_id`.
586
- fn join_thread (
587
- & mut self ,
588
- joined_thread_id : ThreadId ,
589
- data_race_handler : & mut GlobalDataRaceHandler ,
590
- ) -> InterpResult < ' tcx > {
591
- if self . threads [ joined_thread_id] . join_status == ThreadJoinStatus :: Detached {
592
- // On Windows this corresponds to joining on a closed handle.
593
- throw_ub_format ! ( "trying to join a detached thread" ) ;
594
- }
595
-
596
- fn after_join < ' tcx > (
597
- threads : & mut ThreadManager < ' _ > ,
598
- joined_thread_id : ThreadId ,
599
- data_race_handler : & mut GlobalDataRaceHandler ,
600
- ) -> InterpResult < ' tcx > {
601
- match data_race_handler {
602
- GlobalDataRaceHandler :: None => { }
603
- GlobalDataRaceHandler :: Vclocks ( data_race) =>
604
- data_race. thread_joined ( threads, joined_thread_id) ,
605
- GlobalDataRaceHandler :: Genmc ( genmc_ctx) =>
606
- genmc_ctx. handle_thread_join ( threads. active_thread , joined_thread_id) ?,
607
- }
608
- interp_ok ( ( ) )
609
- }
610
-
611
- // Mark the joined thread as being joined so that we detect if other
612
- // threads try to join it.
613
- self . threads [ joined_thread_id] . join_status = ThreadJoinStatus :: Joined ;
614
- if !self . threads [ joined_thread_id] . state . is_terminated ( ) {
615
- trace ! (
616
- "{:?} blocked on {:?} when trying to join" ,
617
- self . active_thread, joined_thread_id
618
- ) ;
619
- // The joined thread is still running, we need to wait for it.
620
- // Unce we get unblocked, perform the appropriate synchronization.
621
- self . block_thread (
622
- BlockReason :: Join ( joined_thread_id) ,
623
- None ,
624
- callback ! (
625
- @capture<' tcx> {
626
- joined_thread_id: ThreadId ,
627
- }
628
- |this, unblock: UnblockKind | {
629
- assert_eq!( unblock, UnblockKind :: Ready ) ;
630
- after_join( & mut this. machine. threads, joined_thread_id, & mut this. machine. data_race)
631
- }
632
- ) ,
633
- ) ;
634
- } else {
635
- // The thread has already terminated - establish happens-before
636
- after_join ( self , joined_thread_id, data_race_handler) ?;
637
- }
638
- interp_ok ( ( ) )
639
- }
640
-
641
- /// Mark that the active thread tries to exclusively join the thread with `joined_thread_id`.
642
- /// If the thread is already joined by another thread, it will throw UB
643
- fn join_thread_exclusive (
644
- & mut self ,
645
- joined_thread_id : ThreadId ,
646
- data_race_handler : & mut GlobalDataRaceHandler ,
647
- ) -> InterpResult < ' tcx > {
648
- if self . threads [ joined_thread_id] . join_status == ThreadJoinStatus :: Joined {
649
- throw_ub_format ! ( "trying to join an already joined thread" ) ;
650
- }
651
-
652
- if joined_thread_id == self . active_thread {
653
- throw_ub_format ! ( "trying to join itself" ) ;
654
- }
655
-
656
- // Sanity check `join_status`.
657
- assert ! (
658
- self . threads
659
- . iter( )
660
- . all( |thread| { !thread. state. is_blocked_on( BlockReason :: Join ( joined_thread_id) ) } ) ,
661
- "this thread already has threads waiting for its termination"
662
- ) ;
663
-
664
- self . join_thread ( joined_thread_id, data_race_handler)
665
- }
666
-
667
585
/// Set the name of the given thread.
668
586
pub fn set_thread_name ( & mut self , thread : ThreadId , new_thread_name : Vec < u8 > ) {
669
587
self . threads [ thread] . thread_name = Some ( new_thread_name) ;
@@ -1114,20 +1032,102 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
1114
1032
this. machine . threads . detach_thread ( thread_id, allow_terminated_joined)
1115
1033
}
1116
1034
1117
- #[ inline]
1118
- fn join_thread ( & mut self , joined_thread_id : ThreadId ) -> InterpResult < ' tcx > {
1035
+ /// Mark that the active thread tries to join the thread with `joined_thread_id`.
1036
+ ///
1037
+ /// When the join is successful (immediately, or as soon as the joined thread finishes), `success_retval` will be written to `return_dest`.
1038
+ fn join_thread (
1039
+ & mut self ,
1040
+ joined_thread_id : ThreadId ,
1041
+ success_retval : Scalar ,
1042
+ return_dest : & MPlaceTy < ' tcx > ,
1043
+ ) -> InterpResult < ' tcx > {
1119
1044
let this = self . eval_context_mut ( ) ;
1120
- this. machine . threads . join_thread ( joined_thread_id, & mut this. machine . data_race ) ?;
1045
+ let thread_mgr = & mut this. machine . threads ;
1046
+ if thread_mgr. threads [ joined_thread_id] . join_status == ThreadJoinStatus :: Detached {
1047
+ // On Windows this corresponds to joining on a closed handle.
1048
+ throw_ub_format ! ( "trying to join a detached thread" ) ;
1049
+ }
1050
+
1051
+ fn after_join < ' tcx > (
1052
+ this : & mut InterpCx < ' tcx , MiriMachine < ' tcx > > ,
1053
+ joined_thread_id : ThreadId ,
1054
+ success_retval : Scalar ,
1055
+ return_dest : & MPlaceTy < ' tcx > ,
1056
+ ) -> InterpResult < ' tcx > {
1057
+ let threads = & this. machine . threads ;
1058
+ match & mut this. machine . data_race {
1059
+ GlobalDataRaceHandler :: None => { }
1060
+ GlobalDataRaceHandler :: Vclocks ( data_race) =>
1061
+ data_race. thread_joined ( threads, joined_thread_id) ,
1062
+ GlobalDataRaceHandler :: Genmc ( genmc_ctx) =>
1063
+ genmc_ctx. handle_thread_join ( threads. active_thread , joined_thread_id) ?,
1064
+ }
1065
+ this. write_scalar ( success_retval, return_dest) ?;
1066
+ interp_ok ( ( ) )
1067
+ }
1068
+
1069
+ // Mark the joined thread as being joined so that we detect if other
1070
+ // threads try to join it.
1071
+ thread_mgr. threads [ joined_thread_id] . join_status = ThreadJoinStatus :: Joined ;
1072
+ if !thread_mgr. threads [ joined_thread_id] . state . is_terminated ( ) {
1073
+ trace ! (
1074
+ "{:?} blocked on {:?} when trying to join" ,
1075
+ thread_mgr. active_thread, joined_thread_id
1076
+ ) ;
1077
+ // The joined thread is still running, we need to wait for it.
1078
+ // Once we get unblocked, perform the appropriate synchronization and write the return value.
1079
+ let dest = return_dest. clone ( ) ;
1080
+ thread_mgr. block_thread (
1081
+ BlockReason :: Join ( joined_thread_id) ,
1082
+ None ,
1083
+ callback ! (
1084
+ @capture<' tcx> {
1085
+ joined_thread_id: ThreadId ,
1086
+ dest: MPlaceTy <' tcx>,
1087
+ success_retval: Scalar ,
1088
+ }
1089
+ |this, unblock: UnblockKind | {
1090
+ assert_eq!( unblock, UnblockKind :: Ready ) ;
1091
+ after_join( this, joined_thread_id, success_retval, & dest)
1092
+ }
1093
+ ) ,
1094
+ ) ;
1095
+ } else {
1096
+ // The thread has already terminated - establish happens-before and write the return value.
1097
+ after_join ( this, joined_thread_id, success_retval, return_dest) ?;
1098
+ }
1121
1099
interp_ok ( ( ) )
1122
1100
}
1123
1101
1124
- #[ inline]
1125
- fn join_thread_exclusive ( & mut self , joined_thread_id : ThreadId ) -> InterpResult < ' tcx > {
1102
+ /// Mark that the active thread tries to exclusively join the thread with `joined_thread_id`.
1103
+ /// If the thread is already joined by another thread, it will throw UB.
1104
+ ///
1105
+ /// When the join is successful (immediately, or as soon as the joined thread finishes), `success_retval` will be written to `return_dest`.
1106
+ fn join_thread_exclusive (
1107
+ & mut self ,
1108
+ joined_thread_id : ThreadId ,
1109
+ success_retval : Scalar ,
1110
+ return_dest : & MPlaceTy < ' tcx > ,
1111
+ ) -> InterpResult < ' tcx > {
1126
1112
let this = self . eval_context_mut ( ) ;
1127
- this. machine
1128
- . threads
1129
- . join_thread_exclusive ( joined_thread_id, & mut this. machine . data_race ) ?;
1130
- interp_ok ( ( ) )
1113
+ let threads = & this. machine . threads . threads ;
1114
+ if threads[ joined_thread_id] . join_status == ThreadJoinStatus :: Joined {
1115
+ throw_ub_format ! ( "trying to join an already joined thread" ) ;
1116
+ }
1117
+
1118
+ if joined_thread_id == this. machine . threads . active_thread {
1119
+ throw_ub_format ! ( "trying to join itself" ) ;
1120
+ }
1121
+
1122
+ // Sanity check `join_status`.
1123
+ assert ! (
1124
+ threads
1125
+ . iter( )
1126
+ . all( |thread| { !thread. state. is_blocked_on( BlockReason :: Join ( joined_thread_id) ) } ) ,
1127
+ "this thread already has threads waiting for its termination"
1128
+ ) ;
1129
+
1130
+ this. join_thread ( joined_thread_id, success_retval, return_dest)
1131
1131
}
1132
1132
1133
1133
#[ inline]
0 commit comments