Merge pull request #4566 from Patrick-6/miri-genmc-rmw

Add more features for GenMC mode (RMW, fences, new printing options)

Author: RalfJung

doc/genmc.md

@@ -24,6 +24,9 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
 ### Supported Parameters
 
 - `-Zmiri-genmc`: Enable GenMC mode (not required if any other GenMC options are used).
+- `-Zmiri-genmc-print-exec-graphs={none,explored,blocked,all}`: Make GenMC print the execution graph of the program after every explored, every blocked, or after every execution (default: None).
+- `-Zmiri-genmc-print-exec-graphs`: Shorthand for suffix `=explored`.
+- `-Zmiri-genmc-print-genmc-output`: Print the output that GenMC provides. NOTE: this output is quite verbose and the events in the printed execution graph are hard to map back to the Rust code location they originate from.
 - `-Zmiri-genmc-log=LOG_LEVEL`: Change the log level for GenMC. Default: `warning`.
   - `quiet`:    Disable logging.
   - `error`:    Print errors.
@@ -34,7 +37,9 @@ Note that `cargo miri test` in GenMC mode is currently not supported.
     - `debug2`:   Print the execution graph after every memory access.
     - `debug3`:   Print reads-from values considered by GenMC.
 
-<!-- FIXME(genmc): explain options. -->
+#### Regular Miri parameters useful for GenMC mode
+
+- `-Zmiri-disable-weak-memory-emulation`: Disable any weak memory effects (effectively upgrading all atomic orderings in the program to `SeqCst`). This option may reduce the number of explored program executions, but any bugs related to weak memory effects will be missed. This option can help determine if an error is caused by weak memory effects (i.e., if it disappears with this option enabled).
 
 <!-- FIXME(genmc): explain Miri-GenMC specific functions. -->
 

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

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 */

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)

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;