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/remote/RemoteSimulation.hpp"
  13
  14 #include <array>
  15
  16 using simgrid::mc::remote;
  17 using simgrid::simix::Simcall;
  18
  19 XBT_LOG_NEW_DEFAULT_SUBCATEGORY(mc_request, mc, "Logging specific to MC (request)");
  20
  21 namespace simgrid {
  22 namespace mc {
  23
  24 bool request_is_enabled_by_idx(smx_simcall_t req, unsigned int idx)
  25 {
  26   kernel::activity::CommImpl* remote_act = nullptr;
  27   switch (req->call_) {
  28     case Simcall::COMM_WAIT:
  29       /* FIXME: check also that src and dst processes are not suspended */
  30       remote_act = simcall_comm_wait__getraw__comm(req);
  31       break;
  32
  33     case Simcall::COMM_WAITANY:
  34       remote_act = mc_model_checker->get_remote_simulation().read(remote(simcall_comm_waitany__get__comms(req) + idx));
  35       break;
  36
  37     case Simcall::COMM_TESTANY:
  38       remote_act = mc_model_checker->get_remote_simulation().read(remote(simcall_comm_testany__get__comms(req) + idx));
  39       break;
  40
  41     default:
  42       return true;
  43   }
  44
  45   Remote<kernel::activity::CommImpl> temp_comm;
  46   mc_model_checker->get_remote_simulation().read(temp_comm, remote(remote_act));
  47   const kernel::activity::CommImpl* comm = temp_comm.get_buffer();
  48   return comm->src_actor_.get() && comm->dst_actor_.get();
  49 }
  50
  51 } // namespace mc
  52 } // namespace simgrid