user0/rust
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

genmc/schedule: Handle new GenMC scheduling API

Browse source 
When GenMC says that an execution should not be explored further,
Miri needs to know why (e.g., so that it returns an appropriate
exit value). Until now, some (erroneous) heuristics were used
for that.

This commit changes the Miri/GenMC API to check the scheduling
result of GenMC (that now reflects the "stop type").
This commit is contained in:
Michalis Kokologiannakis 2025-11-15 17:10:11 +01:00
parent b6cc543c3b
commit 689358ab36
1 changed files with 17 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/tools/miri/genmc-sys/cpp/src/MiriInterface/Exploration.cpp
View file

@ -22,13 +22,23 @@ auto MiriGenmcShim::schedule_next(
// 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 (getExec().getGraph().isBlocked())
return SchedulingResult { ExecutionState::Blocked, 0 };
if (getResult().status.has_value()) // the "value" here is a `VerificationError`
return SchedulingResult { ExecutionState::Error, 0 };
return SchedulingResult { ExecutionState::Finished, 0 };
auto result = GenMCDriver::scheduleNext(threads_action_);
return std::visit(
[](auto&& arg) {
using T = std::decay_t<decltype(arg)>;
if constexpr (std::is_same_v<T, int>)
return SchedulingResult { ExecutionState::Ok, static_cast<int32_t>(arg) };
else if constexpr (std::is_same_v<T, Blocked>)
return SchedulingResult { ExecutionState::Blocked, 0 };
else if constexpr (std::is_same_v<T, Error>)
return SchedulingResult { ExecutionState::Error, 0 };
else if constexpr (std::is_same_v<T, Finished>)
return SchedulingResult { ExecutionState::Finished, 0 };
else
static_assert(false, "non-exhaustive visitor!");
},
result
);
}
/**** Execution start/end handling ****/