src/mc/mc_comm_pattern.cpp

   1 /* Copyright (c) 2007-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 <string.h>
   8
   9 #include <xbt/sysdep.h>
  10 #include <xbt/dynar.h>
  11 #include <xbt/dynar.hpp>
  12
  13 #include "src/mc/mc_comm_pattern.h"
  14 #include "src/mc/mc_smx.h"
  15 #include "src/mc/mc_xbt.hpp"
  16 #include "src/mc/checker/CommunicationDeterminismChecker.hpp"
  17
  18 using simgrid::mc::remote;
  19
  20 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_comm_pattern, mc,
  21                                 "Logging specific to MC communication patterns");
  22
  23 static void MC_patterns_copy(xbt_dynar_t dest,
  24   std::vector<simgrid::mc::PatternCommunication> const& source)
  25 {
  26   xbt_dynar_reset(dest);
  27   for (simgrid::mc::PatternCommunication const& comm : source) {
  28     simgrid::mc::PatternCommunication* copy_comm = new simgrid::mc::PatternCommunication(comm.dup());
  29     xbt_dynar_push(dest, &copy_comm);
  30   }
  31 }
  32
  33 void MC_restore_communications_pattern(simgrid::mc::State* state)
  34 {
  35   simgrid::mc::PatternCommunicationList* list_process_comm;
  36   unsigned int cursor;
  37
  38   xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm)
  39     list_process_comm->index_comm = state->communicationIndices[cursor];
  40
  41   for (unsigned i = 0; i < MC_smx_get_maxpid(); i++)
  42     MC_patterns_copy(
  43       xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t),
  44       state->incomplete_comm_pattern[i]
  45     );
  46 }
  47
  48 void MC_state_copy_incomplete_communications_pattern(simgrid::mc::State* state)
  49 {
  50   state->incomplete_comm_pattern.clear();
  51   for (unsigned i=0; i < MC_smx_get_maxpid(); i++) {
  52     xbt_dynar_t patterns = xbt_dynar_get_as(incomplete_communications_pattern, i, xbt_dynar_t);
  53     std::vector<simgrid::mc::PatternCommunication> res;
  54     simgrid::mc::PatternCommunication* comm;
  55     unsigned int cursor;
  56     xbt_dynar_foreach(patterns, cursor, comm)
  57       res.push_back(comm->dup());
  58     state->incomplete_comm_pattern.push_back(std::move(res));
  59   }
  60 }
  61
  62 void MC_state_copy_index_communications_pattern(simgrid::mc::State* state)
  63 {
  64   state->communicationIndices.clear();
  65   simgrid::mc::PatternCommunicationList* list_process_comm;
  66   unsigned int cursor;
  67   xbt_dynar_foreach(initial_communications_pattern, cursor, list_process_comm)
  68     state->communicationIndices.push_back(list_process_comm->index_comm);
  69 }
  70
  71 void MC_handle_comm_pattern(
  72   e_mc_call_type_t call_type, smx_simcall_t req,
  73   int value, xbt_dynar_t pattern, int backtracking)
  74 {
  75   // HACK, do not rely on the Checker implementation outside of it
  76   simgrid::mc::CommunicationDeterminismChecker* checker =
  77     (simgrid::mc::CommunicationDeterminismChecker*) mc_model_checker->getChecker();
  78
  79   switch(call_type) {
  80   case MC_CALL_TYPE_NONE:
  81     break;
  82   case MC_CALL_TYPE_SEND:
  83   case MC_CALL_TYPE_RECV:
  84     checker->get_comm_pattern(pattern, req, call_type, backtracking);
  85     break;
  86   case MC_CALL_TYPE_WAIT:
  87   case MC_CALL_TYPE_WAITANY:
  88     {
  89       simgrid::mc::RemotePtr<simgrid::kernel::activity::Comm> comm_addr = nullptr;
  90       if (call_type == MC_CALL_TYPE_WAIT)
  91         comm_addr = remote(static_cast<simgrid::kernel::activity::Comm*>(
  92           simcall_comm_wait__get__comm(req)));
  93       else {
  94         simgrid::kernel::activity::Comm* addr;
  95         // comm_addr = REMOTE(xbt_dynar_get_as(simcall_comm_waitany__get__comms(req), value, smx_synchro_t)):
  96         simgrid::mc::read_element(mc_model_checker->process(), &addr,
  97           remote(simcall_comm_waitany__get__comms(req)), value, sizeof(comm_addr));
  98         comm_addr = remote(addr);
  99       }
 100       checker->complete_comm_pattern(pattern, comm_addr,
 101         MC_smx_simcall_get_issuer(req)->pid, backtracking);
 102     }
 103     break;
 104   default:
 105     xbt_die("Unexpected call type %i", (int)call_type);
 106   }
 107
 108 }