Add distinction between 'reset' and 'lock not acquired' for mutex lock. Improve comments. Add mutex deadlock test using std threads.

Patrick-6 · Patrick-6 · commit 46dcb562678f · 2025-10-06T09:17:37.000+02:00
diff --git a/genmc-sys/cpp/include/MiriInterface.hpp b/genmc-sys/cpp/include/MiriInterface.hpp
@@ -366,11 +366,18 @@ inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
 
 namespace MutexLockResultExt {
 inline MutexLockResult ok(bool is_lock_acquired) {
-    return MutexLockResult { /* error: */ nullptr, is_lock_acquired };
+    return MutexLockResult { /* error: */ nullptr, /* is_reset: */ false, is_lock_acquired };
+}
+
+inline MutexLockResult reset() {
+    return MutexLockResult { /* error: */ nullptr,
+                             /* is_reset: */ true,
+                             /* is_lock_acquired: */ false };
 }
 
 inline MutexLockResult from_error(std::unique_ptr<std::string> error) {
     return MutexLockResult { /* error: */ std::move(error),
+                             /* is_reset: */ false,
                              /* is_lock_acquired: */ false };
 }
 } // namespace MutexLockResultExt
diff --git a/genmc-sys/cpp/src/MiriInterface/Mutex.cpp b/genmc-sys/cpp/src/MiriInterface/Mutex.cpp
@@ -48,7 +48,7 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
     // ("Mutex already locked"), Miri should call the handle function again once the current thread
     // is scheduled by GenMC the next time.
     if (std::holds_alternative<Reset>(load_ret))
-        return MutexLockResultExt::ok(false);
+        return MutexLockResultExt::reset();
 
     const auto* ret_val = std::get_if<SVal>(&load_ret);
     ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result.");
@@ -77,7 +77,8 @@ auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint
         );
     } else {
         // We did not acquire the mutex, so we tell GenMC to block the thread until we can acquire
-        // it.
+        // 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);
     }
     return MutexLockResultExt::ok(is_lock_acquired);
diff --git a/genmc-sys/src/lib.rs b/genmc-sys/src/lib.rs
@@ -259,6 +259,8 @@ mod ffi {
     struct MutexLockResult {
         /// If there was an error, it will be stored in `error`, otherwise it is `None`.
         error: UniquePtr<CxxString>,
+        /// If true, GenMC determined that we should retry the mutex lock operation once the thread attempting to lock is scheduled again.
+        is_reset: bool,
         /// Indicate whether the lock was acquired by this thread.
         is_lock_acquired: bool,
     }
diff --git a/src/concurrency/genmc/intercept.rs b/src/concurrency/genmc/intercept.rs
@@ -1,4 +1,4 @@
-use rustc_middle::{throw_unsup_format, ty};
+use rustc_middle::ty;
 use tracing::debug;
 
 use crate::concurrency::genmc::MAX_ACCESS_SIZE;
@@ -42,13 +42,18 @@ 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 {
-            debug!("GenMC: handling Mutex::lock: success: lock acquired.");
             return interp_ok(());
         }
-        debug!("GenMC: handling Mutex::lock failed, blocking thread");
+        // If we did not acquire the mutex and GenMC did not tell us to reset and try again, we have a deadlock.
+        if !result.is_reset {
+            throw_machine_stop!(TerminationInfo::Deadlock);
+        }
         // NOTE: We don't write anything back to Miri's memory, the Mutex state is handled only by GenMC.
-
         this.block_thread(
                 crate::BlockReason::Genmc,
                 None,
@@ -72,10 +77,10 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
                             // FIXME(genmc): improve error handling.
                             throw_ub_format!("{}", error.to_string_lossy());
                         }
-                        // FIXME(genmc): The reported error message is bad, it does not point to the second lock call involved in the deadlock.
-                        // FIXME(genmc): there can be cases where not acquiring a mutex after the second attempt is *not* a deadlock. Reliably detecting deadlocks requires extra analysis (in GenMC).
+                        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 !result.is_lock_acquired {
-                            throw_unsup_format!("Could not lock Mutex, which may indicate a deadlock. (GenMC mode does not fully support deadlock detection yet).")
+                            throw_machine_stop!(TerminationInfo::Deadlock);
                         }
                         interp_ok(())
                     }
@@ -107,7 +112,11 @@ trait EvalContextExtPriv<'tcx>: crate::MiriInterpCxExt<'tcx> {
             // FIXME(genmc): improve error handling.
             throw_ub_format!("{}", error.to_string_lossy());
         }
