Implement more features for GenMC mode

- Support for atomic fences.
- Support for atomic read-modify-write (RMW).
- Add tests using RMW and fences.
- Add options:
  - to disable weak memory effects in GenMC mode.
  - to print GenMC execution graphs.
  - to print GenMC output message.
- Fix GenMC full rebuild issue and run configure step when commit changes.
- Do cleanup.

Co-authored-by: Ralf Jung <post@ralfj.de>

5 files changed, 202 insertions, 20 deletions

diff --git a/src/tools/miri/genmc-sys/build.rs b/src/tools/miri/genmc-sys/build.rs
index 8eb818a6b26..8d437c20a09 100644
--- a/src/tools/miri/genmc-sys/build.rs
+++ b/src/tools/miri/genmc-sys/build.rs
@@ -30,13 +30,23 @@ mod downloading {
     /// The GenMC commit we depend on. It must be available on the specified GenMC repository.
     pub(crate) const GENMC_COMMIT: &str = "af9cc9ccd5d412b16defc35dbf36571c63a19c76";
 
-    pub(crate) fn download_genmc() -> PathBuf {
+    /// Ensure that a local GenMC repo is present and set to the correct commit.
+    /// Return the path of the GenMC repo and whether the checked out commit was changed.
+    pub(crate) fn download_genmc() -> (PathBuf, bool) {
         let Ok(genmc_download_path) = PathBuf::from_str(GENMC_DOWNLOAD_PATH);
         let commit_oid = Oid::from_str(GENMC_COMMIT).expect("Commit should be valid.");
 
         match Repository::open(&genmc_download_path) {
             Ok(repo) => {
                 assert_repo_unmodified(&repo);
+                if let Ok(head) = repo.head()
+                    && let Ok(head_commit) = head.peel_to_commit()
+                    && head_commit.id() == commit_oid
+                {
+                    // Fast path: The expected commit is already checked out.
+                    return (genmc_download_path, false);
+                }
+                // Check if the local repository already contains the commit we need, download it otherwise.
                 let commit = update_local_repo(&repo, commit_oid);
                 checkout_commit(&repo, &commit);
             }
@@ -51,7 +61,7 @@ mod downloading {
             }
         };
 
-        genmc_download_path
+        (genmc_download_path, true)
     }
 
     fn get_remote(repo: &Repository) -> Remote<'_> {
@@ -71,7 +81,8 @@ mod downloading {
 
         // Update remote URL.
         println!(
-            "cargo::warning=GenMC repository remote URL has changed from '{remote_url:?}' to '{GENMC_GITHUB_URL}'"
+            "cargo::warning=GenMC repository remote URL has changed from '{}' to '{GENMC_GITHUB_URL}'",
+            remote_url.unwrap_or_default()
         );
         repo.remote_set_url("origin", GENMC_GITHUB_URL)
             .expect("cannot rename url of remote 'origin'");
@@ -175,7 +186,7 @@ fn link_to_llvm(config_file: &Path) -> (String, String) {
 }
 
 /// Build the GenMC model checker library and the Rust-C++ interop library with cxx.rs
-fn compile_cpp_dependencies(genmc_path: &Path) {
+fn compile_cpp_dependencies(genmc_path: &Path, always_configure: bool) {
     // Give each step a separate build directory to prevent interference.
     let out_dir = PathBuf::from(std::env::var("OUT_DIR").as_deref().unwrap());
     let genmc_build_dir = out_dir.join("genmc");
@@ -184,15 +195,13 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
     // Part 1:
     // Compile the GenMC library using cmake.
 
-    let cmakelists_path = genmc_path.join("CMakeLists.txt");
-
     // FIXME(genmc,cargo): Switch to using `CARGO_CFG_DEBUG_ASSERTIONS` once https://github.com/rust-lang/cargo/issues/15760 is completed.
     // Enable/disable additional debug checks, prints and options for GenMC, based on the Rust profile (debug/release)
     let enable_genmc_debug = matches!(std::env::var("PROFILE").as_deref().unwrap(), "debug");
 
-    let mut config = cmake::Config::new(cmakelists_path);
+    let mut config = cmake::Config::new(genmc_path);
     config
-        .always_configure(false) // We don't need to reconfigure on subsequent compilation runs.
+        .always_configure(always_configure) // We force running the configure step when the GenMC commit changed.
         .out_dir(genmc_build_dir)
         .profile(GENMC_CMAKE_PROFILE)
         .define("GENMC_DEBUG", if enable_genmc_debug { "ON" } else { "OFF" });
@@ -251,7 +260,8 @@ fn compile_cpp_dependencies(genmc_path: &Path) {
 
 fn main() {
     // Select which path to use for the GenMC repo:
-    let genmc_path = if let Some(genmc_src_path) = option_env!("GENMC_SRC_PATH") {
+    let (genmc_path, always_configure) = if let Some(genmc_src_path) = option_env!("GENMC_SRC_PATH")
+    {
         let genmc_src_path =
             PathBuf::from_str(&genmc_src_path).expect("GENMC_SRC_PATH should contain a valid path");
         assert!(
@@ -261,13 +271,18 @@ fn main() {
         );
         // Rebuild files in the given path change.
         println!("cargo::rerun-if-changed={}", genmc_src_path.display());
-        genmc_src_path
+        // We disable `always_configure` when working with a local repository,
+        // since it increases compile times when working on `genmc-sys`.
+        (genmc_src_path, false)
     } else {
+        // Download GenMC if required and ensure that the correct commit is checked out.
+        // If anything changed in the downloaded repository (e.g., the commit),
+        // we set `always_configure` to ensure there are no weird configs from previous builds.
         downloading::download_genmc()
     };
 
     // Build all required components:
-    compile_cpp_dependencies(&genmc_path);
+    compile_cpp_dependencies(&genmc_path, always_configure);
 
     // Only rebuild if anything changes:
     // Note that we don't add the downloaded GenMC repo, since that should never be modified
diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
index 4484f0b73ca..b0769375843 100644
--- a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
+++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
@@ -33,6 +33,7 @@ struct GenmcScalar;
 struct SchedulingResult;
 struct LoadResult;
 struct StoreResult;
+struct ReadModifyWriteResult;
 
 // GenMC uses `int` for its thread IDs.
 using ThreadId = int;
@@ -90,6 +91,15 @@ struct MiriGenmcShim : private GenMCDriver {
         MemOrdering ord,
         GenmcScalar old_val
     );
+    [[nodiscard]] ReadModifyWriteResult handle_read_modify_write(
+        ThreadId thread_id,
+        uint64_t address,
+        uint64_t size,
+        RMWBinOp rmw_op,
+        MemOrdering ordering,
+        GenmcScalar rhs_value,
+        GenmcScalar old_val
+    );
     [[nodiscard]] StoreResult handle_store(
         ThreadId thread_id,
         uint64_t address,
@@ -99,6 +109,8 @@ struct MiriGenmcShim : private GenMCDriver {
         MemOrdering ord
     );
 
+    void handle_fence(ThreadId thread_id, MemOrdering ord);
+
     /**** Memory (de)allocation ****/
     auto handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment) -> uint64_t;
     void handle_free(ThreadId thread_id, uint64_t address);
@@ -271,4 +283,21 @@ inline StoreResult from_error(std::unique_ptr<std::string> error) {
 }
 } // namespace StoreResultExt
 
+namespace ReadModifyWriteResultExt {
+inline ReadModifyWriteResult
+ok(SVal old_value, SVal new_value, bool is_coherence_order_maximal_write) {
+    return ReadModifyWriteResult { /* error: */ std::unique_ptr<std::string>(nullptr),
+                                   /* old_value: */ GenmcScalarExt::from_sval(old_value),
+                                   /* new_value: */ GenmcScalarExt::from_sval(new_value),
+                                   is_coherence_order_maximal_write };
+}
+
+inline ReadModifyWriteResult from_error(std::unique_ptr<std::string> error) {
+    return ReadModifyWriteResult { /* error: */ std::move(error),
+                                   /* old_value: */ GenmcScalarExt::uninit(),
+                                   /* new_value: */ GenmcScalarExt::uninit(),
+                                   /* is_coherence_order_maximal_write: */ false };
+}
+} // namespace ReadModifyWriteResultExt
+
 #endif /* GENMC_MIRI_INTERFACE_HPP */
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
index 7d8f0b16b49..cd28e0d148f 100644
--- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
@@ -89,6 +89,72 @@
     );
 }
 
+void MiriGenmcShim::handle_fence(ThreadId thread_id, MemOrdering ord) {
+    const auto pos = inc_pos(thread_id);
+    GenMCDriver::handleFence(pos, ord, EventDeps());
+}
+
+[[nodiscard]] auto MiriGenmcShim::handle_read_modify_write(
+    ThreadId thread_id,
+    uint64_t address,
+    uint64_t size,
+    RMWBinOp rmw_op,
+    MemOrdering ordering,
+    GenmcScalar rhs_value,
+    GenmcScalar old_val
+) -> ReadModifyWriteResult {
+    // NOTE: Both the store and load events should get the same `ordering`, it should not be split
+    // into a load and a store component. This means we can have for example `AcqRel` loads and
+    // stores, but this is intended for RMW operations.
+
+    // Somewhat confusingly, the GenMC term for RMW read/write labels is
+    // `FaiRead` and `FaiWrite`.
+    const auto load_ret = handle_load_reset_if_none<EventLabel::EventLabelKind::FaiRead>(
+        thread_id,
+        ordering,
+        SAddr(address),
+        ASize(size),
+        AType::Unsigned, // The type is only used for printing.
+        rmw_op,
+        GenmcScalarExt::to_sval(rhs_value),
+        EventDeps()
+    );
+    if (const auto* err = std::get_if<VerificationError>(&load_ret))
+        return ReadModifyWriteResultExt::from_error(format_error(*err));
+
+    const auto* ret_val = std::get_if<SVal>(&load_ret);
+    if (nullptr == ret_val) {
+        ERROR("Unimplemented: read-modify-write returned unexpected result.");
+    }
+    const auto read_old_val = *ret_val;
+    const auto new_value =
+        executeRMWBinOp(read_old_val, GenmcScalarExt::to_sval(rhs_value), size, rmw_op);
+
+    const auto storePos = inc_pos(thread_id);
+    const auto store_ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::FaiWrite>(
+        storePos,
+        ordering,
+        SAddr(address),
+        ASize(size),
+        AType::Unsigned, // The type is only used for printing.
+        new_value
+    );
+    if (const auto* err = std::get_if<VerificationError>(&store_ret))
+        return ReadModifyWriteResultExt::from_error(format_error(*err));
+
+    const auto* store_ret_val = std::get_if<std::monostate>(&store_ret);
+    ERROR_ON(nullptr == store_ret_val, "Unimplemented: RMW store returned unexpected result.");
+
+    // FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once
+    // available).
+    const auto& g = getExec().getGraph();
+    return ReadModifyWriteResultExt::ok(
+        /* old_value: */ read_old_val,
+        new_value,
+        /* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == storePos
+    );
+}
+
 /**** Memory (de)allocation ****/
 
 auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
index 7194ed02da4..5a53fee0592 100644
--- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
@@ -63,9 +63,12 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
     auto conf = std::make_shared<Config>();
 
     // Set whether GenMC should print execution graphs after every explored/blocked execution.
-    // FIXME(genmc): pass these settings from Miri.
-    conf->printExecGraphs = false;
-    conf->printBlockedExecs = false;
+    conf->printExecGraphs =
+        (params.print_execution_graphs == ExecutiongraphPrinting::Explored ||
+         params.print_execution_graphs == ExecutiongraphPrinting::ExploredAndBlocked);
+    conf->printBlockedExecs =
+        (params.print_execution_graphs == ExecutiongraphPrinting::Blocked ||
+         params.print_execution_graphs == ExecutiongraphPrinting::ExploredAndBlocked);
 
     // `1024` is the default value that GenMC uses.
     // If any thread has at least this many events, a warning/tip will be printed.
@@ -79,8 +82,8 @@ static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel
     // Miri.
     conf->warnOnGraphSize = 1024 * 1024;
 
-    // We only support the RC11 memory model for Rust.
-    conf->model = ModelType::RC11;
+    // We only support the `RC11` memory model for Rust, and `SC` when weak memory emulation is disabled.
+    conf->model = params.disable_weak_memory_emulation ? ModelType::SC : ModelType::RC11;
 
     // This prints the seed that GenMC picks for randomized scheduling during estimation mode.
     conf->printRandomScheduleSeed = params.print_random_schedule_seed;
diff --git a/src/tools/miri/genmc-sys/src/lib.rs b/src/tools/miri/genmc-sys/src/lib.rs
index 406c90809fc..1de4c4eb5e8 100644
--- a/src/tools/miri/genmc-sys/src/lib.rs
+++ b/src/tools/miri/genmc-sys/src/lib.rs
@@ -53,7 +53,13 @@ impl GenmcScalar {
 
 impl Default for GenmcParams {
     fn default() -> Self {
-        Self { print_random_schedule_seed: false, do_symmetry_reduction: false }
+        Self {
+            print_random_schedule_seed: false,
+            do_symmetry_reduction: false,
+            // GenMC graphs can be quite large since Miri produces a lot of (non-atomic) events.
+            print_execution_graphs: ExecutiongraphPrinting::None,
+            disable_weak_memory_emulation: false,
+        }
     }
 }
 
@@ -91,7 +97,10 @@ mod ffi {
     struct GenmcParams {
         pub print_random_schedule_seed: bool,
         pub do_symmetry_reduction: bool,
-        // FIXME(GenMC): Add remaining parameters.
+        pub print_execution_graphs: ExecutiongraphPrinting,
+        /// Enabling this will set the memory model used by GenMC to "Sequential Consistency" (SC).
+        /// This will disable any weak memory effects, which reduces the number of program executions that will be explored.
+        pub disable_weak_memory_emulation: bool,
     }
 
     /// This is mostly equivalent to GenMC `VerbosityLevel`, but the debug log levels are always present (not conditionally compiled based on `ENABLE_GENMC_DEBUG`).
@@ -120,6 +129,19 @@ mod ffi {
         Debug3ReadsFrom,
     }
 
+    #[derive(Debug)]
+    /// Setting to control which execution graphs GenMC prints after every execution.
+    enum ExecutiongraphPrinting {
+        /// Print no graphs.
+        None,
+        /// Print graphs of all fully explored executions.
+        Explored,
+        /// Print graphs of all blocked executions.
+        Blocked,
+        /// Print graphs of all executions.
+        ExploredAndBlocked,
+    }
+
     /// This type corresponds to `Option<SVal>` (or `std::optional<SVal>`), where `SVal` is the type that GenMC uses for storing values.
     /// CXX doesn't support `std::optional` currently, so we need to use an extra `bool` to define whether this value is initialized or not.
     #[derive(Debug, Clone, Copy)]
@@ -163,7 +185,21 @@ mod ffi {
         is_coherence_order_maximal_write: bool,
     }
 
-    /**** Types shared between Miri/Rust and GenMC/C++ through cxx_bridge: ****/
+    #[must_use]
+    #[derive(Debug)]
+    struct ReadModifyWriteResult {
+        /// If there was an error, it will be stored in `error`, otherwise it is `None`.
+        error: UniquePtr<CxxString>,
+        /// The value that was read by the RMW operation as the left operand.
+        old_value: GenmcScalar,
+        /// The value that was produced by the RMW operation.
+        new_value: GenmcScalar,
+        /// `true` if the write should also be reflected in Miri's memory representation.
+        is_coherence_order_maximal_write: bool,
+    }
+
+    /**** These are GenMC types that we have to copy-paste here since cxx does not support
+    "importing" externally defined C++ types. ****/
 
     #[derive(Debug)]
     /// Corresponds to GenMC's type with the same name.
@@ -188,6 +224,21 @@ mod ffi {
         SequentiallyConsistent = 6,
     }
 
+    #[derive(Debug)]
+    enum RMWBinOp {
+        Xchg = 0,
+        Add = 1,
+        Sub = 2,
+        And = 3,
+        Nand = 4,
+        Or = 5,
+        Xor = 6,
+        Max = 7,
+        Min = 8,
+        UMax = 9,
+        UMin = 10,
+    }
+
     // # Safety
     //
     // This block is unsafe to allow defining safe methods inside.
@@ -202,9 +253,12 @@ mod ffi {
         /**** Types shared between Miri/Rust and Miri/C++: ****/
         type MiriGenmcShim;
 
-        /**** Types shared between Miri/Rust and GenMC/C++: ****/
+        /**** Types shared between Miri/Rust and GenMC/C++:
+        (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 MemOrdering;
+        type RMWBinOp;
 
         /// Set the log level for GenMC.
         ///
@@ -249,6 +303,16 @@ mod ffi {
             memory_ordering: MemOrdering,
             old_value: GenmcScalar,
         ) -> LoadResult;
+        fn handle_read_modify_write(
+            self: Pin<&mut MiriGenmcShim>,
+            thread_id: i32,
+            address: u64,
+            size: u64,
+            rmw_op: RMWBinOp,
+            ordering: MemOrdering,
+            rhs_value: GenmcScalar,
+            old_value: GenmcScalar,
+        ) -> ReadModifyWriteResult;
         fn handle_store(
             self: Pin<&mut MiriGenmcShim>,
             thread_id: i32,
@@ -258,6 +322,11 @@ mod ffi {
             old_value: GenmcScalar,
             memory_ordering: MemOrdering,
         ) -> StoreResult;
+        fn handle_fence(
+            self: Pin<&mut MiriGenmcShim>,
+            thread_id: i32,
+            memory_ordering: MemOrdering,
+        );
 
         /**** Memory (de)allocation ****/
         fn handle_malloc(