@@ -31,6 +31,9 @@ pub enum SchedulingAction {
31
31
#[ derive( Clone , Copy , Debug , PartialOrd , Ord , PartialEq , Eq , Hash ) ]
32
32
pub struct ThreadId ( usize ) ;
33
33
34
+ /// The main thread. When it terminates, the whole application terminates.
35
+ const MAIN_THREAD : ThreadId = ThreadId ( 0 ) ;
36
+
34
37
impl Idx for ThreadId {
35
38
fn new ( idx : usize ) -> Self {
36
39
ThreadId ( idx)
@@ -42,13 +45,13 @@ impl Idx for ThreadId {
42
45
43
46
impl From < u64 > for ThreadId {
44
47
fn from ( id : u64 ) -> Self {
45
- Self ( id as usize )
48
+ Self ( usize:: try_from ( id ) . unwrap ( ) )
46
49
}
47
50
}
48
51
49
52
impl From < u32 > for ThreadId {
50
53
fn from ( id : u32 ) -> Self {
51
- Self ( id as usize )
54
+ Self ( usize:: try_from ( id ) . unwrap ( ) )
52
55
}
53
56
}
54
57
@@ -82,10 +85,10 @@ pub enum ThreadState {
82
85
/// The thread tried to join the specified thread and is blocked until that
83
86
/// thread terminates.
84
87
BlockedOnJoin ( ThreadId ) ,
85
- /// The thread is blocked and belongs to the given blockset..
88
+ /// The thread is blocked and belongs to the given blockset.
86
89
Blocked ( BlockSetId ) ,
87
90
/// The thread has terminated its execution (we do not delete terminated
88
- /// threads.)
91
+ /// threads).
89
92
Terminated ,
90
93
}
91
94
@@ -150,6 +153,7 @@ pub struct ThreadManager<'mir, 'tcx> {
150
153
impl < ' mir , ' tcx > Default for ThreadManager < ' mir , ' tcx > {
151
154
fn default ( ) -> Self {
152
155
let mut threads = IndexVec :: new ( ) ;
156
+ // Create the main thread and add it to the list of threads.
153
157
threads. push ( Default :: default ( ) ) ;
154
158
Self {
155
159
active_thread : ThreadId :: new ( 0 ) ,
@@ -170,14 +174,13 @@ impl<'mir, 'tcx: 'mir> ThreadManager<'mir, 'tcx> {
170
174
171
175
/// Set the allocation id as the allocation id of the given thread local
172
176
/// static for the active thread.
177
+ ///
178
+ /// Panics if a thread local is initialized twice for the same thread.
173
179
fn set_thread_local_alloc_id ( & self , def_id : DefId , new_alloc_id : AllocId ) {
174
- assert ! (
175
- self . thread_local_alloc_ids
176
- . borrow_mut( )
177
- . insert( ( def_id, self . active_thread) , new_alloc_id)
178
- . is_none( ) ,
179
- "a thread local initialized twice for the same thread"
180
- ) ;
180
+ self . thread_local_alloc_ids
181
+ . borrow_mut ( )
182
+ . insert ( ( def_id, self . active_thread ) , new_alloc_id)
183
+ . unwrap_none ( ) ;
181
184
}
182
185
183
186
/// Borrow the stack of the active thread.
@@ -227,15 +230,20 @@ impl<'mir, 'tcx: 'mir> ThreadManager<'mir, 'tcx> {
227
230
}
228
231
229
232
/// Mark that the active thread tries to join the thread with `joined_thread_id`.
230
- fn join_thread ( & mut self , joined_thread_id : ThreadId ) {
231
- assert ! ( !self . threads[ joined_thread_id] . detached, "Bug: trying to join a detached thread." ) ;
232
- assert_ne ! ( joined_thread_id, self . active_thread, "Bug: trying to join itself" ) ;
233
- assert ! (
234
- self . threads
235
- . iter( )
236
- . all( |thread| thread. state != ThreadState :: BlockedOnJoin ( joined_thread_id) ) ,
237
- "Bug: multiple threads try to join the same thread."
238
- ) ;
233
+ fn join_thread ( & mut self , joined_thread_id : ThreadId ) -> InterpResult < ' tcx > {
234
+ if self . threads [ joined_thread_id] . detached {
235
+ throw_ub_format ! ( "trying to join a detached thread" ) ;
236
+ }
237
+ if joined_thread_id == self . active_thread {
238
+ throw_ub_format ! ( "trying to join itself" ) ;
239
+ }
240
+ if self
241
+ . threads
242
+ . iter ( )
243
+ . any ( |thread| thread. state == ThreadState :: BlockedOnJoin ( joined_thread_id) )
244
+ {
245
+ throw_ub_format ! ( "multiple threads try to join the same thread" ) ;
246
+ }
239
247
if self . threads [ joined_thread_id] . state != ThreadState :: Terminated {
240
248
// The joined thread is still running, we need to wait for it.
241
249
self . active_thread_mut ( ) . state = ThreadState :: BlockedOnJoin ( joined_thread_id) ;
@@ -245,13 +253,23 @@ impl<'mir, 'tcx: 'mir> ThreadManager<'mir, 'tcx> {
245
253
joined_thread_id
246
254
) ;
247
255
}
256
+ Ok ( ( ) )
248
257
}
249
258
250
259
/// Set the name of the active thread.
251
260
fn set_thread_name ( & mut self , new_thread_name : Vec < u8 > ) {
252
261
self . active_thread_mut ( ) . thread_name = Some ( new_thread_name) ;
253
262
}
254
263
264
+ /// Get the name of the active thread.
265
+ fn get_thread_name ( & mut self ) -> InterpResult < ' tcx , Vec < u8 > > {
266
+ if let Some ( ref thread_name) = self . active_thread_mut ( ) . thread_name {
267
+ Ok ( thread_name. clone ( ) )
268
+ } else {
269
+ throw_ub_format ! ( "thread {:?} has no name set" , self . active_thread)
270
+ }
271
+ }
272
+
255
273
/// Allocate a new blockset id.
256
274
fn create_blockset ( & mut self ) -> BlockSetId {
257
275
self . blockset_counter = self . blockset_counter . checked_add ( 1 ) . unwrap ( ) ;
@@ -267,7 +285,7 @@ impl<'mir, 'tcx: 'mir> ThreadManager<'mir, 'tcx> {
267
285
268
286
/// Unblock any one thread from the given blockset if it contains at least
269
287
/// one. Return the id of the unblocked thread.
270
- fn unblock_random_thread ( & mut self , set : BlockSetId ) -> Option < ThreadId > {
288
+ fn unblock_some_thread ( & mut self , set : BlockSetId ) -> Option < ThreadId > {
271
289
for ( id, thread) in self . threads . iter_enumerated_mut ( ) {
272
290
if thread. state == ThreadState :: Blocked ( set) {
273
291
trace ! ( "unblocking {:?} in blockset {:?}" , id, set) ;
@@ -284,6 +302,11 @@ impl<'mir, 'tcx: 'mir> ThreadManager<'mir, 'tcx> {
284
302
}
285
303
286
304
/// Decide which action to take next and on which thread.
305
+ ///
306
+ /// The currently implemented scheduling policy is the one that is commonly
307
+ /// used in stateless model checkers such as Loom: run the active thread as
308
+ /// long as we can and switch only when we have to (the active thread was
309
+ /// blocked, terminated, or was explicitly asked to be preempted).
287
310
fn schedule ( & mut self ) -> InterpResult < ' tcx , SchedulingAction > {
288
311
if self . threads [ self . active_thread ] . check_terminated ( ) {
289
312
// Check if we need to unblock any threads.
@@ -295,14 +318,24 @@ impl<'mir, 'tcx: 'mir> ThreadManager<'mir, 'tcx> {
295
318
}
296
319
return Ok ( SchedulingAction :: ExecuteDtors ) ;
297
320
}
321
+ if self . threads [ MAIN_THREAD ] . state == ThreadState :: Terminated {
322
+ // The main thread terminated; stop the program.
323
+ if self . threads . iter ( ) . any ( |thread| thread. state != ThreadState :: Terminated ) {
324
+ // FIXME: This check should be either configurable or just emit a warning.
325
+ throw_unsup_format ! ( "the main thread terminated without waiting for other threads" ) ;
326
+ }
327
+ return Ok ( SchedulingAction :: Stop ) ;
328
+ }
298
329
if self . threads [ self . active_thread ] . state == ThreadState :: Enabled
299
330
&& !self . yield_active_thread
300
331
{
332
+ // The currently active thread is still enabled, just continue with it.
301
333
return Ok ( SchedulingAction :: ExecuteStep ) ;
302
334
}
335
+ // We need to pick a new thread for execution.
303
336
for ( id, thread) in self . threads . iter_enumerated ( ) {
304
337
if thread. state == ThreadState :: Enabled {
305
- if !( self . yield_active_thread && id == self . active_thread ) {
338
+ if !self . yield_active_thread || id != self . active_thread {
306
339
self . active_thread = id;
307
340
break ;
308
341
}
@@ -312,14 +345,16 @@ impl<'mir, 'tcx: 'mir> ThreadManager<'mir, 'tcx> {
312
345
if self . threads [ self . active_thread ] . state == ThreadState :: Enabled {
313
346
return Ok ( SchedulingAction :: ExecuteStep ) ;
314
347
}
348
+ // We have not found a thread to execute.
315
349
if self . threads . iter ( ) . all ( |thread| thread. state == ThreadState :: Terminated ) {
316
- Ok ( SchedulingAction :: Stop )
350
+ unreachable ! ( ) ;
317
351
} else {
318
352
throw_machine_stop ! ( TerminationInfo :: Deadlock ) ;
319
353
}
320
354
}
321
355
}
322
356
357
+ // Public interface to thread management.
323
358
impl < ' mir , ' tcx : ' mir > EvalContextExt < ' mir , ' tcx > for crate :: MiriEvalContext < ' mir , ' tcx > { }
324
359
pub trait EvalContextExt < ' mir , ' tcx : ' mir > : crate :: MiriEvalContextExt < ' mir , ' tcx > {
325
360
/// A workaround for thread-local statics until
@@ -331,8 +366,8 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
331
366
val : & mut mir:: interpret:: ConstValue < ' tcx > ,
332
367
) -> InterpResult < ' tcx > {
333
368
let this = self . eval_context_ref ( ) ;
334
- match val {
335
- mir:: interpret:: ConstValue :: Scalar ( Scalar :: Ptr ( ptr) ) => {
369
+ match * val {
370
+ mir:: interpret:: ConstValue :: Scalar ( Scalar :: Ptr ( ref mut ptr) ) => {
336
371
let alloc_id = ptr. alloc_id ;
337
372
let alloc = this. tcx . alloc_map . lock ( ) . get ( alloc_id) ;
338
373
let tcx = this. tcx ;
@@ -407,75 +442,94 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: crate::MiriEvalContextExt<'mir, 'tcx
407
442
}
408
443
}
409
444
445
+ #[ inline]
410
446
fn create_thread ( & mut self ) -> InterpResult < ' tcx , ThreadId > {
411
447
let this = self . eval_context_mut ( ) ;
412
448
Ok ( this. machine . threads . create_thread ( ) )
413
449
}
414
450
451
+ #[ inline]
415
452
fn detach_thread ( & mut self , thread_id : ThreadId ) -> InterpResult < ' tcx > {
416
453
let this = self . eval_context_mut ( ) ;
417
454
this. machine . threads . detach_thread ( thread_id) ;
418
455
Ok ( ( ) )
419
456
}
420
457
458
+ #[ inline]
421
459
fn join_thread ( & mut self , joined_thread_id : ThreadId ) -> InterpResult < ' tcx > {
422
460
let this = self . eval_context_mut ( ) ;
423
- this. machine . threads . join_thread ( joined_thread_id) ;
424
- Ok ( ( ) )
461
+ this. machine . threads . join_thread ( joined_thread_id)
425
462
}
426
463
464
+ #[ inline]
427
465
fn set_active_thread ( & mut self , thread_id : ThreadId ) -> InterpResult < ' tcx , ThreadId > {
428
466
let this = self . eval_context_mut ( ) ;
429
467
Ok ( this. machine . threads . set_active_thread_id ( thread_id) )
430
468
}
431
469
470
+ #[ inline]
432
471
fn get_active_thread ( & self ) -> InterpResult < ' tcx , ThreadId > {
433
472
let this = self . eval_context_ref ( ) ;
434
473
Ok ( this. machine . threads . get_active_thread_id ( ) )
435
474
}
436
475
476
+ #[ inline]
437
477
fn has_terminated ( & self , thread_id : ThreadId ) -> InterpResult < ' tcx , bool > {
438
478
let this = self . eval_context_ref ( ) ;
439
479
Ok ( this. machine . threads . has_terminated ( thread_id) )
440
480
}
441
481
482
+ #[ inline]
442
483
fn active_thread_stack ( & self ) -> & [ Frame < ' mir , ' tcx , Tag , FrameData < ' tcx > > ] {
443
484
let this = self . eval_context_ref ( ) ;
444
485
this. machine . threads . active_thread_stack ( )
445
486
}
446
487
488
+ #[ inline]
447
489
fn active_thread_stack_mut ( & mut self ) -> & mut Vec < Frame < ' mir , ' tcx , Tag , FrameData < ' tcx > > > {
448
490
let this = self . eval_context_mut ( ) ;
449
491
this. machine . threads . active_thread_stack_mut ( )
450
492
}
451
493
494
+ #[ inline]
452
495
fn set_active_thread_name ( & mut self , new_thread_name : Vec < u8 > ) -> InterpResult < ' tcx , ( ) > {
453
496
let this = self . eval_context_mut ( ) ;
454
497
Ok ( this. machine . threads . set_thread_name ( new_thread_name) )
455
498
}
456
499
500
+ #[ inline]
501
+ fn get_active_thread_name ( & mut self ) -> InterpResult < ' tcx , Vec < u8 > > {
502
+ let this = self . eval_context_mut ( ) ;
503
+ this. machine . threads . get_thread_name ( )
504
+ }
505
+
506
+ #[ inline]
457
507
fn create_blockset ( & mut self ) -> InterpResult < ' tcx , BlockSetId > {
458
508
let this = self . eval_context_mut ( ) ;
459
509
Ok ( this. machine . threads . create_blockset ( ) )
460
510
}
461
511
512
+ #[ inline]
462
513
fn block_active_thread ( & mut self , set : BlockSetId ) -> InterpResult < ' tcx > {
463
514
let this = self . eval_context_mut ( ) ;
464
515
Ok ( this. machine . threads . block_active_thread ( set) )
465
516
}
466
517
467
- fn unblock_random_thread ( & mut self , set : BlockSetId ) -> InterpResult < ' tcx , Option < ThreadId > > {
518
+ #[ inline]
519
+ fn unblock_some_thread ( & mut self , set : BlockSetId ) -> InterpResult < ' tcx , Option < ThreadId > > {
468
520
let this = self . eval_context_mut ( ) ;
469
- Ok ( this. machine . threads . unblock_random_thread ( set) )
521
+ Ok ( this. machine . threads . unblock_some_thread ( set) )
470
522
}
471
523
524
+ #[ inline]
472
525
fn yield_active_thread ( & mut self ) -> InterpResult < ' tcx > {
473
526
let this = self . eval_context_mut ( ) ;
474
527
this. machine . threads . yield_active_thread ( ) ;
475
528
Ok ( ( ) )
476
529
}
477
530
478
531
/// Decide which action to take next and on which thread.
532
+ #[ inline]
479
533
fn schedule ( & mut self ) -> InterpResult < ' tcx , SchedulingAction > {
480
534
let this = self . eval_context_mut ( ) ;
481
535
this. machine . threads . schedule ( )
0 commit comments