{
XBT_VERB("Creating a guide for the state");
-
if (_sg_mc_strategy == "none")
strategy_ = std::make_shared<BasicStrategy>();
else if (_sg_mc_strategy == "max_match_comm")
else if (_sg_mc_strategy == "min_match_comm")
strategy_ = std::make_shared<MinMatchComm>();
else if (_sg_mc_strategy == "uniform") {
- xbt::random::set_mersenne_seed(_sg_mc_random_seed);
+ xbt::random::set_mersenne_seed(_sg_mc_random_seed);
strategy_ = std::make_shared<UniformStrategy>();
- }
- else
+ } else
THROW_IMPOSSIBLE;
remote_app.get_actors_status(strategy_->actors_to_run_);
strategy_ = std::make_shared<MaxMatchComm>();
else if (_sg_mc_strategy == "min_match_comm")
strategy_ = std::make_shared<MinMatchComm>();
- else if (_sg_mc_strategy == "uniform")
+ else if (_sg_mc_strategy == "uniform")
strategy_ = std::make_shared<UniformStrategy>();
else
THROW_IMPOSSIBLE;
{
// TODO: It would be better not to have such a flag.
if (has_initialized_wakeup_tree) {
+ XBT_DEBUG("Reached a node with the following initialized WuT:");
+ XBT_DEBUG("\n%s", wakeup_tree_.string_of_whole_tree().c_str());
+
return;
}
// TODO: Note that the next action taken by the actor may be updated
void State::sprout_tree_from_parent_state()
{
+
+ XBT_DEBUG("Initializing Wut with parent one:");
+ XBT_DEBUG("\n%s", parent_state_->wakeup_tree_.string_of_whole_tree().c_str());
+
+
xbt_assert(parent_state_ != nullptr, "Attempting to construct a wakeup tree for the root state "
"(or what appears to be, rather for state without a parent defined)");
const auto min_process_node = parent_state_->wakeup_tree_.get_min_single_process_node();
wakeup_tree_.remove_min_single_process_subtree();
}
+ void State::remove_subtree_at_aid(const aid_t proc) {
+ wakeup_tree_.remove_subtree_at_aid(proc);
+
+ }
+
odpor::WakeupTree::InsertionResult State::insert_into_wakeup_tree(const odpor::PartialExecution& pe,
const odpor::Execution& E)
{
* `N` running actor `p` of this state's wakeup tree
*/
void remove_subtree_using_current_out_transition();
+ void remove_subtree_at_aid(aid_t proc);
bool has_empty_tree() const { return this->wakeup_tree_.empty(); }
+ std::string string_of_wut() const { return this->wakeup_tree_.string_of_whole_tree(); }
+
/**
* @brief
*/
XBT_INFO("DFS exploration ended. %ld unique states visited; %lu backtracks (%lu transition replays, %lu states "
"visited overall)",
State::get_expanded_states(), backtrack_count_, Transition::get_replayed_transitions(),
- visited_states_count_);
+ visited_states_count_);
Exploration::log_state();
}
const aid_t next = reduction_mode_ == ReductionMode::odpor ? state->next_odpor_transition()
: std::get<0>(state->next_transition_guided());
+
if (next < 0 || not state->is_actor_enabled(next)) {
if (next >= 0) { // Actor is not enabled, then
XBT_INFO("Reduction %s wants to execute a disabled transition %s. If it's ODPOR, ReversibleRace is suboptimal.",
XBT_INFO("Current trace:");
for (auto elm : get_textual_trace())
XBT_ERROR("%s", elm.c_str());
+ // Remove the disabled transition from the wakeup tree so that ODPOR doesn't try it again
+ state->remove_subtree_at_aid(next);
+ state->add_sleep_set(state->get_actors_list().at(next).get_transition());
}
}
// If there is no more transition in the current state (or if ODPOR picked an actor that is not enabled --
XBT_DEBUG("\tPerformed ODPOR 'clean-up'. Sleep set has:");
for (const auto& [aid, transition] : state->get_sleep_set())
XBT_DEBUG("\t <%ld,%s>", aid, transition->to_string().c_str());
- if (not state->has_empty_tree()) {
- return state;
- }
}
return nullptr;
}
* ("eventually looks like C", viz. the `~_E` relation)
*/
for (auto e_prime = static_cast<odpor::Execution::EventHandle>(0); e_prime <= last_event.value(); ++e_prime) {
+ XBT_DEBUG("ODPOR: Now considering all possible race with `%u`", e_prime);
for (const auto e : execution_seq_.get_reversible_races_of(e_prime)) {
XBT_DEBUG("ODPOR: Reversible race detected between events `%u` and `%u`", e, e_prime);
State& prev_state = *stack_[e];
if (const auto v = execution_seq_.get_odpor_extension_from(e, e_prime, prev_state); v.has_value()) {
switch (prev_state.insert_into_wakeup_tree(v.value(), execution_seq_.get_prefix_before(e))) {
case odpor::WakeupTree::InsertionResult::root: {
- XBT_DEBUG("ODPOR: Reversible race with `%u` unaccounted for in the wakeup tree for "
- "the execution prior to event `%u`:",
- e_prime, e);
+ XBT_DEBUG("ODPOR: Reversible race with `%u`(%ld: %.20s) unaccounted for in the wakeup tree for "
+ "the execution prior to event `%u`(%ld: %.20s):",
+ e_prime, stack_[e_prime]->get_transition_out()->aid_,
+ stack_[e_prime]->get_transition_out()->to_string(true).c_str(), e,
+ prev_state.get_transition_out()->aid_,
+ prev_state.get_transition_out()->to_string(true).c_str());
break;
}
case odpor::WakeupTree::InsertionResult::interior_node: {
#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::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;
}
// then e_i --->_E target indirectly (either through
// e_j directly, or transitively through 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);
}
#include <xbt/asserts.h>
#include <xbt/ex.h>
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_odpor_reversible_race, mc_dfs, "ODPOR exploration algorithm of the model-checker");
+
namespace simgrid::mc::odpor {
+/**
+ The reversible race detector should only be used if we already have the assumption
+ e1 <* e2 (see Source set: a foundation for ODPOR). In particular this means that :
+ - e1 -->_E e2
+ - proc(e1) != proc(e2)
+ - there is no event e3 s.t. e1 --> e3 --> e2
+*/
+
bool ReversibleRaceCalculator::is_race_reversible(const Execution& E, Execution::EventHandle e1,
Execution::EventHandle e2)
{
bool ReversibleRaceCalculator::is_race_reversible_MutexWait(const Execution& E, Execution::EventHandle e1,
const Transition* /*e2*/)
{
- // TODO: Get the semantics correct here
- const auto e1_action = E.get_transition_for_handle(e1)->type_;
- return e1_action != Transition::Type::MUTEX_ASYNC_LOCK && e1_action != Transition::Type::MUTEX_UNLOCK;
+ // TODO: for now we over approximate the reversibility
+
+ return true;
}
bool ReversibleRaceCalculator::is_race_reversible_SemAsyncLock(const Execution&, Execution::EventHandle /*e1*/,
bool ReversibleRaceCalculator::is_race_reversible_SemWait(const Execution& E, Execution::EventHandle e1,
const Transition* /*e2*/)
{
- // Reversible with everynbody but unlock which creates a free token
+
const auto e1_transition = E.get_transition_for_handle(e1);
if (e1_transition->type_ == Transition::Type::SEM_UNLOCK &&
- static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1)
+ static_cast<const SemaphoreTransition*>(e1_transition)->get_capacity() <= 1) {
return false;
+ }
+ xbt_assert(false, "SEM_WAIT that is dependent with a SEM_UNLOCK should not be reversible. FixMe");
return true;
}
#include <memory>
#include <queue>
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_wut, mc, "Logging specific to ODPOR WakeupTrees");
+
namespace simgrid::mc::odpor {
void WakeupTreeNode::add_child(WakeupTreeNode* node)
node->parent_ = this;
}
+std::string WakeupTreeNode::string_of_whole_tree(int indentation_level) const
+{
+ std::string tabulations = "";
+ for (int i = 0; i < indentation_level; i++)
+ tabulations += " ";
+ std::string final_string = action_ == nullptr ? "<>\n"
+ : tabulations + "Actor " + std::to_string(action_->aid_) + ": " +
+ action_->to_string(true) + "\n";
+ for (auto node : children_)
+ final_string += node->string_of_whole_tree(indentation_level + 1);
+ return final_string;
+}
+
PartialExecution WakeupTreeNode::get_sequence() const
{
// TODO: Prevent having to compute this at the node level
return this->root_->children_.front();
}
+std::string WakeupTree::string_of_whole_tree() const
+{
+ return root_->string_of_whole_tree(0);
+}
+
WakeupTree WakeupTree::make_subtree_rooted_at(WakeupTreeNode* root)
{
// Perform a BFS search to perform a deep copy of the portion
}
}
+void WakeupTree::remove_subtree_at_aid(aid_t proc)
+{
+ for (const auto& child : root_->get_ordered_children())
+ if (child->get_actor() == proc) {
+ this->remove_subtree_rooted_at(child);
+ break;
+ }
+}
+
void WakeupTree::remove_min_single_process_subtree()
{
if (const auto node = get_min_single_process_node(); node.has_value()) {
std::shared_ptr<Transition> get_action() const { return action_; }
const std::list<WakeupTreeNode*>& get_ordered_children() const { return children_; }
+ std::string string_of_whole_tree(int indentation_level) const;
+
/** Insert a node `node` as a new child of this node */
void add_child(WakeupTreeNode* node);
};
std::vector<std::string> get_single_process_texts() const;
+ std::string string_of_whole_tree() const;
+
/**
* @brief Remove the subtree of the smallest (with respect
* to the tree's "<" relation) single-process node.
*/
void remove_min_single_process_subtree();
+ void remove_subtree_at_aid(aid_t proc);
+
/**
* @brief Whether or not this tree is considered empty
*
auto res = xbt::string_printf("WaitAny{ ");
for (auto const* t : transitions_)
res += t->to_string(verbose);
- res += " }";
+ res += " } (times considered = " + std::to_string(times_considered_) + ")";
return res;
}
bool WaitAnyTransition::depends(const Transition* other) const
std::string SemaphoreTransition::to_string(bool verbose) const
{
if (type_ == Type::SEM_ASYNC_LOCK || type_ == Type::SEM_UNLOCK)
- return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), capacity_, sem_);
+ return xbt::string_printf("%s(semaphore: %u, capacity: %u)", Transition::to_c_str(type_), sem_, capacity_);
if (type_ == Type::SEM_WAIT)
- return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), capacity_,
- sem_, granted_ ? "yes" : "no");
+ return xbt::string_printf("%s(semaphore: %u, capacity: %u, granted: %s)", Transition::to_c_str(type_), sem_,
+ capacity_,
+ granted_ ? "yes" : "no");
THROW_IMPOSSIBLE;
}
SemaphoreTransition::SemaphoreTransition(aid_t issuer, int times_considered, Type type, std::stringstream& stream)
if (type_ == Type::SEM_UNLOCK && other->type_ == Type::SEM_UNLOCK)
return false;
+ // UNLCOK indep with a WAIT if the semaphore had enought capacity anyway
+ if (type_ == Type::SEM_UNLOCK && capacity_ > 1 && other->type_ == Type::SEM_WAIT )
+ return false;
+
// WAIT indep WAIT:
// if both enabled (may happen in the initial value is sufficient), the ordering has no impact on the result.
// If only one enabled, the other won't be enabled by the first one.
if (type_ == Type::SEM_WAIT && other->type_ == Type::SEM_WAIT)
return false;
+
return true; // Other semaphore cases are dependent
}