@@ -61,7 +61,8 @@ impl ThreadId {
61
61
}
62
62
}
63
63
64
- /// An identifier of a set of blocked threads.
64
+ /// An identifier of a set of blocked threads. 0 is used to indicate the absence
65
+ /// of a blockset identifier and, therefore, is not a valid identifier.
65
66
#[ derive( Clone , Copy , Debug , PartialOrd , Ord , PartialEq , Eq , Hash ) ]
66
67
pub struct BlockSetId ( NonZeroU32 ) ;
67
68
@@ -116,8 +117,8 @@ pub struct Thread<'mir, 'tcx> {
116
117
}
117
118
118
119
impl < ' mir , ' tcx > Thread < ' mir , ' tcx > {
119
- /// Check if the thread terminated. If yes, change the state to terminated
120
- /// and return `true`.
120
+ /// Check if the thread is done executing (no more stack frames). If yes,
121
+ /// change the state to terminated and return `true`.
121
122
fn check_terminated ( & mut self ) -> bool {
122
123
if self . state == ThreadState :: Enabled {
123
124
if self . stack . is_empty ( ) {
@@ -174,6 +175,7 @@ impl<'mir, 'tcx> Default for ThreadManager<'mir, 'tcx> {
174
175
let mut threads = IndexVec :: new ( ) ;
175
176
// Create the main thread and add it to the list of threads.
176
177
let mut main_thread = Thread :: default ( ) ;
178
+ // The main thread can *not* be joined on.
177
179
main_thread. join_status = ThreadJoinStatus :: Detached ;
178
180
threads. push ( main_thread) ;
179
181
Self {
@@ -282,7 +284,7 @@ impl<'mir, 'tcx: 'mir> ThreadManager<'mir, 'tcx> {
282
284
self . threads
283
285
. iter( )
284
286
. all( |thread| thread. state != ThreadState :: BlockedOnJoin ( joined_thread_id) ) ,
285
- "a joinable thread has threads waiting for its termination"
287
+ "a joinable thread already has threads waiting for its termination"
286
288
) ;
287
289
// Mark the joined thread as being joined so that we detect if other
288
290
// threads try to join it.
@@ -349,7 +351,7 @@ impl<'mir, 'tcx: 'mir> ThreadManager<'mir, 'tcx> {
349
351
/// The currently implemented scheduling policy is the one that is commonly
350
352
/// used in stateless model checkers such as Loom: run the active thread as
351
353
/// long as we can and switch only when we have to (the active thread was
352
- /// blocked, terminated, or was explicitly asked to be preempted).
354
+ /// blocked, terminated, or has explicitly asked to be preempted).
353
355
fn schedule ( & mut self ) -> InterpResult < ' tcx , SchedulingAction > {
354
356
if self . threads [ self . active_thread ] . check_terminated ( ) {
355
357
// Check if we need to unblock any threads.
0 commit comments