Simplify scheduling, do cleanup

Author: Patrick-6

src/concurrency/genmc/dummy.rs

@@ -226,6 +226,15 @@ impl GenmcCtx {
         unreachable!()
     }
 
+    /**** Scheduling functionality ****/
+
+    pub fn schedule_thread<'tcx>(
+        &self,
+        _ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
+    ) -> InterpResult<'tcx, ThreadId> {
+        unreachable!()
+    }
+
     /**** Blocking instructions ****/
 
     #[allow(unused)]

src/concurrency/genmc/mod.rs

@@ -18,11 +18,10 @@ use self::helper::{
 use self::mapping::{min_max_to_genmc_rmw_op, to_genmc_rmw_op};
 use self::thread_info_manager::ThreadInfoManager;
 use crate::concurrency::genmc::helper::{is_terminator_atomic, split_access};
-use crate::concurrency::thread::{EvalContextExt as _, ThreadState};
 use crate::{
-    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, BlockReason, MemoryKind,
-    MiriConfig, MiriMachine, MiriMemoryKind, Scalar, TerminationInfo, ThreadId, ThreadManager,
-    VisitProvenance, VisitWith,
+    AtomicFenceOrd, AtomicReadOrd, AtomicRwOrd, AtomicWriteOrd, MemoryKind, MiriConfig,
+    MiriMachine, MiriMemoryKind, Scalar, TerminationInfo, ThreadId, ThreadManager, VisitProvenance,
+    VisitWith,
 };
 
 mod config;
@@ -853,7 +852,7 @@ impl GenmcCtx {
 
     /**** Scheduling functionality ****/
 
-    fn schedule_thread<'tcx>(
+    pub fn schedule_thread<'tcx>(
         &self,
         ecx: &InterpCx<'tcx, MiriMachine<'tcx>>,
     ) -> InterpResult<'tcx, ThreadId> {
@@ -920,49 +919,6 @@ impl GenmcCtx {
     }
 }
 
-/// Other functionality not directly related to event handling
-impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
-pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
-    /**** Scheduling functionality ****/
-
-    /// Ask for a scheduling decision. This should be called before every MIR instruction.
-    ///
-    /// GenMC may realize that the execution is blocked, then this function will return a `InterpErrorKind::MachineStop` with error kind `TerminationInfo::GenmcBlockedExecution`).
-    ///
-    /// This is **not** an error by iself! Treat this as if the program ended normally: `handle_execution_end` should be called next, which will determine if were are any actual errors.
-    fn genmc_schedule_thread(&mut self) -> InterpResult<'tcx, ThreadId> {
-        let this = self.eval_context_mut();
-        loop {
-            let genmc_ctx = this.machine.data_race.as_genmc_ref().unwrap();
-            let next_thread_id = genmc_ctx.schedule_thread(this)?;
-
-            match this.machine.threads.threads_ref()[next_thread_id].get_state() {
-                ThreadState::Blocked {
-                    reason: block_reason @ (BlockReason::Mutex | BlockReason::GenmcAssume),
-                    ..
-                } => {
-                    info!(
-                        "GenMC: schedule returned thread {next_thread_id:?}, which is blocked, so we unblock it now."
-                    );
-                    this.unblock_thread(next_thread_id, *block_reason)?;
-
-                    // In some cases, like waiting on a Mutex::lock, the thread might still be blocked here:
-                    if this.machine.threads.threads_ref()[next_thread_id]
-                        .get_state()
-                        .is_blocked_on(crate::BlockReason::Mutex)
-                    {
-                        info!("GenMC: Unblocked thread is blocked on a Mutex again!");
-                        continue;
-                    }
-                }
-                _ => {}
-            }
-
-            return interp_ok(next_thread_id);
-        }
-    }
-}
-
 impl VisitProvenance for GenmcCtx {
     fn visit_provenance(&self, _visit: &mut VisitWith<'_>) {
         // We don't have any tags.

src/concurrency/mod.rs

@@ -22,5 +22,5 @@ pub mod weak_memory;
 mod genmc;
 
 pub use self::data_race_handler::{AllocDataRaceHandler, GlobalDataRaceHandler};
-pub use self::genmc::{EvalContextExt as GenmcEvalContextExt, GenmcConfig, GenmcCtx, miri_genmc};
+pub use self::genmc::{GenmcConfig, GenmcCtx, miri_genmc};
 pub use self::vector_clock::VClock;

src/concurrency/thread.rs

@@ -16,7 +16,7 @@ use rustc_middle::mir::Mutability;
 use rustc_middle::ty::layout::TyAndLayout;
 use rustc_span::Span;
 
-use crate::concurrency::{GenmcEvalContextExt as _, GlobalDataRaceHandler};
+use crate::concurrency::GlobalDataRaceHandler;
 use crate::shims::tls;
 use crate::*;
 
@@ -110,8 +110,6 @@ pub enum BlockReason {
     Eventfd,
     /// Blocked on unnamed_socket.
     UnnamedSocket,
-    /// Blocked on a GenMC `assume` statement (GenMC mode only).
-    GenmcAssume,
 }
 
 /// The state of a thread.
@@ -535,11 +533,6 @@ impl<'tcx> ThreadManager<'tcx> {
         self.active_thread
     }
 
-    pub fn threads_ref(&self) -> &IndexVec<ThreadId, Thread<'tcx>> {
-        // TODO GENMC: should this implementation detail be exposed?
-        &self.threads
-    }
-
     /// Get the total number of threads that were ever spawn by this program.
     pub fn get_total_thread_count(&self) -> usize {
         self.threads.len()
@@ -725,8 +718,8 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
         let this = self.eval_context_mut();
 
         // In GenMC mode, we let GenMC do the scheduling.
-        if this.machine.data_race.as_genmc_ref().is_some() {
-            let next_thread_id = this.genmc_schedule_thread()?;
+        if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
+            let next_thread_id = genmc_ctx.schedule_thread(this)?;
 
             let thread_manager = &mut this.machine.threads;
             thread_manager.active_thread = next_thread_id;