#include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
#include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/transition/Transition.hpp"
+#include "src/mc/transition/TransitionSynchro.hpp"
#include <functional>
#include <unordered_map>
bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
const Transition* /*e2*/)
{
- // The only possibilities for e1 to satisfy the pre-condition are :
- // - MUTEX_ASYNC_LOCK
+ // TODO: for now we over approximate the reversibility
-
- const auto e1_action = E.get_transition_for_handle(e1)->type_;
- xbt_assert(e1_action == Transition::Type::MUTEX_UNLOCK);
- return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK;
+ return true;
}
bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
return true;
}
-bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution&, Execution::EventHandle /*e1*/,
+bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1,
const Transition* /*e2*/)
{
- // TODO: Get the semantics correct here
- // Certainement qu'il suffit de considérer les SemUnlock. ⋀ a priori,
- // il doit même suffir de considérer le cas où leur capacity après execution est <=1
- // ces cas disent qu'avant éxecution la capacity était de 0. Donc aucune chance de pouvoir
- // wait avant le unlock.
- return false;
+
+ const auto e1_transition = E.get_transition_for_handle(e1);
+ if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
+ static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1) {
+ return false;
+ }
+ xbt_assert(false, "SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
+ return true;
}
bool ReversibleRaceCalculator::is_race_reversible_ObjectAccess(const Execution&, Execution::EventHandle /*e1*/,
{
// TODO: We need to check if any of the transitions
// waited on occurred before `e1`
- return false;
+ return true; // Let's overapproximate to not miss branches
}
} // namespace simgrid::mc::odpor