if ((_sg_mc_checkpoint > 0 && (num_ % _sg_mc_checkpoint == 0)) || _sg_mc_termination) {
auto snapshot_ptr = api::get().take_snapshot(num_);
system_state_ = std::shared_ptr<simgrid::mc::Snapshot>(snapshot_ptr);
- if (_sg_mc_comms_determinism || _sg_mc_send_determinism) {
- copy_incomplete_comm_pattern();
- copy_index_comm_pattern();
- }
}
}
transition_.reset(mc_model_checker->handle_simcall(aid, times_considered, true));
mc_model_checker->wait_for_requests();
}
-
-void State::copy_incomplete_comm_pattern()
-{
- incomplete_comm_pattern_.clear();
- const unsigned long maxpid = api::get().get_maxpid();
- for (unsigned long i = 0; i < maxpid; i++) {
- std::vector<simgrid::mc::PatternCommunication> res;
- for (auto const& comm : incomplete_communications_pattern[i])
- res.push_back(comm->dup());
- incomplete_comm_pattern_.push_back(std::move(res));
- }
-}
-
-void State::copy_index_comm_pattern()
-{
- communication_indices_.clear();
- for (auto const& list_process_comm : initial_communications_pattern)
- this->communication_indices_.push_back(list_process_comm.index_comm);
-}
-
} // namespace mc
} // namespace simgrid
namespace mc {
/* A node in the exploration graph (kind-of) */
-class XBT_PRIVATE State {
+class XBT_PRIVATE State : public xbt::Extendable<State> {
static long expended_states_; /* Count total amount of states, for stats */
/* Outgoing transition: what was the last transition that we took to leave this state? Useful for replay */
/** Snapshot of system state (if needed) */
std::shared_ptr<simgrid::mc::Snapshot> system_state_;
- // For CommunicationDeterminismChecker
- std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;
- std::vector<unsigned> communication_indices_;
-
/* Returns a positive number if there is another transition to pick, or -1 if not */
int next_transition() const;
- /* Explore a new path */
+ /* Explore a new path; the parameter must be the result of a previous call to next_transition() */
void execute_next(int next);
std::size_t count_todo() const;
/* Returns the total amount of states created so far (for statistics) */
static long get_expanded_states() { return expended_states_; }
-
-private:
- void copy_incomplete_comm_pattern();
- void copy_index_comm_pattern();
};
} // namespace mc
} // namespace simgrid
/********** Static functions ***********/
+namespace simgrid {
+namespace mc {
+
+class StateCommDet {
+ // State* state_;
+
+public:
+ std::vector<std::vector<simgrid::mc::PatternCommunication>> incomplete_comm_pattern_;
+ std::vector<unsigned> communication_indices_;
+
+ static simgrid::xbt::Extension<simgrid::mc::State, StateCommDet> EXTENSION_ID;
+ explicit StateCommDet(State* /* ptr*/) //: state_(ptr)
+ {
+ copy_incomplete_comm_pattern();
+ copy_index_comm_pattern();
+ }
+
+ void copy_incomplete_comm_pattern()
+ {
+ incomplete_comm_pattern_.clear();
+ const unsigned long maxpid = api::get().get_maxpid();
+ for (unsigned long i = 0; i < maxpid; i++) {
+ std::vector<simgrid::mc::PatternCommunication> res;
+ for (auto const& comm : incomplete_communications_pattern[i])
+ res.push_back(comm->dup());
+ incomplete_comm_pattern_.push_back(std::move(res));
+ }
+ }
+
+ void copy_index_comm_pattern()
+ {
+ communication_indices_.clear();
+ for (auto const& list_process_comm : initial_communications_pattern)
+ this->communication_indices_.push_back(list_process_comm.index_comm);
+ }
+};
+
+simgrid::xbt::Extension<simgrid::mc::State, StateCommDet> StateCommDet::EXTENSION_ID;
+
+} // namespace mc
+} // namespace simgrid
+
static simgrid::mc::CommPatternDifference compare_comm_pattern(const simgrid::mc::PatternCommunication* comm1,
const simgrid::mc::PatternCommunication* comm2)
{
static void restore_communications_pattern(simgrid::mc::State* state)
{
for (size_t i = 0; i < initial_communications_pattern.size(); i++)
- initial_communications_pattern[i].index_comm = state->communication_indices_[i];
+ initial_communications_pattern[i].index_comm =
+ state->extension<simgrid::mc::StateCommDet>()->communication_indices_[i];
const unsigned long maxpid = api::get().get_maxpid();
for (unsigned long i = 0; i < maxpid; i++)
- patterns_copy(incomplete_communications_pattern[i], state->incomplete_comm_pattern_[i]);
+ patterns_copy(incomplete_communications_pattern[i],
+ state->extension<simgrid::mc::StateCommDet>()->incomplete_comm_pattern_[i]);
}
static char* print_determinism_result(simgrid::mc::CommPatternDifference diff, aid_t process,
}
}
-CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session* session) : Checker(session) {}
+CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session* session) : Checker(session)
+{
+ StateCommDet::EXTENSION_ID = simgrid::mc::State::extension_create<StateCommDet>();
+}
CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
incomplete_communications_pattern.resize(maxpid);
auto initial_state = std::make_unique<State>();
+ initial_state->extension_set(new StateCommDet(initial_state.get()));
XBT_DEBUG("********* Start communication determinism verification *********");
/* Create the new expanded state */
auto next_state = std::make_unique<State>();
+ next_state->extension_set(new StateCommDet(next_state.get()));
/* If comm determinism verification, we cannot stop the exploration if some communications are not finished (at
* least, data are transferred). These communications are incomplete and they cannot be analyzed and compared