"parent with an empty wakeup tree. This indicates either that ODPOR "
"actor selection in State.cpp is incorrect, or that the code "
"deciding when to make subtrees in ODPOR is incorrect");
- xbt_assert((parent_state_->get_transition_out()->aid_ == min_process_node.value()->get_actor()) &&
- (parent_state_->get_transition_out()->type_ == min_process_node.value()->get_action()->type_),
+ xbt_assert((get_transition_in()->aid_ == min_process_node.value()->get_actor()) &&
+ (get_transition_in()->type_ == min_process_node.value()->get_action()->type_),
"We tried to make a subtree from a parent state who claimed to have executed `%s` "
"but whose wakeup tree indicates it should have executed `%s`. This indicates "
"that exploration is not following ODPOR. Are you sure you're choosing actors "
"to schedule from the wakeup tree?",
- parent_state_->get_transition_out()->to_string(false).c_str(),
+ get_transition_in()->to_string(false).c_str(),
min_process_node.value()->get_action()->to_string(false).c_str());
this->wakeup_tree_ = odpor::WakeupTree::make_subtree_rooted_at(min_process_node.value());
}
w_now.erase(action_by_p_in_w);
}
// Is `E ⊢ p ◇ w`?
- else if (E_v.is_independent_with_execution_of(w, next_E_p)) {
+ else if (E_v.is_independent_with_execution_of(w_now, next_E_p)) {
// INVARIANT: Note that it is impossible for `p` to be
// excluded from the set `I_[E](w)` BUT ALSO be contained in
// `w` itself if `E ⊢ p ◇ w` (intuitively, the fact that `E ⊢ p ◇ w`
REQUIRE_FALSE(execution.happens_before(3, 2));
}
}
+
+ SECTION("Example 3: Happens-before is transitively-closed")
+ {
+ // Given a reversible race between events `e1` and `e3` in a simulation,
+ // we assert that `e5` would be eliminated from being contained in
+ // the sequence `notdep(e1, E)`
+ const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+
+ Execution execution;
+ execution.push_transition(e0);
+ execution.push_transition(e1);
+ execution.push_transition(e2);
+ execution.push_transition(e3);
+ execution.push_transition(e4);
+
+ REQUIRE(execution.happens_before(0, 2));
+ REQUIRE(execution.happens_before(2, 4));
+ REQUIRE(execution.happens_before(0, 4));
+ }
}
TEST_CASE("simgrid::mc::odpor::Execution: Testing Racing Events and Initials")
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);
- const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
- const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ // In this example, `e0` and `e1` are lock actions that
+ // are in a race. We assert that
+ const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e2 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
Execution execution;
- execution.push_transition(a1);
- execution.push_transition(a2);
- execution.push_transition(a3);
- execution.push_transition(a4);
- execution.push_transition(a5);
-
+ execution.push_transition(e0);
+ execution.push_transition(e1);
+ execution.push_transition(e2);
+ execution.push_transition(e3);
+ execution.push_transition(e4);
REQUIRE(execution.get_racing_events_of(4) == std::unordered_set<Execution::EventHandle>{0});
}
}
}
-TEST_CASE("simgrid::mc::odpor::Execution: Testing Races and Conditions")
+TEST_CASE("simgrid::mc::odpor::Execution: notdep(e, E) Simulation")
{
- 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);
- const auto a4 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
- const auto a5 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ // Given a reversible race between events `e1` and `e3` in a simulation,
+ // we assert that `e5` would be eliminated from being contained in
+ // the sequence `notdep(e1, E)`
+ const auto e0 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
+ const auto e1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e2 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
+ const auto e3 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 1);
+ const auto e4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 3);
Execution execution;
- execution.push_transition(a1);
- execution.push_transition(a2);
- execution.push_transition(a3);
- execution.push_transition(a4);
- execution.push_transition(a5);
+ execution.push_transition(e0);
+ execution.push_transition(e1);
+ execution.push_transition(e2);
+ execution.push_transition(e3);
+ execution.push_transition(e4);
+
+ REQUIRE(execution.happens_before(0, 4));
}
TEST_CASE("simgrid::mc::odpor::Execution: Independence Tests")
REQUIRE(insertion.value() == PartialExecution{});
}
}
-
- SECTION("") {}
}
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;
+ xbt_die("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());
}
}
const auto a1 = std::make_shared<IndependentAction>(Transition::Type::UNKNOWN, 4);
const auto a2 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 1);
const auto a3 = std::make_shared<ConditionallyDependentAction>(Transition::Type::UNKNOWN, 4);
+ const auto a4 = std::make_shared<DependentAction>(Transition::Type::UNKNOWN, 2);
Execution execution;
execution.push_transition(a0);
execution.push_transition(a1);
execution.push_transition(a2);
execution.push_transition(a3);
+ execution.push_transition(a4);
REQUIRE(execution.get_racing_events_of(2) == std::unordered_set<Execution::EventHandle>{0});
REQUIRE(execution.get_racing_events_of(3) == std::unordered_set<Execution::EventHandle>{0});
// / /
// a0 a1
// / /
- // a3 a2
+ // a3 a4
//
// Recall that new nodes (in this case the one with
// action `a2`) are added such that they are "greater than" (under
// the tree's `<` relation) all those that exist under the given parent.
- tree.insert(Execution(), {a1, a2});
+ tree.insert(Execution(), {a1, a4});
test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
- PartialExecution{a1, a2}, PartialExecution{a1},
+ PartialExecution{a1, a4}, PartialExecution{a1},
PartialExecution{}});
}
+
+ SECTION("Inserting an equivalent sequence to a leaf should preserve the tree as-is")
+ {
+ // `a1.a2` is equivalent to `a1.a3` since `a2` and `a3` are independent
+ // (`E ⊢ p ◊ w` where `p := proc(a2)` and `w := a3`). Thus, the tree
+ // should now STILL look as follows:
+ //
+ // {}
+ // / /
+ // a0 a1
+ // /
+ // a3
+ //
+ // Recall that new nodes (in this case the one with
+ // action `a2`) are added such that they are "greater than" (under
+ // the tree's `<` relation) all those that exist under the given parent.
+ tree.insert(Execution(), {a1, a3});
+ test_tree_iterator(tree, std::vector<PartialExecution>{PartialExecution{a0}, PartialExecution{a1, a3},
+ PartialExecution{a1}, PartialExecution{}});
+ }
}
SECTION("Performing Arbitrary Insertions")
return ReductionMode::odpor;
} else if (cfg_mc_reduction.get() == "udpor") {
XBT_INFO("No reduction will be used: "
- "UDPOR is has a dedicated invocation 'model-check/unfolding-checker' "
- "but is not yet supported in SimGrid");
+ "UDPOR has a dedicated invocation 'model-check/unfolding-checker' "
+ "but is not yet fully supported in SimGrid");
return ReductionMode::none;
} else {
XBT_INFO("Unknown reduction mode: defaulting to no reduction");
