Clean up Mutex lock (un)blocking code.

Author: Patrick-6

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`.
-        // NOTE: The blocking happens on the Miri side.
+        GenMCDriver::handleAssume(inc_pos(thread_id), AssumeType::Spinloop);
     }
     return MutexLockResultExt::ok(is_lock_acquired);
 }

src/concurrency/genmc/intercept.rs

@@ -91,54 +91,43 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
             // FIXME(genmc): improve error handling.
             throw_ub_format!("{}", error.to_string_lossy());
         }
-        debug!(
-            "GenMC: Mutex::lock(): is_reset: {}, is_lock_acquired: {}",
-            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(());
-        }
-        // 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 {
-            // GenMC expects us to block the thread if we did get a `reset`.
-            genmc_ctx.handle_assume_block(&this.machine, AssumeType::Spinloop)?;
-        }
-        // Block the thread on the Miri side.
-        this.block_thread(
+        if result.is_reset {
+            debug!("GenMC: Mutex::lock: Reset");
+            // GenMC informed us to reset and try the lock again later.
+            // We block the current thread until GenMC schedules it again.
+            this.block_thread(
                 crate::BlockReason::Genmc,
                 None,
                 crate::callback!(
                     @capture<'tcx> {
                         mutex: MPlaceTy<'tcx>,
                     }
                     |this, unblock: crate::UnblockKind| {
-                        debug!("GenMC: handling Mutex::lock: unblocking callback called.");
+                        debug!("GenMC: Mutex::lock: unblocking callback called, attempting to lock the Mutex again.");
                         assert_eq!(unblock, crate::UnblockKind::Ready);
-                        let genmc_ctx = this.machine.data_race.as_genmc_ref().unwrap();
-                        let result = genmc_ctx.handle
-                            .borrow_mut()
-                            .pin_mut()
-                            .handle_mutex_lock(
-                                genmc_ctx.active_thread_genmc_tid(&this.machine),
-                                mutex.ptr().addr().bytes(),
-                                mutex.layout.size.bytes(),
-                            );
-                        if let Some(error) = result.error.as_ref() {
-                            // FIXME(genmc): improve error handling.
-                            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 block this thread for the remainder of the current execution.
-                        if !result.is_lock_acquired {
-                            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()?;
-                        }
+                        this.intercept_mutex_lock(mutex)?;
                         interp_ok(())
                     }
                 ),
             );
+        } else if result.is_lock_acquired {
+            debug!("GenMC: Mutex::lock successfully acquired the Mutex.");
+        } else {
+            debug!("GenMC: Mutex::lock failed to acquire the Mutex, permanently blocking thread.");
+            // NOTE: `handle_mutex_lock` already blocked the current thread on the GenMC side.
+            this.block_thread(
+                crate::BlockReason::Genmc,
+                None,
+                crate::callback!(
+                    @capture<'tcx> {
+                        mutex: MPlaceTy<'tcx>,
+                    }
+                    |this, _unblock: crate::UnblockKind| {
+                        unreachable!("A thread blocked on `Mutex::lock` should not be unblocked again.");
+                    }
+                ),
+            );
+        }
         // NOTE: We don't write anything back to Miri's memory where the Mutex is located, that state is handled only by GenMC.
         interp_ok(())
     }