#include "src/mc/explo/odpor/Execution.hpp"
#include "src/mc/api/State.hpp"
+#include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
#include "xbt/asserts.h"
#include <algorithm>
#include <limits>
std::unordered_set<Execution::EventHandle> Execution::get_reversible_races_of(EventHandle handle) const
{
- // TODO: Implement this
- return std::unordered_set<EventHandle>{};
+ std::unordered_set<EventHandle> reversible_races;
+ for (EventHandle race : get_racing_events_of(handle)) {
+ if (ReversibleRaceCalculator::is_race_reversible(*this, race, handle)) {
+ reversible_races.insert(race);
+ }
+ }
+ return reversible_races;
}
Execution Execution::get_prefix_before(Execution::EventHandle handle) const
Execution(std::vector<Event>&& contents) : contents_(std::move(contents)) {}
public:
- using Handle = decltype(contents_)::const_iterator;
using EventHandle = uint32_t;
Execution() = default;
*/
aid_t get_actor_with_handle(EventHandle handle) const { return get_event_with_handle(handle).get_transition()->aid_; }
+ /**
+ * @brief Determines the transition associated with the given handle `handle`
+ */
+ const Transition* get_transition_for_handle(EventHandle handle) const
+ {
+ return get_event_with_handle(handle).get_transition().get();
+ }
+
/**
* @brief Returns a handle to the newest event of the execution,
* if such an event exists
+/* Copyright (c) 2008-2023. The SimGrid Team. All rights reserved. */
+
+/* This program is free software; you can redistribute it and/or modify it
+ * under the terms of the license (GNU LGPL) which comes with this package. */
+
+#include "src/mc/explo/odpor/ReversibleRaceCalculator.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
+
+#include <functional>
+#include <unordered_map>
+#include <xbt/asserts.h>
+#include <xbt/ex.h>
+
+namespace simgrid::mc::odpor {
+
+bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1,
+ Execution::EventHandle e2)
+{
+ using Action = Transition::Type;
+ using Handler = std::function<bool(const Execution&, Execution::EventHandle, const Transition*)>;
+ using HandlerMap = std::unordered_map<Action, Handler>;
+
+ const static HandlerMap handlers =
+ HandlerMap{{Action::COMM_ASYNC_RECV, &ReversibleRaceCalculator::is_race_reversible_CommRecv},
+ {Action::COMM_ASYNC_SEND, &ReversibleRaceCalculator::is_race_reversible_CommSend},
+ {Action::COMM_WAIT, &ReversibleRaceCalculator::is_race_reversible_CommWait}};
+
+ const auto e2_action = E.get_transition_for_handle(e2);
+ if (const auto handler = handlers.find(e2_action->type_); handler != handlers.end()) {
+ return handler->second(E, e1, e2_action);
+ } else {
+ xbt_assert(false,
+ "There is currently no specialized computation for the transition "
+ "'%s' for computing reversible races in ODPOR, so the model checker cannot "
+ "determine how to proceed. Please submit a bug report requesting "
+ "that the transition be supported in SimGrid using ODPPR and consider "
+ "using the other model-checking algorithms supported by SimGrid instead "
+ "in the meantime",
+ e2_action->to_string().c_str());
+ DIE_IMPOSSIBLE;
+ }
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // CommRecv is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_CommSend(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // CommSend is always enabled
+ return true;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_CommWait(const Execution& E, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ // If the other event communication event, then we
+ // are not reversible. Otherwise we are reversible.
+ const auto e1_action = E.get_transition_for_handle(e1)->type_;
+ return e1_action != Transition::Type::COMM_ASYNC_SEND and e1_action != Transition::Type::COMM_ASYNC_RECV;
+}
+
+bool ReversibleRaceCalculator::is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1,
+ const Transition* e2)
+{
+ return false;
+}
+
+} // namespace simgrid::mc::odpor
\ No newline at end of file
#ifndef SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
#define SIMGRID_MC_ODPOR_REVERSIBLE_RACE_CALCULATOR_HPP
-#include "src/mc/explo/udpor/EventSet.hpp"
-#include "src/mc/explo/udpor/udpor_forward.hpp"
+#include "src/mc/explo/odpor/Execution.hpp"
+#include "src/mc/explo/odpor/odpor_forward.hpp"
#include "src/mc/transition/Transition.hpp"
#include "src/mc/transition/TransitionActorJoin.hpp"
#include "src/mc/transition/TransitionAny.hpp"
* is only sensible in the context of a race
*/
struct ReversibleRaceCalculator final {
- static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr<Transition>);
- static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr<Transition>);
- static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr<Transition>);
- static EventSet is_race_reversible(const Execution&, Execution::Handle e1, std::shared_ptr<Transition>);
+ static bool is_race_reversible_CommRecv(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_CommSend(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_CommWait(const Execution&, Execution::EventHandle e1, const Transition* e2);
+ static bool is_race_reversible_CommTest(const Execution&, Execution::EventHandle e1, const Transition* e2);
public:
- static EventSet is_race_reversible(const Execution&, Execution::Handle e1, Execution::Handle e2);
+ static bool is_race_reversible(const Execution&, Execution::EventHandle e1, Execution::EventHandle e2);
};
} // namespace simgrid::mc::odpor
namespace simgrid::mc::odpor {
-using PartialExecution = std::list<std::shared_ptr<Transition>>;
-using ExecutionSequence = std::list<const Transition*>;
+using PartialExecution = std::list<std::shared_ptr<Transition>>;
class Event;
class Execution;
+class ReversibleRaceCalculator;
class WakeupTree;
class WakeupTreeNode;
class WakeupTreeIterator;
