From 61af5da8dfc9f5fd6e2d36f8316f7bf5884f5388 Mon Sep 17 00:00:00 2001 From: Patrick-6 Date: Fri, 14 Mar 2025 09:58:46 +0100 Subject: 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 --- .../miri/genmc-sys/cpp/include/MiriInterface.hpp | 29 ++++++++++ .../cpp/src/MiriInterface/EventHandling.cpp | 66 ++++++++++++++++++++++ .../miri/genmc-sys/cpp/src/MiriInterface/Setup.cpp | 13 +++-- 3 files changed, 103 insertions(+), 5 deletions(-) (limited to 'src/tools/miri/genmc-sys/cpp') 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 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(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 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( + 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(&load_ret)) + return ReadModifyWriteResultExt::from_error(format_error(*err)); + + const auto* ret_val = std::get_if(&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( + storePos, + ordering, + SAddr(address), + ASize(size), + AType::Unsigned, // The type is only used for printing. + new_value + ); + if (const auto* err = std::get_if(&store_ret)) + return ReadModifyWriteResultExt::from_error(format_error(*err)); + + const auto* store_ret_val = std::get_if(&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(); // 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; -- cgit 1.4.1-3-g733a5