-        debug!("GenMC: Mutex::try_lock(): is_lock_acquired: {}", result.is_lock_acquired);
+        debug!(
+            "GenMC: Mutex::try_lock(): is_reset: {}, is_lock_acquired: {}",
+            result.is_reset, result.is_lock_acquired
+        );
+        assert!(!result.is_reset);
         // 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.
diff --git a/tests/genmc/fail/intercept/mutex_deadlock.rs b/tests/genmc/fail/intercept/mutex_deadlock.rs
@@ -1,5 +1,7 @@
 //@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
-//@error-in-other-file: unsupported operation
+//@error-in-other-file: the evaluated program deadlocked
+//@error-in-other-file: the evaluated program deadlocked
+//@error-in-other-file: the evaluated program deadlocked
 
 // Test that we can detect a deadlock involving `std::sync::Mutex` in GenMC mode.
 // FIXME(genmc): The error message for such deadlocks is currently not good, it does not show both involved lock call locations.
diff --git a/tests/genmc/fail/intercept/mutex_deadlock.stderr b/tests/genmc/fail/intercept/mutex_deadlock.stderr
@@ -1,11 +1,64 @@
 Running GenMC Verification...
-error: unsupported operation: Could not lock Mutex, which may indicate a deadlock. (GenMC mode does not fully support deadlock detection yet).
+error: the evaluated program deadlocked
   --> RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
    |
 LL |             self.inner.lock();
