#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);
}
}
-static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
+namespace simgrid {
+namespace mc {
+
+void CommunicationDeterminismChecker::deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
simgrid::mc::PatternCommunicationList* list =
xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
if(!backtracking){
- simgrid::mc::PatternCommunication* initial_comm =
- xbt_dynar_get_as(list->list, list->index_comm, simgrid::mc::PatternCommunication*);
e_mc_comm_pattern_difference_t diff =
- compare_comm_pattern(initial_comm, comm);
+ compare_comm_pattern(list->list[list->index_comm].get(), comm);
if (diff != NONE_DIFF) {
if (comm->type == SIMIX_COMM_SEND){
- simgrid::mc::initial_global_state->send_deterministic = 0;
- if(simgrid::mc::initial_global_state->send_diff != nullptr)
- xbt_free(simgrid::mc::initial_global_state->send_diff);
- simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
+ this->send_deterministic = 0;
+ if (this->send_diff != nullptr)
+ xbt_free(this->send_diff);
+ this->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
}else{
- simgrid::mc::initial_global_state->recv_deterministic = 0;
- if(simgrid::mc::initial_global_state->recv_diff != nullptr)
- xbt_free(simgrid::mc::initial_global_state->recv_diff);
- simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
+ this->recv_deterministic = 0;
+ if (this->recv_diff != nullptr)
+ xbt_free(this->recv_diff);
+ this->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
}
- if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
+ if(_sg_mc_send_determinism && !this->send_deterministic){
XBT_INFO("*********************************************************");
XBT_INFO("***** Non-send-deterministic communications pattern *****");
XBT_INFO("*********************************************************");
- 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);
+ XBT_INFO("%s", this->send_diff);
+ xbt_free(this->send_diff);
+ this->send_diff = nullptr;
+ 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->recv_deterministic)) {
+ && (!this->send_deterministic && !this->recv_deterministic)) {
XBT_INFO("****************************************************");
XBT_INFO("***** Non-deterministic communications pattern *****");
XBT_INFO("****************************************************");
- XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
- XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
- xbt_free(simgrid::mc::initial_global_state->send_diff);
- 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);
+ XBT_INFO("%s", this->send_diff);
+ XBT_INFO("%s", this->recv_diff);
+ xbt_free(this->send_diff);
+ this->send_diff = nullptr;
+ xbt_free(this->recv_diff);
+ this->recv_diff = nullptr;
+ simgrid::mc::session->logState();
mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
}
}
}
-
- delete comm;
-
}
/********** Non Static functions ***********/
-void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
+void CommunicationDeterminismChecker::get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
{
const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
- simgrid::mc::PatternCommunication* pattern = new simgrid::mc::PatternCommunication();
+ std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
+ std::unique_ptr<simgrid::mc::PatternCommunication>(
+ new simgrid::mc::PatternCommunication());
pattern->index =
initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
(std::uint64_t) pattern->comm_addr);
char* remote_name = mc_model_checker->process().read<char*>(
- (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
+ (std::uint64_t)(synchro.comm.mbox ? &synchro.comm.mbox->name : &synchro.comm.mbox_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 =
remote(synchro.comm.src_buff));
}
if(mpi_request.detached){
- if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
+ if (!this->initial_communications_pattern_done) {
/* Store comm pattern */
- xbt_dynar_push(
- xbt_dynar_get_as(
- initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
- )->list,
- &pattern);
+ simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
+ initial_communications_pattern, pattern->src_proc,
+ simgrid::mc::PatternCommunicationList*);
+ list->list.push_back(std::move(pattern));
} else {
/* Evaluate comm determinism */
- deterministic_comm_pattern(pattern->src_proc, pattern, backtracking);
+ this->deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
xbt_dynar_get_as(
initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
)->index_comm++;
char* remote_name;
mc_model_checker->process().read(&remote_name,
- remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
+ remote(synchro.comm.mbox ? &synchro.comm.mbox->name : &synchro.comm.mbox_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);
- xbt_dynar_push(
- xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t),
- &pattern);
-
- XBT_DEBUG("Insert incomplete comm pattern %p for process %lu", pattern, issuer->pid);
+ XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
+ pattern.get(), issuer->pid);
+ xbt_dynar_t dynar =
+ xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
+ simgrid::mc::PatternCommunication* pattern2 = pattern.release();
+ xbt_dynar_push(dynar, &pattern2);
}
-void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
+
+void CommunicationDeterminismChecker::complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking)
+{
simgrid::mc::PatternCommunication* current_comm_pattern;
unsigned int cursor = 0;
- simgrid::mc::PatternCommunication* comm_pattern;
+ std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
int completed = 0;
/* Complete comm pattern */
if (current_comm_pattern->comm_addr == comm_addr) {
update_comm_pattern(current_comm_pattern, comm_addr);
completed = 1;
+ simgrid::mc::PatternCommunication* temp;
xbt_dynar_remove_at(
xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
- cursor, &comm_pattern);
+ cursor, &temp);
+ comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
break;
}
simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
- if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
+ if (!this->initial_communications_pattern_done)
/* Store comm pattern */
- xbt_dynar_push(pattern->list, &comm_pattern);
+ pattern->list.push_back(std::move(comm_pattern));
else {
/* Evaluate comm determinism */
- deterministic_comm_pattern(issuer, comm_pattern, backtracking);
+ this->deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
pattern->index_comm++;
}
}
-
-/************************ Main algorithm ************************/
-
-namespace simgrid {
-namespace mc {
-
CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
: Checker(session)
{
}
-// 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 &&
+ !this->recv_deterministic &&
+ this->send_deterministic) {
+ XBT_INFO("******************************************************");
+ XBT_INFO("**** Only-send-deterministic communication pattern ****");
+ XBT_INFO("******************************************************");
+ XBT_INFO("%s", this->recv_diff);
+ } else if(_sg_mc_comms_determinism &&
+ !this->send_deterministic &&
+ this->recv_deterministic) {
+ XBT_INFO("******************************************************");
+ XBT_INFO("**** Only-recv-deterministic communication pattern ****");
+ XBT_INFO("******************************************************");
+ XBT_INFO("%s", this->send_diff);
+ }
+ XBT_INFO("Expanded states = %lu", expandedStatesCount_);
+ 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", !this->send_deterministic ? "No" : "Yes");
+ if (_sg_mc_comms_determinism)
+ XBT_INFO("Recv-deterministic : %s",
+ !this->recv_deterministic ? "No" : "Yes");
+}
+
void CommunicationDeterminismChecker::prepare()
{
initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
for (i=0; i < maxpid; i++){
simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
- process_list_pattern->list = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunication>();
- process_list_pattern->index_comm = 0;
xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
}
}
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));
}
return true;
}
+void CommunicationDeterminismChecker::restoreState()
+{
+ /* Intermediate backtracking */
+ {
+ simgrid::mc::State* state = stack_.back().get();
+ if (state->system_state) {
+ simgrid::mc::restore_snapshot(state->system_state);
+ MC_restore_communications_pattern(state);
+ return;
+ }
+ }
+
+ /* Restore the initial state */
+ simgrid::mc::session->restoreInitialState();
+
+ // int n = xbt_dynar_length(incomplete_communications_pattern);
+ unsigned n = MC_smx_get_maxpid();
+ assert(n == xbt_dynar_length(incomplete_communications_pattern));
+ assert(n == xbt_dynar_length(initial_communications_pattern));
+ for (unsigned j=0; j < n ; j++) {
+ xbt_dynar_reset((xbt_dynar_t)xbt_dynar_get_as(incomplete_communications_pattern, j, xbt_dynar_t));
+ xbt_dynar_get_as(initial_communications_pattern, j, simgrid::mc::PatternCommunicationList*)->index_comm = 0;
+ }
+
+ /* Traverse the stack from the state at position start and re-execute the transitions */
+ for (std::unique_ptr<simgrid::mc::State> const& state : stack_) {
+ if (state == stack_.back())
+ break;
+
+ int req_num = state->transition.argument;
+ smx_simcall_t saved_req = &state->executed_req;
+ xbt_assert(saved_req);
+
+ /* because we got a copy of the executed request, we have to fetch the
+ real one, pointed by the request field of the issuer process */
+
+ const smx_process_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ smx_simcall_t req = &issuer->simcall;
+
+ /* TODO : handle test and testany simcalls */
+ e_mc_call_type_t call = MC_get_call_type(req);
+ mc_model_checker->handle_simcall(state->transition);
+ MC_handle_comm_pattern(call, req, req_num, nullptr, 1);
+ mc_model_checker->wait_for_requests();
+
+ /* Update statistics */
+ mc_model_checker->visited_states++;
+ mc_model_checker->executed_transitions++;
+ }
+}
+
int CommunicationDeterminismChecker::main(void)
{
- int value;
std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
smx_simcall_t req = nullptr;
state->interleaveSize());
/* Update statistics */
- mc_stats->visited_states++;
+ mc_model_checker->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++;
+ mc_model_checker->executed_transitions++;
/* TODO : handle test and testany simcalls */
e_mc_call_type_t call = MC_CALL_TYPE_NONE;
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);
+ if (!this->initial_communications_pattern_done)
+ 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).
These communications are incomplete and they cannot be analyzed and
compared with the initial pattern. */
bool compare_snapshots = all_communications_are_finished()
- && initial_global_state->initial_communications_pattern_done;
+ && this->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",
XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
stack_.size());
- if (!initial_global_state->initial_communications_pattern_done)
- initial_global_state->initial_communications_pattern_done = 1;
+ if (!this->initial_communications_pattern_done)
+ this->initial_communications_pattern_done = 1;
/* Trash the current state, no longer needed */
XBT_DEBUG("Delete state %d at depth %zi",
state->num, stack_.size() + 1);
stack_.push_back(std::move(state));
- simgrid::mc::replay(stack_);
+ this->restoreState();
XBT_DEBUG("Back-tracking to state %d at depth %zi done",
stack_.back()->num, stack_.size());
}
}
- MC_print_statistics(mc_stats);
+ simgrid::mc::session->logState();
return SIMGRID_MC_EXIT_SUCCESS;
}
int CommunicationDeterminismChecker::run()
{
XBT_INFO("Check communication determinism");
- mc_model_checker->wait_for_requests();
+ simgrid::mc::session->initialize();
this->prepare();
- initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
- initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
- initial_global_state->initial_communications_pattern_done = 0;
- initial_global_state->recv_deterministic = 1;
- initial_global_state->send_deterministic = 1;
- initial_global_state->recv_diff = nullptr;
- initial_global_state->send_diff = nullptr;
+ this->initial_communications_pattern_done = 0;
+ this->recv_deterministic = 1;
+ this->send_deterministic = 1;
+ this->recv_diff = nullptr;
+ this->send_diff = nullptr;
int res = this->main();
- initial_global_state = nullptr;
return res;
}
}
}
-}
\ No newline at end of file
+}