* This means there may be a way to store the list once and apply differences
* rather than repeating elements frequently.
*/
- std::vector<std::unique_ptr<Transition>> pending_transitions_;
+ std::vector<std::shared_ptr<Transition>> pending_transitions_;
/* Possible exploration status of an actor transition in a state.
* Either the checker did not consider the transition, or it was considered and still to do, or considered and
public:
ActorState(aid_t aid, bool enabled, unsigned int max_consider) : ActorState(aid, enabled, max_consider, {}) {}
- ActorState(aid_t aid, bool enabled, unsigned int max_consider, std::vector<std::unique_ptr<Transition>> transitions)
+ ActorState(aid_t aid, bool enabled, unsigned int max_consider, std::vector<std::shared_ptr<Transition>> transitions)
: pending_transitions_(std::move(transitions)), aid_(aid), max_consider_(max_consider), enabled_(enabled)
{
}
unsigned int do_consider()
{
if (max_consider_ <= times_considered_ + 1)
- set_done();
+ mark_done();
return times_considered_++;
}
unsigned int get_times_considered() const { return times_considered_; }
this->state_ = InterleavingType::todo;
this->times_considered_ = 0;
}
- void set_done() { this->state_ = InterleavingType::done; }
+ void mark_done() { this->state_ = InterleavingType::done; }
inline Transition* get_transition(unsigned times_considered)
{
}
}
+State::State(const RemoteApp& remote_app, const State* previous_state)
+ : default_transition_(std::make_unique<Transition>()), num_(++expended_states_)
+{
+
+ remote_app.get_actors_status(actors_to_run_);
+
+ transition_ = default_transition_.get();
+
+ /* Stateful model checking */
+ if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
+ system_state_ = std::make_shared<simgrid::mc::Snapshot>(num_);
+ }
+
+ /* For each actor in the previous sleep set, keep it if it is not dependent with current transition.
+ * And if we kept it and the actor is enabled in this state, mark the actor as already done, so that
+ * it is not explored*/
+ for (auto& [aid, transition] : previous_state->get_sleep_set()) {
+
+ if (not previous_state->get_transition()->depends(&transition)) {
+
+ sleep_set_.emplace(aid, transition);
+ if (actors_to_run_.count(aid) != 0) {
+ XBT_DEBUG("Actor %ld will not be explored, for it is in the sleep set", aid);
+
+ actors_to_run_.at(aid).mark_done();
+ }
+ } else
+ XBT_DEBUG("Transition >>%s<< removed from the sleep set because it was dependent with >>%s<<",
+ transition.to_string().c_str(), previous_state->get_transition()->to_string().c_str());
+ }
+}
+
std::size_t State::count_todo() const
{
return boost::range::count_if(this->actors_to_run_, [](auto& pair) { return pair.second.is_todo(); });
}
- void State::mark_all_todo()
+ void State::mark_all_enabled_todo()
{
- for (auto& [aid, actor] : actors_to_run_) {
-
- if (actor.is_enabled() and not actor.is_done() and not actor.is_todo())
- actor.mark_todo();
+ for (auto const& [aid, _] : this->get_actors_list()) {
- if (this->is_actor_enabled(aid)) {
++ if (this->is_actor_enabled(aid) and not is_actor_done(aid)) {
+ this->mark_todo(aid);
+ }
}
}
XBT_DEBUG("Search for an actor to run. %zu actors to consider", actors_to_run_.size());
for (auto const& [aid, actor] : actors_to_run_) {
/* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application */
- if (not actor.is_todo() || not actor.is_enabled())
+ if (not actor.is_todo() || not actor.is_enabled() || actor.is_done()) {
+
+ if (not actor.is_todo())
+ XBT_DEBUG("Can't run actor %ld because it is not todo", aid);
+
+ if (not actor.is_enabled())
+ XBT_DEBUG("Can't run actor %ld because it is not enabled", aid);
+
+ if (actor.is_done())
+ XBT_DEBUG("Can't run actor %ld because it has already been done", aid);
+
continue;
+ }
return aid;
}
/** Snapshot of system state (if needed) */
std::shared_ptr<Snapshot> system_state_;
+ /* Sleep sets are composed of the actor and the corresponding transition that made it being added to the sleep
+ * set. With this information, it is check whether it should be removed from it or not when exploring a new
+ * transition */
+ std::map<aid_t, Transition> sleep_set_;
+
public:
explicit State(const RemoteApp& remote_app);
-
+ explicit State(const RemoteApp& remote_app, const State* previous_state);
/* Returns a positive number if there is another transition to pick, or -1 if not */
aid_t next_transition() const;
long get_num() const { return num_; }
std::size_t count_todo() const;
void mark_todo(aid_t actor) { actors_to_run_.at(actor).mark_todo(); }
- void mark_done(aid_t actor) { actors_to_run_.at(actor).mark_done();}
- void mark_all_todo();
- bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
+ void mark_all_enabled_todo();
- bool is_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
++ bool is_actor_done(aid_t actor) const { return actors_to_run_.at(actor).is_done(); }
Transition* get_transition() const;
void set_transition(Transition* t) { transition_ = t; }
std::map<aid_t, ActorState> const& get_actors_list() const { return actors_to_run_; }
Snapshot* get_system_state() const { return system_state_.get(); }
void set_system_state(std::shared_ptr<Snapshot> state) { system_state_ = std::move(state); }
+ std::map<aid_t, Transition> const& get_sleep_set() const { return sleep_set_; }
+ void add_sleep_set(Transition* t) {sleep_set_.insert_or_assign(t->aid_, Transition(t->type_, t->aid_, t->times_considered_)); }
+
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
};
if (next < 0) { // If there is no more transition in the current state, backtrack.
XBT_DEBUG("There remains %lu actors, but none to interleave (depth %zu).", state->get_actor_count(),
stack_.size() + 1);
-
+
if (state->get_actor_count() == 0) {
mc_model_checker->finalize_app();
XBT_VERB("Execution came to an end at %s (state: %ld, depth: %zu)", get_record_trace().to_string().c_str(),
state->get_num(), stack_.size());
+
}
+
this->backtrack();
continue;
}
+ if (_sg_mc_sleep_set) {
+ XBT_VERB("Sleep set actually containing:");
+ for (auto & [aid, transition] : state->get_sleep_set()) {
+
+ XBT_VERB(" <%ld,%s>", aid, transition.to_string().c_str());
+
+ }
+ }
/* Actually answer the request: let's execute the selected request (MCed does one step) */
state->execute_next(next);
on_transition_execute_signal(state->get_transition(), get_remote_app());
state->get_transition()->to_string().c_str(), stack_.size(), state->get_num(), state->count_todo());
/* Create the new expanded state (copy the state of MCed into our MCer data) */
- auto next_state = std::make_unique<State>(get_remote_app());
+ std::unique_ptr<State> next_state;
+
+ /* If we want sleep set reduction, pass the old state to the new state so it can
+ * both copy the sleep set and eventually removes things from it locally */
+ if (_sg_mc_sleep_set)
+ next_state = std::make_unique<State>(get_remote_app(), state);
+ else
+ next_state = std::make_unique<State>(get_remote_app());
+
on_state_creation_signal(next_state.get(), get_remote_app());
+
if (_sg_mc_termination)
this->check_non_termination(next_state.get());
if (visited_state_ == nullptr) {
/* Get an enabled process and insert it in the interleave set of the next state */
for (auto const& [aid, _] : next_state->get_actors_list()) {
- if (next_state->is_actor_enabled(aid) and not next_state->is_done(aid)) {
- if (next_state->is_actor_enabled(aid)) {
++ if (next_state->is_actor_enabled(aid) and not next_state->is_actor_done(aid)) {
next_state->mark_todo(aid);
if (reduction_mode_ == ReductionMode::dpor)
break; // With DPOR, we take the first enabled transition
backtrack_count_++;
XBT_VERB("Backtracking from %s", get_record_trace().to_string().c_str());
on_backtracking_signal(get_remote_app());
- stack_.pop_back();
-
get_remote_app().check_deadlock();
+ /* We may backtrack from somewhere either because it's leaf, or because every enabled process are in done/sleep set.
+ * In the first case, we need to remove the last transition corresponding to the Finalize */
+ if (stack_.back()->get_transition()->aid_ == 0)
+ stack_.pop_back();
+
/* Traverse the stack backwards until a state with a non empty interleave set is found, deleting all the states that
* have it empty in the way. For each deleted state, check if the request that has generated it (from its
- * predecessor state), depends on any other previous request executed before it. If it does then add it to the
- * interleave set of the state that executed that previous request. */
+ * predecessor state) depends on any other previous request executed before it on another process. If there exists one,
+ * find the more recent, and add its process to the interleave set. If the process is not enabled at this point,
+ * then add every enabled process to the interleave */
bool found_backtracking_point = false;
while (not stack_.empty() && not found_backtracking_point) {
std::unique_ptr<State> state = std::move(stack_.back());
+
stack_.pop_back();
+
+ XBT_DEBUG("Marking Transition >>%s<< of process %ld done and adding it to the sleep set", state->get_transition()->to_string().c_str(), state->get_transition()->aid_);
+ state->add_sleep_set(state->get_transition()); // Actors are marked done when they are considerd in ActorState
+
if (reduction_mode_ == ReductionMode::dpor) {
aid_t issuer_id = state->get_transition()->aid_;
for (auto i = stack_.rbegin(); i != stack_.rend(); ++i) {
if (state->get_transition()->aid_ == prev_state->get_transition()->aid_) {
XBT_DEBUG("Simcall >>%s<< and >>%s<< with same issuer %ld", state->get_transition()->to_string().c_str(),
prev_state->get_transition()->to_string().c_str(), issuer_id);
- break;
+ continue;
} else if (prev_state->get_transition()->depends(state->get_transition())) {
XBT_VERB("Dependent Transitions:");
XBT_VERB(" %s (state=%ld)", prev_state->get_transition()->to_string().c_str(), prev_state->get_num());
XBT_VERB(" %s (state=%ld)", state->get_transition()->to_string().c_str(), state->get_num());
- if (not prev_state->is_done(issuer_id))
- prev_state->mark_todo(issuer_id);
- else
- XBT_DEBUG("Actor %ld is in done set", issuer_id);
+ if (prev_state->is_actor_enabled(issuer_id)){
- if (not prev_state->is_done(issuer_id))
++ if (not prev_state->is_actor_done(issuer_id))
+ prev_state->mark_todo(issuer_id);
+ else
+ XBT_DEBUG("Actor %ld is already in done set: no need to explore it again", issuer_id);
+ } else {
+ XBT_DEBUG("Actor %ld is not enabled: DPOR may be failing. To stay sound, we are marking every enabled transition as todo", issuer_id);
- prev_state->mark_all_todo();
++ prev_state->mark_all_enabled_todo();
+ }
break;
} else {
XBT_VERB("INDEPENDENT Transitions:");
}
}
- if (state->count_todo() == 0) { // Empty interleaving set
+ if (state->count_todo() == 0) { // Empty interleaving set: exploration at this level is over
XBT_DEBUG("Delete state %ld at depth %zu", state->get_num(), stack_.size() + 1);
} else {
- XBT_DEBUG("Back-tracking to state %ld at depth %zu", state->get_num(), stack_.size() + 1);
- stack_.push_back(std::move(state)); // Put it back on the stack
+ XBT_DEBUG("Back-tracking to state %ld at depth %zu: %lu transitions left to be explored", state->get_num(),
+ stack_.size() + 1, state->count_todo());
+ stack_.push_back(std::move(state)); // Put it back on the stack so we can explore the next transition of the interleave
found_backtracking_point = true;
}
}
