#include <limits>
#include <vector>
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_execution, mc_dfs, "ODPOR exploration algorithm of the model-checker");
+
namespace simgrid::mc::odpor {
std::vector<std::string> get_textual_trace(const PartialExecution& w)
{
std::vector<std::string> trace;
for (const auto& t : w) {
- const auto a = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
- trace.push_back(std::move(a));
+ auto a = xbt::string_printf("Actor %ld: %s", t->aid_, t->to_string(true).c_str());
+ trace.emplace_back(std::move(a));
}
return trace;
}
+Execution::Execution(const PartialExecution& w)
+{
+ push_partial_execution(w);
+}
+
void Execution::push_transition(std::shared_ptr<Transition> t)
{
if (t == nullptr) {
contents_.push_back(Event({std::move(t), max_clock_vector}));
}
+void Execution::push_partial_execution(const PartialExecution& w)
+{
+ for (const auto& t : w) {
+ push_transition(t);
+ }
+}
+
std::vector<std::string> Execution::get_textual_trace() const
{
std::vector<std::string> trace;
for (const auto& t : this->contents_) {
- const auto a =
- xbt::string_printf("Actor %ld: %s", t.get_transition()->aid_, t.get_transition()->to_string(true).c_str());
- trace.push_back(std::move(a));
+ auto a = xbt::string_printf("Actor %ld: %s", t.get_transition()->aid_, t.get_transition()->to_string(true).c_str());
+ trace.emplace_back(std::move(a));
}
return trace;
}
std::unordered_set<Execution::EventHandle> Execution::get_racing_events_of(Execution::EventHandle target) const
{
std::unordered_set<Execution::EventHandle> racing_events;
+ // This keep tracks of events that happens-before the target
std::unordered_set<Execution::EventHandle> disqualified_events;
// For each event of the execution
for (auto e_i = target; e_i != std::numeric_limits<Execution::EventHandle>::max(); e_i--) {
// We need `e_i -->_E target` as a necessary condition
if (not happens_before(e_i, target)) {
+ XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` discarded because `%u` --\\-->_E `%u`", target, e_i, e_i, target);
continue;
}
// Further, `proc(e_i) != proc(target)`
if (get_actor_with_handle(e_i) == get_actor_with_handle(target)) {
disqualified_events.insert(e_i);
+ XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because proc(`%u`)=proc(`%u`)", target, e_i, e_i,
+ target);
continue;
}
// 2. disqualified_events.count(e_j) > 0
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through e_j)
- if (disqualified_events.count(e_j) > 0 and happens_before(e_i, e_j)) {
+ if (disqualified_events.count(e_j) > 0 && happens_before(e_i, e_j)) {
+ XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` disqualified because `%u` happens-between `%u`-->`%u`-->`%u`)",
+ target, e_i, e_j, e_i, e_j, target);
disqualified_events.insert(e_i);
break;
}
// it (since this would transitively make it the event
// which "happens-between" `target` and `e`)
if (disqualified_events.count(e_i) == 0) {
+ XBT_DEBUG("ODPOR_RACING_EVENTS with `%u` : `%u` is a valid racing event", target, e_i);
racing_events.insert(e_i);
disqualified_events.insert(e_i);
}
// happen after `e` is a member of `v`. In addition to marking
// the event in `v`, we also "simulate" running the action `v`
// from E'
- if (not happens_before(e, e_prime) or e_prime == next_E_p) {
+ if (not happens_before(e, e_prime) || e_prime == next_E_p) {
// First, push the transition onto the hypothetical execution
E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
}
}
}
- xbt_assert(!I_E_prime_v.empty(),
+ xbt_assert(not I_E_prime_v.empty(),
"For any non-empty execution, we know that "
"at minimum one actor is an initial since "
"some execution is possible with respect to a "
if (disqualified_actors.count(q) > 0) { // Did we already note that `q` is not an initial?
continue;
}
- const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_star) {
- return E_prime_v.happens_before(e_star, e_star_in_E_prime_v);
+ const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+ return E_prime_v.happens_before(handle, e_star_in_E_prime_v);
});
if (is_initial) {
// If the sleep set already contains `q`, we're done:
//
// Note the form of `v` in the pseudocode:
// `v := notdep(e, E).e'^
- {
- E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
- v.push_back(get_event_with_handle(e_prime).get_transition());
-
- const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
- v_handles.push_back(e_prime_in_E_prime_v);
-
- const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& e_star) {
- return E_prime_v.happens_before(e_star, e_prime_in_E_prime_v);
- });
- if (is_initial) {
- if (const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); sleep_E_prime.count(q) > 0) {
- return std::nullopt;
- } else {
- WI_E_prime_v.insert(q);
- }
+ E_prime_v.push_transition(get_event_with_handle(e_prime).get_transition());
+ v.push_back(get_event_with_handle(e_prime).get_transition());
+
+ const EventHandle e_prime_in_E_prime_v = E_prime_v.get_latest_event_handle().value();
+ v_handles.push_back(e_prime_in_E_prime_v);
+
+ const bool is_initial = std::none_of(v_handles.begin(), v_handles.end(), [&](const auto& handle) {
+ return E_prime_v.happens_before(handle, e_prime_in_E_prime_v);
+ });
+ if (is_initial) {
+ if (const aid_t q = E_prime_v.get_actor_with_handle(e_prime_in_E_prime_v); sleep_E_prime.count(q) > 0) {
+ return std::nullopt;
+ } else {
+ WI_E_prime_v.insert(q);
}
}
- {
- const Execution pre_E_e = get_prefix_before(e);
- const auto sleeping_actors = state_at_e.get_sleeping_actors();
-
- // Check if any enabled actor independent with this execution after `v`
- // is contained in the sleep set
- for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
- // TODO: We have to be able to react appropriately here when adding new
- // types of transitions (multiple choices can be made :( )
- if (astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition(0))) {
- if (sleeping_actors.count(aid) > 0) {
- return std::nullopt;
- }
- }
- }
+
+ const Execution pre_E_e = get_prefix_before(e);
+ const auto sleeping_actors = state_at_e.get_sleeping_actors();
+
+ // Check if any enabled actor that is independent with
+ // this execution after `v` is contained in the sleep set
+ for (const auto& [aid, astate] : state_at_e.get_actors_list()) {
+ const bool is_in_WI_E =
+ astate.is_enabled() and pre_E_e.is_independent_with_execution_of(v, astate.get_transition());
+ const bool is_in_sleep_set = sleeping_actors.count(aid) > 0;
+
+ // `action(aid)` is in `WI_[E](v)` but also is contained in the sleep set.
+ // This implies that the intersection between the two is non-empty
+ if (is_in_WI_E && is_in_sleep_set)
+ return std::nullopt;
}
+
return v;
}
auto w_now = w;
for (const auto& next_E_p : v) {
- const aid_t p = next_E_p->aid_;
-
// Is `p in `I_[E](w)`?
- if (E_v.is_initial_after_execution_of(w_now, p)) {
+ if (const aid_t p = next_E_p->aid_; E_v.is_initial_after_execution_of(w_now, p)) {
// Remove `p` from w and continue
- // TODO: If `p` occurs in `w`, it had better refer to the same
+ // INVARIANT: If `p` occurs in `w`, it had better refer to the same
// transition referenced by `v`. Unfortunately, we have two
// sources of truth here which can be manipulated at the same
// time as arguments to the function. If ODPOR works correctly,
return false;
}
-} // namespace simgrid::mc::odpor
\ No newline at end of file
+} // namespace simgrid::mc::odpor
