src/mc/CommunicationDeterminismChecker.cpp

   1 /* Copyright (c) 2008-2015. The SimGrid Team.
   2  * All rights reserved.                                                     */
   3
   4 /* This program is free software; you can redistribute it and/or modify it
   5  * under the terms of the license (GNU LGPL) which comes with this package. */
   6
   7 #include <cstdint>
   8
   9 #include <xbt/dynar.h>
  10 #include <xbt/dynar.hpp>
  11 #include <xbt/log.h>
  12 #include <xbt/sysdep.h>
  13
  14 #include "src/mc/mc_state.h"
  15 #include "src/mc/mc_comm_pattern.h"
  16 #include "src/mc/mc_request.h"
  17 #include "src/mc/mc_safety.h"
  18 #include "src/mc/mc_private.h"
  19 #include "src/mc/mc_record.h"
  20 #include "src/mc/mc_smx.h"
  21 #include "src/mc/Client.hpp"
  22 #include "src/mc/CommunicationDeterminismChecker.hpp"
  23 #include "src/mc/mc_exit.h"
  24 #include "src/mc/VisitedState.hpp"
  25
  26 using simgrid::mc::remote;
  27
  28 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_determinism, mc,
  29                                 "Logging specific to MC communication determinism detection");
  30
  31 /********** Global variables **********/
  32
  33 xbt_dynar_t initial_communications_pattern;
  34 xbt_dynar_t incomplete_communications_pattern;
  35
  36 /********** Static functions ***********/
  37
  38 static e_mc_comm_pattern_difference_t compare_comm_pattern(simgrid::mc::PatternCommunication* comm1, simgrid::mc::PatternCommunication* comm2) {
  39   if(comm1->type != comm2->type)
  40     return TYPE_DIFF;
  41   if (comm1->rdv != comm2->rdv)
  42     return RDV_DIFF;
  43   if (comm1->src_proc != comm2->src_proc)
  44     return SRC_PROC_DIFF;
  45   if (comm1->dst_proc != comm2->dst_proc)
  46     return DST_PROC_DIFF;
  47   if (comm1->tag != comm2->tag)
  48     return TAG_DIFF;
  49   if (comm1->data.size() != comm2->data.size())
  50     return DATA_SIZE_DIFF;
  51   if (comm1->data != comm2->data)
  52     return DATA_DIFF;
  53   return NONE_DIFF;
  54 }
  55
  56 static char* print_determinism_result(e_mc_comm_pattern_difference_t diff, int process, simgrid::mc::PatternCommunication* comm, unsigned int cursor) {
  57   char *type, *res;
  58
  59   if(comm->type == SIMIX_COMM_SEND)
  60     type = bprintf("The send communications pattern of the process %d is different!", process - 1);
  61   else
  62     type = bprintf("The recv communications pattern of the process %d is different!", process - 1);
  63
  64   switch(diff) {
  65   case TYPE_DIFF:
  66     res = bprintf("%s Different type for communication #%d", type, cursor);
  67     break;
  68   case RDV_DIFF:
  69     res = bprintf("%s Different rdv for communication #%d", type, cursor);
  70     break;
  71   case TAG_DIFF:
  72     res = bprintf("%s Different tag for communication #%d", type, cursor);
  73     break;
  74   case SRC_PROC_DIFF:
  75       res = bprintf("%s Different source for communication #%d", type, cursor);
  76     break;
  77   case DST_PROC_DIFF:
  78       res = bprintf("%s Different destination for communication #%d", type, cursor);
  79     break;
  80   case DATA_SIZE_DIFF:
  81     res = bprintf("%s\n Different data size for communication #%d", type, cursor);
  82     break;
  83   case DATA_DIFF:
  84     res = bprintf("%s\n Different data for communication #%d", type, cursor);
  85     break;
  86   default:
  87     res = nullptr;
  88     break;
  89   }
  90
  91   return res;
  92 }
  93
  94 static void update_comm_pattern(simgrid::mc::PatternCommunication* comm_pattern, smx_synchro_t comm_addr)
  95 {
  96   s_smx_synchro_t comm;
  97   mc_model_checker->process().read(&comm, remote(comm_addr));
  98
  99   smx_process_t src_proc = mc_model_checker->process().resolveProcess(
 100     simgrid::mc::remote(comm.comm.src_proc));
 101   smx_process_t dst_proc = mc_model_checker->process().resolveProcess(
 102     simgrid::mc::remote(comm.comm.dst_proc));
 103   comm_pattern->src_proc = src_proc->pid;
 104   comm_pattern->dst_proc = dst_proc->pid;
 105   comm_pattern->src_host = MC_smx_process_get_host_name(src_proc);
 106   comm_pattern->dst_host = MC_smx_process_get_host_name(dst_proc);
 107   if (comm_pattern->data.size() == 0 && comm.comm.src_buff != nullptr) {
 108     size_t buff_size;
 109     mc_model_checker->process().read(
 110       &buff_size, remote(comm.comm.dst_buff_size));
 111     comm_pattern->data.resize(buff_size);
 112     mc_model_checker->process().read_bytes(
 113       comm_pattern->data.data(), comm_pattern->data.size(),
 114       remote(comm.comm.src_buff));
 115   }
 116 }
 117
 118 static void deterministic_comm_pattern(int process, simgrid::mc::PatternCommunication* comm, int backtracking) {
 119
 120   simgrid::mc::PatternCommunicationList* list =
 121     xbt_dynar_get_as(initial_communications_pattern, process, simgrid::mc::PatternCommunicationList*);
 122
 123   if(!backtracking){
 124     e_mc_comm_pattern_difference_t diff =
 125       compare_comm_pattern(list->list[list->index_comm].get(), comm);
 126
 127     if (diff != NONE_DIFF) {
 128       if (comm->type == SIMIX_COMM_SEND){
 129         simgrid::mc::initial_global_state->send_deterministic = 0;
 130         if(simgrid::mc::initial_global_state->send_diff != nullptr)
 131           xbt_free(simgrid::mc::initial_global_state->send_diff);
 132         simgrid::mc::initial_global_state->send_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
 133       }else{
 134         simgrid::mc::initial_global_state->recv_deterministic = 0;
 135         if(simgrid::mc::initial_global_state->recv_diff != nullptr)
 136           xbt_free(simgrid::mc::initial_global_state->recv_diff);
 137         simgrid::mc::initial_global_state->recv_diff = print_determinism_result(diff, process, comm, list->index_comm + 1);
 138       }
 139       if(_sg_mc_send_determinism && !simgrid::mc::initial_global_state->send_deterministic){
 140         XBT_INFO("*********************************************************");
 141         XBT_INFO("***** Non-send-deterministic communications pattern *****");
 142         XBT_INFO("*********************************************************");
 143         XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
 144         xbt_free(simgrid::mc::initial_global_state->send_diff);
 145         simgrid::mc::initial_global_state->send_diff = nullptr;
 146         MC_print_statistics(mc_stats);
 147         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
 148       }else if(_sg_mc_comms_determinism
 149           && (!simgrid::mc::initial_global_state->send_deterministic
 150             && !simgrid::mc::initial_global_state->recv_deterministic)) {
 151         XBT_INFO("****************************************************");
 152         XBT_INFO("***** Non-deterministic communications pattern *****");
 153         XBT_INFO("****************************************************");
 154         XBT_INFO("%s", simgrid::mc::initial_global_state->send_diff);
 155         XBT_INFO("%s", simgrid::mc::initial_global_state->recv_diff);
 156         xbt_free(simgrid::mc::initial_global_state->send_diff);
 157         simgrid::mc::initial_global_state->send_diff = nullptr;
 158         xbt_free(simgrid::mc::initial_global_state->recv_diff);
 159         simgrid::mc::initial_global_state->recv_diff = nullptr;
 160         MC_print_statistics(mc_stats);
 161         mc_model_checker->exit(SIMGRID_MC_EXIT_NON_DETERMINISM);
 162       }
 163     }
 164   }
 165 }
 166
 167 /********** Non Static functions ***********/
 168
 169 void MC_get_comm_pattern(xbt_dynar_t list, smx_simcall_t request, e_mc_call_type_t call_type, int backtracking)
 170 {
 171   const smx_process_t issuer = MC_smx_simcall_get_issuer(request);
 172   simgrid::mc::PatternCommunicationList* initial_pattern = xbt_dynar_get_as(
 173     initial_communications_pattern, issuer->pid, simgrid::mc::PatternCommunicationList*);
 174   xbt_dynar_t incomplete_pattern = xbt_dynar_get_as(
 175     incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
 176
 177   std::unique_ptr<simgrid::mc::PatternCommunication> pattern =
 178     std::unique_ptr<simgrid::mc::PatternCommunication>(
 179       new simgrid::mc::PatternCommunication());
 180   pattern->index =
 181     initial_pattern->index_comm + xbt_dynar_length(incomplete_pattern);
 182
 183   if (call_type == MC_CALL_TYPE_SEND) {
 184     /* Create comm pattern */
 185     pattern->type = SIMIX_COMM_SEND;
 186     pattern->comm_addr = simcall_comm_isend__get__result(request);
 187
 188     s_smx_synchro_t synchro = mc_model_checker->process().read<s_smx_synchro_t>(
 189       (std::uint64_t) pattern->comm_addr);
 190
 191     char* remote_name = mc_model_checker->process().read<char*>(
 192       (std::uint64_t)(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
 193     pattern->rdv = mc_model_checker->process().read_string(remote_name);
 194     pattern->src_proc = mc_model_checker->process().resolveProcess(
 195       simgrid::mc::remote(synchro.comm.src_proc))->pid;
 196     pattern->src_host = MC_smx_process_get_host_name(issuer);
 197
 198     struct s_smpi_mpi_request mpi_request =
 199       mc_model_checker->process().read<s_smpi_mpi_request>(
 200         (std::uint64_t) simcall_comm_isend__get__data(request));
 201     pattern->tag = mpi_request.tag;
 202
 203     if(synchro.comm.src_buff != nullptr){
 204       pattern->data.resize(synchro.comm.src_buff_size);
 205       mc_model_checker->process().read_bytes(
 206         pattern->data.data(), pattern->data.size(),
 207         remote(synchro.comm.src_buff));
 208     }
 209     if(mpi_request.detached){
 210       if (!simgrid::mc::initial_global_state->initial_communications_pattern_done) {
 211         /* Store comm pattern */
 212         simgrid::mc::PatternCommunicationList* list = xbt_dynar_get_as(
 213           initial_communications_pattern, pattern->src_proc,
 214           simgrid::mc::PatternCommunicationList*);
 215         list->list.push_back(std::move(pattern));
 216       } else {
 217         /* Evaluate comm determinism */
 218         deterministic_comm_pattern(pattern->src_proc, pattern.get(), backtracking);
 219         xbt_dynar_get_as(
 220           initial_communications_pattern, pattern->src_proc, simgrid::mc::PatternCommunicationList*
 221         )->index_comm++;
 222       }
 223       return;
 224     }
 225   } else if (call_type == MC_CALL_TYPE_RECV) {
 226     pattern->type = SIMIX_COMM_RECEIVE;
 227     pattern->comm_addr = simcall_comm_irecv__get__result(request);
 228
 229     struct s_smpi_mpi_request mpi_request;
 230     mc_model_checker->process().read(
 231       &mpi_request, remote((struct s_smpi_mpi_request*)simcall_comm_irecv__get__data(request)));
 232     pattern->tag = mpi_request.tag;
 233
 234     s_smx_synchro_t synchro;
 235     mc_model_checker->process().read(&synchro, remote(pattern->comm_addr));
 236
 237     char* remote_name;
 238     mc_model_checker->process().read(&remote_name,
 239       remote(synchro.comm.rdv ? &synchro.comm.rdv->name : &synchro.comm.rdv_cpy->name));
 240     pattern->rdv = mc_model_checker->process().read_string(remote_name);
 241     pattern->dst_proc = mc_model_checker->process().resolveProcess(
 242       simgrid::mc::remote(synchro.comm.dst_proc))->pid;
 243     pattern->dst_host = MC_smx_process_get_host_name(issuer);
 244   } else
 245     xbt_die("Unexpected call_type %i", (int) call_type);
 246
 247   XBT_DEBUG("Insert incomplete comm pattern %p for process %lu",
 248     pattern.get(), issuer->pid);
 249   xbt_dynar_t dynar =
 250     xbt_dynar_get_as(incomplete_communications_pattern, issuer->pid, xbt_dynar_t);
 251   simgrid::mc::PatternCommunication* pattern2 = pattern.release();
 252   xbt_dynar_push(dynar, &pattern2);
 253 }
 254
 255 void MC_complete_comm_pattern(xbt_dynar_t list, smx_synchro_t comm_addr, unsigned int issuer, int backtracking) {
 256   simgrid::mc::PatternCommunication* current_comm_pattern;
 257   unsigned int cursor = 0;
 258   std::unique_ptr<simgrid::mc::PatternCommunication> comm_pattern;
 259   int completed = 0;
 260
 261   /* Complete comm pattern */
 262   xbt_dynar_foreach(xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t), cursor, current_comm_pattern)
 263     if (current_comm_pattern->comm_addr == comm_addr) {
 264       update_comm_pattern(current_comm_pattern, comm_addr);
 265       completed = 1;
 266       simgrid::mc::PatternCommunication* temp;
 267       xbt_dynar_remove_at(
 268         xbt_dynar_get_as(incomplete_communications_pattern, issuer, xbt_dynar_t),
 269         cursor, &temp);
 270       comm_pattern = std::unique_ptr<simgrid::mc::PatternCommunication>(temp);
 271       XBT_DEBUG("Remove incomplete comm pattern for process %u at cursor %u", issuer, cursor);
 272       break;
 273     }
 274
 275   if(!completed)
 276     xbt_die("Corresponding communication not found!");
 277
 278   simgrid::mc::PatternCommunicationList* pattern = xbt_dynar_get_as(
 279     initial_communications_pattern, issuer, simgrid::mc::PatternCommunicationList*);
 280
 281   if (!simgrid::mc::initial_global_state->initial_communications_pattern_done)
 282     /* Store comm pattern */
 283     pattern->list.push_back(std::move(comm_pattern));
 284   else {
 285     /* Evaluate comm determinism */
 286     deterministic_comm_pattern(issuer, comm_pattern.get(), backtracking);
 287     pattern->index_comm++;
 288   }
 289 }
 290
 291
 292 /************************ Main algorithm ************************/
 293
 294 namespace simgrid {
 295 namespace mc {
 296
 297 CommunicationDeterminismChecker::CommunicationDeterminismChecker(Session& session)
 298   : Checker(session)
 299 {
 300
 301 }
 302
 303 CommunicationDeterminismChecker::~CommunicationDeterminismChecker()
 304 {
 305
 306 }
 307
 308 RecordTrace CommunicationDeterminismChecker::getRecordTrace() // override
 309 {
 310   RecordTrace res;
 311   for (auto const& state : stack_)
 312     res.push_back(state->getRecordElement());
 313   return res;
 314 }
 315
 316 std::vector<std::string> CommunicationDeterminismChecker::getTextualTrace() // override
 317 {
 318   std::vector<std::string> trace;
 319   for (auto const& state : stack_) {
 320     smx_simcall_t req = &state->executed_req;
 321     if (req)
 322       trace.push_back(simgrid::mc::request_to_string(
 323         req, state->req_num, simgrid::mc::RequestType::executed));
 324   }
 325   return trace;
 326 }
 327
 328 void CommunicationDeterminismChecker::prepare()
 329 {
 330
 331   int i;
 332   const int maxpid = MC_smx_get_maxpid();
 333
 334   // Create initial_communications_pattern elements:
 335   initial_communications_pattern = simgrid::xbt::newDeleteDynar<simgrid::mc::PatternCommunicationList*>();
 336   for (i=0; i < maxpid; i++){
 337     simgrid::mc::PatternCommunicationList* process_list_pattern = new simgrid::mc::PatternCommunicationList();
 338     xbt_dynar_insert_at(initial_communications_pattern, i, &process_list_pattern);
 339   }
 340
 341   // Create incomplete_communications_pattern elements:
 342   incomplete_communications_pattern = xbt_dynar_new(sizeof(xbt_dynar_t), xbt_dynar_free_voidp);
 343   for (i=0; i < maxpid; i++){
 344     xbt_dynar_t process_pattern = xbt_dynar_new(sizeof(simgrid::mc::PatternCommunication*), nullptr);
 345     xbt_dynar_insert_at(incomplete_communications_pattern, i, &process_pattern);
 346   }
 347
 348   std::unique_ptr<simgrid::mc::State> initial_state =
 349     std::unique_ptr<simgrid::mc::State>(MC_state_new());
 350
 351   XBT_DEBUG("********* Start communication determinism verification *********");
 352
 353   /* Wait for requests (schedules processes) */
 354   mc_model_checker->wait_for_requests();
 355
 356   /* Get an enabled process and insert it in the interleave set of the initial state */
 357   for (auto& p : mc_model_checker->process().simix_processes())
 358     if (simgrid::mc::process_is_enabled(&p.copy))
 359       initial_state->interleave(&p.copy);
 360
 361   stack_.push_back(std::move(initial_state));
 362 }
 363
 364 static inline
 365 bool all_communications_are_finished()
 366 {
 367   for (size_t current_process = 1; current_process < MC_smx_get_maxpid(); current_process++) {
 368     xbt_dynar_t pattern = xbt_dynar_get_as(
 369       incomplete_communications_pattern, current_process, xbt_dynar_t);
 370     if (!xbt_dynar_is_empty(pattern)) {
 371       XBT_DEBUG("Some communications are not finished, cannot stop the exploration ! State not visited.");
 372       return false;
 373     }
 374   }
 375   return true;
 376 }
 377
 378 int CommunicationDeterminismChecker::main(void)
 379 {
 380   std::unique_ptr<simgrid::mc::VisitedState> visited_state = nullptr;
 381   smx_simcall_t req = nullptr;
 382
 383   while (!stack_.empty()) {
 384
 385     /* Get current state */
 386     simgrid::mc::State* state = stack_.back().get();
 387
 388     XBT_DEBUG("**************************************************");
 389     XBT_DEBUG("Exploration depth = %zi (state = %d, interleaved processes = %zd)",
 390               stack_.size(), state->num,
 391               state->interleaveSize());
 392
 393     /* Update statistics */
 394     mc_stats->visited_states++;
 395
 396     if (stack_.size() <= (std::size_t) _sg_mc_max_depth
 397         && (req = MC_state_get_request(state)) != nullptr
 398         && (visited_state == nullptr)) {
 399
 400       int req_num = state->req_num;
 401
 402       XBT_DEBUG("Execute: %s",
 403         simgrid::mc::request_to_string(
 404           req, req_num, simgrid::mc::RequestType::simix).c_str());
 405
 406       std::string req_str;
 407       if (dot_output != nullptr)
 408         req_str = simgrid::mc::request_get_dot_output(req, req_num);
 409
 410       mc_stats->executed_transitions++;
 411
 412       /* TODO : handle test and testany simcalls */
 413       e_mc_call_type_t call = MC_CALL_TYPE_NONE;
 414       if (_sg_mc_comms_determinism || _sg_mc_send_determinism)
 415         call = MC_get_call_type(req);
 416
 417       /* Answer the request */
 418       simgrid::mc::handle_simcall(req, req_num);    /* After this call req is no longer useful */
 419
 420       if(!initial_global_state->initial_communications_pattern_done)
 421         MC_handle_comm_pattern(call, req, req_num, initial_communications_pattern, 0);
 422       else
 423         MC_handle_comm_pattern(call, req, req_num, nullptr, 0);
 424
 425       /* Wait for requests (schedules processes) */
 426       mc_model_checker->wait_for_requests();
 427
 428       /* Create the new expanded state */
 429       std::unique_ptr<simgrid::mc::State> next_state =
 430         std::unique_ptr<simgrid::mc::State>(MC_state_new());
 431
 432       /* If comm determinism verification, we cannot stop the exploration if
 433          some communications are not finished (at least, data are transfered).
 434          These communications  are incomplete and they cannot be analyzed and
 435          compared with the initial pattern. */
 436       bool compare_snapshots = all_communications_are_finished()
 437         && initial_global_state->initial_communications_pattern_done;
 438
 439       if (_sg_mc_visited == 0
 440           || (visited_state = visitedStates_.addVisitedState(next_state.get(), compare_snapshots)) == nullptr) {
 441
 442         /* Get enabled processes and insert them in the interleave set of the next state */
 443         for (auto& p : mc_model_checker->process().simix_processes())
 444           if (simgrid::mc::process_is_enabled(&p.copy))
 445             next_state->interleave(&p.copy);
 446
 447         if (dot_output != nullptr)
 448           fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 449             state->num,  next_state->num, req_str.c_str());
 450
 451       } else if (dot_output != nullptr)
 452         fprintf(dot_output, "\"%d\" -> \"%d\" [%s];\n",
 453           state->num, visited_state->other_num == -1 ? visited_state->num : visited_state->other_num, req_str.c_str());
 454
 455       stack_.push_back(std::move(next_state));
 456
 457     } else {
 458
 459       if (stack_.size() > (std::size_t) _sg_mc_max_depth)
 460         XBT_WARN("/!\\ Max depth reached ! /!\\ ");
 461       else if (visited_state != nullptr)
 462         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);
 463       else
 464         XBT_DEBUG("There are no more processes to interleave. (depth %zi)",
 465           stack_.size());
 466
 467       if (!initial_global_state->initial_communications_pattern_done)
 468         initial_global_state->initial_communications_pattern_done = 1;
 469
 470       /* Trash the current state, no longer needed */
 471       XBT_DEBUG("Delete state %d at depth %zi",
 472         state->num, stack_.size());
 473       stack_.pop_back();
 474
 475       visited_state = nullptr;
 476
 477       /* Check for deadlocks */
 478       if (mc_model_checker->checkDeadlock()) {
 479         MC_show_deadlock();
 480         return SIMGRID_MC_EXIT_DEADLOCK;
 481       }
 482
 483       while (!stack_.empty()) {
 484         std::unique_ptr<simgrid::mc::State> state = std::move(stack_.back());
 485         stack_.pop_back();
 486         if (state->interleaveSize()
 487             && stack_.size() < (std::size_t) _sg_mc_max_depth) {
 488           /* We found a back-tracking point, let's loop */
 489           XBT_DEBUG("Back-tracking to state %d at depth %zi",
 490             state->num, stack_.size() + 1);
 491           stack_.push_back(std::move(state));
 492
 493           simgrid::mc::replay(stack_);
 494
 495           XBT_DEBUG("Back-tracking to state %d at depth %zi done",
 496             stack_.back()->num, stack_.size());
 497
 498           break;
 499         } else {
 500           XBT_DEBUG("Delete state %d at depth %zi",
 501             state->num, stack_.size() + 1);
 502         }
 503       }
 504     }
 505   }
 506
 507   MC_print_statistics(mc_stats);
 508   return SIMGRID_MC_EXIT_SUCCESS;
 509 }
 510
 511 int CommunicationDeterminismChecker::run()
 512 {
 513   XBT_INFO("Check communication determinism");
 514   mc_model_checker->wait_for_requests();
 515
 516   this->prepare();
 517
 518   initial_global_state = std::unique_ptr<s_mc_global_t>(new s_mc_global_t());
 519   initial_global_state->snapshot = simgrid::mc::take_snapshot(0);
 520   initial_global_state->initial_communications_pattern_done = 0;
 521   initial_global_state->recv_deterministic = 1;
 522   initial_global_state->send_deterministic = 1;
 523   initial_global_state->recv_diff = nullptr;
 524   initial_global_state->send_diff = nullptr;
 525
 526   int res = this->main();
 527   initial_global_state = nullptr;
 528   return res;
 529 }
 530
 531 Checker* createCommunicationDeterminismChecker(Session& session)
 532 {
 533   return new CommunicationDeterminismChecker(session);
 534 }
 535
 536 }
 537 }