Implement std::sync::Mutex interception for GenMC mode.

genmc-sys/build.rs

@@ -233,6 +233,7 @@ fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
     let cpp_files = [
         "MiriInterface/EventHandling.cpp",
         "MiriInterface/Exploration.cpp",
+        "MiriInterface/Mutex.cpp",
         "MiriInterface/Setup.cpp",
         "MiriInterface/ThreadManagement.cpp",
     ]

genmc-sys/cpp/include/MiriInterface.hpp

@@ -12,7 +12,6 @@
 
 // GenMC headers:
 #include "ExecutionGraph/EventLabel.hpp"
-#include "Static/ModuleID.hpp"
 #include "Support/MemOrdering.hpp"
 #include "Support/RMWOps.hpp"
 #include "Verification/Config.hpp"
@@ -36,6 +35,7 @@ struct LoadResult;
 struct StoreResult;
 struct ReadModifyWriteResult;
 struct CompareExchangeResult;
+struct MutexLockResult;
 
 // GenMC uses `int` for its thread IDs.
 using ThreadId = int;
@@ -136,10 +136,13 @@ 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;
+    auto handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size)
+        -> MutexLockResult;
+    auto handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size) -> StoreResult;
 
     /***** Exploration related functionality *****/
 
@@ -358,4 +361,22 @@ inline CompareExchangeResult from_error(std::unique_ptr<std::string> error) {
 }
 } // namespace CompareExchangeResultExt
 
