@@ -689,6 +689,17 @@ pub trait EvalContextExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
689
689
Ok ( ( ) )
690
690
}
691
691
}
692
+
693
+ /// After all threads are done running, this allows data races to occur for subsequent
694
+ /// 'administrative' machine accesses (that logically happen outside of the Abstract Machine).
695
+ fn allow_data_races_all_threads_done ( & mut self ) {
696
+ let this = self . eval_context_ref ( ) ;
697
+ assert ! ( this. have_all_terminated( ) ) ;
698
+ if let Some ( data_race) = & this. machine . data_race {
699
+ let old = data_race. ongoing_action_data_race_free . replace ( true ) ;
700
+ assert ! ( !old, "cannot nest allow_data_races" ) ;
701
+ }
702
+ }
692
703
}
693
704
694
705
/// Vector clock metadata for a logical memory allocation.
@@ -955,8 +966,8 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
955
966
fn allow_data_races_ref < R > ( & self , op : impl FnOnce ( & MiriEvalContext < ' mir , ' tcx > ) -> R ) -> R {
956
967
let this = self . eval_context_ref ( ) ;
957
968
if let Some ( data_race) = & this. machine . data_race {
958
- assert ! ( ! data_race. ongoing_action_data_race_free. get ( ) , "cannot nest allow_data_races" ) ;
959
- data_race . ongoing_action_data_race_free . set ( true ) ;
969
+ let old = data_race. ongoing_action_data_race_free . replace ( true ) ;
970
+ assert ! ( !old , "cannot nest allow_data_races" ) ;
960
971
}
961
972
let result = op ( this) ;
962
973
if let Some ( data_race) = & this. machine . data_race {
@@ -975,8 +986,8 @@ trait EvalContextPrivExt<'mir, 'tcx: 'mir>: MiriEvalContextExt<'mir, 'tcx> {
975
986
) -> R {
976
987
let this = self . eval_context_mut ( ) ;
977
988
if let Some ( data_race) = & this. machine . data_race {
978
- assert ! ( ! data_race. ongoing_action_data_race_free. get ( ) , "cannot nest allow_data_races" ) ;
979
- data_race . ongoing_action_data_race_free . set ( true ) ;
989
+ let old = data_race. ongoing_action_data_race_free . replace ( true ) ;
990
+ assert ! ( !old , "cannot nest allow_data_races" ) ;
980
991
}
981
992
let result = op ( this) ;
982
993
if let Some ( data_race) = & this. machine . data_race {
0 commit comments