Implement basic support for running Miri with GenMC.

- Implement memory allocation compatible with GenMC.
  - Extract address generator struct from Miri's allocator.
- Support thread creation and joining.
- Support atomic load and store.
- Support scheduling through GenMC.
- Add tests for GenMC mode.
- Add clang-format file for C++ code in Miri.
- Update genmc-sys crate license to MIT/Apache to match GenMC dependency.
- Add documentation for GenMC mode.

Note: this commit depends on changes to GenMC not yet upstreamed to its official repository.

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

6 files changed, 696 insertions, 0 deletions

diff --git a/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
new file mode 100644
index 00000000000..4484f0b73ca
--- /dev/null
+++ b/src/tools/miri/genmc-sys/cpp/include/MiriInterface.hpp
@@ -0,0 +1,274 @@
+#ifndef GENMC_MIRI_INTERFACE_HPP
+#define GENMC_MIRI_INTERFACE_HPP
+
+// CXX.rs generated headers:
+#include "rust/cxx.h"
+
+// GenMC generated headers:
+#include "config.h"
+
+// Miri `genmc-sys/src_cpp` headers:
+#include "ResultHandling.hpp"
+
+// GenMC headers:
+#include "ExecutionGraph/EventLabel.hpp"
+#include "Static/ModuleID.hpp"
+#include "Support/MemOrdering.hpp"
+#include "Support/RMWOps.hpp"
+#include "Verification/Config.hpp"
+#include "Verification/GenMCDriver.hpp"
+
+// C++ headers:
+#include <cstdint>
+#include <format>
+#include <iomanip>
+#include <memory>
+
+/**** Types available to both Rust and C++ ****/
+
+struct GenmcParams;
+enum class LogLevel : std::uint8_t;
+
+struct GenmcScalar;
+struct SchedulingResult;
+struct LoadResult;
+struct StoreResult;
+
+// GenMC uses `int` for its thread IDs.
+using ThreadId = int;
+
+/// Set the log level for GenMC.
+///
+/// # Safety
+///
+/// This function is not thread safe, since it writes to the global, mutable, non-atomic `logLevel`
+/// variable. Any GenMC function may read from `logLevel` unsynchronized.
+/// The safest way to use this function is to set the log level exactly once before first calling
+/// `create_handle`.
+/// Never calling this function is safe, GenMC will fall back to its default log level.
+/* unsafe */ void set_log_level_raw(LogLevel log_level);
+
+struct MiriGenmcShim : private GenMCDriver {
+
+  public:
+    MiriGenmcShim(std::shared_ptr<const Config> conf, Mode mode /* = VerificationMode{} */)
+        : GenMCDriver(std::move(conf), nullptr, mode) {}
+
+    /// Create a new `MiriGenmcShim`, which wraps a `GenMCDriver`.
+    ///
+    /// # Safety
+    ///
+    /// This function is marked as unsafe since the `logLevel` global variable is non-atomic.
+    /// This function should not be called in an unsynchronized way with `set_log_level_raw`,
+    /// since this function and any methods on the returned `MiriGenmcShim` may read the
+    /// `logLevel`, causing a data race. The safest way to use these functions is to call
+    /// `set_log_level_raw` once, and only then start creating handles. There should not be any
+    /// other (safe) way to create a `MiriGenmcShim`.
+    /* unsafe */ static auto create_handle(const GenmcParams& params)
+        -> std::unique_ptr<MiriGenmcShim>;
+
+    virtual ~MiriGenmcShim() {}
+
+    /**** Execution start/end handling ****/
+
+    // This function must be called at the start of any execution, before any events are
+    // reported to GenMC.
+    void handle_execution_start();
+    // This function must be called at the end of any execution, even if an error was found
+    // during the execution.
+    // Returns `null`, or a string containing an error message if an error occured.
+    std::unique_ptr<std::string> handle_execution_end();
+
+    /***** Functions for handling events encountered during program execution. *****/
+
+    /**** Memory access handling ****/
+
+    [[nodiscard]] LoadResult handle_load(
+        ThreadId thread_id,
+        uint64_t address,
+        uint64_t size,
+        MemOrdering ord,
+        GenmcScalar old_val
+    );
+    [[nodiscard]] StoreResult handle_store(
+        ThreadId thread_id,
+        uint64_t address,
+        uint64_t size,
+        GenmcScalar value,
+        GenmcScalar old_val,
+        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);
+
+    /**** Thread management ****/
+    void handle_thread_create(ThreadId thread_id, ThreadId parent_id);
+    void handle_thread_join(ThreadId thread_id, ThreadId child_id);
+    void handle_thread_finish(ThreadId thread_id, uint64_t ret_val);
+    void handle_thread_kill(ThreadId thread_id);
+
+    /***** Exploration related functionality *****/
+
+    /** Ask the GenMC scheduler for a new thread to schedule and return whether the execution is
+     * finished, blocked, or can continue.
+     * Updates the next instruction kind for the given thread id. */
+    auto schedule_next(const int curr_thread_id, const ActionKind curr_thread_next_instr_kind)
+        -> SchedulingResult;
+
+    /**
+     * Check whether there are more executions to explore.
+     * If there are more executions, this method prepares for the next execution and returns
+     * `true`. Returns true if there are no more executions to explore. */
+    auto is_exploration_done() -> bool {
+        return GenMCDriver::done();
+    }
+
+    /**** Result querying functionality. ****/
+
+    // NOTE: We don't want to share the `VerificationResult` type with the Rust side, since it
+    // is very large, uses features that CXX.rs doesn't support and may change as GenMC changes.
+    // Instead, we only use the result on the C++ side, and only expose these getter function to
+    // the Rust side.
+
+    // Note that CXX.rs doesn't support returning a C++ string to Rust by value,
+    // it must be behind an indirection like a `unique_ptr` (tested with CXX 1.0.170).
+
+    /// Get the number of blocked executions encountered by GenMC (cast into a fixed with
+    /// integer)
+    auto get_blocked_execution_count() const -> uint64_t {
+        return static_cast<uint64_t>(getResult().exploredBlocked);
+    }
+
+    /// Get the number of executions explored by GenMC (cast into a fixed with integer)
+    auto get_explored_execution_count() const -> uint64_t {
+        return static_cast<uint64_t>(getResult().explored);
+    }
+
+    /// Get all messages that GenMC produced (errors, warnings), combined into one string.
+    auto get_result_message() const -> std::unique_ptr<std::string> {
+        return std::make_unique<std::string>(getResult().message);
+    }
+
+    /// If an error occurred, return a string describing the error, otherwise, return `nullptr`.
+    auto get_error_string() const -> std::unique_ptr<std::string> {
+        const auto& result = GenMCDriver::getResult();
+        if (result.status.has_value())
+            return format_error(result.status.value());
+        return nullptr;
+    }
+
+  private:
+    /** Increment the event index in the given thread by 1 and return the new event. */
+    [[nodiscard]] inline auto inc_pos(ThreadId tid) -> Event {
+        ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds");
+        return ++threads_action_[tid].event;
+    }
+    /** Decrement the event index in the given thread by 1 and return the new event. */
+    inline auto dec_pos(ThreadId tid) -> Event {
+        ERROR_ON(tid >= threads_action_.size(), "ThreadId out of bounds");
+        return --threads_action_[tid].event;
+    }
+
+    /**
+     * Helper function for loads that need to reset the event counter when no value is returned.
+     * Same syntax as `GenMCDriver::handleLoad`, but this takes a thread id instead of an Event.
+     * Automatically calls `inc_pos` and `dec_pos` where needed for the given thread.
+     */
+    template <EventLabel::EventLabelKind k, typename... Ts>
+    auto handle_load_reset_if_none(ThreadId tid, Ts&&... params) -> HandleResult<SVal> {
+        const auto pos = inc_pos(tid);
+        const auto ret = GenMCDriver::handleLoad<k>(pos, std::forward<Ts>(params)...);
+        // If we didn't get a value, we have to reset the index of the current thread.
+        if (!std::holds_alternative<SVal>(ret)) {
+            dec_pos(tid);
+        }
+        return ret;
+    }
+
+    /**
+     * GenMC uses the term `Action` to refer to a struct of:
+     * - `ActionKind`, storing whether the next instruction in a thread may be a load
+     * - `Event`, storing the most recent event index added for a thread
+     *
+     * Here we store the "action" for each thread. In particular we use this to assign event
+     * indices, since GenMC expects us to do that.
+     */
+    std::vector<Action> threads_action_;
+};
+
+/// Get the bit mask that GenMC expects for global memory allocations.
+/// FIXME(genmc): currently we use `get_global_alloc_static_mask()` to ensure the
+/// `SAddr::staticMask` constant is consistent between Miri and GenMC, but if
+/// https://github.com/dtolnay/cxx/issues/1051 is fixed we could share the constant
+///   directly.
+constexpr auto get_global_alloc_static_mask() -> uint64_t {
+    return SAddr::staticMask;
+}
+
+// CXX.rs generated headers:
+// NOTE: this must be included *after* `MiriGenmcShim` and all the other types we use are defined,
+// otherwise there will be compilation errors due to missing definitions.
+#include "genmc-sys/src/lib.rs.h"
+
+/**** Result handling ****/
+// NOTE: these must come after the cxx_bridge generated code, since that contains the actual
+// definitions of these types.
+
+namespace GenmcScalarExt {
+inline GenmcScalar uninit() {
+    return GenmcScalar {
+        /* value: */ 0,
+        /* is_init: */ false,
+    };
+}
+
+inline GenmcScalar from_sval(SVal sval) {
+    return GenmcScalar {
+        /* value: */ sval.get(),
+        /* is_init: */ true,
+    };
+}
+
+inline SVal to_sval(GenmcScalar scalar) {
+    ERROR_ON(!scalar.is_init, "Cannot convert an uninitialized `GenmcScalar` into an `SVal`\n");
+    return SVal(scalar.value);
+}
+} // namespace GenmcScalarExt
+
+namespace LoadResultExt {
+inline LoadResult no_value() {
+    return LoadResult {
+        /* error: */ std::unique_ptr<std::string>(nullptr),
+        /* has_value: */ false,
+        /* read_value: */ GenmcScalarExt::uninit(),
+    };
+}
+
+inline LoadResult from_value(SVal read_value) {
+    return LoadResult { /* error: */ std::unique_ptr<std::string>(nullptr),
+                        /* has_value: */ true,
+                        /* read_value: */ GenmcScalarExt::from_sval(read_value) };
+}
+
+inline LoadResult from_error(std::unique_ptr<std::string> error) {
+    return LoadResult { /* error: */ std::move(error),
+                        /* has_value: */ false,
+                        /* read_value: */ GenmcScalarExt::uninit() };
+}
+} // namespace LoadResultExt
+
+namespace StoreResultExt {
+inline StoreResult ok(bool is_coherence_order_maximal_write) {
+    return StoreResult { /* error: */ std::unique_ptr<std::string>(nullptr),
+                         is_coherence_order_maximal_write };
+}
+
+inline StoreResult from_error(std::unique_ptr<std::string> error) {
+    return StoreResult { /* error: */ std::move(error),
+                         /* is_coherence_order_maximal_write: */ false };
+}
+} // namespace StoreResultExt
+
+#endif /* GENMC_MIRI_INTERFACE_HPP */
diff --git a/src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp b/src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp
new file mode 100644
index 00000000000..189f32e6f51
--- /dev/null
+++ b/src/tools/miri/genmc-sys/cpp/include/ResultHandling.hpp
@@ -0,0 +1,21 @@
+#ifndef GENMC_RESULT_HANDLING_HPP
+#define GENMC_RESULT_HANDLING_HPP
+
+// CXX.rs generated headers:
+#include "rust/cxx.h"
+
+// GenMC headers:
+#include "Verification/VerificationError.hpp"
+
+#include <string>
+
+/** Information about an error, formatted as a string to avoid having to share an error enum and
+ * printing functionality with the Rust side. */
+static auto format_error(VerificationError err) -> std::unique_ptr<std::string> {
+    auto buf = std::string();
+    auto s = llvm::raw_string_ostream(buf);
+    s << err;
+    return std::make_unique<std::string>(s.str());
+}
+
+#endif /* GENMC_RESULT_HANDLING_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
new file mode 100644
index 00000000000..7d8f0b16b49
--- /dev/null
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/EventHandling.cpp
@@ -0,0 +1,120 @@
+/** This file contains functionality related to handling events encountered
+ * during an execution, such as loads, stores or memory (de)allocation. */
+
+#include "MiriInterface.hpp"
+
+// CXX.rs generated headers:
+#include "genmc-sys/src/lib.rs.h"
+
+// GenMC headers:
+#include "ADT/value_ptr.hpp"
+#include "ExecutionGraph/EventLabel.hpp"
+#include "ExecutionGraph/LoadAnnotation.hpp"
+#include "Runtime/InterpreterEnumAPI.hpp"
+#include "Static/ModuleID.hpp"
+#include "Support/ASize.hpp"
+#include "Support/Error.hpp"
+#include "Support/Logger.hpp"
+#include "Support/MemAccess.hpp"
+#include "Support/RMWOps.hpp"
+#include "Support/SAddr.hpp"
+#include "Support/SVal.hpp"
+#include "Support/ThreadInfo.hpp"
+#include "Support/Verbosity.hpp"
+#include "Verification/GenMCDriver.hpp"
+#include "Verification/MemoryModel.hpp"
+
+// C++ headers:
+#include <cstddef>
+#include <cstdint>
+#include <memory>
+#include <utility>
+
+/**** Memory access handling ****/
+
+[[nodiscard]] auto MiriGenmcShim::handle_load(
+    ThreadId thread_id,
+    uint64_t address,
+    uint64_t size,
+    MemOrdering ord,
+    GenmcScalar old_val
+) -> LoadResult {
+    // `type` is only used for printing.
+    const auto type = AType::Unsigned;
+    const auto ret = handle_load_reset_if_none<EventLabel::EventLabelKind::Read>(
+        thread_id,
+        ord,
+        SAddr(address),
+        ASize(size),
+        type
+    );
+
+    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);
+    if (ret_val == nullptr)
+        ERROR("Unimplemented: load returned unexpected result.");
+    return LoadResultExt::from_value(*ret_val);
+}
+
+[[nodiscard]] auto MiriGenmcShim::handle_store(
+    ThreadId thread_id,
+    uint64_t address,
+    uint64_t size,
+    GenmcScalar value,
+    GenmcScalar old_val,
+    MemOrdering ord
+) -> StoreResult {
+    const auto pos = inc_pos(thread_id);
+    const auto ret = GenMCDriver::handleStore<EventLabel::EventLabelKind::Write>(
+        pos,
+        ord,
+        SAddr(address),
+        ASize(size),
+        /* type */ AType::Unsigned, // `type` is only used for printing.
+        GenmcScalarExt::to_sval(value),
+        EventDeps()
+    );
+
+    if (const auto* err = std::get_if<VerificationError>(&ret))
+        return StoreResultExt::from_error(format_error(*err));
+    if (!std::holds_alternative<std::monostate>(ret))
+        ERROR("store returned unexpected result");
+
+    // FIXME(genmc,mixed-accesses): Use the value that GenMC returns from handleStore (once
+    // available).
+    const auto& g = getExec().getGraph();
+    return StoreResultExt::ok(
+        /* is_coherence_order_maximal_write */ g.co_max(SAddr(address))->getPos() == pos
+    );
+}
+
+/**** Memory (de)allocation ****/
+
+auto MiriGenmcShim::handle_malloc(ThreadId thread_id, uint64_t size, uint64_t alignment)
+    -> uint64_t {
+    const auto pos = inc_pos(thread_id);
+
+    // These are only used for printing and features Miri-GenMC doesn't support (yet).
+    const auto storage_duration = StorageDuration::SD_Heap;
+    // Volatile, as opposed to "persistent" (i.e., non-volatile memory that persists over reboots)
+    const auto storage_type = StorageType::ST_Volatile;
+    const auto address_space = AddressSpace::AS_User;
+
+    const SVal ret_val = GenMCDriver::handleMalloc(
+        pos,
+        size,
+        alignment,
+        storage_duration,
+        storage_type,
+        address_space,
+        EventDeps()
+    );
+    return ret_val.get();
+}
+
+void MiriGenmcShim::handle_free(ThreadId thread_id, uint64_t address) {
+    const auto pos = inc_pos(thread_id);
+    GenMCDriver::handleFree(pos, SAddr(address), EventDeps());
+    // FIXME(genmc): add error handling once GenMC returns errors from `handleFree`
+}
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp
new file mode 100644
index 00000000000..c51b59e8651
--- /dev/null
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp
@@ -0,0 +1,42 @@
+/** This file contains functionality related to exploration, such as scheduling.  */
+
+#include "MiriInterface.hpp"
+
+// CXX.rs generated headers:
+#include "genmc-sys/src/lib.rs.h"
+
+// GenMC headers:
+#include "Support/Error.hpp"
+#include "Support/Verbosity.hpp"
+
+// C++ headers:
+#include <cstdint>
+
+auto MiriGenmcShim::schedule_next(
+    const int curr_thread_id,
+    const ActionKind curr_thread_next_instr_kind
+) -> SchedulingResult {
+    // The current thread is the only one where the `kind` could have changed since we last made
+    // a scheduling decision.
+    threads_action_[curr_thread_id].kind = curr_thread_next_instr_kind;
+
+    if (const auto result = GenMCDriver::scheduleNext(threads_action_))
+        return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(result.value()) };
+    if (GenMCDriver::isExecutionBlocked())
+        return SchedulingResult { ExecutionState::Blocked, 0 };
+    return SchedulingResult { ExecutionState::Finished, 0 };
+}
+
+/**** Execution start/end handling ****/
+
+void MiriGenmcShim::handle_execution_start() {
+    threads_action_.clear();
+    threads_action_.push_back(Action(ActionKind::Load, Event::getInit()));
+    GenMCDriver::handleExecutionStart();
+}
+
+auto MiriGenmcShim::handle_execution_end() -> std::unique_ptr<std::string> {
+    // FIXME(genmc): add error handling once GenMC returns an error here.
+    GenMCDriver::handleExecutionEnd();
+    return {};
+}
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
new file mode 100644
index 00000000000..7194ed02da4
--- /dev/null
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp
@@ -0,0 +1,185 @@
+/** This file contains functionality related to creation of the GenMCDriver,
+ * including translating settings set by Miri.  */
+
+#include "MiriInterface.hpp"
+
+// CXX.rs generated headers:
+#include "genmc-sys/src/lib.rs.h"
+
+// GenMC headers:
+#include "Support/Error.hpp"
+#include "Support/Verbosity.hpp"
+#include "Verification/InterpreterCallbacks.hpp"
+
+// C++ headers:
+#include <cstdint>
+
+/**
+ * Translate the Miri-GenMC `LogLevel` to the GenMC `VerbosityLevel`.
+ * Downgrade any debug options to `Tip` if `ENABLE_GENMC_DEBUG` is not enabled.
+ */
+static auto to_genmc_verbosity_level(const LogLevel log_level) -> VerbosityLevel {
+    switch (log_level) {
+        case LogLevel::Quiet:
+            return VerbosityLevel::Quiet;
+        case LogLevel::Error:
+            return VerbosityLevel::Error;
+        case LogLevel::Warning:
+            return VerbosityLevel::Warning;
+        case LogLevel::Tip:
+            return VerbosityLevel::Tip;
+#ifdef ENABLE_GENMC_DEBUG
+        case LogLevel::Debug1Revisits:
+            return VerbosityLevel::Debug1;
+        case LogLevel::Debug2MemoryAccesses:
+            return VerbosityLevel::Debug2;
+        case LogLevel::Debug3ReadsFrom:
+            return VerbosityLevel::Debug3;
+#else
+        // Downgrade to `Tip` if the debug levels are not available.
+        case LogLevel::Debug1Revisits:
+        case LogLevel::Debug2MemoryAccesses:
+        case LogLevel::Debug3ReadsFrom:
+            return VerbosityLevel::Tip;
+#endif
+        default:
+            WARN_ONCE(
+                "unknown-log-level",
+                "Unknown `LogLevel`, defaulting to `VerbosityLevel::Tip`."
+            );
+            return VerbosityLevel::Tip;
+    }
+}
+
+/* unsafe */ void set_log_level_raw(LogLevel log_level) {
+    // The `logLevel` is a static, non-atomic variable.
+    // It should never be changed if `MiriGenmcShim` still exists, since any of its methods may read
+    // the `logLevel`, otherwise it may cause data races.
+    logLevel = to_genmc_verbosity_level(log_level);
+}
+
+/* unsafe */ auto MiriGenmcShim::create_handle(const GenmcParams& params)
+    -> std::unique_ptr<MiriGenmcShim> {
+    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;
+
+    // `1024` is the default value that GenMC uses.
+    // If any thread has at least this many events, a warning/tip will be printed.
+    //
+    // Miri produces a lot more events than GenMC, so the graph size warning triggers on almost
+    // all programs. The current value is large enough so the warning is not be triggered by any
+    // reasonable programs.
+    // FIXME(genmc): The emitted warning mentions features not supported by Miri ('--unroll'
+    // parameter).
+    // FIXME(genmc): A more appropriate limit should be chosen once the warning is useful for
+    // Miri.
+    conf->warnOnGraphSize = 1024 * 1024;
+
+    // We only support the RC11 memory model for Rust.
+    conf->model = ModelType::RC11;
+
+    // This prints the seed that GenMC picks for randomized scheduling during estimation mode.
+    conf->printRandomScheduleSeed = params.print_random_schedule_seed;
+
+    // FIXME(genmc): supporting IPR requires annotations for `assume` and `spinloops`.
+    conf->ipr = false;
+    // FIXME(genmc): supporting BAM requires `Barrier` support + detecting whether return value
+    // of barriers are used.
+    conf->disableBAM = true;
+
+    // Instruction caching could help speed up verification by filling the graph from cache, if
+    // the list of values read by all load events in a thread have been seen before. Combined
+    // with not replaying completed threads, this can also reducing the amount of Mir
+    // interpretation required by Miri. With the current setup, this would be incorrect, since
+    // Miri doesn't give GenMC the actual values read by non-atomic reads.
+    conf->instructionCaching = false;
+    // Many of Miri's checks work under the assumption that threads are only executed in an
+    // order that could actually happen during a normal execution. Formally, this means that
+    // replaying an execution needs to respect the po-rf-relation of the executiongraph (po ==
+    // program-order, rf == reads-from). This means, any event in the graph, when replayed, must
+    // happen after any events that happen before it in the same graph according to the program
+    // code, and all (non-atomic) reads must happen after the write event they read from.
+    //
+    // Not replaying completed threads means any read event from that thread never happens in
+    // Miri's memory, so this would only work if there are never any non-atomic reads from any
+    // value written by the skipped thread.
+    conf->replayCompletedThreads = true;
+
+    // FIXME(genmc): implement symmetry reduction.
+    ERROR_ON(
+        params.do_symmetry_reduction,
+        "Symmetry reduction is currently unsupported in GenMC mode."
+    );
+    conf->symmetryReduction = params.do_symmetry_reduction;
+
+    // FIXME(genmc): expose this setting to Miri (useful for testing Miri-GenMC).
+    conf->schedulePolicy = SchedulePolicy::WF;
+
+    // Set the mode used for this driver, either estimation or verification.
+    // FIXME(genmc): implement estimation mode.
+    const auto mode = GenMCDriver::Mode(GenMCDriver::VerificationMode {});
+
+    // Running Miri-GenMC without race detection is not supported.
+    // Disabling this option also changes the behavior of the replay scheduler to only schedule
+    // at atomic operations, which is required with Miri. This happens because Miri can generate
+    // multiple GenMC events for a single MIR terminator. Without this option, the scheduler
+    // might incorrectly schedule an atomic MIR terminator because the first event it creates is
+    // a non-atomic (e.g., `StorageLive`).
+    conf->disableRaceDetection = false;
+
+    // Miri can already check for unfreed memory. Also, GenMC cannot distinguish between memory
+    // that is allowed to leak and memory that is not.
+    conf->warnUnfreedMemory = false;
+
+    // FIXME(genmc,error handling): This function currently exits on error, but will return an
+    // error value in the future. The return value should be checked once this change is made.
+    checkConfig(*conf);
+
+    // Create the actual driver and Miri-GenMC communication shim.
+    auto driver = std::make_unique<MiriGenmcShim>(std::move(conf), mode);
+
+    // FIXME(genmc,HACK): Until a proper solution is implemented in GenMC, these callbacks will
+    // allow Miri to return information about global allocations and override uninitialized memory
+    // checks for non-atomic loads (Miri handles those without GenMC, so the error would be wrong).
+    auto interpreter_callbacks = InterpreterCallbacks {
+        // Miri already ensures that memory accesses are valid, so this check doesn't matter.
+        // We check that the address is static, but skip checking if it is part of an actual
+        // allocation.
+        /* isStaticallyAllocated: */ [](SAddr addr) { return addr.isStatic(); },
+        // FIXME(genmc,error reporting): Once a proper a proper API for passing such information is
+        // implemented in GenMC, Miri should use it to improve the produced error messages.
+        /* getStaticName: */ [](SAddr addr) { return "[UNKNOWN STATIC]"; },
+        // This function is called to get the initial value stored at the given address.
+        //
+        // From a Miri perspective, this API doesn't work very well: most memory starts out
+        // "uninitialized";
+        // only statics have an initial value. And their initial value is just a sequence of bytes,
+        // but GenMC
+        // expect this to be already split into separate atomic variables. So we return a dummy
+        // value.
+        // This value should never be visible to the interpreted program.
+        // GenMC does not understand uninitialized memory the same way Miri does, which may cause
+        // this function to be called. The returned value can be visible to Miri or the user:
+        // - Printing the execution graph may contain this value in place of uninitialized values.
+        //   FIXME(genmc): NOTE: printing the execution graph is not yet implemented.
+        // - Non-atomic loads may return this value, but Miri ignores values of non-atomic loads.
+        // - Atomic loads will *not* see this value once mixed atomic-non-atomic support is added.
+        //   Currently, atomic loads can see this value, unless initialized by an *atomic* store.
+        //   FIXME(genmc): update this comment once mixed atomic-non-atomic support is added.
+        //
+        // FIXME(genmc): implement proper support for uninitialized memory in GenMC. Ideally, the
+        // initial value getter would return an `optional<SVal>`, since the memory location may be
+        // uninitialized.
+        /* initValGetter: */ [](const AAccess& a) { return SVal(0xDEAD); },
+        // Miri serves non-atomic loads from its own memory and these GenMC checks are wrong in
+        // that case. This should no longer be required with proper mixed-size access support.
+        /* skipUninitLoadChecks: */ [](MemOrdering ord) { return ord == MemOrdering::NotAtomic; },
+    };
+    driver->setInterpCallbacks(std::move(interpreter_callbacks));
+
+    return driver;
+}
diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp
new file mode 100644
index 00000000000..352d27adc3e
--- /dev/null
+++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/ThreadManagement.cpp
@@ -0,0 +1,54 @@
+
+/** This file contains functionality related thread management (creation, finishing, join, etc.)  */
+
+#include "MiriInterface.hpp"
+
+// CXX.rs generated headers:
+#include "genmc-sys/src/lib.rs.h"
+
+// GenMC headers:
+#include "Support/Error.hpp"
+#include "Support/Verbosity.hpp"
+
+// C++ headers:
+#include <cstdint>
+
+void MiriGenmcShim::handle_thread_create(ThreadId thread_id, ThreadId parent_id) {
+    // NOTE: The threadCreate event happens in the parent:
+    const auto pos = inc_pos(parent_id);
+    // FIXME(genmc): for supporting symmetry reduction, these will need to be properly set:
+    const unsigned fun_id = 0;
+    const SVal arg = SVal(0);
+    const ThreadInfo child_info = ThreadInfo { thread_id, parent_id, fun_id, arg };
+
+    // NOTE: Default memory ordering (`Release`) used here.
+    const auto child_tid = GenMCDriver::handleThreadCreate(pos, child_info, EventDeps());
+    // Sanity check the thread id, which is the index in the `threads_action_` array.
+    BUG_ON(child_tid != thread_id || child_tid <= 0 || child_tid != threads_action_.size());
+    threads_action_.push_back(Action(ActionKind::Load, Event(child_tid, 0)));
+}
+
+void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) {
+    // The thread join event happens in the parent.
+    const auto pos = inc_pos(thread_id);
+
+    // NOTE: Default memory ordering (`Acquire`) used here.
+    const auto ret = GenMCDriver::handleThreadJoin(pos, child_id, EventDeps());
+    // If the join failed, decrease the event index again:
+    if (!std::holds_alternative<SVal>(ret)) {
+        dec_pos(thread_id);
+    }
+
+    // NOTE: Thread return value is ignored, since Miri doesn't need it.
+}
+
+void MiriGenmcShim::handle_thread_finish(ThreadId thread_id, uint64_t ret_val) {
+    const auto pos = inc_pos(thread_id);
+    // NOTE: Default memory ordering (`Release`) used here.
+    GenMCDriver::handleThreadFinish(pos, SVal(ret_val));
+}
+
+void MiriGenmcShim::handle_thread_kill(ThreadId thread_id) {
+    const auto pos = inc_pos(thread_id);
+    GenMCDriver::handleThreadKill(pos);
+}