+namespace MutexLockResultExt {
+inline MutexLockResult ok(bool 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
+
 #endif /* GENMC_MIRI_INTERFACE_HPP */

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

@@ -32,8 +32,9 @@
 
 /**** Blocking instructions ****/
 
-void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
-    GenMCDriver::handleAssume(inc_pos(thread_id), AssumeType::User);
+void MiriGenmcShim::handle_assume_block(ThreadId thread_id, AssumeType assume_type) {
+    BUG_ON(getExec().getGraph().isThreadBlocked(thread_id));
+    GenMCDriver::handleAssume(inc_pos(thread_id), assume_type);
 }
 
 /**** Memory access handling ****/
@@ -59,6 +60,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
     if (const auto* err = std::get_if<VerificationError>(&ret))
         return LoadResultExt::from_error(format_error(*err));
     const auto* ret_val = std::get_if<SVal>(&ret);
+    // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
     if (ret_val == nullptr)
         ERROR("Unimplemented: load returned unexpected result.");
     return LoadResultExt::from_value(*ret_val);
@@ -88,6 +90,7 @@ void MiriGenmcShim::handle_assume_block(ThreadId thread_id) {
         return StoreResultExt::from_error(format_error(*err));
 
     const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
+    // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
     ERROR_ON(
         nullptr == is_coherence_order_maximal_write,
         "Unimplemented: Store returned unexpected result."
@@ -130,6 +133,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
         return ReadModifyWriteResultExt::from_error(format_error(*err));
 
     const auto* ret_val = std::get_if<SVal>(&load_ret);
+    // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
     if (nullptr == ret_val) {
         ERROR("Unimplemented: read-modify-write returned unexpected result.");
     }
@@ -151,6 +155,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
         return ReadModifyWriteResultExt::from_error(format_error(*err));
 
     const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
+    // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
     ERROR_ON(
         nullptr == is_coherence_order_maximal_write,
         "Unimplemented: RMW store returned unexpected result."
@@ -195,6 +200,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
     if (const auto* err = std::get_if<VerificationError>(&load_ret))
         return CompareExchangeResultExt::from_error(format_error(*err));
     const auto* ret_val = std::get_if<SVal>(&load_ret);
+    // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
     ERROR_ON(nullptr == ret_val, "Unimplemented: load returned unexpected result.");
     const auto read_old_val = *ret_val;
     if (read_old_val != expectedVal)
@@ -215,6 +221,7 @@ void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
     if (const auto* err = std::get_if<VerificationError>(&store_ret))
         return CompareExchangeResultExt::from_error(format_error(*err));
     const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
+    // FIXME(genmc): handle `HandleResult::{Invalid, Reset}` return values.
     ERROR_ON(
         nullptr == is_coherence_order_maximal_write,
         "Unimplemented: compare-exchange store returned unexpected result."

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

@@ -0,0 +1,159 @@
+/** This file contains functionality related to handling mutexes.  */
+
+#include "MiriInterface.hpp"
+
+// GenMC headers:
+#include "Static/ModuleID.hpp"
+
+// CXX.rs generated headers:
+#include "genmc-sys/src/lib.rs.h"
+
+#define MUTEX_UNLOCKED SVal(0)
+#define MUTEX_LOCKED SVal(1)
+
+auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size)
+    -> MutexLockResult {
+    // This annotation informs GenMC about the condition required to make this lock call succeed.
+    // It stands for `value_read_by_load != MUTEX_LOCKED`.
+    const auto size_bits = size * 8;
+    const auto annot = std::move(Annotation(
+        AssumeType::Spinloop,
+        Annotation::ExprVP(
+            NeExpr<ModuleID::ID>::create(
+                // `RegisterExpr` marks the value of the current expression, i.e., the loaded value.
+                // The `id` is ignored by GenMC; it is only used by the LLI frontend to substitute
+                // other variables from previous expressions that may be used here.
+                RegisterExpr<ModuleID::ID>::create(size_bits, /* id */ 0),
+                ConcreteExpr<ModuleID::ID>::create(size_bits, MUTEX_LOCKED)
+            )
+                .release()
+        )
+    ));
+
+    // As usual, we need to tell GenMC which value was stored at this location before this atomic
+    // access, if there previously was a non-atomic initializing access. We set the initial state of
+    // a mutex to be "unlocked".
+    const auto old_val = MUTEX_UNLOCKED;
+    const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::LockCasRead>(
+        thread_id,
+        old_val,
+        address,
+        size,
+        annot,
+        EventDeps()
+    );
+    if (const auto* err = std::get_if<VerificationError>(&load_ret))
+        return MutexLockResultExt::from_error(format_error(*err));
+    // If we get a `Reset`, GenMC decided that this lock operation should not yet run, since it
+    // would not acquire the mutex. Like the handling of the case further down where we read a `1`
+    // ("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::reset();
+
+    const auto* ret_val = std::get_if<SVal>(&load_ret);
+    ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result.");
+    ERROR_ON(
+        *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
+        "Mutex read value was neither 0 nor 1"
+    );
+    const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
+    if (is_lock_acquired) {
+        const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::LockCasWrite>(
+            inc_pos(thread_id),
+            old_val,
+            address,
+            size,
+            EventDeps()
+        );
+        if (const auto* err = std::get_if<VerificationError>(&store_ret))
+            return MutexLockResultExt::from_error(format_error(*err));
+        // We don't update Miri's memory for this operation so we don't need to know if the store
+        // was the co-maximal store, but we still check that we at least get a boolean as the result
+        // of the store.
+        const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
+        ERROR_ON(
+            nullptr == is_coherence_order_maximal_write,
+            "Unimplemented: store part of mutex try_lock returned unexpected result."
+        );
+    } else {
+        // 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`.
+        this->handle_assume_block(thread_id, AssumeType::Spinloop);
+    }
+    return MutexLockResultExt::ok(is_lock_acquired);
+}
+
+auto MiriGenmcShim::handle_mutex_try_lock(ThreadId thread_id, uint64_t address, uint64_t size)
+    -> MutexLockResult {
+    auto& currPos = threads_action_[thread_id].event;
+    // As usual, we need to tell GenMC which value was stored at this location before this atomic
+    // access, if there previously was a non-atomic initializing access. We set the initial state of
+    // a mutex to be "unlocked".
+    const auto old_val = MUTEX_UNLOCKED;
+    const auto load_ret = GenMCDriver::handleLoad<EventLabel::EventLabelKind::TrylockCasRead>(
+        ++currPos,
+        old_val,
+        SAddr(address),
+        ASize(size)
+    );
+    if (const auto* err = std::get_if<VerificationError>(&load_ret))
+        return MutexLockResultExt::from_error(format_error(*err));
+    const auto* ret_val = std::get_if<SVal>(&load_ret);
+    if (nullptr == ret_val) {
+        ERROR("Unimplemented: mutex trylock load returned unexpected result.");
+    }
+
+    ERROR_ON(
+        *ret_val != MUTEX_UNLOCKED && *ret_val != MUTEX_LOCKED,
+        "Mutex read value was neither 0 nor 1"
+    );
+    const bool is_lock_acquired = *ret_val == MUTEX_UNLOCKED;
+    if (!is_lock_acquired) {
+        return MutexLockResultExt::ok(false); /* Lock already held. */
+    }
+
+    const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::TrylockCasWrite>(
+        ++currPos,
+        old_val,
+        SAddr(address),
+        ASize(size)
+    );
+    if (const auto* err = std::get_if<VerificationError>(&store_ret))
+        return MutexLockResultExt::from_error(format_error(*err));
+    // We don't update Miri's memory for this operation so we don't need to know if the store was
+    // co-maximal, but we still check that we get a boolean result.
+    const bool* is_coherence_order_maximal_write = std::get_if<bool>(&store_ret);
+    ERROR_ON(
+        nullptr == is_coherence_order_maximal_write,
+        "Unimplemented: store part of mutex try_lock returned unexpected result."
+    );
+    return MutexLockResultExt::ok(true);
+}
+
+auto MiriGenmcShim::handle_mutex_unlock(ThreadId thread_id, uint64_t address, uint64_t size)
+    -> StoreResult {
+    const auto pos = inc_pos(thread_id);
+    const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::UnlockWrite>(
+        pos,
+        // As usual, we need to tell GenMC which value was stored at this location before this
+        // atomic access, if there previously was a non-atomic initializing access. We set the
+        // initial state of a mutex to be "unlocked".
+        /* old_val */ MUTEX_UNLOCKED,
+        MemOrdering::Release,
+        SAddr(address),
+        ASize(size),
+        AType::Signed,
+        /* store_value */ MUTEX_UNLOCKED,
+        EventDeps()
+    );
+    if (const auto* err = std::get_if<VerificationError>(&ret))
+        return StoreResultExt::from_error(format_error(*err));
+    const bool* is_coherence_order_maximal_write = std::get_if<bool>(&ret);
+    ERROR_ON(
+        nullptr == is_coherence_order_maximal_write,
+        "Unimplemented: store part of mutex unlock returned unexpected result."
+    );
+    return StoreResultExt::ok(*is_coherence_order_maximal_write);
+}

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

@@ -38,6 +38,7 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
     if (!std::holds_alternative<SVal>(ret)) {
         dec_pos(thread_id);
     }
+    // FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values.
 
     // NOTE: Thread return value is ignored, since Miri doesn't need it.
 }

genmc-sys/src/lib.rs

@@ -254,6 +254,17 @@ mod ffi {
         is_coherence_order_maximal_write: bool,
     }
 
+    #[must_use]
+    #[derive(Debug)]
+    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,
+    }
+
     /**** These are GenMC types that we have to copy-paste here since cxx does not support
     "importing" externally defined C++ types. ****/
 
@@ -305,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.
@@ -323,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;
@@ -430,7 +449,31 @@ 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(
+            self: Pin<&mut MiriGenmcShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+        ) -> MutexLockResult;
+        fn handle_mutex_try_lock(
+            self: Pin<&mut MiriGenmcShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+        ) -> MutexLockResult;
+        fn handle_mutex_unlock(
+            self: Pin<&mut MiriGenmcShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+        ) -> StoreResult;
 
         /***** Exploration related functionality *****/
 

src/concurrency/genmc/dummy.rs

@@ -43,6 +43,15 @@ mod intercept {
 
     impl<'tcx> EvalContextExt<'tcx> for crate::MiriInterpCx<'tcx> {}
     pub trait EvalContextExt<'tcx>: crate::MiriInterpCxExt<'tcx> {
+        fn genmc_intercept_function(
+            &mut self,
+            _instance: rustc_middle::ty::Instance<'tcx>,
+            _args: &[rustc_const_eval::interpret::FnArg<'tcx, crate::Provenance>],
+            _dest: &crate::PlaceTy<'tcx>,
+        ) -> InterpResult<'tcx, bool> {
+            unreachable!()
+        }
+
         fn handle_genmc_verifier_assume(&mut self, _condition: &OpTy<'tcx>) -> InterpResult<'tcx> {
             unreachable!();
         }