Improve blocking in GenMC mode, fix deadlock test (deadlock is not currently detected)

Author: Patrick-6

genmc-sys/cpp/include/MiriInterface.hpp

@@ -136,10 +136,7 @@ struct MiriGenmcShim : private GenMCDriver {
 
     /**** Blocking instructions ****/
     /// Inform GenMC that the thread should be blocked.
-    /// Note: this function is currently hardcoded for `AssumeType::User`, corresponding to user
-    /// supplied assume statements. This can become a parameter once more types of assumes are
-    /// added.
-    void handle_assume_block(ThreadId thread_id);
+    void handle_assume_block(ThreadId thread_id, AssumeType assume_type);
 
     /**** Mutex handling ****/
     auto handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size) -> MutexLockResult;

genmc-sys/cpp/src/MiriInterface/EventHandling.cpp

@@ -32,9 +32,9 @@
 
 /**** Blocking instructions ****/
 
-void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
+void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) {
     BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
-    GenMCDriver::handleAssume(inc_pos(thread_id), AssumeType::User);
+    GenMCDriver::handleAssume(inc_pos(thread_id), assume_type);
 }
 
 /**** Memory access handling ****/

genmc-sys/cpp/src/MiriInterface/Mutex.cpp

@@ -80,7 +80,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
         // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
         // it. GenMC determines this based on the annotation we pass with the load further up in
         // this function, namely when that load will read a value other than `MUTEX_LOCKED`.
-        GenMCDriver::handleAssume(inc_pos(thread_id), AssumeType::Spinloop);
+        // NOTE: The blocking happens on the Miri side.
     }
     return MutexLockResultExt::ok(is_lock_acquired);
 }

genmc-sys/src/lib.rs

@@ -316,6 +316,13 @@ mod ffi {
         UMin = 10,
     }
 
+    #[derive(Debug)]
+    enum AssumeType {
+        User = 0,
+        Barrier = 1,
+        Spinloop = 2,
+    }
+
     // # Safety
     //
     // This block is unsafe to allow defining safe methods inside.
@@ -334,6 +341,7 @@ mod ffi {
         (This tells cxx that the enums defined above are already defined on the C++ side;
         it will emit assertions to ensure that the two definitions agree.) ****/
         type ActionKind;
+        type AssumeType;
         type MemOrdering;
         type RMWBinOp;
         type SchedulePolicy;
@@ -441,7 +449,11 @@ mod ffi {
         /// Inform GenMC that the thread should be blocked.
         /// Note: this function is currently hardcoded for `AssumeType::User`, corresponding to user supplied assume statements.
         /// This can become a parameter once more types of assumes are added.
-        fn handle_assume_block(self: Pin<&mut MiriGenmcShim>, thread_id: i32);
+        fn handle_assume_block(
+            self: Pin<&mut MiriGenmcShim>,
+            thread_id: i32,
+            assume_type: AssumeType,
+        );
 
         /**** Mutex handling ****/
         fn handle_mutex_lock(

src/concurrency/genmc/intercept.rs

@@ -1,10 +1,29 @@
+use genmc_sys::AssumeType;
 use rustc_middle::ty;
 use tracing::debug;
 
 use crate::concurrency::genmc::MAX_ACCESS_SIZE;
 use crate::concurrency::thread::EvalContextExt as _;
 use crate::*;
 
+impl GenmcCtx {
+    /// Handle a user thread getting blocked.
+    /// This may happen due to an manual `assume` statement added by a user
+    /// or added by some automated program transformation, e.g., for spinloops.
+    fn handle_assume_block<'tcx>(
+        &self,
+        machine: &MiriMachine<'tcx>,
+        assume_type: AssumeType,
+    ) -> InterpResult<'tcx> {
+        debug!("GenMC: assume statement, blocking active thread.");
+        self.handle
+            .borrow_mut()
+            .pin_mut()
+            .handle_assume_block(self.active_thread_genmc_tid(machine), assume_type);
+        interp_ok(())
+    }
+}
+
 // Handling of code intercepted by Miri in GenMC mode, such as assume statement or `std::sync::Mutex`.
 
 impl<'tcx> EvalContextExtPriv<'tcx> for crate::MiriInterpCx<'tcx> {}
@@ -23,6 +42,36 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
         panic!("{} is a diagnostic item expected to have {} arguments", instance, N);
     }
 
