Implement std::sync::Mutex interception

Author: Patrick-6

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

@@ -36,10 +36,15 @@ struct LoadResult;
 struct StoreResult;
 struct ReadModifyWriteResult;
 struct CompareExchangeResult;
+struct MutexLockResult;
 
 // GenMC uses `int` for its thread IDs.
 using ThreadId = int;
 
+// Types used for GenMC annotations, e.g., in `handle_mutex_lock`.
+using AnnotID = ModuleID::ID;
+using AnnotT = SExpr<AnnotID>;
+
 /// Set the log level for GenMC.
 ///
 /// # Safety
@@ -141,6 +146,12 @@ struct MiriGenmcShim : private GenMCDriver {
     /// added.
     void handle_assume_block(ThreadId thread_id);
 
+    /**** 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 *****/
 
     /** Ask the GenMC scheduler for a new thread to schedule and return whether the execution is
@@ -234,6 +245,14 @@ struct MiriGenmcShim : private GenMCDriver {
      * indices, since GenMC expects us to do that.
      */
     std::vector<Action> threads_action_;
+
+    /**
+     * Map of already used annotation ids (e.g., for mutexes).
+     * FIXME(GenMC): Ensure that these are consistent with how GenMC expects them once Miri supports
+     * multithreading in GenMC mode.
+     */
+    std::unordered_map<uint64_t, ModuleID::ID> annotation_id {};
+    ModuleID::ID annotation_id_counter = 0;
 };
 
 /// Get the bit mask that GenMC expects for global memory allocations.
@@ -358,4 +377,15 @@ 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_lock_acquired };
+}
+
+inline MutexLockResult from_error(std::unique_ptr<std::string> error) {
+    return MutexLockResult { /* error: */ std::move(error),
+                             /* is_lock_acquired: */ false };
+}
+} // namespace MutexLockResultExt
+
 #endif /* GENMC_MIRI_INTERFACE_HPP */

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

@@ -0,0 +1,142 @@
+/** This file contains functionality related to handling mutexes.  */
+
+#include "MiriInterface.hpp"
+
+// CXX.rs generated headers:
+#include "genmc-sys/src/lib.rs.h"
+
+auto MiriGenmcShim::handle_mutex_lock(ThreadId thread_id, uint64_t address, uint64_t size)
+    -> MutexLockResult {
+    // FIXME(genmc,multithreading): ensure this annotation id is unique even if Miri runs GenMC mode
+    // multithreaded. We cannot use the address directly, since it is 64 bits, and `ID` is an
+    // `unsigned int`.
+    ModuleID::ID annot_id;
+    auto [it, inserted] = annotation_id.try_emplace(address, annotation_id_counter);
+    if (inserted) {
+        annot_id = annotation_id_counter++;
+    } else {
+        annot_id = it->second;
+    }
+    const auto annot = std::move(Annotation(
+        AssumeType::Spinloop,
+        Annotation::ExprVP(NeExpr<AnnotID>::create(
+                               RegisterExpr<AnnotID>::create(ASize(size).getBits(), annot_id),
+                               ConcreteExpr<AnnotID>::create(ASize(size).getBits(), SVal(1))
+        )
+                               .release())
+    ));
+
+    // Mutex starts out unlocked, so we always say the previous value is "unlocked".
+    const auto old_val = SVal(0);
+    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::ok(false);
+
+    const auto* ret_val = std::get_if<SVal>(&load_ret);
+    ERROR_ON(!ret_val, "Unimplemented: mutex lock returned unexpected result.");
+    ERROR_ON(*ret_val != SVal(0) && *ret_val != SVal(1), "Mutex read value was neither 0 nor 1");
+    const bool is_lock_acquired = *ret_val == SVal(0);
+    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.
+        GenMCDriver::handleAssume(inc_pos(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;
+    // Mutex starts out unlocked, so we always say the previous value is "unlocked".
+    const auto old_val = SVal(0);
+    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 != SVal(0) && *ret_val != SVal(1), "Mutex read value was neither 0 nor 1");
+    const bool is_lock_acquired = *ret_val == SVal(0);
+    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,
+        // Mutex starts out unlocked, so we always say the previous value is "unlocked".
+        /* old_val */ SVal(0),
+        MemOrdering::Release,
+        SAddr(address),
+        ASize(size),
+        AType::Signed,
+        SVal(0),
+        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/src/lib.rs

@@ -254,6 +254,15 @@ 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>,
+        /// 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. ****/
 
@@ -432,6 +441,26 @@ mod ffi {
         /// This can become a parameter once more types of assumes are added.
         fn handle_assume_block(self: Pin<&mut MiriGenmcShim>, thread_id: i32);
 
+        /**** 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 *****/
 
         /// Ask the GenMC scheduler for a new thread to schedule and

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 check_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!();
         }