#include <xbt/dynar.h>
#include <xbt/dynar.hpp>
-#include <xbt/fifo.h>
#include <xbt/log.h>
#include <xbt/sysdep.h>
#include "src/mc/Client.hpp"
#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;
XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
"Logging specific to MC communication determinism detection");
-XBT_PRIVATE static std::list<simgrid::mc::State*> mc_stack;
-
/********** Global variables **********/
xbt_dynar_t initial_communications_pattern;
/********** Static functions ***********/
-static e_mc_comm_pattern_difference_t compare_comm_pattern(mc_comm_pattern_t comm1, mc_comm_pattern_t comm2) {
+static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2)
+{
if(comm1->type != comm2->type)
return TYPE_DIFF;
- if (strcmp(comm1->rdv, comm2->rdv) != 0)
+ if (comm1->rdv != comm2->rdv)
return RDV_DIFF;
if (comm1->src_proc != comm2->src_proc)
return SRC_PROC_DIFF;
return DST_PROC_DIFF;
if (comm1->tag != comm2->tag)
return TAG_DIFF;
- if (comm1->data_size != comm2->data_size)
+ if (comm1->data.size() != comm2->data.size())
return DATA_SIZE_DIFF;
- if(comm1->data == nullptr && comm2->data == NULL)
- return NONE_DIFF;
- if(comm1->data != nullptr && comm2->data !=NULL) {
- if (!memcmp(comm1->data, comm2->data, comm1->data_size))
- return NONE_DIFF;
- return DATA_DIFF;
- } else
+ if (comm1->data != comm2->data)
return DATA_DIFF;
return NONE_DIFF;
}
-static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, mc_comm_pattern_t comm, unsigned int cursor) {
+static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
char *type, *res;
- if(comm->type == SIMIX_COMM_SEND)
+ if (comm->type == simgrid::mc::PatternCommunicationType::send)
type = bprintf("The send communications pattern of the process %d is different!", process - 1);
else
type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
return res;
}
-static void update_comm_pattern(mc_comm_pattern_t comm_pattern, smx_synchro_t comm_addr)
+static void update_comm_pattern(
+ simgrid::mc::PatternCommunication* comm_pattern,
+ simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr)
{
- s_smx_synchro_t comm;
- mc_model_checker->process().read(&comm, remote(comm_addr));
+ // HACK, type punning
+ simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
+ mc_model_checker->process().read(temp_comm, comm_addr);
+ simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
- 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_actor_t src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->src_proc));
+ smx_actor_t dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(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);
- comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
- if (comm_pattern->data_size == -1 && comm.comm.src_buff != nullptr) {
+ comm_pattern->src_host = MC_smx_actor_get_host_name(src_proc);
+ comm_pattern->dst_host = MC_smx_actor_get_host_name(dst_proc);
+ if (comm_pattern->data.size() == 0 && comm->src_buff != nullptr) {
size_t buff_size;
mc_model_checker->process().read(
- &buff_size, remote(comm.comm.dst_buff_size));
- comm_pattern->data_size = buff_size;
- comm_pattern->data = xbt_malloc0(comm_pattern->data_size);
+ &buff_size, remote(comm->dst_buff_size));
+ comm_pattern->data.resize(buff_size);
mc_model_checker->process().read_bytes(
- comm_pattern->data, comm_pattern->data_size,
- remote(comm.comm.src_buff));
+ comm_pattern->data.data(), comm_pattern->data.size(),
+ remote(comm->src_buff));
}
}
-static void deterministic_comm_pattern(int process, mc_comm_pattern_t comm, int backtracking) {
+namespace simgrid {
+namespace mc {
- mc_list_comm_pattern_t list =
- xbt_dynar_get_as(initial_communications_pattern, process, mc_list_comm_pattern_t);
+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){
- mc_comm_pattern_t initial_comm =
- xbt_dynar_get_as(list->list, list->index_comm, mc_comm_pattern_t);
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);
- }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);
+ if (comm->type == simgrid::mc::PatternCommunicationType::send) {
+ 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 {
+ 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);
}
}
}
-
- MC_comm_pattern_free(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);
- mc_list_comm_pattern_t initial_pattern = xbt_dynar_get_as(
- initial_communications_pattern, issuer->pid, mc_list_comm_pattern_t);
+ const smx_actor_t issuer = MC_smx_simcall_get_issuer(request);
+ simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
+ initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
- mc_comm_pattern_t pattern = xbt_new0(s_mc_comm_pattern_t, 1);
- pattern->data_size = -1;
- pattern->data = nullptr;
+ 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);
if (call_type == MC_CALL_TYPE_SEND) {
/* Create comm pattern */
- pattern->type = SIMIX_COMM_SEND;
+ pattern->type = simgrid::mc::PatternCommunicationType::send;
pattern->comm_addr = simcall_comm_isend__get__result(request);
- s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
- (std::uint64_t) pattern->comm_addr);
+ simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_synchro;
+ mc_model_checker->process().read(temp_synchro, remote(
+ static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
+ simgrid::kernel::activity::Comm* synchro =
+ static_cast<simgrid::kernel::activity::Comm*>(temp_synchro.getBuffer());
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->mbox ? &synchro->mbox->name : &synchro->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_host = MC_smx_process_get_host_name(issuer);
+ pattern->src_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(synchro->src_proc))->pid;
+ pattern->src_host = MC_smx_actor_get_host_name(issuer);
struct s_smpi_mpi_request mpi_request =
mc_model_checker->process().read<s_smpi_mpi_request>(
(std::uint64_t) simcall_comm_isend__get__data(request));
pattern->tag = mpi_request.tag;
- if(synchro.comm.src_buff != nullptr){
- pattern->data_size = synchro.comm.src_buff_size;
- pattern->data = xbt_malloc0(pattern->data_size);
+ if (synchro->src_buff != nullptr){
+ pattern->data.resize(synchro->src_buff_size);
mc_model_checker->process().read_bytes(
- pattern->data, pattern->data_size, remote(synchro.comm.src_buff));
+ pattern->data.data(), pattern->data.size(),
+ remote(synchro->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, mc_list_comm_pattern_t
- )->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, mc_list_comm_pattern_t
+ initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
)->index_comm++;
}
return;
}
} else if (call_type == MC_CALL_TYPE_RECV) {
- pattern->type = SIMIX_COMM_RECEIVE;
+ pattern->type = simgrid::mc::PatternCommunicationType::receive;
pattern->comm_addr = simcall_comm_irecv__get__result(request);
struct s_smpi_mpi_request mpi_request;
&mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
pattern->tag = mpi_request.tag;
- s_smx_synchro_t synchro;
- mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
+ simgrid::mc::Remote<simgrid::kernel::activity::Comm> temp_comm;
+ mc_model_checker->process().read(temp_comm, remote(
+ static_cast<simgrid::kernel::activity::Comm*>(pattern->comm_addr)));
+ simgrid::kernel::activity::Comm* comm = temp_comm.getBuffer();
char* remote_name;
mc_model_checker->process().read(&remote_name,
- remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
+ remote(comm->mbox ? &comm->mbox->name : &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_host = MC_smx_process_get_host_name(issuer);
+ pattern->dst_proc = mc_model_checker->process().resolveActor(simgrid::mc::remote(comm->dst_proc))->pid;
+ pattern->dst_host = MC_smx_actor_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) {
- mc_comm_pattern_t current_comm_pattern;
+
+void CommunicationDeterminismChecker::complete_comm_pattern(
+ xbt_dynar_t list, simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr,
+ unsigned int issuer, int backtracking)
+{
+ simgrid::mc::PatternCommunication* current_comm_pattern;
unsigned int cursor = 0;
- mc_comm_pattern_t comm_pattern;
+ std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
int completed = 0;
/* Complete comm pattern */
xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
- if (current_comm_pattern->comm_addr == comm_addr) {
+ if (remote(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;
}
if(!completed)
xbt_die("Corresponding communication not found!");
- mc_list_comm_pattern_t pattern = xbt_dynar_get_as(
- initial_communications_pattern, issuer, mc_list_comm_pattern_t);
+ 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 (simgrid::mc::State* state : mc_stack) {
- int value = 0;
- smx_simcall_t saved_req = MC_state_get_executed_request(state, &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 (simgrid::mc::State* state : mc_stack) {
- int value;
- smx_simcall_t req = MC_state_get_executed_request(state, &value);
- if (req) {
- char* req_str = simgrid::mc::request_to_string(
- req, value, simgrid::mc::RequestType::executed);
- trace.push_back(req_str);
- xbt_free(req_str);
- }
+ for (auto const& state : stack_) {
+ smx_simcall_t req = &state->executed_req;
+ if (req)
+ trace.push_back(simgrid::mc::request_to_string(
+ 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()
{
- simgrid::mc::State* initial_state = nullptr;
+
int i;
const int maxpid = MC_smx_get_maxpid();
- simgrid::mc::visited_states.clear();
-
// Create initial_communications_pattern elements:
- initial_communications_pattern = xbt_dynar_new(sizeof(mc_list_comm_pattern_t), MC_list_comm_pattern_free_voidp);
+ initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
for (i=0; i < maxpid; i++){
- mc_list_comm_pattern_t process_list_pattern = xbt_new0(s_mc_list_comm_pattern_t, 1);
- process_list_pattern->list = xbt_dynar_new(sizeof(mc_comm_pattern_t), MC_comm_pattern_free_voidp);
- process_list_pattern->index_comm = 0;
+ simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
}
// Create incomplete_communications_pattern elements:
incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
for (i=0; i < maxpid; i++){
- xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(mc_comm_pattern_t), nullptr);
+ xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
}
- initial_state = MC_state_new();
+ std::unique_ptr<simgrid::mc::State> initial_state =
+ std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++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, &p.copy);
+ /* Get an enabled actor and insert it in the interleave set of the initial state */
+ for (auto& actor : mc_model_checker->process().actors())
+ if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
+ initial_state->interleave(actor.copy.getBuffer());
- mc_stack.push_back(initial_state);
+ stack_.push_back(std::move(initial_state));
}
static inline
bool all_communications_are_finished()
{
- for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
- xbt_dynar_t pattern = xbt_dynar_get_as(
- incomplete_communications_pattern, current_process, xbt_dynar_t);
+ for (size_t current_actor = 1; current_actor < MC_smx_get_maxpid(); current_actor++) {
+ xbt_dynar_t pattern = xbt_dynar_get_as(incomplete_communications_pattern, current_actor, xbt_dynar_t);
if (!xbt_dynar_is_empty(pattern)) {
XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
return false;
return true;
}
-int CommunicationDeterminismChecker::main(void)
+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_actor_t issuer = MC_smx_simcall_get_issuer(saved_req);
+ smx_simcall_t req = &issuer->simcall;
- char *req_str = nullptr;
- int value;
+ /* 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)
+{
std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
smx_simcall_t req = nullptr;
- simgrid::mc::State* next_state = nullptr;
- while (!mc_stack.empty()) {
+ while (!stack_.empty()) {
/* Get current state */
- simgrid::mc::State* state = mc_stack.back();
+ simgrid::mc::State* state = stack_.back().get();
XBT_DEBUG("**************************************************");
- XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %d)",
- mc_stack.size(), state->num,
- MC_state_interleave_size(state));
+ XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
+ stack_.size(), state->num,
+ state->interleaveSize());
/* Update statistics */
- mc_stats->visited_states++;
+ mc_model_checker->visited_states++;
- if (mc_stack.size() <= _sg_mc_max_depth
- && (req = MC_state_get_request(state, &value))
+ if (stack_.size() <= (std::size_t) _sg_mc_max_depth
+ && (req = MC_state_get_request(state)) != nullptr
&& (visited_state == nullptr)) {
- req_str = simgrid::mc::request_to_string(req, value, simgrid::mc::RequestType::simix);
- XBT_DEBUG("Execute: %s", req_str);
- xbt_free(req_str);
+ int req_num = state->transition.argument;
+ XBT_DEBUG("Execute: %s",
+ simgrid::mc::request_to_string(
+ 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 */
- next_state = MC_state_new();
+ std::unique_ptr<simgrid::mc::State> next_state =
+ std::unique_ptr<simgrid::mc::State>(new simgrid::mc::State(++expandedStatesCount_));
/* If comm determinism verification, we cannot stop the exploration if
- some communications are not finished (at least, data are transfered).
+ some communications are not finished (at least, data are transferred).
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 = simgrid::mc::is_visited_state(next_state, compare_snapshots)) == nullptr) {
+ if (_sg_mc_visited == 0
+ || (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, &p.copy);
+ /* Get enabled actors and insert them in the interleave set of the next state */
+ for (auto& actor : mc_model_checker->process().actors())
+ if (simgrid::mc::actor_is_enabled(actor.copy.getBuffer()))
+ next_state->interleave(actor.copy.getBuffer());
if (dot_output != nullptr)
- fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n", state->num, next_state->num, req_str);
+ fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
+ state->num, next_state->num, req_str.c_str());
} else if (dot_output != nullptr)
fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
- state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str);
-
- mc_stack.push_back(next_state);
+ state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
- if (dot_output != nullptr)
- xbt_free(req_str);
+ stack_.push_back(std::move(next_state));
} else {
- if (mc_stack.size() > _sg_mc_max_depth)
+ if (stack_.size() > (std::size_t) _sg_mc_max_depth)
XBT_WARN("/!\\ Max depth reached ! /!\\ ");
else if (visited_state != nullptr)
XBT_DEBUG("State already visited (equal to state %d), exploration stopped on this path.", visited_state->other_num == -1 ? visited_state->num : visited_state->other_num);
else
XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
- mc_stack.size());
+ 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 */
- mc_stack.pop_back();
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
XBT_DEBUG("Delete state %d at depth %zi",
- state->num, mc_stack.size() + 1);
+ state->num, stack_.size());
+ stack_.pop_back();
visited_state = nullptr;
return SIMGRID_MC_EXIT_DEADLOCK;
}
- while (!mc_stack.empty()) {
- simgrid::mc::State* state = mc_stack.back();
- mc_stack.pop_back();
- if (MC_state_interleave_size(state)
- && mc_stack.size() < _sg_mc_max_depth) {
+ while (!stack_.empty()) {
+ std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
+ stack_.pop_back();
+ if (state->interleaveSize()
+ && stack_.size() < (std::size_t) _sg_mc_max_depth) {
/* We found a back-tracking point, let's loop */
XBT_DEBUG("Back-tracking to state %d at depth %zi",
- state->num, mc_stack.size() + 1);
- mc_stack.push_back(state);
+ state->num, stack_.size() + 1);
+ stack_.push_back(std::move(state));
- simgrid::mc::replay(mc_stack);
+ this->restoreState();
XBT_DEBUG("Back-tracking to state %d at depth %zi done",
- state->num, mc_stack.size());
+ stack_.back()->num, stack_.size());
break;
} else {
XBT_DEBUG("Delete state %d at depth %zi",
- state->num, mc_stack.size() + 1);
- MC_state_delete(state, !state->in_visited_states ? 1 : 0);
+ state->num, stack_.size() + 1);
}
}
}
}
- 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();
-
- if (mc_mode == MC_MODE_CLIENT)
- // This will move somehwere else:
- simgrid::mc::Client::get()->handleMessages();
-
- /* Create exploration stack */
- mc_stack.clear();
+ 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;
}
+Checker* createCommunicationDeterminismChecker(Session& session)
+{
+ return new CommunicationDeterminismChecker(session);
+}
+
+}
}
-}
\ No newline at end of file