+    /**** Blocking functionality ****/
+
+    /// Handle a thread getting blocked by a user assume (not an automatically generated assume).
+    /// Unblocking this thread in the current execution will cause a panic.
+    /// Miri does not provide GenMC with the annotations to determine when to unblock the thread, so it should never be unblocked.
+    fn handle_user_assume_block(&mut self) -> InterpResult<'tcx> {
+        let this = self.eval_context_mut();
+        debug!(
+            "GenMC: block thread {:?} due to failing assume statement.",
+            this.machine.threads.active_thread()
+        );
+        assert!(this.machine.threads.active_thread_ref().is_enabled());
+        // Block the thread on the GenMC side.
+        let genmc_ctx = this.machine.data_race.as_genmc_ref().unwrap();
+        genmc_ctx.handle_assume_block(&this.machine, AssumeType::User)?;
+        // Block the thread on the Miri side.
+        this.block_thread(
+            BlockReason::Genmc,
+            None,
+            callback!(
+                @capture<'tcx> {}
+                |_this, unblock: UnblockKind| {
+                    assert_eq!(unblock, UnblockKind::Ready);
+                    unreachable!("GenMC should never unblock a thread blocked by an `assume`.");
+                }
+            ),
+        );
+        interp_ok(())
+    }
+
     fn intercept_mutex_lock(&mut self, mutex: MPlaceTy<'tcx>) -> InterpResult<'tcx> {
         debug!("GenMC: handling Mutex::lock()");
         let this = self.eval_context_mut();
@@ -47,13 +96,15 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
             result.is_reset, result.is_lock_acquired
         );
         if result.is_lock_acquired {
+            // NOTE: We don't write anything back to Miri's memory, the Mutex state is handled only by GenMC.
             return interp_ok(());
         }
-        // If we did not acquire the mutex and GenMC did not tell us to reset and try again, we have a deadlock.
+        // We either did not acquire the mutex, or GenMC informed us to reset and try the lock again later, so we block the current thread.
         if !result.is_reset {
-            throw_machine_stop!(TerminationInfo::Deadlock);
+            // GenMC expects us to block the thread if we did get a `reset`.
+            genmc_ctx.handle_assume_block(&this.machine, AssumeType::Spinloop)?;
         }
-        // NOTE: We don't write anything back to Miri's memory, the Mutex state is handled only by GenMC.
+        // Block the thread on the Miri side.
         this.block_thread(
                 crate::BlockReason::Genmc,
                 None,
@@ -78,9 +129,11 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
                             throw_ub_format!("{}", error.to_string_lossy());
                         }
                         assert!(!result.is_reset, "We should not get a reset on the second lock attempt.");
-                        // If we did not acquire the mutex and GenMC did not tell us to reset and try again, we have a deadlock.
+                        // If we did not acquire the mutex and GenMC did not tell us to reset and try again, we block this thread for the remainder of the current execution.
                         if !result.is_lock_acquired {
-                            throw_machine_stop!(TerminationInfo::Deadlock);
+                            debug!("GenMC: Mutex::lock failed to acquire the Mutex twice, permanently blocking thread.");
+                            // This is equivalent to a user inserted `assume(false)`.
+                            this.handle_user_assume_block()?;
                         }
                         interp_ok(())
                     }
@@ -116,7 +169,7 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
             "GenMC: Mutex::try_lock(): is_reset: {}, is_lock_acquired: {}",
             result.is_reset, result.is_lock_acquired
         );
-        assert!(!result.is_reset);
+        assert!(!result.is_reset, "GenMC returned 'reset' for a mutex lock multiple times.");
         // Write the return value of try_lock, i.e., whether we acquired the mutex.
         this.write_scalar(Scalar::from_bool(result.is_lock_acquired), dest)?;
         // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC.