-   |                             ^ unsupported operation occurred here
+   |             ^^^^^^^^^^^^^^^^^ this thread got stuck here
+   |
+   = note: BACKTRACE on thread `unnamed-ID`:
+   = note: inside `std::sync::Mutex::<u64>::lock` at RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
+note: inside closure
+  --> tests/genmc/fail/intercept/mutex_deadlock.rs:LL:CC
+   |
+LL |             let mut y = Y.lock().unwrap();
+   |                         ^^^^^^^^
+   = note: inside `<std::boxed::Box<{closure@tests/genmc/fail/intercept/mutex_deadlock.rs:LL:CC}> as std::ops::FnOnce<()>>::call_once` at RUSTLIB/alloc/src/boxed.rs:LL:CC
+note: inside `genmc::spawn_pthread_closure::thread_func::<{closure@tests/genmc/fail/intercept/mutex_deadlock.rs:LL:CC}>`
+  --> tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC
+   |
+LL |         f();
+   |         ^^^
+
+error: the evaluated program deadlocked
+  --> tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC
+   |
+LL |     if unsafe { libc::pthread_join(thread_id, std::ptr::null_mut()) } != 0 {
+   |                                                                   ^ this thread got stuck here
+   |
+   = note: BACKTRACE:
+   = note: inside `genmc::join_pthread` at tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC
+note: inside closure
+  --> tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC
+   |
+LL |     let _ = thread_ids.map(|id| join_pthread(id));
+   |                                 ^^^^^^^^^^^^^^^^
+   = note: inside closure at RUSTLIB/core/src/ops/try_trait.rs:LL:CC
+   = note: inside `<std::iter::Map<std::array::drain::Drain<'_, u64>, {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_1<u64, {closure@tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC}>::{closure#0}}> as std::iter::traits::unchecked_iterator::UncheckedIterator>::next_unchecked` at RUSTLIB/core/src/iter/adapters/map.rs:LL:CC
+   = note: inside closure at RUSTLIB/core/src/array/mod.rs:LL:CC
+   = note: inside `std::array::try_from_fn_erased::<(), std::ops::try_trait::NeverShortCircuit<()>, {closure@std::array::try_from_trusted_iterator::next<std::ops::try_trait::NeverShortCircuit<()>, std::iter::Map<std::array::drain::Drain<'_, u64>, {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_1<u64, {closure@tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC}>::{closure#0}}>>::{closure#0}}>` at RUSTLIB/core/src/array/mod.rs:LL:CC
+   = note: inside `std::array::try_from_fn::<std::ops::try_trait::NeverShortCircuit<()>, 2, {closure@std::array::try_from_trusted_iterator::next<std::ops::try_trait::NeverShortCircuit<()>, std::iter::Map<std::array::drain::Drain<'_, u64>, {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_1<u64, {closure@tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC}>::{closure#0}}>>::{closure#0}}>` at RUSTLIB/core/src/array/mod.rs:LL:CC
+   = note: inside `std::array::try_from_trusted_iterator::<(), std::ops::try_trait::NeverShortCircuit<()>, 2, std::iter::Map<std::array::drain::Drain<'_, u64>, {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_1<u64, {closure@tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC}>::{closure#0}}>>` at RUSTLIB/core/src/array/mod.rs:LL:CC
+   = note: inside closure at RUSTLIB/core/src/array/mod.rs:LL:CC
+   = note: inside `std::array::drain::drain_array_with::<u64, std::ops::try_trait::NeverShortCircuit<[(); 2]>, 2, {closure@std::array::<impl [u64; 2]>::try_map<std::ops::try_trait::NeverShortCircuit<()>, {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_1<u64, {closure@tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC}>::{closure#0}}>::{closure#0}}>` at RUSTLIB/core/src/array/drain.rs:LL:CC
+   = note: inside `std::array::<impl [u64; 2]>::try_map::<std::ops::try_trait::NeverShortCircuit<()>, {closure@std::ops::try_trait::NeverShortCircuit<()>::wrap_mut_1<u64, {closure@tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC}>::{closure#0}}>` at RUSTLIB/core/src/array/mod.rs:LL:CC
+   = note: inside `std::array::<impl [u64; 2]>::map::<{closure@tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC}, ()>` at RUSTLIB/core/src/array/mod.rs:LL:CC
+note: inside `genmc::join_pthreads::<TAG>`
+  --> tests/genmc/fail/intercept/../../../utils/genmc.rs:LL:CC
+   |
+LL |     let _ = thread_ids.map(|id| join_pthread(id));
+   |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
+note: inside `miri_start`
+  --> tests/genmc/fail/intercept/mutex_deadlock.rs:LL:CC
+   |
+LL |         join_pthreads([t0, t1]);
+   |         ^^^^^^^^^^^^^^^^^^^^^^^
+
+error: the evaluated program deadlocked
+  --> RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
+   |
+LL |             self.inner.lock();
+   |                             ^ this thread got stuck here
    |
-   = help: this is likely not a bug in the program; it indicates that the program performed an operation that Miri does not support
    = note: BACKTRACE on thread `unnamed-ID`:
    = note: inside `std::sync::Mutex::<u64>::lock` at RUSTLIB/std/src/sync/poison/mutex.rs:LL:CC
 note: inside closure
@@ -22,5 +75,5 @@ LL |         f();
 
 note: add `-Zmiri-genmc-print-genmc-output` to MIRIFLAGS to see the detailed GenMC error report
 
-error: aborting due to 1 previous error
+error: aborting due to 3 previous errors
 
diff --git a/tests/genmc/fail/intercept/mutex_deadlock_std.rs b/tests/genmc/fail/intercept/mutex_deadlock_std.rs
@@ -0,0 +1,29 @@
+//@compile-flags: -Zmiri-genmc -Zmiri-disable-stacked-borrows
+//@error-in-other-file: the evaluated program deadlocked
+//@error-in-other-file: the evaluated program deadlocked
+//@error-in-other-file: the evaluated program deadlocked
+
+// Test that we can detect a deadlock involving `std::sync::Mutex` in GenMC mode.
+// FIXME(genmc): The error message for such deadlocks is currently not good, it does not show both involved lock call locations.
+
+use std::sync::Mutex;
+
+static X: Mutex<u64> = Mutex::new(0);
+static Y: Mutex<u64> = Mutex::new(0);
+
+fn main() {
+    let t0 = std::thread::spawn(|| {
+        let mut x = X.lock().unwrap();
+        let mut y = Y.lock().unwrap();
+        *x += 1;
+        *y += 1;
+    });
+    let t1 = std::thread::spawn(|| {
+        let mut y = Y.lock().unwrap();
+        let mut x = X.lock().unwrap();
+        *x += 1;
+        *y += 1;
+    });
+    t0.join().unwrap();
+    t1.join().unwrap();
+}
diff --git a/tests/genmc/fail/intercept/mutex_deadlock_std.stderr b/tests/genmc/fail/intercept/mutex_deadlock_std.stderr

Original file line number	Diff line number	Diff line change
`@@ -259,6 +259,8 @@ mod ffi {`
`259`	`259`	`struct MutexLockResult {`
`260`	`260`	/// If there was an error, it will be stored in `error`, otherwise it is `None`.
`261`	`261`	`error: UniquePtr<CxxString>,`
	`262`	`+ /// If true, GenMC determined that we should retry the mutex lock operation once the thread attempting to lock is scheduled again.`
	`263`	`+ is_reset: bool,`
`262`	`264`	`/// Indicate whether the lock was acquired by this thread.`
`263`	`265`	`is_lock_acquired: bool,`
`264`	`266`	`}`