src/mc/mc_request.cpp

   1 /* Copyright (c) 2008-2021. The SimGrid Team. All rights reserved.          */
   2
   3 /* This program is free software; you can redistribute it and/or modify it
   4  * under the terms of the license (GNU LGPL) which comes with this package. */
   5
   6 #include "src/mc/mc_request.hpp"
   7 #include "src/include/mc/mc.h"
   8 #include "src/kernel/activity/CommImpl.hpp"
   9 #include "src/kernel/activity/MutexImpl.hpp"
  10 #include "src/mc/ModelChecker.hpp"
  11 #include "src/mc/checker/SimcallObserver.hpp"
  12 #include "src/mc/mc_smx.hpp"
  13 #include <array>
  14
  15 using simgrid::mc::remote;
  16 using simgrid::simix::Simcall;
  17
  18 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc, "Logging specific to MC (request)");
  19
  20 namespace simgrid {
  21 namespace mc {
  22
  23 bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
  24 {
  25   kernel::activity::CommImpl* remote_act = nullptr;
  26   switch (req->call_) {
  27     case Simcall::COMM_WAIT:
  28       /* FIXME: check also that src and dst processes are not suspended */
  29       remote_act = simcall_comm_wait__getraw__comm(req);
  30       break;
  31
  32     case Simcall::COMM_WAITANY:
  33       remote_act = mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__get__comms(req) + idx));
  34       break;
  35
  36     case Simcall::COMM_TESTANY:
  37       remote_act = mc_model_checker->get_remote_simulation().read(remote(simcall_comm_testany__get__comms(req) + idx));
  38       break;
  39
  40     default:
  41       return true;
  42   }
  43
  44   Remote<kernel::activity::CommImpl> temp_comm;
  45   mc_model_checker->get_remote_simulation().read(temp_comm, remote(remote_act));
  46   const kernel::activity::CommImpl* comm = temp_comm.get_buffer();
  47   return comm->src_actor_.get() && comm->dst_actor_.get();
  48 }
  49
  50 } // namespace mc
  51 } // namespace simgrid