@@ -187,19 +240,6 @@ pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
         if condition_bool {
             return interp_ok(());
         }
-        let genmc_ctx = this.machine.data_race.as_genmc_ref().unwrap();
-        genmc_ctx.handle_assume_block(&this.machine)?;
-        this.block_thread(
-            BlockReason::Genmc,
-            None,
-            callback!(
-                @capture<'tcx> {}
-                |_this, unblock: UnblockKind| {
-                    assert_eq!(unblock, UnblockKind::Ready);
-                    unreachable!("GenMC should never unblock a thread blocked by an `assume`.");
-                }
-            ),
-        );
-        interp_ok(())
+        this.handle_user_assume_block()
     }
 }

src/concurrency/genmc/mod.rs

@@ -870,20 +870,6 @@ impl GenmcCtx {
         };
         interp_ok((old_value_scalar, new_value_scalar))
     }
-
-    /**** Blocking functionality ****/
-
-    /// Handle a user thread getting blocked.
-    /// This may happen due to an manual `assume` statement added by a user
-    /// or added by some automated program transformation, e.g., for spinloops.
-    fn handle_assume_block<'tcx>(&self, machine: &MiriMachine<'tcx>) -> InterpResult<'tcx> {
-        debug!("GenMC: assume statement, blocking active thread.");
-        self.handle
-            .borrow_mut()
-            .pin_mut()
-            .handle_assume_block(self.active_thread_genmc_tid(machine));
-        interp_ok(())
-    }
 }
 
 impl VisitProvenance for GenmcCtx {

src/concurrency/thread.rs

@@ -708,21 +708,31 @@ trait EvalContextPrivExt<'tcx>: MiriInterpCxExt<'tcx> {
         let this = self.eval_context_mut();
 
         // In GenMC mode, we let GenMC do the scheduling.
-        if let Some(genmc_ctx) = this.machine.data_race.as_genmc_ref() {
-            let Some(next_thread_id) = genmc_ctx.schedule_thread(this)? else {
-                return interp_ok(SchedulingAction::ExecuteStep);
-            };
-            // If a thread is blocked on GenMC, we have to implicitly unblock it when it gets scheduled again.
-            if this.machine.threads.threads[next_thread_id].state.is_blocked_on(BlockReason::Genmc)
-            {
-                info!("GenMC: scheduling blocked thread {next_thread_id:?}, so we unblock it now.");
-                this.unblock_thread(next_thread_id, BlockReason::Genmc)?;
+        if this.machine.data_race.as_genmc_ref().is_some() {
+            loop {
+                let genmc_ctx = this.machine.data_race.as_genmc_ref().unwrap();
+                let Some(next_thread_id) = genmc_ctx.schedule_thread(this)? else {
+                    return interp_ok(SchedulingAction::ExecuteStep);
+                };
+                // If a thread is blocked on GenMC, we have to implicitly unblock it when it gets scheduled again.
+                if this.machine.threads.threads[next_thread_id]
+                    .state
+                    .is_blocked_on(BlockReason::Genmc)
+                {
+                    info!(
+                        "GenMC: scheduling blocked thread {next_thread_id:?}, so we unblock it now."
+                    );
+                    this.unblock_thread(next_thread_id, BlockReason::Genmc)?;
+                }
+                // Set the new active thread.
+                let thread_manager = &mut this.machine.threads;
+                thread_manager.active_thread = next_thread_id;
+                // A thread blocked by GenMC may get blocked again during the unblocking callback.
+                // In that case, we need to ask for a different thread to run next.
+                if thread_manager.threads[thread_manager.active_thread].state.is_enabled() {
+                    return interp_ok(SchedulingAction::ExecuteStep);
+                }
             }
-            // Set the new active thread.
-            let thread_manager = &mut this.machine.threads;
-            thread_manager.active_thread = next_thread_id;
-            assert!(thread_manager.threads[thread_manager.active_thread].state.is_enabled());
-            return interp_ok(SchedulingAction::ExecuteStep);
         }
 
         // We are not in GenMC mode, so we control the scheduling.