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