if (prev_state->is_actor_enabled(p)) {
// NOTE: To incorporate the idea of attempting to select the "best"
// backtrack point into SDPOR, instead of selecting the `first` initial,
- // we should instead compute all choices and decide which is bes
+ // we should instead compute all choices and decide which is best
const std::optional<aid_t> q =
execution_seq_.get_first_sdpor_initial_from(racing_event_handle, prev_state->get_backtrack_set());
if (q.has_value()) {
TEST_CASE("simgrid::mc::ClockVector: Constructing Vectors")
{
- ClockVector cv;
- REQUIRE(cv.size() == 0);
+ SECTION("Without values")
+ {
+ ClockVector cv;
+ REQUIRE(cv.size() == 0);
+
+ // Verify `cv` doesn't map any values
+ REQUIRE_FALSE(cv.get(0).has_value());
+ REQUIRE_FALSE(cv.get(1).has_value());
+ REQUIRE_FALSE(cv.get(2).has_value());
+ REQUIRE_FALSE(cv.get(3).has_value());
+ }
- // Verify `cv` doesn't map any values
- REQUIRE_FALSE(cv.get(0).has_value());
- REQUIRE_FALSE(cv.get(1).has_value());
- REQUIRE_FALSE(cv.get(2).has_value());
- REQUIRE_FALSE(cv.get(3).has_value());
+ SECTION("With initial values")
+ {
+ ClockVector cv{
+ {1, 5}, {3, 1}, {7, 10}, {6, 5}, {8, 1}, {10, 10},
+ };
+ REQUIRE(cv.size() == 6);
+
+ // Verify `cv` maps each value
+ REQUIRE(cv.get(1).has_value());
+ REQUIRE(cv.get(1).value() == 5);
+ REQUIRE(cv[1] == 5);
+ REQUIRE(cv.get(3).has_value());
+ REQUIRE(cv.get(3).value() == 1);
+ REQUIRE(cv[3] == 1);
+ REQUIRE(cv.get(7).has_value());
+ REQUIRE(cv.get(7).value() == 10);
+ REQUIRE(cv[7] == 10);
+ REQUIRE(cv.get(6).has_value());
+ REQUIRE(cv.get(6).value() == 5);
+ REQUIRE(cv[6] == 5);
+ REQUIRE(cv.get(8).has_value());
+ REQUIRE(cv.get(8).value() == 1);
+ REQUIRE(cv[8] == 1);
+ REQUIRE(cv.get(10).has_value());
+ REQUIRE(cv.get(10).value() == 10);
+ REQUIRE(cv[10] == 10);
+ }
}
TEST_CASE("simgrid::mc::ClockVector: Testing operator[]")
contents_.push_back(Event({t, max_clock_vector}));
}
-void Execution::pop_latest()
-{
- contents_.pop_back();
-}
-
std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
{
std::unordered_set<Execution::EventHandle> racing_events;
return std::nullopt;
}
+ // To actually compute `I_[E'](v) ∩ backtrack(E')`, we must
+ // first compute `E'` and "move" in the direction of `v`.
+ // We perform a scan over `E` (this execution) and make
+ // note of any events which occur after `e` but don't
+ // "happen-after" `e` by pushing them onto `E'`. Note that
+ // correctness is still preserved in computing `v` "on-the-fly"
+ // to determine if an actor `q` is an initial for `E'` after `v`:
+ // only those events that "occur-before" `v`
+ // could happen-before `v` for any valid happens-before relation.
+
// First, grab `E' := pre(e, E)` and determine what actor `p` is
// TODO: Instead of copying around these big structs, it
// would behoove us to incorporate some way to reference
/**
* @brief Computes the "core" portion the SDPOR algorithm,
* viz. the intersection of the backtracking set and the
- * set of initials with respect to the end
+ * set of initials with respect to the *last* event added
+ * to the execution
+ *
+ * The "core" portion of the SDPOR algorithm is found on
+ * lines 6-9 of the pseudocode:
+ *
+ * 6 | let E' := pre(E, e)
+ * 7 | let v := notdep(e, E).p
+ * 8 | if I_[E'](v) ∩ backtrack(E') = empty then
+ * 9 | --> add some q in I_[E'](v) to backtrack(E')
+ *
+ * This method computes all of the lines simultaneously,
+ * returning some actor `q` if it passes line 8 and exists.
+ * The event `e` and the set `backtrack(E')` are the provided
+ * arguments to the method.
+ *
+ * @param e the event with respect to which to determine
+ * whether a backtrack point needs to be added for the
+ * prefix corresponding to the execution prior to `e`
+ *
+ * @param backtrack_set The set of actors which should
+ * not be considered for selection as an SDPOR initial.
+ * While this set need not necessarily correspond to the
+ * backtrack set `backtrack(E')`, doing so provides what
+ * is expected for SDPOR
*
* See the SDPOR algorithm pseudocode in [1] for more
* details for the context of the function.
*
* @invariant: This method assumes that events `e` and
* `e' := get_latest_event_handle()` are in a *reversible* race
- * as is the case in SDPOR
+ * as is explicitly the case in SDPOR
*
* @returns an actor not contained in `disqualified` which
* can serve as an initial to reverse the race between `e`
* and `e'`
*/
- std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> disqualified) const;
+ std::optional<aid_t> get_first_sdpor_initial_from(EventHandle e, std::unordered_set<aid_t> backtrack_set) const;
/**
* @brief Determines the event associated with
*/
bool happens_before(EventHandle e1, EventHandle e2) const;
- /**
- * @brief Removes the last event of the execution,
- * if such an event exists
- *
- * @note: When you remove events from an execution, any views
- * of the execution referring to those removed events
- * become invalidated
- */
- void pop_latest();
-
/**
* @brief Extends the execution by one more step
*
SECTION("Example 3: Testing 'Lock' Example")
{
+ // In this example,
const auto a1 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
const auto a2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
const auto a3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{0});
}
+
+ SECTION("Example 4: Indirect Races")
+ {
+ const auto a0 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 6);
+ const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto a6 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a7 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto a8 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a9 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 2);
+
+ Execution execution;
+ execution.push_transition(a0.get());
+ execution.push_transition(a1.get());
+ execution.push_transition(a2.get());
+ execution.push_transition(a3.get());
+ execution.push_transition(a4.get());
+ execution.push_transition(a5.get());
+ execution.push_transition(a6.get());
+ execution.push_transition(a7.get());
+ execution.push_transition(a8.get());
+ execution.push_transition(a9.get());
+
+ // Nothing comes before event 0
+ REQUIRE(execution.get_racing_events_of(0) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 0 and 1 are independent
+ REQUIRE(execution.get_racing_events_of(1) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 1 and 2 are independent
+ REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{});
+
+ // Events 1 and 3 are independent; the rest are executed by the same actor
+ REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{});
+
+ // 1. Events 3 and 4 race
+ // 2. Events 2 and 4 do NOT race since 2 --> 3 --> 4
+ // 3. Events 1 and 4 do NOT race since 1 is independent of 4
+ // 4. Events 0 and 4 do NOT race since 0 --> 2 --> 4
+ REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{3});
+
+ // Events 4 and 5 race; and because everyone before 4 (including 3) either
+ // a) happens-before, b) races, or c) does not race with 4, 4 is the race
+ REQUIRE(execution.get_racing_events_of(5) == std::unordered_set<Execution::EventHandle>{4});
+
+ // The same logic that applied to event 5 applies to event 6
+ REQUIRE(execution.get_racing_events_of(6) == std::unordered_set<Execution::EventHandle>{5});
+
+ // The same logic applies, except that this time since events 6 and 7 are run
+ // by the same actor, they don'tt actually race with one another
+ REQUIRE(execution.get_racing_events_of(7) == std::unordered_set<Execution::EventHandle>{});
+
+ // Event 8 is independent with everything
+ REQUIRE(execution.get_racing_events_of(8) == std::unordered_set<Execution::EventHandle>{});
+
+ // Event 9 is independent with events 7 and 8; event 6, however, is in race with 9.
+ // The same logic above eliminates events before 6
+ REQUIRE(execution.get_racing_events_of(9) == std::unordered_set<Execution::EventHandle>{6});
+ }
}
\ No newline at end of file