#include "src/mc/checker/CommunicationDeterminismChecker.hpp"
#include "src/kernel/activity/MailboxImpl.hpp"
-#include "src/mc/VisitedState.hpp"
+#include "src/mc/Session.hpp"
+#include "src/mc/mc_config.hpp"
#include "src/mc/mc_exit.hpp"
#include "src/mc/mc_private.hpp"
-#include "src/mc/mc_record.hpp"
#include "src/mc/mc_request.hpp"
#include "src/mc/mc_smx.hpp"
-#include "src/mc/mc_state.hpp"
-#include "src/mc/remote/Client.hpp"
#if HAVE_SMPI
#include "smpi_request.hpp"
XBT_INFO("%s", this->send_diff);
xbt_free(this->send_diff);
this->send_diff = nullptr;
- simgrid::mc::session->logState();
+ simgrid::mc::session->log_state();
mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
} else if (_sg_mc_comms_determinism && (not this->send_deterministic && not this->recv_deterministic)) {
XBT_INFO("****************************************************");
this->send_diff = nullptr;
xbt_free(this->recv_diff);
this->recv_diff = nullptr;
- simgrid::mc::session->logState();
+ simgrid::mc::session->log_state();
mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
}
}
simgrid::kernel::activity::CommImpl* synchro =
static_cast<simgrid::kernel::activity::CommImpl*>(temp_synchro.getBuffer());
- char* remote_name = mc_model_checker->process().read<char*>(
- RemotePtr<char*>((uint64_t)(synchro->mbox ? &synchro->mbox->name_ : &synchro->mbox_cpy->name_)));
+ char* remote_name = mc_model_checker->process().read<char*>(RemotePtr<char*>(
+ (uint64_t)(synchro->get_mailbox() ? &synchro->get_mailbox()->name_ : &synchro->mbox_cpy->name_)));
pattern->rdv = mc_model_checker->process().read_string(RemotePtr<char>(remote_name));
pattern->src_proc =
mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_actor_.get()))->get_pid();
pattern->src_host = MC_smx_actor_get_host_name(issuer);
#if HAVE_SMPI
- simgrid::smpi::Request mpi_request = mc_model_checker->process().read<simgrid::smpi::Request>(
- RemotePtr<simgrid::smpi::Request>((std::uint64_t)simcall_comm_isend__get__data(request)));
+ simgrid::smpi::Request mpi_request;
+ mc_model_checker->process().read(
+ &mpi_request, remote(static_cast<simgrid::smpi::Request*>(simcall_comm_isend__get__data(request))));
pattern->tag = mpi_request.tag();
#endif
#if HAVE_SMPI
simgrid::smpi::Request mpi_request;
- mc_model_checker->process().read(&mpi_request,
- remote((simgrid::smpi::Request*)simcall_comm_irecv__get__data(request)));
+ mc_model_checker->process().read(
+ &mpi_request, remote(static_cast<simgrid::smpi::Request*>(simcall_comm_irecv__get__data(request))));
pattern->tag = mpi_request.tag();
#endif
simgrid::kernel::activity::CommImpl* comm = temp_comm.getBuffer();
char* remote_name;
- mc_model_checker->process().read(
- &remote_name, remote(comm->mbox ? &simgrid::xbt::string::to_string_data(comm->mbox->name_).data
- : &simgrid::xbt::string::to_string_data(comm->mbox_cpy->name_).data));
+ mc_model_checker->process().read(&remote_name,
+ remote(comm->get_mailbox()
+ ? &simgrid::xbt::string::to_string_data(comm->get_mailbox()->name_).data
+ : &simgrid::xbt::string::to_string_data(comm->mbox_cpy->name_).data));
pattern->rdv = mc_model_checker->process().read_string(RemotePtr<char>(remote_name));
pattern->dst_proc =
mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_actor_.get()))->get_pid();
CommunicationDeterminismChecker::~CommunicationDeterminismChecker() = default;
-RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
+RecordTrace CommunicationDeterminismChecker::get_record_trace() // override
{
RecordTrace res;
for (auto const& state : stack_)
return res;
}
-std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
+std::vector<std::string> CommunicationDeterminismChecker::get_textual_trace() // override
{
std::vector<std::string> trace;
for (auto const& state : stack_) {
return trace;
}
-void CommunicationDeterminismChecker::logState() // override
+void CommunicationDeterminismChecker::log_state() // override
{
if (_sg_mc_comms_determinism && not this->recv_deterministic && this->send_deterministic) {
XBT_INFO("******************************************************");
XBT_INFO("******************************************************");
XBT_INFO("%s", this->send_diff);
}
- XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+ XBT_INFO("Expanded states = %lu", expanded_states_count_);
XBT_INFO("Visited states = %lu", mc_model_checker->visited_states);
XBT_INFO("Executed transitions = %lu", mc_model_checker->executed_transitions);
XBT_INFO("Send-deterministic : %s", not this->send_deterministic ? "No" : "Yes");
incomplete_communications_pattern.resize(maxpid);
std::unique_ptr<simgrid::mc::State> initial_state =
- std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
+ std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
XBT_DEBUG("********* Start communication determinism verification *********");
/* Intermediate backtracking */
simgrid::mc::State* last_state = stack_.back().get();
if (last_state->system_state) {
- simgrid::mc::restore_snapshot(last_state->system_state);
+ last_state->system_state->restore(&mc_model_checker->process());
MC_restore_communications_pattern(last_state);
return;
}
/* Restore the initial state */
- simgrid::mc::session->restoreInitialState();
+ simgrid::mc::session->restore_initial_state();
unsigned n = MC_smx_get_maxpid();
assert(n == incomplete_communications_pattern.size());
/* Create the new expanded state */
std::unique_ptr<simgrid::mc::State> next_state =
- std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
+ std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expanded_states_count_));
/* 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
bool compare_snapshots = all_communications_are_finished() && this->initial_communications_pattern_done;
if (_sg_mc_max_visited_states != 0)
- visited_state = visitedStates_.addVisitedState(expandedStatesCount_, next_state.get(), compare_snapshots);
+ visited_state = visited_states_.addVisitedState(expanded_states_count_, next_state.get(), compare_snapshots);
else
visited_state = nullptr;
}
}
- simgrid::mc::session->logState();
+ simgrid::mc::session->log_state();
}
void CommunicationDeterminismChecker::run()