namespace simgrid::mc::udpor {
-UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true)
-{
- // Initialize the map
-}
+UdporChecker::UdporChecker(const std::vector<char*>& args) : Exploration(args, true) {}
void UdporChecker::run()
{
const bool enabled_at_config_k = false;
if (enabled_at_config_k) {
- auto candidate_handle = std::make_unique<UnfoldingEvent>(maximal_subset, action);
- if (auto candidate_event = candidate_handle.get(); not unfolding.contains_event_equivalent_to(candidate_event)) {
- // This is a new event (i.e. one we haven't yet seen)
- unfolding.insert(std::move(candidate_handle));
- incremental_exC.insert(candidate_event);
- }
+ auto event = std::make_unique<UnfoldingEvent>(maximal_subset, action);
+ const auto handle = unfolding.insert(std::move(event));
+ incremental_exC.insert(handle);
}
}
return incremental_exC;
// check the invariant regardless as a sanity check
}
+Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {}
+
Configuration::Configuration(const EventSet& events) : events_(events)
{
if (!events_.is_valid_configuration()) {
throw std::invalid_argument("The events do not form a valid configuration");
}
-}
-Configuration::Configuration(const History& history) : Configuration(history.get_all_events()) {}
+ // Since we add in topological order under `<`, we know that the "most-recent"
+ // transition executed by each actor will appear last
+ for (const UnfoldingEvent* e : get_topologically_sorted_events()) {
+ this->latest_event_mapping[e->get_actor()] = e;
+ }
+}
void Configuration::add_event(const UnfoldingEvent* e)
{
}
this->events_.insert(e);
- this->newest_event = e;
+ this->newest_event = e;
+ this->latest_event_mapping[e->get_actor()] = e;
// Preserves the property that the configuration is causally closed
if (auto history = History(e); !this->events_.contains(history)) {
return Configuration(History(map_events(*alternative)));
}
+std::optional<const UnfoldingEvent*> Configuration::get_latest_event_of(aid_t aid) const
+{
+ if (const auto latest_event = latest_event_mapping.find(aid); latest_event != latest_event_mapping.end()) {
+ return std::optional<const UnfoldingEvent*>{latest_event->second};
+ }
+ return std::nullopt;
+}
+
+std::optional<const Transition*> Configuration::get_latest_action_of(aid_t aid) const
+{
+ if (const auto latest_event = get_latest_event_of(aid); latest_event.has_value()) {
+ return std::optional<const Transition*>{latest_event.value()->get_transition()};
+ }
+ return std::nullopt;
+}
+
} // namespace simgrid::mc::udpor
#include "src/mc/explo/udpor/udpor_forward.hpp"
#include <optional>
+#include <unordered_map>
namespace simgrid::mc::udpor {
*/
EventSet get_minimally_reproducible_events() const;
+ /**
+ * @brief Determines the event in the configuration whose associated
+ * transition is the latest of the given actor
+ *
+ * @invariant: At most one event in the configuration will correspond
+ * to `preEvt(C, a)` for any action `a`. This can be argued by contradiction.
+ *
+ * If there were more than one event (`e` and `e'`) in any configuration whose
+ * associated transitions `a` were run by the same actor at the same step, then they
+ * could not be causally related (`<`) since `a` could not be enabled in
+ * both subconfigurations C' and C'' containing the hypothetical events
+ * `e` and `e` + `e'`. Since they would not be contained in each other's histories,
+ * they would be in conflict, which cannot happen between any pair of events
+ * in a configuration. Thus `e` and `e'` cannot exist simultaneously
+ */
+ std::optional<const UnfoldingEvent*> get_latest_event_of(aid_t) const;
+ /**
+ * @brief Determines the most recent transition of the given actor
+ * in this configuration, or `pre(a)` as denoted in the thesis of
+ * The Anh Pham
+ *
+ * Conceptually, the execution of an interleaving of the transitions
+ * (i.e. a topological ordering) of a configuration yields a unique
+ * state `state(C)`. Since actions taken by the same actor are always
+ * dependent with one another, any such interleaving always yields a
+ * unique
+ *
+ * @returns the most recent transition of the given actor
+ * in this configuration, or `std::nullopt` if there are no transitions
+ * in this configuration run by the given actor
+ */
+ std::optional<const Transition*> get_latest_action_of(aid_t aid) const;
+ std::optional<const UnfoldingEvent*> pre_event(aid_t aid) const { return get_latest_event_of(aid); }
+
private:
/**
* @brief The most recent event added to the configuration
*
* @invariant For each event `e` in `events_`, the set of
* dependencies of `e` is also contained in `events_`
+ *
+ * @invariant For each pair of events `e` and `e'` in
+ * `events_`, `e` and `e'` are not in conflict
*/
EventSet events_;
+
+ /**
+ * @brief Maps actors to the latest events which
+ * are executed by the actor
+ *
+ * @invariant: The events that are contained in the map
+ * are also contained in the set `events_`
+ */
+ std::unordered_map<aid_t, const UnfoldingEvent*> latest_event_mapping;
};
} // namespace simgrid::mc::udpor
#include <unordered_map>
+using namespace simgrid::mc;
using namespace simgrid::mc::udpor;
TEST_CASE("simgrid::mc::udpor::Configuration: Constructing Configurations")
// then `e4`, and then `e7`
Unfolding U;
- auto e0 = std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<ConditionallyDependentAction>());
+ auto e0 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 0));
auto e0_handle = e0.get();
- auto e1 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<DependentAction>());
+ auto e1 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
auto e1_handle = e1.get();
- auto e2 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e2 = std::make_unique<UnfoldingEvent>(
+ EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
auto e2_handle = e2.get();
- auto e3 = std::make_unique<UnfoldingEvent>(EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e3 = std::make_unique<UnfoldingEvent>(
+ EventSet({e1_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
auto e3_handle = e3.get();
- auto e4 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e4 = std::make_unique<UnfoldingEvent>(
+ EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
auto e4_handle = e4.get();
- auto e5 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle}), std::make_shared<DependentAction>());
+ auto e5 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
auto e5_handle = e5.get();
- auto e6 = std::make_unique<UnfoldingEvent>(EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e6 = std::make_unique<UnfoldingEvent>(
+ EventSet({e5_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
auto e6_handle = e6.get();
- auto e7 = std::make_unique<UnfoldingEvent>(EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e7 = std::make_unique<UnfoldingEvent>(
+ EventSet({e0_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2));
auto e7_handle = e7.get();
- auto e8 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}), std::make_shared<DependentAction>());
+ auto e8 = std::make_unique<UnfoldingEvent>(EventSet({e4_handle, e7_handle}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
auto e8_handle = e8.get();
- auto e9 = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}), std::make_shared<DependentAction>());
+ auto e9 = std::make_unique<UnfoldingEvent>(EventSet({e7_handle}),
+ std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 0));
auto e9_handle = e9.get();
- auto e10 = std::make_unique<UnfoldingEvent>(EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>());
+ auto e10 = std::make_unique<UnfoldingEvent>(
+ EventSet({e9_handle}), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1));
auto e10_handle = e10.get();
SECTION("Alternative computation call 1")
this->event_handles.remove(e);
}
-void Unfolding::insert(std::unique_ptr<UnfoldingEvent> e)
+const UnfoldingEvent* Unfolding::insert(std::unique_ptr<UnfoldingEvent> e)
{
const UnfoldingEvent* handle = e.get();
if (auto loc = this->global_events_.find(handle); loc != this->global_events_.end()) {
"This will result in a double free error and must be fixed.");
}
- // Map the handle to its owner
+ if (auto loc = this->find_equivalent(handle); loc != this->end()) {
+ // There's already an event in the unfolding that is semantically
+ // equivalent. Return the handle to that event and ignore adding in
+ // a duplicate event
+ return *loc;
+ }
+
this->event_handles.insert(handle);
this->global_events_[handle] = std::move(e);
-}
-
-bool Unfolding::contains_event_equivalent_to(const UnfoldingEvent* e) const
-{
- // Notice the use of `==` equality here. `e` may not be contained in the
- // unfolding; but some event which is "equivalent" to it could be.
- for (const auto event : *this) {
- if (*event == *e) {
- return true;
- }
- }
- return false;
+ return handle;
}
EventSet Unfolding::get_immediate_conflicts_of(const UnfoldingEvent* e) const
namespace simgrid::mc::udpor {
class Unfolding {
+public:
+ Unfolding() = default;
+ Unfolding& operator=(Unfolding&&) = default;
+ Unfolding(Unfolding&&) = default;
+
+ auto begin() const { return this->event_handles.begin(); }
+ auto end() const { return this->event_handles.end(); }
+ auto cbegin() const { return this->event_handles.cbegin(); }
+ auto cend() const { return this->event_handles.cend(); }
+ size_t size() const { return this->event_handles.size(); }
+ bool empty() const { return this->event_handles.empty(); }
+
+ void remove(const UnfoldingEvent* e);
+ void remove(const EventSet& events);
+
+ /// @brief Adds a new event `e` to the Unfolding if that
+ /// event is not equivalent to any of those already contained
+ /// in the unfolding
+ const UnfoldingEvent* insert(std::unique_ptr<UnfoldingEvent> e);
+
+ /// @brief Computes "#ⁱ_U(e)" for the given event
+ EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
+
private:
/**
* @brief All of the events that are currently are a part of the unfolding
*/
EventSet G;
-public:
- Unfolding() = default;
- Unfolding& operator=(Unfolding&&) = default;
- Unfolding(Unfolding&&) = default;
-
- void remove(const UnfoldingEvent* e);
- void remove(const EventSet& events);
- void insert(std::unique_ptr<UnfoldingEvent> e);
- bool contains_event_equivalent_to(const UnfoldingEvent* e) const;
-
- auto begin() const { return this->event_handles.begin(); }
- auto end() const { return this->event_handles.end(); }
- auto cbegin() const { return this->event_handles.cbegin(); }
- auto cend() const { return this->event_handles.cend(); }
- size_t size() const { return this->global_events_.size(); }
- bool empty() const { return this->global_events_.empty(); }
-
- /// @brief Computes "#ⁱ_U(e)" for the given event
- EventSet get_immediate_conflicts_of(const UnfoldingEvent*) const;
+ auto find_equivalent(const UnfoldingEvent* e)
+ {
+ return std::find_if(begin(), end(), [=](const UnfoldingEvent* e_i) { return *e == *e_i; });
+ }
};
} // namespace simgrid::mc::udpor
const EventSet& get_immediate_causes() const { return this->immediate_causes; }
Transition* get_transition() const { return this->associated_transition.get(); }
+ aid_t get_actor() const { return get_transition()->aid_; }
bool operator==(const UnfoldingEvent&) const;
bool operator!=(const UnfoldingEvent& other) const { return not(*this == other); }
TEST_CASE("simgrid::mc::udpor::Unfolding: Inserting and removing events with an unfolding")
{
Unfolding unfolding;
- auto e1 = std::make_unique<UnfoldingEvent>();
- auto e2 = std::make_unique<UnfoldingEvent>();
+ auto e1 = std::make_unique<UnfoldingEvent>(
+ EventSet(), std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 0));
+ auto e2 =
+ std::make_unique<UnfoldingEvent>(EventSet(), std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1));
const auto e1_handle = e1.get();
const auto e2_handle = e2.get();
REQUIRE(unfolding.empty());
}
-TEST_CASE("simgrid::mc::udpor::Unfolding: Checking for semantically equivalent events")
-{
- Unfolding unfolding;
- auto e1 = std::make_unique<UnfoldingEvent>(
- EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
- auto e2 = std::make_unique<UnfoldingEvent>(
- EventSet(), std::make_shared<IndependentAction>(Transition::Type::BARRIER_ASYNC_LOCK, 6, 2));
-
- // e1 and e2 are equivalent
- REQUIRE(*e1 == *e2);
-
- const auto e1_handle = e1.get();
- const auto e2_handle = e2.get();
- unfolding.insert(std::move(e1));
-
- REQUIRE(unfolding.contains_event_equivalent_to(e1_handle));
- REQUIRE(unfolding.contains_event_equivalent_to(e2_handle));
-}
-
TEST_CASE("simgrid::mc::udpor::Unfolding: Checking all immediate conflicts restricted to an unfolding") {}
\ No newline at end of file
#ifndef SIMGRID_MC_UDPOR_FORWARD_HPP
#define SIMGRID_MC_UDPOR_FORWARD_HPP
+#include "src/mc/mc_forward.hpp"
+#include <simgrid/forward.h>
+
namespace simgrid::mc::udpor {
+class Comb;
+class ExtensionSetCalculator;
class EventSet;
class Configuration;
class History;
struct IndependentAction : public Transition {
IndependentAction() = default;
- IndependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+ IndependentAction(Type type, aid_t issuer, int times_considered = 0) : Transition(type, issuer, times_considered) {}
// Independent with everyone else
bool depends(const Transition* other) const override { return false; }
struct DependentAction : public Transition {
DependentAction() = default;
- DependentAction(Type type, aid_t issuer, int times_considered) : Transition(type, issuer, times_considered) {}
+ DependentAction(Type type, aid_t issuer, int times_considered = 0) : Transition(type, issuer, times_considered) {}
// Dependent with everyone else (except IndependentAction)
bool depends(const Transition* other) const override
struct ConditionallyDependentAction : public Transition {
ConditionallyDependentAction() = default;
- ConditionallyDependentAction(Type type, aid_t issuer, int times_considered)
+ ConditionallyDependentAction(Type type, aid_t issuer, int times_considered = 0)
: Transition(type, issuer, times_considered)
{
}
