From d42fe7175ad770fd0a4618ceeb4833ca4ebc66cc Mon Sep 17 00:00:00 2001 From: Michalis Kokologiannakis Date: Sun, 12 Apr 2026 15:42:16 +0200 Subject: [PATCH] genmc/exploration: Add a FIXME for join --- .../genmc-sys/cpp/src/MiriInterface/Exploration.cpp | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) diff --git a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp index 4fae640ca240..6be28ad229e0 100644 --- a/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp +++ b/src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp @@ -576,11 +576,19 @@ void MiriGenmcShim::handle_thread_join(ThreadId thread_id, ThreadId child_id) { const auto ret = GenMCDriver::handleThreadJoin(nullptr, curr_pos(thread_id), child_id, EventDeps()); inc_pos(thread_id, ret.count); - // FIXME(genmc): handle `HandleResult::{Invalid, Reset, VerificationError}` return values. + // FIXME(genmc): handle `HandleResult::{Invalid, VerificationError}` return values. ERROR_ON( !std::holds_alternative(ret.result) && !std::holds_alternative(ret.result), "Unimplemented: unexpected return value for thread join" ); + // FIXME(genmc): Here Reset{} is silently accepted. Double-check why that is. + // The reason is likely that, although GenMC wants to re-run the join instruction, + // when GenMC deems that the join has executed, it will also deem it successful, + // i.e., the return value is guaranteed to be 0 (or at least we assume that). + // In this case, it doesn't matter that we don't re-run the instruction, since + // Miri sets the correct return value, and GenMC will only schedule this thread + // when it knows the child has terminated. + // NOTE: Thread return value is ignored, since Miri doesn't need it. }