@@ -582,88 +582,6 @@ impl<'tcx> ThreadManager<'tcx> {
582582 interp_ok ( ( ) )
583583 }
584584
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-
667585 /// Set the name of the given thread.
668586 pub fn set_thread_name ( & mut self , thread : ThreadId , new_thread_name : Vec < u8 > ) {
669587 self . threads [ thread] . thread_name = Some ( new_thread_name) ;
@@ -1114,20 +1032,102 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
11141032 this. machine . threads . detach_thread ( thread_id, allow_terminated_joined)
11151033 }
11161034
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 > {
11191044 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+ }
11211099 interp_ok ( ( ) )
11221100 }
11231101
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 > {
11261112 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)
11311131 }
11321132
11331133 #[ inline]
0 commit comments