#include "src/mc/CommunicationDeterminismChecker.hpp"
#include "src/mc/mc_exit.h"
#include "src/mc/VisitedState.hpp"
+#include "src/mc/Transition.hpp"
using simgrid::mc::remote;
s_smx_synchro_t comm;
mc_model_checker->process().read(&comm, remote(comm_addr));
- smx_process_t src_proc = MC_smx_resolve_process(comm.comm.src_proc);
- smx_process_t dst_proc = MC_smx_resolve_process(comm.comm.dst_proc);
+ smx_process_t src_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(comm.comm.src_proc));
+ smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(comm.comm.dst_proc));
comm_pattern->src_proc = src_proc->pid;
comm_pattern->dst_proc = dst_proc->pid;
comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
xbt_free(simgrid::mc::initial_global_state->send_diff);
simgrid::mc::initial_global_state->send_diff = nullptr;
- MC_print_statistics(mc_stats);
+ simgrid::mc::session->logState();
mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
}else if(_sg_mc_comms_determinism
&& (!simgrid::mc::initial_global_state->send_deterministic
simgrid::mc::initial_global_state->send_diff = nullptr;
xbt_free(simgrid::mc::initial_global_state->recv_diff);
simgrid::mc::initial_global_state->recv_diff = nullptr;
- MC_print_statistics(mc_stats);
+ simgrid::mc::session->logState();
mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
}
}
char* remote_name = mc_model_checker->process().read<char*>(
(std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
pattern->rdv = mc_model_checker->process().read_string(remote_name);
- pattern->src_proc = MC_smx_resolve_process(synchro.comm.src_proc)->pid;
+ pattern->src_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(synchro.comm.src_proc))->pid;
pattern->src_host = MC_smx_process_get_host_name(issuer);
struct s_smpi_mpi_request mpi_request =
mc_model_checker->process().read(&remote_name,
remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
pattern->rdv = mc_model_checker->process().read_string(remote_name);
- pattern->dst_proc = MC_smx_resolve_process(synchro.comm.dst_proc)->pid;
+ pattern->dst_proc = mc_model_checker->process().resolveProcess(
+ simgrid::mc::remote(synchro.comm.dst_proc))->pid;
pattern->dst_host = MC_smx_process_get_host_name(issuer);
} else
xbt_die("Unexpected call_type %i", (int) call_type);
}
-// TODO, deduplicate with SafetyChecker
RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
{
RecordTrace res;
- for (auto const& state : stack_) {
- int value = 0;
- smx_simcall_t saved_req = MC_state_get_executed_request(state.get(), &value);
- const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
- const int pid = issuer->pid;
- res.push_back(RecordTraceElement(pid, value));
- }
+ for (auto const& state : stack_)
+ res.push_back(state->getTransition());
return res;
}
-// TODO, deduplicate with SafetyChecker
std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
{
std::vector<std::string> trace;
for (auto const& state : stack_) {
- int value;
- smx_simcall_t req = MC_state_get_executed_request(state.get(), &value);
+ smx_simcall_t req = &state->executed_req;
if (req)
trace.push_back(simgrid::mc::request_to_string(
- req, value, simgrid::mc::RequestType::executed));
+ req, state->transition.argument, simgrid::mc::RequestType::executed));
}
return trace;
}
+void CommunicationDeterminismChecker::logState() // override
+{
+ Checker::logState();
+ if (_sg_mc_comms_determinism &&
+ !simgrid::mc::initial_global_state->recv_deterministic &&
+ simgrid::mc::initial_global_state->send_deterministic) {
+ XBT_INFO("******************************************************");
+ XBT_INFO("**** Only-send-deterministic communication pattern ****");
+ XBT_INFO("******************************************************");
+ XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
+ } else if(_sg_mc_comms_determinism &&
+ !simgrid::mc::initial_global_state->send_deterministic &&
+ simgrid::mc::initial_global_state->recv_deterministic) {
+ XBT_INFO("******************************************************");
+ XBT_INFO("**** Only-recv-deterministic communication pattern ****");
+ XBT_INFO("******************************************************");
+ XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
+ }
+ XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+ XBT_INFO("Visited states = %lu", mc_stats->visited_states);
+ XBT_INFO("Executed transitions = %lu", mc_stats->executed_transitions);
+ if (simgrid::mc::initial_global_state != nullptr)
+ XBT_INFO("Send-deterministic : %s",
+ !simgrid::mc::initial_global_state->send_deterministic ? "No" : "Yes");
+ if (simgrid::mc::initial_global_state != nullptr && _sg_mc_comms_determinism)
+ XBT_INFO("Recv-deterministic : %s",
+ !simgrid::mc::initial_global_state->recv_deterministic ? "No" : "Yes");
+}
+
void CommunicationDeterminismChecker::prepare()
{
}
std::unique_ptr<simgrid::mc::State> initial_state =
- std::unique_ptr<simgrid::mc::State>(MC_state_new());
+ std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
XBT_DEBUG("********* Start communication determinism verification *********");
- /* Wait for requests (schedules processes) */
- mc_model_checker->wait_for_requests();
-
/* Get an enabled process and insert it in the interleave set of the initial state */
for (auto& p : mc_model_checker->process().simix_processes())
if (simgrid::mc::process_is_enabled(&p.copy))
- MC_state_interleave_process(initial_state.get(), &p.copy);
+ initial_state->interleave(&p.copy);
stack_.push_back(std::move(initial_state));
}
int CommunicationDeterminismChecker::main(void)
{
- int value;
std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
smx_simcall_t req = nullptr;
mc_stats->visited_states++;
if (stack_.size() <= (std::size_t) _sg_mc_max_depth
- && (req = MC_state_get_request(state, &value))
+ && (req = MC_state_get_request(state)) != nullptr
&& (visited_state == nullptr)) {
+ int req_num = state->transition.argument;
+
XBT_DEBUG("Execute: %s",
simgrid::mc::request_to_string(
- req, value, simgrid::mc::RequestType::simix).c_str());
+ req, req_num, simgrid::mc::RequestType::simix).c_str());
std::string req_str;
if (dot_output != nullptr)
- req_str = simgrid::mc::request_get_dot_output(req, value);
+ req_str = simgrid::mc::request_get_dot_output(req, req_num);
- MC_state_set_executed_request(state, req, value);
mc_stats->executed_transitions++;
/* TODO : handle test and testany simcalls */
call = MC_get_call_type(req);
/* Answer the request */
- simgrid::mc::handle_simcall(req, value); /* After this call req is no longer useful */
+ mc_model_checker->handle_simcall(state->transition);
+ /* After this call req is no longer useful */
if(!initial_global_state->initial_communications_pattern_done)
- MC_handle_comm_pattern(call, req, value, initial_communications_pattern, 0);
+ MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
else
- MC_handle_comm_pattern(call, req, value, nullptr, 0);
+ MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
/* Wait for requests (schedules processes) */
mc_model_checker->wait_for_requests();
/* Create the new expanded state */
std::unique_ptr<simgrid::mc::State> next_state =
- std::unique_ptr<simgrid::mc::State>(MC_state_new());
+ std::unique_ptr<simgrid::mc::State>(MC_state_new(++expandedStatesCount_));
/* If comm determinism verification, we cannot stop the exploration if
some communications are not finished (at least, data are transfered).
&& initial_global_state->initial_communications_pattern_done;
if (_sg_mc_visited == 0
- || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
+ || (visited_state = visitedStates_.addVisitedState(
+ expandedStatesCount_, next_state.get(), compare_snapshots)) == nullptr) {
/* Get enabled processes and insert them in the interleave set of the next state */
for (auto& p : mc_model_checker->process().simix_processes())
if (simgrid::mc::process_is_enabled(&p.copy))
- MC_state_interleave_process(next_state.get(), &p.copy);
+ next_state->interleave(&p.copy);
if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
}
}
- MC_print_statistics(mc_stats);
+ simgrid::mc::session->logState();
return SIMGRID_MC_EXIT_SUCCESS;
}