} // namespace kernel
namespace mc {
class CommunicationDeterminismChecker;
+class State;
}
} // namespace simgrid
#include "src/mc/Transition.hpp"
#include "src/mc/ModelChecker.hpp"
#include "src/mc/Session.hpp"
+#include "src/mc/mc_state.hpp"
+#include "src/mc/remote/RemoteProcess.hpp"
#include "xbt/asserts.h"
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_transition, mc, "Logging specific to MC transitions");
+
namespace simgrid {
namespace mc {
unsigned long Transition::executed_transitions_ = 0;
return textual_;
}
-RemotePtr<simgrid::kernel::actor::SimcallObserver> Transition::execute()
+RemotePtr<simgrid::kernel::actor::SimcallObserver> Transition::execute(simgrid::mc::State* state, int next)
{
+ std::vector<ActorInformation>& actors = mc_model_checker->get_remote_process().actors();
+
+ kernel::actor::ActorImpl* actor = actors[next].copy.get_buffer();
+ aid_t aid = actor->get_pid();
+
+ simgrid::mc::ActorState* actor_state = &state->actor_states_[aid];
+ /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */
+ if (actor->simcall_.observer_ != nullptr) {
+ state->transition_.times_considered_ = actor_state->get_times_considered_and_inc();
+ if (actor->simcall_.mc_max_consider_ <= actor_state->get_times_considered())
+ actor_state->set_done();
+ } else {
+ state->transition_.times_considered_ = 0;
+ actor_state->set_done();
+ }
+
+ aid_ = aid;
+ state->executed_req_ = actor->simcall_;
+
textual_ = mc_model_checker->simcall_to_string(aid_, times_considered_);
+ XBT_DEBUG("Let's run actor %ld, going for transition %s", aid, textual_.c_str());
+
+ return replay();
+}
+RemotePtr<simgrid::kernel::actor::SimcallObserver> Transition::replay()
+{
executed_transitions_++;
simgrid::mc::RemotePtr<simgrid::kernel::actor::SimcallObserver> res = mc_model_checker->handle_simcall(*this);
return res;
}
+
} // namespace mc
} // namespace simgrid
int times_considered_ = 0;
std::string to_string();
- RemotePtr<simgrid::kernel::actor::SimcallObserver> execute();
+ /* Explore a new path */
+ RemotePtr<simgrid::kernel::actor::SimcallObserver> execute(simgrid::mc::State* state, int next);
+ /* Moves the application toward a path that was already explored, but don't change the current transition */
+ RemotePtr<simgrid::kernel::actor::SimcallObserver> replay();
+
+ /* Returns the total amount of transitions executed so far (for statistics) */
static unsigned long get_executed_transitions() { return executed_transitions_; }
};
simgrid::mc::dumpRecordPath();
}
-/* Search for an enabled transition amongst actors
- *
- * This is the first actor marked TODO by the checker, and currently enabled in the application.
- *
- * Once we found it, prepare its execution (increase the times_considered of its observer and remove it as done on need)
- *
- * If we can't find any actor, return false
- */
-
-bool Api::mc_state_choose_request(simgrid::mc::State* state) const
-{
- RemoteProcess& process = mc_model_checker->get_remote_process();
- XBT_DEBUG("Search for an actor to run. %zu actors to consider", process.actors().size());
- for (auto& actor_info : process.actors()) {
- auto actor = actor_info.copy.get_buffer();
- simgrid::mc::ActorState* actor_state = &state->actor_states_[actor->get_pid()];
-
- /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application*/
- if (not actor_state->is_todo() || not simgrid::mc::actor_is_enabled(actor))
- continue;
-
- /* This actor is ready to be executed. Prepare its execution when simcall_handle will be called on it */
- if (actor->simcall_.observer_ != nullptr) {
- state->transition_.times_considered_ = actor_state->get_times_considered_and_inc();
- if (actor->simcall_.mc_max_consider_ <= actor_state->get_times_considered())
- actor_state->set_done();
- } else {
- state->transition_.times_considered_ = 0;
- actor_state->set_done();
- }
-
- state->transition_.aid_ = actor->get_pid();
- state->executed_req_ = actor->simcall_;
-
- XBT_DEBUG("Let's run actor %ld, going for transition %s", actor->get_pid(),
- SIMIX_simcall_name(state->executed_req_));
- return true;
- }
- return false;
-}
-
std::string Api::request_get_dot_output(aid_t aid, int value) const
{
const char* color = get_color(aid - 1);
void mc_check_deadlock() const;
XBT_ATTRIB_NORETURN void mc_exit(int status) const;
void dump_record_path() const;
- bool mc_state_choose_request(simgrid::mc::State* state) const;
// SIMCALL APIs
bool requests_are_dependent(RemotePtr<kernel::actor::SimcallObserver> obs1,
/* TODO : handle test and testany simcalls */
CallType call = MC_get_call_type(req);
- state->transition_.execute();
+ state->transition_.replay();
handle_comm_pattern(call, req, req_num, 1);
/* Update statistics */
/* Update statistics */
api::get().mc_inc_visited_states();
- bool found_transition = false;
+ int next_transition = -1;
if (stack_.size() <= (std::size_t)_sg_mc_max_depth)
- found_transition = api::get().mc_state_choose_request(cur_state);
+ next_transition = cur_state->next_transition();
+
+ if (next_transition >= 0 && visited_state == nullptr) {
+ cur_state->transition_.execute(cur_state, next_transition);
- if (found_transition && visited_state == nullptr) {
aid_t aid = cur_state->transition_.aid_;
int req_num = cur_state->transition_.times_considered_;
smx_simcall_t req = &cur_state->executed_req_;
if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
call = MC_get_call_type(req);
- /* Answer the request */
- cur_state->transition_.execute();
- /* After this call req is no longer useful */
-
handle_comm_pattern(call, req, req_num, 0);
/* Create the new expanded state */
std::shared_ptr<State> state = pair->graph_state;
if (pair->exploration_started) {
- state->transition_.execute();
+ state->transition_.replay();
XBT_DEBUG("Replay (depth = %d) : %s (%p)", depth, state->transition_.to_string().c_str(), state.get());
}
}
}
- api::get().mc_state_choose_request(current_pair->graph_state.get());
- aid_t aid = current_pair->graph_state->transition_.aid_;
- int req_num = current_pair->graph_state->transition_.times_considered_;
+ int next = current_pair->graph_state->next_transition();
+
+ current_pair->graph_state->transition_.execute(current_pair->graph_state.get(), next);
+
+ aid_t aid = current_pair->graph_state->transition_.aid_;
+ int req_num = current_pair->graph_state->transition_.times_considered_;
+ XBT_DEBUG("Execute: %s", current_pair->graph_state->transition_.to_string().c_str());
if (dot_output != nullptr) {
if (this->previous_pair_ != 0 && this->previous_pair_ != current_pair->num) {
fflush(dot_output);
}
- current_pair->graph_state->transition_.execute();
- XBT_DEBUG("Execute: %s", current_pair->graph_state->transition_.to_string().c_str());
-
if (not current_pair->exploration_started)
visited_pairs_count_++;
continue;
}
- // Search for the next transition. If found, state is modified accordingly (transition and executed_req are set)
- // If there is no more transition in the current state, backtrack.
+ // Search for the next transition
+ int next = state->next_transition();
- if (not api::get().mc_state_choose_request(state)) {
+ if (next < 0) { // If there is no more transition in the current state, backtrack.
XBT_DEBUG("There remains %zu actors, but none to interleave (depth %zu).",
mc_model_checker->get_remote_process().actors().size(), stack_.size() + 1);
}
/* Actually answer the request: let execute the selected request (MCed does one step) */
- auto remote_observer = state->transition_.execute();
+ auto remote_observer = state->transition_.execute(state, next);
// If there are processes to interleave and the maximum depth has not been
// reached then perform one step of the exploration algorithm.
for (std::unique_ptr<State> const& state : stack_) {
if (state == stack_.back())
break;
- state->transition_.execute();
+ state->transition_.replay();
/* Update statistics */
api::get().mc_inc_visited_states();
}
* under the terms of the license (GNU LGPL) which comes with this package. */
#include "src/mc/mc_state.hpp"
-#include "src/mc/mc_config.hpp"
+#include "src/mc/Session.hpp"
#include "src/mc/api.hpp"
+#include "src/mc/mc_config.hpp"
#include <boost/range/algorithm.hpp>
+XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_state, mc, "Logging specific to MC states");
+
using simgrid::mc::remote;
using api = simgrid::mc::Api;
return this->transition_;
}
+int State::next_transition() const
+{
+ std::vector<ActorInformation>& actors = mc_model_checker->get_remote_process().actors();
+ XBT_DEBUG("Search for an actor to run. %zu actors to consider", actors.size());
+ for (unsigned int i = 0; i < actors.size(); i++) {
+ aid_t aid = actors[i].copy.get_buffer()->get_pid();
+ const ActorState* actor_state = &actor_states_[aid];
+
+ /* Only consider actors (1) marked as interleaving by the checker and (2) currently enabled in the application*/
+ if (not actor_state->is_todo() || not simgrid::mc::session_singleton->actor_is_enabled(aid))
+ continue;
+
+ return i;
+ }
+ return -1;
+}
+
void State::copy_incomplete_comm_pattern()
{
incomplete_comm_pattern_.clear();
explicit State(unsigned long state_number);
+ /* Returns a positive number if there is another transition to pick, or -1 if not */
+ int next_transition() const;
+
std::size_t count_todo() const;
void mark_todo(aid_t actor) { this->actor_states_[actor].mark_todo(); }
Transition get_transition() const;
